Outline

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

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)
… mathematics of statistical physics
On universal morphisms

References


Sequel of

Link to graph
Log In
Improvements of the human condition