Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 4 | ∀a: (a·0)=0 | |||||||||
| (2) | Spezialisierung (1) a ← Sc | (Sc·0)=0 | |||||||||
| (3) | Theorem 14 | ∀a: ∀b: <(a·b)=0 ⇒ ¬<¬a=0∧¬b=0>> | |||||||||
| (4) | Spezialisierung (3) a ← Sc | ∀b: <(Sc·b)=0 ⇒ ¬<¬Sc=0∧¬b=0>> | |||||||||
| (5) | Spezialisierung (4) b ← a | <(Sc·a)=0 ⇒ ¬<¬Sc=0∧¬a=0>> | |||||||||
| (6) | Axiom 1 | ∀a: ¬Sa=0 | |||||||||
| (7) | Spezialisierung (6) a ← c | ¬Sc=0 | |||||||||
| (8) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (9) | Spezialisierung (8) a ← Sc | ∀b: (Sc·Sb)=((Sc·b)+Sc) | |||||||||
| (10) | Spezialisierung (9) b ← a | (Sc·Sa)=((Sc·a)+Sc) | |||||||||
| (11) | Spezialisierung (9) b ← b | (Sc·Sb)=((Sc·b)+Sc) | |||||||||
| (12) | Theorem 22 | ∀a: ∀b: ∀c: <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (13) | Spezialisierung (12) a ← (c·a) | ∀b: ∀c: <((c·a)+c)=(b+c) ⇒ (c·a)=b> | |||||||||
| (14) | Spezialisierung (13) b ← (c·b) | ∀c: <((c·a)+c)=((c·b)+c) ⇒ (c·a)=(c·b)> | |||||||||
| (15) | Spezialisierung (14) c ← Sc | <((Sc·a)+Sc)=((Sc·b)+Sc) ⇒ (Sc·a)=(Sc·b)> | |||||||||
| (16) | Hypothese | (Sc·a)=(Sc·0) | |||||||||
| (17) | Übernahme (2) | (Sc·0)=0 | |||||||||
| (18) | Transitivität (16), (17) | (Sc·a)=0 | |||||||||
| (19) | Übernahme (5) | <(Sc·a)=0 ⇒ ¬<¬Sc=0∧¬a=0>> | |||||||||
| (20) | Modus ponens (19), (18) | ¬<¬Sc=0∧¬a=0> | |||||||||
| (21) | Hypothese | ¬a=0 | |||||||||
| (22) | Übernahme (7) | ¬Sc=0 | |||||||||
| (23) | Konjunktion (22), (21) | <¬Sc=0∧¬a=0> | |||||||||
| (24) | Konklusion (21), (23) | <¬a=0 ⇒ <¬Sc=0∧¬a=0>> | |||||||||
| (25) | Kontraposition (24) | <¬<¬Sc=0∧¬a=0> ⇒ ¬¬a=0> | |||||||||
| (26) | Modus ponens (25), (20) | ¬¬a=0 | |||||||||
| (27) | Doppelte Negation (26) | a=0 | |||||||||
| (28) | Konklusion (16), (27) | <(Sc·a)=(Sc·0) ⇒ a=0> | |||||||||
| (29) | Verallgemeinerung (28) nach a | ∀a: <(Sc·a)=(Sc·0) ⇒ a=0> | |||||||||
| (30) | Spezialisierung (29) a ← Sb | <(Sc·Sb)=(Sc·0) ⇒ Sb=0> | |||||||||
| (31) | Hypothese | (Sc·0)=(Sc·Sb) | |||||||||
| (32) | Symmetrie (31) | (Sc·Sb)=(Sc·0) | |||||||||
| (33) | Übernahme (30) | <(Sc·Sb)=(Sc·0) ⇒ Sb=0> | |||||||||
| (34) | Modus ponens (33), (32) | Sb=0 | |||||||||
| (35) | Symmetrie (34) | 0=Sb | |||||||||
| (36) | Konklusion (31), (35) | <(Sc·0)=(Sc·Sb) ⇒ 0=Sb> | |||||||||
| (37) | Hypothese | ∀a: <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
| (38) | Spezialisierung (37) a ← a | <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
| (39) | Hypothese | (Sc·Sa)=(Sc·Sb) | |||||||||
| (40) | Übernahme (10) | (Sc·Sa)=((Sc·a)+Sc) | |||||||||
| (41) | Symmetrie (40) | ((Sc·a)+Sc)=(Sc·Sa) | |||||||||
| (42) | Transitivität (41), (39) | ((Sc·a)+Sc)=(Sc·Sb) | |||||||||
| (43) | Übernahme (11) | (Sc·Sb)=((Sc·b)+Sc) | |||||||||
| (44) | Transitivität (42), (43) | ((Sc·a)+Sc)=((Sc·b)+Sc) | |||||||||
| (45) | Übernahme (15) | <((Sc·a)+Sc)=((Sc·b)+Sc) ⇒ (Sc·a)=(Sc·b)> | |||||||||
| (46) | Modus ponens (45), (44) | (Sc·a)=(Sc·b) | |||||||||
| (47) | Übernahme (38) | <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
| (48) | Modus ponens (47), (46) | a=b | |||||||||
| (49) | S hinzufügen (48) | Sa=Sb | |||||||||
| (50) | Konklusion (39), (49) | <(Sc·Sa)=(Sc·Sb) ⇒ Sa=Sb> | |||||||||
| (51) | Hypothese | <(Sc·a)=(Sc·Sb) ⇒ a=Sb> | |||||||||
| (52) | Übernahme (50) | <(Sc·Sa)=(Sc·Sb) ⇒ Sa=Sb> | |||||||||
| (53) | Konklusion (51), (52) | <<(Sc·a)=(Sc·Sb) ⇒ a=Sb> ⇒ <(Sc·Sa)=(Sc·Sb) ⇒ Sa=Sb>> | |||||||||
| (54) | Verallgemeinerung (53) nach a | ∀a: <<(Sc·a)=(Sc·Sb) ⇒ a=Sb> ⇒ <(Sc·Sa)=(Sc·Sb) ⇒ Sa=Sb>> | |||||||||
| (55) | Übernahme (36) | <(Sc·0)=(Sc·Sb) ⇒ 0=Sb> | |||||||||
| (56) | Induktion (55), (54) | ∀a: <(Sc·a)=(Sc·Sb) ⇒ a=Sb> | |||||||||
| (57) | Konklusion (37), (56) | <∀a: <(Sc·a)=(Sc·b) ⇒ a=b> ⇒ ∀a: <(Sc·a)=(Sc·Sb) ⇒ a=Sb>> | |||||||||
| (58) | Verallgemeinerung (57) nach b | ∀b: <∀a: <(Sc·a)=(Sc·b) ⇒ a=b> ⇒ ∀a: <(Sc·a)=(Sc·Sb) ⇒ a=Sb>> | |||||||||
| (59) | Induktion (29), (58) | ∀b: ∀a: <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
| (60) | Spezialisierung (59) b ← b | ∀a: <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
| (61) | Spezialisierung (60) a ← a | <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
| (62) | Verallgemeinerung (61) nach c | ∀c: <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
| (63) | Verallgemeinerung (62) nach b | ∀b: ∀c: <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
| (64) | Verallgemeinerung (63) nach a | ∀a: ∀b: ∀c: <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
Interpretation:
Kürzungsregel für Faktoren