Übersicht

Axiome

(1) Axiom 1 ∀a: ¬Sa=0
(2) Axiom 2 ∀a: (a+0)=a
(3) Axiom 3 ∀a: ∀b: (a+Sb)=S(a+b)
(4) Axiom 4 ∀a: (a·0)=0
(5) Axiom 5 ∀a: ∀b: (a·Sb)=((a·b)+a)

Bisherige Theoreme

Gleichheit ist reflexiv
(1) Theorem 1 ∀a: a=a
(2) Theorem 2 ∀a: ¬Sa=a
Nur 0 hat keinen Vorgänger
(3) Theorem 3 ∀a: <∀b: ¬Sb=a ⇒ a=0>
Eine Summe ist nur dann 0, wenn beide Summanden 0 sind
(4) Theorem 4 ∀a: ∀b: <(a+b)=0 ⇒ <a=0∧b=0>>
0 ist auch linksneutral bei der Addition
(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)
Addition ist kommutativ
(8) Theorem 8 ∀a: ∀b: (a+b)=(b+a)
Addition ist eine Funktion im ersten Summanden
(9) Theorem 9 ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)>
Addition ist eine Funktion in beiden Summanden
(10) Theorem 10 ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a+b)=(c+d)>
Axiom 2 in Funktionsinterpretation
(11) Theorem 11 ∀a: ∀b: <b=0 ⇒ (a+b)=a>
Addition ist assoziativ
(12) Theorem 12 ∀a: ∀b: ∀c: (a+(b+c))=((a+b)+c)
0 annihiliert bei Multiplikation auch von links
(13) Theorem 13 ∀a: (0·a)=0
Ein Produkt ist nur dann 0, wenn ein Faktor 0 ist
(14) Theorem 14 ∀a: ∀b: <(a·b)=0 ⇒ ¬<¬a=0∧¬b=0>>
(15) Theorem 15 ∀a: ∀b: (Sa·b)=((a·b)+b)
Multiplikation ist kommutativ
(16) Theorem 16 ∀a: ∀b: (a·b)=(b·a)
Multipliaktion ist eine Funktion im ersten Faktor
(17) Theorem 17 ∀a: ∀b: ∀c: <a=b ⇒ (a·c)=(b·c)>
Das Produkt ist eine Funktion in beiden Variablen
(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>
Multiplikation ist rechtsdistributiv über die Addition
(20) Theorem 20 ∀a: ∀b: ∀c: (a·(b+c))=((a·b)+(a·c))
Multiplikation ist assoziativ
(21) Theorem 21 ∀a: ∀b: ∀c: (a·(b·c))=((a·b)·c)
Kürzungsregel für Summanden
(22) Theorem 22 ∀a: ∀b: ∀c: <(a+c)=(b+c) ⇒ a=b>
Es gibt keine Zahl zwischen 4 und 5
(23) Theorem 23 ∀b: ¬<¬∀c: ¬(SSSS0+Sc)=b∧¬∀d: ¬(b+Sd)=SSSSS0>
Es gibt keine Zahl zwischen 4 und 5 (direkt aus den Axiomen gezeigt)
(24) Theorem 24 ∀b: ¬<¬∀c: ¬(SSSS0+Sc)=b∧¬∀d: ¬(b+Sd)=SSSSS0>
1 ist multiplikativ rechtsneutral
(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>
Kürzungsregel für Faktoren
(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>>
≤ ist reflexiv
(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>
≤ ist transitiv
(36) Theorem 36 ∀a: ∀b: ∀c: <<¬∀e: ¬(a+e)=b∧¬∀f: ¬(b+f)=c> ⇒ ¬∀d: ¬(a+d)=c>
≤ ist eine Ordnungsrelation
(37) Theorem 37 ∀a: ∀b: <<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> ⇒ a=b>
0 ist die kleinste Zahl bezüglich ≤
(38) Theorem 38 ∀a: ¬∀b: ¬(0+b)=a
≤ ist bei 0 eine Totalordnung
(39) Theorem 39 ∀b: <∀c: ¬(0+c)=b ⇒ ¬∀c: ¬(b+c)=0>
≤ ist eine Totalordnung
(40) Theorem 40 ∀a: ∀b: <∀c: ¬(a+c)=b ⇒ ¬∀c: ¬(b+c)=a>
'teilt' ist reflexiv
(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>
'teilt' ist transitiv
(45) Theorem 45 ∀a: ∀b: ∀c: <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀d: ¬(a·Sd)=c>
'teilt' ist eine Ordnungsrelation
(46) Theorem 46 ∀a: ∀b: <<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> ⇒ a=b>
Ist a<=Sb so a=Sb oder a<=b
(47) Theorem 47 ∀a: ∀b: <<¬∀d: ¬(a+d)=Sb∧¬a=Sb> ⇒ ¬∀d: ¬(a+d)=b>
Gibt es ein gemeinsames Vielfaches von 1...n so auch von 1...Sn
(48) Theorem 48 

Übersicht