List of theorems
List of theorems in general/Basic_arithmetic_implies_Peano_axioms.gh:
Succ
(= (succ a) (+ a (1)))
Successor
(↔ (= (succ a) (succ b)) (= a b))
AdditiveIdentity
(= (+ a (0)) a)
Addition
(= (+ a (succ b)) (succ (+ a b)))
MultiplicativeZero
(= (· a (0)) (0))
Multiplication
(= (· a (succ b)) (+ a (· a b)))
Induction
(→ (∧ (subst (0) n φ) (∀ k (→ (subst k n φ) (subst (succ k) n φ)))) (∀ n φ))
ZeroNotSuccessor
(¬ (= (0) (succ a)))