Foundational temp1
| Drawing arrows and coding functions $\succ$ Foundational temp1 $\succ$ Foundational temp1b |
Guide
(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.
Sequel of
