## Outline

An apple pie from scratch $\succ$ Outline $\succ$ Drawing arrows and coding functions |

### Guide

Here is an outline structure (work in progress):

#### Concepts in the incarnation of a programming language

- Assume knowledge of integers $-2,-1,0,1,2,3$ with binary operations $+,-,*$.
- More on that languages syntax and examples (which are instances of relevant concepts to be discussed later)

#### Computation and logic (presented bottom-up)

- Comment on syntax
- Type theories: Simple type theory $\to$ Polymorphic type theory $\to$ Dependent type theory
- Formal logic: Intuitionist logic $\to$ First order logic (here, at the latest, it might be good to introduce the non-computing language, i.e. go away from the programming language and use a formal logic, as is traditional, in a descriptive fashion)
- Comment on curry-Howard correspondence
- Axiomatization of category theory within dependent type theory, plus comment on first order axiomatization
- Axiomatization of set theory within first order logic
- Informal discussion of the very first constructions in those frameworks, respectively
- Comment on how cats and set can be used to study type theory and logic itself

#### Mathematical core (presented top-down)

- Formal definitions from the main body of this wiki. The
**Set**entries can be thought of as defining sets which ZFC shows to be non-empty. Some category theoretical definitions use sets (e.g. when setting up a category of sets, for which we wanted to add a large cardinal axiom), but conversely the set entries are independent of those (but of course a notion of categories can and is defined within ZFC).

#### Physics

Eventually, make a list of mutually properly distinct physical frameworks - i.e. mathematical theories used in physics, usually coming with some state space and dynamics, see Perspective. In the latter sense, they must be exhaustively specified, of course, together with a concise list of their respective axioms. Some frameworks contain black boxes that are further given insight into in more detailed theories. Here, when it comes to physics, I tend to like to have the rougher theories first.

'that list' |

Now one can reference real life systems and associate mathematical models in this and that framework with them. Develop them like this:

mechanics |

todo: examples of experiments

… phenomenological thermodynamics |

todo: examples of experiments

(Phenomenological thermodynamics leads to a lot of basic chemistry)

electronics |

todo: examples of experiments

electromagnetic field theory |

### Entries

Preface |
---|

An apple pie from scratch |

Guideline |

Outline (this entry) |

**Logical prerequisites**

Meta |
---|

On syntax |

Symbols |

Types, terms and programming |

up to dependent type theory (?MLTT, etc.) |

type of natural numbers |

type of categories |

informal Curry-Howard correspondence |

Foundational temp1 |

Formal logic |

Intuitionistic logic (independent of type theory) |

First order logic (i.e. adding LEM to Intuitionistic logic) |

Axioms for set theory (e.g. GT-set-theory, and then U= type of sets) |

**Mathematical core**

todo: the following line of “apple pie from scratch” entries have some gaps

I have neither been able to find a good n-category basis instead of the 1-category approach I take here

nor have I formalized “up to iso” anywhere (this point is relate to the one above)

Formal part |
---|

On category theory basics |

On universal morphisms |

Foundational temp3 |

Foundational temp4 |

… |

… mathematics of statistical physics |

On universal morphisms |