# Experimental interface for Peano arithmetic # We conjecture the following properties about this interface, with at # this point only a moderate amount of confidence: # # * It encapsulates PA soundly and completely. # * It is possible to interpret in a set.mm universe. # * It is reasonably useful. # # There are two extensions that may improve usefulness: classes and # ax-11. The latter would enable a substitution operator with all the # expected properties. However, it makes the syntactic interpretation # in set.mm problematic. param (PROP prop.ghi () "") param (PEANO_MIN peano_min.ghi (PROP) "") tvar (wff ph ps ch) tvar (nat A B C D) var (nat x y z) # Definition of exists - could be done through def instead of axiom here. term (wff (E. x ph)) ## Definition of ∃ ## right('Equivalence', '∀') stmt (df-ex () () (<-> (E. x ph) (-. (A. x (-. ph))))) # Exists-unique is handy for iota def, but could be expanded there term (wff (E! x ph)) stmt (df-eu ((ph y)) () (<-> (E! x ph) (E. y (A. x (<-> ph (= x y)))))) term (nat (1)) stmt (df-1 () () (= (1) (S (0)))) # Definition of less than or equal to. term (wff (<= A B)) stmt (df-le ((A x) (B x)) () (<-> (<= A B) (E. x (= (+ A x) B)))) term (wff (< A B)) stmt (df-lt () () (<-> (< A B) (/\ (<= A B) (-. (= A B))))) term (wff ([/] A x ph) (x A)) stmt (df-subst ((A z) (ph z)) () (<-> ([/] A x ph) (E. z (/\ (= z A) (E. x (/\ (= x z) ph)))))) term (wff (rwff x ph)) stmt (df-rwff () () (<-> (rwff x ph) (A. x (<-> ph ([/] x x ph))))) # iota is a draft at this point. # term (nat (iota x ph)) #stmt (ax-iota ((ph y)) () # (-> (E! x ph) # (E. y (/\ (= y (iota x ph)) # (E. x (/\ (= x y) ph))))))