* presentation of mathematical concepts in a top-down way: The focus is on how “mathematical data” can be set up in set theory and I also use category theory for “structural characterizations”.

(As foundational paradigms, both set- and category theory have strong merits and disadvantages. While it's possible to develop a version of categories, functors and natural transformations in set theory and a version of sets in category theory, I rather use both paradigms early on. As a side note, it's also possible to axiomatize categories in logic directly and also to specify sets in type theory, but that's pretty nonstandard and more difficult. In discussion sections, I will often use categorcal language to to characterize sets a the category of sets.)

• Be self-contained

I start out with an more or less informal explanation of formal languages and foundational theories and common axioms. The structure of the presentation is summarized below. The primitive notions in this wiki, discussed in the first block, are summarized in Domain of discourse.

• Use a “two models” principle:

For each abstract definition, I'll try to exemplify it with two different structures.

• Convey information in different visual language languages:

- proper cat'ish drawing

$$ \require{AMScd} \begin{CD} {\large\hbar} @>{\large{!}}>> {\large{*}} \\ @V{{\large{m}}}VV @VV{{\large\top}}V \\ {\large\heartsuit} @>>{\large{\chi}}> {\large{\Omega}} \end{CD} $$

- drawing where you see terms, circled (the type universe is circled as well)

- typey syntax

- FOL/SOL

Here the structure:

• (Maybe playing around with stuff that a computer evaluates)
• 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

• 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).

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.

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

todo: examples of experiments

todo: examples of experiments

(Phenomenological thermodynamics leads to a lot of basic chemistry)

todo: examples of experiments

Logical prerequisites

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)

An apple pie from scratch

An apple pie from scratch