s-TODO
Doing
s-Peano-axioms
doing Sequent calculus
cf. https://en.wikipedia.org/wiki/Peano_axioms
0 is a natural number
|- for all x { x = x }
|- for all x, y { x = y -> y = x }
|- for all x, y, z { x = y & y = z -> x = z }
|- for all x { S(x) is a natural number }
|- for all x, y { S(x) = S(y) -> x = y }
|- for all x { 0 != S(x) }
let φ any predicate, φ(0); φ(x) -> φ(x + 1) |- for all x φ(x)
Formalize the first theorems in ASTs
2 + 2 = 4
Use Peano Postulates
Decide first N(now 8) theorems - done
De Rham's theorem ( in ZFC )
2 + 2 = 4 ( in Peano axioms )
Fundamental theorem of arithmetic ( in Peano axioms )
Fermat's little theorem ( in Peano axioms )
Stokes' theorem ( in ZFC )
Banach-Tarski paradox ( in ZFC )
Yoneda Lemma ( in ETCC )
Homomorphism theorem of groups ( in ZFC )
Fundamental thoerem of calculus ( in ZFC )
#s