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 build our mathematics.
We will start by observing an interesting shadow set of the same structure and, more interestingly, we will name the 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 logic side and 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 structures. 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 as lambda calculus 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
- Hypothese and Free Variables
- Modus Ponens and Application
- Conditionality and Abstraction
We will also examine the following aspects of the correspondences: