Foundational temp1

Drawing arrows and coding functions $\succ$ Foundational temp1 $\succ$ Foundational temp1b


(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


(Framework) First-order Peano arithmetic


(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

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


(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.

Sequel of

Link to graph
Log In
Improvements of the human condition