This will be the 2020's web series about the foundation, architecture and deconstruction of mathematics. We will be mainly concerned with structures on top of which all of mathematics can find its foundations. However one cannot do much with just the foundations. We are going to discuss the known and the novel constructs with which we have built our mathematics.
We will start by observing an interesting shadow set of the same structure and, more interestingly, we will name the different shadows but not the structure itself. Once you have shadows from all the infinite steradians, you have the complete silhouette. You can go further and map the details of the structure instead of just getting its topographical outline.
When you map geological points and events in a network, you will see that it helps to have topological maps aside from geologically correct maps. Maps are concerned with distances and physicality of things. However mathematical spaces and sets are concerned with other variables such as time and arbitrarily many mathematical or physical concepts.
In this section, we will talk about how the logic side and the programming side of things are equivalent in a sense. Technically we call this an isomorphism. Hilbert style deduction systems are based on intuitionistic logic, axiom schemes and deduction or proof systems. A model of computation called lambda calculus is concerned with similar equivalent structures as well. Similar models based on type theory , combinatory logic and Gentzen's sequent calculus also exist. In the so-called BHK interpretation , intuitionistic proofs are functions and since lambda calculus proofs form a class of function, there is a correspondence between natural deduction and lambda calculus.
Going further than the Curry-Howard correspondence we have so far, there is a generalized Curry-Howard-Lambek correspondence . It shows that proofs of intuitionistic propositional logic and combinators of typed combinatory logic share an equational theory and form cartesian closed categories .
We will learn about constructions that operate on these logical propositions or abstract categories or types. We will deal with pairs such as
- quantification and generalization
- sum and product
- implication and function
- conjunction and product
- disjunction and sum
- truth and unity
- falsehood and depth
- Hypotheses and Free Variables
- Modus Ponens and Application
- Conditionality and Abstraction
We will also examine the following aspects of the correspondences and related concepts:
- Hibert-style deduction and Type System for Combinatory Logic
- Natural Deduction and Type System for Lambda Calculus
- Closed Monoidal Categories
- Internal Language
- Linear Type System & Linear Logic
- Homotopic Equivalence & Equality
Here we will talk about rule based knowledge bases and logical calculus for extracting knowledge from constraints, rules and propositions. Formalisms for these will also be introduced.
We will mostly obsess with quaternions and n-dimensional tuples which may mutate to equivalent structures in other dimensions.
These mutators are called transformers if they shift the tuple towards structures in the same dimensions as before.
We will agree upon an intuitive encoding for matrices and various kinds of graphs.
We will examine a memory arrays & meshes based architecture for a collaborative system for computational problem solving.
Based on 6, we will create a model for inter-planetary level computational collaborations and national level collaborations, named in the examples as nep.work.
We will take a step back and examine the constructors of our abstractions. We will study spoken and written language structures describing the aforementioned concepts and knowledge base.
We will continue 8 with a shifted focus towards how language is intensionally and extensionally shared and heard. Essentially we take a sharp and brief look at understanding of understanding itself.
We will continue 9 with a further shifted focus towards internal language systems and the capacity for an externally shared language. We will look unbiasedly at both Chomsky's Universal Grammar and Deutscher's Universal Relativism.
Certain nodes in our directed graphs and networks are sources or sinks or both. The edge's representation as a line or a n-D enclosure is known as a link and it may be directional and/or contextual.
After looking at sinks and links, we focus ourselves on sources. The rest of the courses will be about sources and actors prevailing in such a meta-platform for mathematics, politics, economics, physics and engineering.