| |
(1) | Theorem 1 | ∀a: a=a |
(2) | Theorem 2 | ∀a: ¬Sa=a |
| |
(3) | Theorem 3 | ∀a: <∀b: ¬Sb=a ⇒ a=0> |
| |
(4) | Theorem 4 | ∀a: ∀b: <(a+b)=0 ⇒ <a=0∧b=0>> |
| |
(5) | Theorem 5 | ∀a: (0+a)=a |
(6) | Theorem 6 | ∀a: ∀b: (Sa+b)=S(a+b) |
(7) | Theorem 7 | ∀a: ∀b: (a+Sb)=(Sa+b) |
| |
(8) | Theorem 8 | ∀a: ∀b: (a+b)=(b+a) |
| |
(9) | Theorem 9 | ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> |
| |
(10) | Theorem 10 | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a+b)=(c+d)> |
| |
(11) | Theorem 11 | ∀a: ∀b: <b=0 ⇒ (a+b)=a> |
| |
(12) | Theorem 12 | ∀a: ∀b: ∀c: (a+(b+c))=((a+b)+c) |
| |
(13) | Theorem 13 | ∀a: (0·a)=0 |
| |
(14) | Theorem 14 | ∀a: ∀b: <(a·b)=0 ⇒ ¬<¬a=0∧¬b=0>> |
(15) | Theorem 15 | ∀a: ∀b: (Sa·b)=((a·b)+b) |
| |
(16) | Theorem 16 | ∀a: ∀b: (a·b)=(b·a) |
| |
(17) | Theorem 17 | ∀a: ∀b: ∀c: <a=b ⇒ (a·c)=(b·c)> |
| |
(18) | Theorem 18 | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a·b)=(c·d)> |
(19) | Theorem 19 | ∀a: ∀b: <b=0 ⇒ (a·b)=0> |
| |
(20) | Theorem 20 | ∀a: ∀b: ∀c: (a·(b+c))=((a·b)+(a·c)) |
| |
(21) | Theorem 21 | ∀a: ∀b: ∀c: (a·(b·c))=((a·b)·c) |
| |
(22) | Theorem 22 | ∀a: ∀b: ∀c: <(a+c)=(b+c) ⇒ a=b> |
| |
(23) | Theorem 23 | ∀b: ¬<¬∀c: ¬(SSSS0+Sc)=b∧¬∀d: ¬(b+Sd)=SSSSS0> |
| |
(24) | Theorem 24 | ∀b: ¬<¬∀c: ¬(SSSS0+Sc)=b∧¬∀d: ¬(b+Sd)=SSSSS0> |
| |
(25) | Theorem 25 | ∀a: (a·S0)=a |
(26) | Theorem 26 | ∀a: ∀b: <b=S0 ⇒ (a·b)=a> |
(27) | Theorem 27 | ∀a: ∀b: <(a+b)=a ⇒ b=0> |
| |
(28) | Theorem 28 | ∀a: ∀b: ∀c: <(Sc·a)=(Sc·b) ⇒ a=b> |
(29) | Theorem 29 | ∀a: ∀b: <(Sa·b)=0 ⇒ b=0> |
(30) | Theorem 30 | ∀a: ∀b: <(Sa·b)=Sa ⇒ b=S0> |
(31) | Theorem 31 | ∀a: ∀b: <(a·b)=S0 ⇒ <a=S0∧b=S0>> |
| |
(32) | Theorem 32 | ∀a: ¬∀d: ¬(a+d)=a |
(33) | Theorem 33 | <<¬∀e: ¬(a+e)=b∧¬∀f: ¬(b+f)=c> ⇒ ¬∀e: ∀f: ¬<(a+e)=b∧(b+f)=c>> |
(34) | Theorem 34 | <∀e: ∀f: <<(a+e)=b∧(b+f)=c> ⇒ (a+(e+f))=c> ⇒ <¬∀e: ∀f: ¬<(a+e)=b∧(b+f)=c> ⇒ ¬∀e: ∀f: ¬(a+(e+f))=c>> |
(35) | Theorem 35 | <¬∀e: ∀f: ¬(a+(e+f))=c ⇒ ¬∀d: ¬(a+d)=c> |
| |
(36) | Theorem 36 | ∀a: ∀b: ∀c: <<¬∀e: ¬(a+e)=b∧¬∀f: ¬(b+f)=c> ⇒ ¬∀d: ¬(a+d)=c> |
| |
(37) | Theorem 37 | ∀a: ∀b: <<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> ⇒ a=b> |
| |
(38) | Theorem 38 | ∀a: ¬∀b: ¬(0+b)=a |
| |
(39) | Theorem 39 | ∀b: <∀c: ¬(0+c)=b ⇒ ¬∀c: ¬(b+c)=0> |
| |
(40) | Theorem 40 | ∀a: ∀b: <∀c: ¬(a+c)=b ⇒ ¬∀c: ¬(b+c)=a> |
| |
(41) | Theorem 41 | ∀a: ¬∀b: ¬(a·Sb)=a |
(42) | Theorem 42 | <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c>> |
(43) | Theorem 43 | <∀e: ∀f: <<(a·Se)=b∧(b·Sf)=c> ⇒ (a·(Se·Sf))=c> ⇒ <¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c> ⇒ ¬∀e: ∀f: ¬(a·(Se·Sf))=c>> |
(44) | Theorem 44 | <¬∀e: ∀f: ¬(a·(Se·Sf))=c ⇒ ¬∀d: ¬(a·Sd)=c> |
| |
(45) | Theorem 45 | ∀a: ∀b: ∀c: <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀d: ¬(a·Sd)=c> |
| |
(46) | Theorem 46 | ∀a: ∀b: <<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> ⇒ a=b> |
| |
(47) | Theorem 47 | ∀a: ∀b: <<¬∀d: ¬(a+d)=Sb∧¬a=Sb> ⇒ ¬∀d: ¬(a+d)=b> |
| |
(48) | Theorem 48 | |