# 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 () "") kind (num) tvar (wff ph ps ch) tvar (num A B C D) var (num x y z) term (wff (A. x ph)) term (wff (= A B)) # roughly equivalent to ax-17 stmt (alnfi ((ph x)) () (-> ph (A. x ph))) stmt (gen () (ph) (A. x ph)) # roughly Margaris A5, but without the subst stmt (ax-4 () () (-> (A. x ph) ph)) # Margaris A4 stmt (ax-alim () () (-> (A. x (-> ph ps)) (-> (A. x ph) (A. x ps)))) # Similar to ax-8, but for num's instead of var's. stmt (ax-eqtr () () (-> (/\ (= A B) (= A C)) (= B C))) # Similar to ax-9, but expanded to num's instead of var's. stmt (ax-tyex ((A x)) () (-. (A. x (-. (= x A))))) # Properties of numbers: Peano axioms term (num (0)) term (num (S A)) term (num (+ A B)) term (num (* A B)) # Equality axiom for addition stmt (addeq12 () () (-> (/\ (= A B) (= C D)) (= (+ A C) (+ B D)))) # Equality axiom for multiplication stmt (muleq12 () () (-> (/\ (= A B) (= C D)) (= (* A C) (* B D)))) stmt (pa_ax1 () () (-. (= (0) (S A)))) # Note that the biconditional captures equality properties of S as # well as the traditional Peano axiom 2. stmt (pa_ax2 () () (<-> (= A B) (= (S A) (S B)))) stmt (pa_ax3 () () (= (+ A (0)) A)) stmt (pa_ax4 () () (= (+ A (S B)) (S (+ A B)))) stmt (pa_ax5 () () (= (* A (0)) (0))) stmt (pa_ax6 () () (= (* A (S B)) (+ (* A B) A))) stmt (pa_ind ((ph y)) () (-> (/\ (A. x (-> (= x (0)) ph)) (A. y (-> (A. x (-> (= x y) ph)) (A. x (-> (= x (S y)) ph))))) (A. x ph))) # Definition of exists - could be done through def instead of axiom here. term (wff (E. x ph)) 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)))))) # iota is a draft at this point. term (num (iota x ph)) stmt (ax-iota ((ph y)) () (-> (E! x ph) (E. y (/\ (= y (iota x ph)) (E. x (/\ (= x y) ph))))))