(Note) Logic

(Note) Specifying syntax

Remark: With the Framework entries, I go up in complexity. Then, with the entries with mathematical content, I start with abstract and go to concrete.

(Framework) Intuitionistic propositional logic

(Note) Predicate logic

(Note) First-order theory of groups

todo

(Framework) First-order Peano arithmetic

todo

(Framework) Set theory

Explanation of axiomatics, in particular ZFC and also the Grothendieck-Tarski axiom (a large cardinal axiom).

Discussion of basic concepts such as the Unordered pair.

(Framework) Category theory

Todo:
Split Category theory in two. I.e. make a (Framework) entry on Category theory, axiomized directly in logic and another (Note) entry for Category theory within type theory.

(Note) Type theory

todo

(Type) Type

(Type) Function type

(Type) Product type

Todo: Introduce in a chain of entries more and more expressible type theories. The guideline being that each entry is a “faithful subset” of the next.

Drawing arrows and coding functions