Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 5 | ∀a: (0+a)=a | |||||||||
| (2) | Spezialisierung (1) a ← Sa | (0+Sa)=Sa | |||||||||
| (3) | Hypothese | ∀c: ¬(0+c)=Sa | |||||||||
| (4) | Spezialisierung (3) c ← Sa | ¬(0+Sa)=Sa | |||||||||
| (5) | Konklusion (3), (4) | <∀c: ¬(0+c)=Sa ⇒ ¬(0+Sa)=Sa> | |||||||||
| (6) | Kontraposition (5) | <¬¬(0+Sa)=Sa ⇒ ¬∀c: ¬(0+c)=Sa> | |||||||||
| (7) | Doppelte Negation (2) | ¬¬(0+Sa)=Sa | |||||||||
| (8) | Modus ponens (6), (7) | ¬∀c: ¬(0+c)=Sa | |||||||||
| (9) | Theorem 6 | ∀a: ∀b: (Sa+b)=S(a+b) | |||||||||
| (10) | Spezialisierung (9) a ← d | ∀b: (Sd+b)=S(d+b) | |||||||||
| (11) | Spezialisierung (10) b ← c | (Sd+c)=S(d+c) | |||||||||
| (12) | Hypothese | (d+c)=b | |||||||||
| (13) | S hinzufügen (12) | S(d+c)=Sb | |||||||||
| (14) | Übernahme (11) | (Sd+c)=S(d+c) | |||||||||
| (15) | Transitivität (14), (13) | (Sd+c)=Sb | |||||||||
| (16) | Konklusion (12), (15) | <(d+c)=b ⇒ (Sd+c)=Sb> | |||||||||
| (17) | Kontraposition (16) | <¬(Sd+c)=Sb ⇒ ¬(d+c)=b> | |||||||||
| (18) | Verallgemeinerung (17) nach d | ∀d: <¬(Sd+c)=Sb ⇒ ¬(d+c)=b> | |||||||||
| (19) | Spezialisierung (18) d ← a | <¬(Sa+c)=Sb ⇒ ¬(a+c)=b> | |||||||||
| (20) | Verallgemeinerung (18) nach b | ∀b: ∀d: <¬(Sd+c)=Sb ⇒ ¬(d+c)=b> | |||||||||
| (21) | Spezialisierung (20) b ← a | ∀d: <¬(Sd+c)=Sa ⇒ ¬(d+c)=a> | |||||||||
| (22) | Spezialisierung (21) d ← b | <¬(Sb+c)=Sa ⇒ ¬(b+c)=a> | |||||||||
| (23) | Hypothese | ∀c: ¬(Sa+c)=0 | |||||||||
| (24) | Übernahme (8) | ¬∀c: ¬(0+c)=Sa | |||||||||
| (25) | Konklusion (23), (24) | <∀c: ¬(Sa+c)=0 ⇒ ¬∀c: ¬(0+c)=Sa> | |||||||||
| (26) | Hypothese | ∀b: <∀c: ¬(a+c)=b ⇒ ¬∀c: ¬(b+c)=a> | |||||||||
| (27) | Spezialisierung (26) b ← b | <∀c: ¬(a+c)=b ⇒ ¬∀c: ¬(b+c)=a> | |||||||||
| (28) | Übernahme (25) | <∀c: ¬(Sa+c)=0 ⇒ ¬∀c: ¬(0+c)=Sa> | |||||||||
| (29) | Hypothese | ∀c: ¬(Sa+c)=Sb | |||||||||
| (30) | Spezialisierung (29) c ← c | ¬(Sa+c)=Sb | |||||||||
| (31) | Übernahme (19) | <¬(Sa+c)=Sb ⇒ ¬(a+c)=b> | |||||||||
| (32) | Modus ponens (31), (30) | ¬(a+c)=b | |||||||||
| (33) | Verallgemeinerung (32) nach c | ∀c: ¬(a+c)=b | |||||||||
| (34) | Übernahme (27) | <∀c: ¬(a+c)=b ⇒ ¬∀c: ¬(b+c)=a> | |||||||||
| (35) | Modus ponens (34), (33) | ¬∀c: ¬(b+c)=a | |||||||||
| (36) | Hypothese | ∀c: ¬(Sb+c)=Sa | |||||||||
| (37) | Spezialisierung (36) c ← c | ¬(Sb+c)=Sa | |||||||||
| (38) | Übernahme (22) | <¬(Sb+c)=Sa ⇒ ¬(b+c)=a> | |||||||||
| (39) | Modus ponens (38), (37) | ¬(b+c)=a | |||||||||
| (40) | Verallgemeinerung (39) nach c | ∀c: ¬(b+c)=a | |||||||||
| (41) | Konklusion (36), (40) | <∀c: ¬(Sb+c)=Sa ⇒ ∀c: ¬(b+c)=a> | |||||||||
| (42) | Kontraposition (41) | <¬∀c: ¬(b+c)=a ⇒ ¬∀c: ¬(Sb+c)=Sa> | |||||||||
| (43) | Modus ponens (42), (35) | ¬∀c: ¬(Sb+c)=Sa | |||||||||
| (44) | Konklusion (29), (43) | <∀c: ¬(Sa+c)=Sb ⇒ ¬∀c: ¬(Sb+c)=Sa> | |||||||||
| (45) | Hypothese | <∀c: ¬(Sa+c)=b ⇒ ¬∀c: ¬(b+c)=Sa> | |||||||||
| (46) | Übernahme (44) | <∀c: ¬(Sa+c)=Sb ⇒ ¬∀c: ¬(Sb+c)=Sa> | |||||||||
| (47) | Konklusion (45), (46) | <<∀c: ¬(Sa+c)=b ⇒ ¬∀c: ¬(b+c)=Sa> ⇒ <∀c: ¬(Sa+c)=Sb ⇒ ¬∀c: ¬(Sb+c)=Sa>> | |||||||||
| (48) | Verallgemeinerung (47) nach b | ∀b: <<∀c: ¬(Sa+c)=b ⇒ ¬∀c: ¬(b+c)=Sa> ⇒ <∀c: ¬(Sa+c)=Sb ⇒ ¬∀c: ¬(Sb+c)=Sa>> | |||||||||
| (49) | Induktion (28), (48) | ∀b: <∀c: ¬(Sa+c)=b ⇒ ¬∀c: ¬(b+c)=Sa> | |||||||||
| (50) | Konklusion (26), (49) | <∀b: <∀c: ¬(a+c)=b ⇒ ¬∀c: ¬(b+c)=a> ⇒ ∀b: <∀c: ¬(Sa+c)=b ⇒ ¬∀c: ¬(b+c)=Sa>> | |||||||||
| (51) | Verallgemeinerung (50) nach a | ∀a: <∀b: <∀c: ¬(a+c)=b ⇒ ¬∀c: ¬(b+c)=a> ⇒ ∀b: <∀c: ¬(Sa+c)=b ⇒ ¬∀c: ¬(b+c)=Sa>> | |||||||||
| (52) | Theorem 39 | ∀b: <∀c: ¬(0+c)=b ⇒ ¬∀c: ¬(b+c)=0> | |||||||||
| (53) | Induktion (52), (51) | ∀a: ∀b: <∀c: ¬(a+c)=b ⇒ ¬∀c: ¬(b+c)=a> | |||||||||
Interpretation:
≤ ist eine Totalordnung