Proof libraries

  • Isabelle archive of formal proofs: here
  • Metamath: here

http://www.cs.ru.nl/~freek/comparison/comparison.pdf

http://www.cogsys.wiai.uni-bamberg.de/teaching/ss07/hs_rc/slides/tc.pdf

https://github.com/raphlinus/ghilbert

GHilbert: Builds on MM but adds new definition mechanism. Also adds

https://github.com/abliss/caghni

Caghni: builds on GHilbert but uses a CAS

Little Theories

http://imps.mcmaster.ca/doc/little-theories.pdf

Robinson arithmetic

  • Nonary element 0
  • Unary operator S
  • Binary operators + and x

https://en.wikipedia.org/wiki/Robinson_arithmetic

Peano Axioms

https://en.wikipedia.org/wiki/Peano_axioms

  • 0 is a natural number.

  • For every natural number x, x = x. That is, equality is reflexive.
  • For all natural numbers x and y, if x = y, then y = x. That is, equality is symmetric.
  • For all natural numbers x, y and z, if x = y and y = z, then x = z. That is, equality is transitive.

  • For all a and b, if b is a natural number and a = b, then a is also a natural number. That is, the natural numbers are closed under equality.

  • For every natural number n, S(n) is a natural number.
  • For all natural numbers m and n, m = n if and only if S(m) = S(n). That is, S is an injection.

  • For every natural number n, S(n) = 0 is false. That is, there is no natural number whose successor is 0.

Induction. Can be defined either using predicates or sets.

Willard’s self verifying theories

https://en.wikipedia.org/wiki/Self-verifying_theories

Weaker than Robinson’s. So weak that Gödel’s incompletness does not apply. Yet they can prove their own consistency!