# Building up theorems of peano arithmetic. # until param is working... import (COMBINED combined.ghi () "") #import (PROP prop.ghi () "") #import (PEANO peano_ax.ghi (PROP) "") tvar (wff ph ps ch th ta) tvar (num A B C D A' B' C') var (num x y z x' y') # Pure predicate calculus thm (19.3 ((ph x)) () (<-> (A. x ph) ph) x ph ax-4 ph x alnfi impbii ) # aka 19.7 thm (alnex () () (<-> (A. x (-. ph)) (-. (E. x ph))) x ph df-ex con2bii ) thm (19.9 ((ph x)) () (<-> (E. x ph) ph) x (-. ph) 19.3 x ph alnex bitr3i con4bii bicomi ) thm (19.15 () () (-> (A. x (<-> ph ps)) (<-> (A. x ph) (A. x ps))) ph ps bi1 x gen x (<-> ph ps) (-> ph ps) ax-alim ax-mp x ph ps ax-alim syl ph ps bi2 x gen x (<-> ph ps) (-> ps ph) ax-alim ax-mp x ps ph ax-alim syl impbid ) thm (19.15i () (hyp (A. x (<-> ph ps))) (<-> (A. x ph) (A. x ps)) hyp x ph ps 19.15 ax-mp) thm (albii () (hyp (<-> ph ps)) (<-> (A. x ph) (A. x ps)) hyp x gen 19.15i) thm (19.20i () (hyp (-> ph ps)) (-> (A. x ph) (A. x ps)) hyp x gen x ph ps ax-alim ax-mp) thm (19.21 ((ph x)) () (<-> (A. x (-> ph ps)) (-> ph (A. x ps))) x ph ps ax-alim ph x alnfi syl5 (-> ph (A. x ps)) x alnfi x ps ax-4 ph imim2i x 19.20i syl impbii ) thm (19.22 () () (-> (A. x (-> ph ps)) (-> (E. x ph) (E. x ps))) ph ps con34b x albii x (-. ps) (-. ph) ax-alim sylbi con3d x ph df-ex x ps df-ex imbi12i sylibr ) thm (19.22i () (hyp (-> ph ps)) (-> (E. x ph) (E. x ps)) hyp x gen x ph ps 19.22 ax-mp) thm (19.32 ((ph x)) () (<-> (A. x (\/ ph ps)) (\/ ph (A. x ps))) x (-. ph) ps 19.21 ph ps df-or x albii ph (A. x ps) df-or 3bitr4i ) thm (19.31 ((ps x)) () (<-> (A. x (\/ ph ps)) (\/ (A. x ph) ps)) x ps ph 19.32 ph ps orcom x albii (A. x ph) ps orcom 3bitr4i ) thm (19.23 ((ps x)) () (<-> (A. x (-> ph ps)) (-> (E. x ph) ps)) ph ps imor x albii x (-. ph) ps 19.31 bitri x ph alnex ps orbi1i bitri (E. x ph) ps imor bitr4i ) thm (19.23ai ((ps x)) (hyp (-> ph ps)) (-> (E. x ph) ps) hyp x 19.22i x ps 19.9 sylib ) # Predicate calculus with equality thm (tyex ((A x)) () (E. x (= x A)) x A ax-tyex x (= x A) df-ex mpbir ) thm (vtocle ((A x) (ph x)) (hyp (-> (= x A) ph)) ph x A tyex hyp x 19.23ai ax-mp ) thm (eqid () () (= A A) x A A ax-eqtr anidms vtocle ) thm (eqcom () () (<-> (= A B) (= B A)) A eqid A B A ax-eqtr mpan2 B eqid B A B ax-eqtr mpan2 impbii ) thm (eqcomi () (hyp (= A B)) (= B A) hyp A B eqcom mpbi) thm (eqcomd () (hyp (-> ph (= A B))) (-> ph (= B A)) hyp A B eqcom sylib) thm (eqcoms () (hyp (-> (= A B) ph)) (-> (= B A) ph) B A eqcom hyp sylbi ) thm (eqeq1 () () (-> (= A B) (<-> (= A C) (= B C))) A B C ax-eqtr ex B A C ax-eqtr ex eqcoms impbid ) thm (eqeq2 () () (-> (= A B) (<-> (= C A) (= C B))) A B C eqeq1 A C eqcom B C eqcom bibi12i sylib ) thm (eqeq1i () (hyp (= A B)) (<-> (= A C) (= B C)) hyp A B C eqeq1 ax-mp) thm (eqeq1d () (hyp (-> ph (= A B))) (-> ph (<-> (= A C) (= B C))) hyp A B C eqeq1 syl) thm (eqeq2i () (hyp (= A B)) (<-> (= C A) (= C B)) hyp A B C eqeq2 ax-mp) thm (eqeq2d () (hyp (-> ph (= A B))) (-> ph (<-> (= C A) (= C B))) hyp A B C eqeq2 syl) thm (eqeq12d () (hyp1 (-> ph (= A B)) hyp2 (-> ph (= C D))) (-> ph (<-> (= A C) (= B D))) hyp1 C eqeq1d hyp2 B eqeq2d bitrd ) thm (eqtr3 () (hyp1 (= A B) hyp2 (= A C)) (= B C) hyp1 hyp2 A B C ax-eqtr mp2an ) thm (eqtr () (hyp1 (= A B) hyp2 (= B C)) (= A C) hyp1 eqcomi hyp2 eqtr3 ) thm (eqtr4 () (hyp1 (= A B) hyp2 (= C B)) (= A C) hyp1 hyp2 eqcomi eqtr ) thm (eqtrd () (hyp1 (-> ph (= A B)) hyp2 (-> ph (= B C))) (-> ph (= A C)) hyp1 hyp2 A eqeq2d mpbid ) thm (syl5eq () (hyp1 (-> ph (= A B)) hyp2 (= C A)) (-> ph (= C B)) hyp2 ph a1i hyp1 eqtrd ) thm (syl5eqr () (hyp1 (-> ph (= A B)) hyp2 (= A C)) (-> ph (= C B)) hyp2 eqcomi ph a1i hyp1 eqtrd ) thm (syl6eq () (hyp1 (-> ph (= A B)) hyp2 (= B C)) (-> ph (= A C)) hyp1 hyp2 ph a1i eqtrd ) thm (syl6eqr () (hyp1 (-> ph (= A B)) hyp2 (= C B)) (-> ph (= A C)) hyp1 hyp2 eqcomi ph a1i eqtrd ) thm (3eqtr4g () (hyp1 (-> ph (= A B)) hyp2 (= C A) hyp3 (= D B)) (-> ph (= C D)) hyp1 hyp2 syl5eq hyp3 syl6eqr ) thm (vtocl ((A x) (ps x)) (hyp1 (-> (= x A) (<-> ph ps)) hyp2 ph) ps hyp2 hyp1 mpbii vtocle ) thm (ceqsal ((A x) (ps x)) (hyp (-> (= x A) (<-> ph ps))) (<-> (A. x (-> (= x A) ph)) ps) hyp pm5.74i x albii x (= x A) ps 19.23 bitri x A tyex ps a1bi bitr4i ) # Peano arithmetic thm (addeq1 () () (-> (= A B) (= (+ A C) (+ B C))) C eqid A B C C addeq12 mpan2) thm (addeq2 () () (-> (= A B) (= (+ C A) (+ C B))) C eqid C C A B addeq12 mpan) thm (addeq12i () (hyp1 (= A B) hyp2 (= C D)) (= (+ A C) (+ B D)) hyp1 hyp2 A B C D addeq12 mp2an ) thm (addeq1d () (hyp (-> ph (= A B))) (-> ph (= (+ A C) (+ B C))) hyp C eqid A B C C addeq12 mpan2 syl ) thm (addeq12d () (hyp1 (-> ph (= A B)) hyp2 (-> ph (= C D))) (-> ph (= (+ A C) (+ B D))) hyp1 hyp2 jca A B C D addeq12 syl ) thm (addeq1i () (hyp (= A B)) (= (+ A C) (+ B C)) hyp C eqid A B C C addeq12 mp2an ) thm (addeq2i () (hyp (= A B)) (= (+ C A) (+ C B)) C eqid hyp C C A B addeq12 mp2an ) thm (muleq1 () () (-> (= A B) (= (* A C) (* B C))) C eqid A B C C muleq12 mpan2) thm (muleq2 () () (-> (= A B) (= (* C A) (* C B))) C eqid C C A B muleq12 mpan) thm (muleq12i () (hyp1 (= A B) hyp2 (= C D)) (= (* A C) (* B D)) hyp1 hyp2 A B C D muleq12 mp2an ) thm (muleq1d () (hyp (-> ph (= A B))) (-> ph (= (* A C) (* B C))) hyp C eqid A B C C muleq12 mpan2 syl ) thm (muleq1i () (hyp (= A B)) (= (* A C) (* B C)) hyp C eqid A B C C muleq12 mp2an ) thm (suceqd () (hyp (-> ph (= A B))) (-> ph (= (S A) (S B))) hyp A B pa_ax2 sylib) thm (finds ((A x) (ps x) (ch x) (th x) (ta x) (ph y)) (hyp1 (-> (= x (0)) (<-> ph ps)) hyp2 (-> (= x y) (<-> ph ch)) hyp3 (-> (= x (S y)) (<-> ph th)) hyp4 (-> (= x A) (<-> ph ta)) hyp5 ps hyp6 (-> ch th)) ta hyp4 hyp5 hyp1 mpbiri x gen hyp6 hyp2 ceqsal hyp3 ceqsal 3imtr4i y gen x ph y pa_ind mp2an x ph ax-4 ax-mp vtocl ) thm (pa_ax3r () () (= (+ (0) A) A) x (0) (0) addeq2 (= x (0)) id eqeq12d x y (0) addeq2 (= x y) id eqeq12d x (S y) (0) addeq2 (= x (S y)) id eqeq12d x A (0) addeq2 (= x A) id eqeq12d (0) pa_ax3 (+ (0) y) y pa_ax2 (0) y pa_ax4 (S y) eqeq1i bitr4i biimpi finds ) thm (pa_ax4r () () (= (+ (S A) B) (S (+ A B))) x (0) (S A) addeq2 x (0) A addeq2 suceqd eqeq12d x y (S A) addeq2 x y A addeq2 suceqd eqeq12d x (S y) (S A) addeq2 x (S y) A addeq2 suceqd eqeq12d x B (S A) addeq2 x B A addeq2 suceqd eqeq12d (S A) pa_ax3 A pa_ax3 (+ A (0)) A pa_ax2 mpbi eqtr4 (+ (S A) y) (S (+ A y)) pa_ax2 biimpi A y pa_ax4 (+ A (S y)) (S (+ A y)) pa_ax2 mpbi syl6eqr (S A) y pa_ax4 syl5eq finds ) thm (addcom () () (= (+ A B) (+ B A)) x (0) B addeq1 x (0) B addeq2 eqeq12d x y B addeq1 x y B addeq2 eqeq12d x (S y) B addeq1 x (S y) B addeq2 eqeq12d x A B addeq1 x A B addeq2 eqeq12d B pa_ax3r B pa_ax3 eqtr4 (+ y B) (+ B y) pa_ax2 biimpi y B pa_ax4r syl5eq B y pa_ax4 syl6eqr finds ) thm (addass () () (= (+ (+ A B) C) (+ A (+ B C))) x (0) B addeq1 C addeq1d x (0) (+ B C) addeq1 eqeq12d x y B addeq1 C addeq1d x y (+ B C) addeq1 eqeq12d x (S y) B addeq1 C addeq1d x (S y) (+ B C) addeq1 eqeq12d x A B addeq1 C addeq1d x A (+ B C) addeq1 eqeq12d B pa_ax3r C addeq1i (+ B C) pa_ax3r eqtr4 (+ (+ y B) C) (+ y (+ B C)) pa_ax2 biimpi y B pa_ax4r C addeq1i (+ y B) C pa_ax4r eqtr y (+ B C) pa_ax4r 3eqtr4g finds ) thm (pa_ax5r () () (= (* (0) A) (0)) x (0) (0) muleq2 (0) eqeq1d x y (0) muleq2 (0) eqeq1d x (S y) (0) muleq2 (0) eqeq1d x A (0) muleq2 (0) eqeq1d (0) pa_ax5 (0) y pa_ax6 (* (0) y) pa_ax3 eqtr (0) eqeq1i biimpri finds ) thm (pa_ax6r () () (= (* (S A) B) (+ (* A B) B)) x (0) (S A) muleq2 x (0) A muleq2 (= x (0)) id addeq12d eqeq12d x y (S A) muleq2 x y A muleq2 (= x y) id addeq12d eqeq12d x (S y) (S A) muleq2 x (S y) A muleq2 (= x (S y)) id addeq12d eqeq12d x B (S A) muleq2 x B A muleq2 (= x B) id addeq12d eqeq12d (S A) pa_ax5 A pa_ax5 (0) addeq1i (0) pa_ax3 eqtr eqtr4 (* (S A) y) (+ (* A y) y) (S A) addeq1 (S A) y pa_ax6 syl5eq (+ (* A y) y) A pa_ax4 syl6eq (* A y) y A addass y A addcom (* A y) addeq2i eqtr (* A y) A y addass eqtr4 (+ (+ (* A y) y) A) (+ (+ (* A y) A) y) pa_ax2 mpbi syl6eq A y pa_ax6 (S y) addeq1i (+ (* A y) A) y pa_ax4 eqtr syl6eqr finds ) thm (mulcom () () (= (* A B) (* B A)) x (0) B muleq1 x (0) B muleq2 eqeq12d x y B muleq1 x y B muleq2 eqeq12d x (S y) B muleq1 x (S y) B muleq2 eqeq12d x A B muleq1 x A B muleq2 eqeq12d B pa_ax5r B pa_ax5 eqtr4 (* y B) (* B y) B addeq1 y B pa_ax6r syl5eq B y pa_ax6 syl6eqr finds ) thm (add23 () () (= (+ (+ A B) C) (+ (+ A C) B)) A B C addass B C addcom A addeq2i eqtr A C B addass eqtr4 ) thm (add4 () () (= (+ (+ A B) (+ C D)) (+ (+ A C) (+ B D))) (+ A B) C D addass A B C add23 D addeq1i eqtr3 (+ A C) B D addass eqtr ) thm (distr () () (= (* A (+ B C)) (+ (* A B) (* A C))) x (0) (+ B C) muleq1 x (0) B muleq1 x (0) C muleq1 addeq12d eqeq12d x y (+ B C) muleq1 x y B muleq1 x y C muleq1 addeq12d eqeq12d x (S y) (+ B C) muleq1 x (S y) B muleq1 x (S y) C muleq1 addeq12d eqeq12d x A (+ B C) muleq1 x A B muleq1 x A C muleq1 addeq12d eqeq12d (+ B C) pa_ax5r B pa_ax5r C pa_ax5r addeq12i (0) pa_ax3 eqtr eqtr4 (* y (+ B C)) (+ (* y B) (* y C)) (+ B C) addeq1 y (+ B C) pa_ax6r syl5eq y B pa_ax6r y C pa_ax6r addeq12i (* y B) B (* y C) C add4 eqtr syl6eqr finds ) thm (mulass () () (= (* (* A B) C) (* A (* B C))) x (0) B muleq1 C muleq1d x (0) (* B C) muleq1 eqeq12d x y B muleq1 C muleq1d x y (* B C) muleq1 eqeq12d x (S y) B muleq1 C muleq1d x (S y) (* B C) muleq1 eqeq12d x A B muleq1 C muleq1d x A (* B C) muleq1 eqeq12d B pa_ax5r C muleq1i C pa_ax5r eqtr (* B C) pa_ax5r eqtr4 (* (* y B) C) (* y (* B C)) (* B C) addeq1 y B pa_ax6r C muleq1i C (+ (* y B) B) mulcom C (* y B) B distr eqtr3 eqtr C (* y B) mulcom C B mulcom addeq12i eqtr syl5eq y (* B C) pa_ax6r syl6eqr finds )