Mathematics' Architecture & Processes for Programmers
Tags: mathematics, logic, hypergraphs, calculus
Published: 2020-01-17 15:52:24

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](https://en.wikipedia.org/wiki/Steradian), 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. 

# 1. Logic, Categories and Types

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](http://mathworld.wolfram.com/Isomorphism.html).  [Hilbert style deduction systems](https://en.wikipedia.org/wiki/Hilbert_system)  are based on intuitionistic logic, axiom schemes and deduction or proof systems. A model of computation called  [lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus)  is concerned with similar equivalent structures as well. Similar models based on  [type theory](https://en.wikipedia.org/wiki/Type_theory) ,  [combinatory logic](https://en.wikipedia.org/wiki/Combinatory_logic)  and  [Gentzen's sequent calculus](https://en.wikipedia.org/wiki/Sequent_calculus)  also exist. In the so-called  [BHK interpretation](https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_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](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) . It shows that proofs of  [intuitionistic propositional logic](https://en.wikipedia.org/wiki/Intuitionistic_logic)  and combinators of typed  [combinatory logic](https://en.wikipedia.org/wiki/Combinatory_logic)  share an  [equational theory](https://en.wikipedia.org/wiki/Universal_algebra)  and form  [cartesian closed categories](https://en.wikipedia.org/wiki/Cartesian_closed_category) . 

We will learn about constructions that operate on these logical propositions or abstract categories or types. We will deal with pairs such as 
*  [quantification](https://en.wikipedia.org/wiki/Quantifier_(logic))  and  [generalization](https://en.wikipedia.org/wiki/Generalization) 
*  [sum](https://en.wikipedia.org/wiki/Coproduct)  and  [product](https://en.wikipedia.org/wiki/Product_(category_theory)) 
*  [implication](https://en.wikipedia.org/wiki/Logical_consequence)  and  [function](https://en.wikipedia.org/wiki/Function_(mathematics)) 
*  [conjunction](https://en.wikipedia.org/wiki/Logical_conjunction)  and product
*  [disjunction](https://en.wikipedia.org/wiki/Logical_disjunction)  and sum
*  [truth](https://en.wikipedia.org/wiki/Truth_value)  and  [unity](https://en.wikipedia.org/wiki/Unit_type) 
*  [falsehood](https://en.wikipedia.org/wiki/False_(logic))  and  [depth](https://en.wikipedia.org/wiki/Bottom_type) 
*  [Hypotheses](https://en.wikipedia.org/wiki/Abductive_reasoning)  and  [Free Variables](https://en.wikipedia.org/wiki/Free_variables_and_bound_variables) 
*  [Modus Ponens](https://en.wikipedia.org/wiki/Modus_ponens)  and  [Application](https://en.wikipedia.org/wiki/Apply) 
*  [Conditionality](https://en.wikipedia.org/wiki/Conditional_proof)  and  [Abstraction](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/Closed_monoidal_category)   
*  [Internal Language](https://en.wikipedia.org/wiki/Categorical_logic) 
*  [Linear Type System](https://en.wikipedia.org/wiki/Substructural_type_system)  &  [Linear Logic](https://en.wikipedia.org/wiki/Linear_logic) 
*  [Homotopic Equivalence & Equality](https://en.wikipedia.org/wiki/Homotopy#Homotopy_equivalence) 



# 2. Propositions and Constraints

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.

# 3. Operators and n-Tuples

We will mostly obsess with quaternions and n-dimensional tuples which may mutate to equivalent structures in other dimensions. 

# 4. Transformers and Mutators

These mutators are called transformers if they shift the tuple towards structures in the same dimensions as before.

# 5. Matrices and Hypergraphs

We will agree upon an intuitive encoding for matrices and various kinds of graphs.

# 6. MAMBA and COSYS

We will examine a memory arrays & meshes based architecture for a collaborative system for computational problem solving.

# 7. COPLA and NEP.WORK

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.

# 8. Spoken and Written Lang

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.

# 9. Shared and Heard Lang

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.

# X. Internal Lang and Lang

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.

# 11. Sink and Link

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.

# 12. Source and Course

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.

![Alt Text](https://thepracticaldev.s3.amazonaws.com/i/c6rnffs564ztbugo0xl7.png)