Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 9 | ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (2) | Spezialisierung (1) a ← (a+d) | ∀b: ∀c: <(a+d)=b ⇒ ((a+d)+c)=(b+c)> | |||||||||
| (3) | Spezialisierung (2) b ← b | ∀c: <(a+d)=b ⇒ ((a+d)+c)=(b+c)> | |||||||||
| (4) | Spezialisierung (3) c ← e | <(a+d)=b ⇒ ((a+d)+e)=(b+e)> | |||||||||
| (5) | Theorem 12 | ∀a: ∀b: ∀c: (a+(b+c))=((a+b)+c) | |||||||||
| (6) | Spezialisierung (5) a ← a | ∀b: ∀c: (a+(b+c))=((a+b)+c) | |||||||||
| (7) | Spezialisierung (6) b ← d | ∀c: (a+(d+c))=((a+d)+c) | |||||||||
| (8) | Spezialisierung (7) c ← e | (a+(d+e))=((a+d)+e) | |||||||||
| (9) | Theorem 27 | ∀a: ∀b: <(a+b)=a ⇒ b=0> | |||||||||
| (10) | Spezialisierung (9) a ← a | ∀b: <(a+b)=a ⇒ b=0> | |||||||||
| (11) | Spezialisierung (10) b ← (d+e) | <(a+(d+e))=a ⇒ (d+e)=0> | |||||||||
| (12) | Theorem 4 | ∀a: ∀b: <(a+b)=0 ⇒ <a=0∧b=0>> | |||||||||
| (13) | Spezialisierung (12) a ← d | ∀b: <(d+b)=0 ⇒ <d=0∧b=0>> | |||||||||
| (14) | Spezialisierung (13) b ← e | <(d+e)=0 ⇒ <d=0∧e=0>> | |||||||||
| (15) | Theorem 11 | ∀a: ∀b: <b=0 ⇒ (a+b)=a> | |||||||||
| (16) | Spezialisierung (15) a ← a | ∀b: <b=0 ⇒ (a+b)=a> | |||||||||
| (17) | Spezialisierung (16) b ← d | <d=0 ⇒ (a+d)=a> | |||||||||
| (18) | Hypothese | <(a+d)=b∧(b+e)=a> | |||||||||
| (19) | Abtrennung I (18) | (a+d)=b | |||||||||
| (20) | Abtrennung II (18) | (b+e)=a | |||||||||
| (21) | Übernahme (4) | <(a+d)=b ⇒ ((a+d)+e)=(b+e)> | |||||||||
| (22) | Modus ponens (21), (19) | ((a+d)+e)=(b+e) | |||||||||
| (23) | Transitivität (22), (20) | ((a+d)+e)=a | |||||||||
| (24) | Übernahme (8) | (a+(d+e))=((a+d)+e) | |||||||||
| (25) | Transitivität (24), (23) | (a+(d+e))=a | |||||||||
| (26) | Übernahme (11) | <(a+(d+e))=a ⇒ (d+e)=0> | |||||||||
| (27) | Modus ponens (26), (25) | (d+e)=0 | |||||||||
| (28) | Übernahme (14) | <(d+e)=0 ⇒ <d=0∧e=0>> | |||||||||
| (29) | Modus ponens (28), (27) | <d=0∧e=0> | |||||||||
| (30) | Abtrennung I (29) | d=0 | |||||||||
| (31) | Übernahme (17) | <d=0 ⇒ (a+d)=a> | |||||||||
| (32) | Modus ponens (31), (30) | (a+d)=a | |||||||||
| (33) | Symmetrie (32) | a=(a+d) | |||||||||
| (34) | Transitivität (33), (19) | a=b | |||||||||
| (35) | Konklusion (18), (34) | <<(a+d)=b∧(b+e)=a> ⇒ a=b> | |||||||||
| (36) | Kontraposition (35) | <¬a=b ⇒ ¬<(a+d)=b∧(b+e)=a>> | |||||||||
| (37) | Hypothese | ¬a=b | |||||||||
| (38) | Übernahme (36) | <¬a=b ⇒ ¬<(a+d)=b∧(b+e)=a>> | |||||||||
| (39) | Modus ponens (38), (37) | ¬<(a+d)=b∧(b+e)=a> | |||||||||
| (40) | Hypothese | (a+d)=b | |||||||||
| (41) | Hypothese | (b+e)=a | |||||||||
| (42) | Übernahme (40) | (a+d)=b | |||||||||
| (43) | Konjunktion (42), (41) | <(a+d)=b∧(b+e)=a> | |||||||||
| (44) | Konklusion (41), (43) | <(b+e)=a ⇒ <(a+d)=b∧(b+e)=a>> | |||||||||
| (45) | Kontraposition (44) | <¬<(a+d)=b∧(b+e)=a> ⇒ ¬(b+e)=a> | |||||||||
| (46) | Übernahme (39) | ¬<(a+d)=b∧(b+e)=a> | |||||||||
| (47) | Modus ponens (45), (46) | ¬(b+e)=a | |||||||||
| (48) | Verallgemeinerung (47) nach e | ∀e: ¬(b+e)=a | |||||||||
| (49) | Spezialisierung (48) e ← c | ¬(b+c)=a | |||||||||
| (50) | Verallgemeinerung (49) nach c | ∀c: ¬(b+c)=a | |||||||||
| (51) | Konklusion (40), (50) | <(a+d)=b ⇒ ∀c: ¬(b+c)=a> | |||||||||
| (52) | Kontraposition (51) | <¬∀c: ¬(b+c)=a ⇒ ¬(a+d)=b> | |||||||||
| (53) | Hypothese | ¬∀c: ¬(b+c)=a | |||||||||
| (54) | Übernahme (52) | <¬∀c: ¬(b+c)=a ⇒ ¬(a+d)=b> | |||||||||
| (55) | Modus ponens (54), (53) | ¬(a+d)=b | |||||||||
| (56) | Verallgemeinerung (55) nach d | ∀d: ¬(a+d)=b | |||||||||
| (57) | Spezialisierung (56) d ← c | ¬(a+c)=b | |||||||||
| (58) | Verallgemeinerung (57) nach c | ∀c: ¬(a+c)=b | |||||||||
| (59) | Konklusion (53), (58) | <¬∀c: ¬(b+c)=a ⇒ ∀c: ¬(a+c)=b> | |||||||||
| (60) | Hypothese | <¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> | |||||||||
| (61) | Abtrennung I (60) | ¬∀c: ¬(b+c)=a | |||||||||
| (62) | Hypothese | <¬∀c: ¬(b+c)=a ⇒ ∀c: ¬(a+c)=b> | |||||||||
| (63) | Übernahme (61) | ¬∀c: ¬(b+c)=a | |||||||||
| (64) | Modus ponens (62), (63) | ∀c: ¬(a+c)=b | |||||||||
| (65) | Konklusion (62), (64) | <<¬∀c: ¬(b+c)=a ⇒ ∀c: ¬(a+c)=b> ⇒ ∀c: ¬(a+c)=b> | |||||||||
| (66) | Kontraposition (65) | <¬∀c: ¬(a+c)=b ⇒ ¬<¬∀c: ¬(b+c)=a ⇒ ∀c: ¬(a+c)=b>> | |||||||||
| (67) | Abtrennung II (60) | ¬∀c: ¬(a+c)=b | |||||||||
| (68) | Modus ponens (66), (67) | ¬<¬∀c: ¬(b+c)=a ⇒ ∀c: ¬(a+c)=b> | |||||||||
| (69) | Konklusion (60), (68) | <<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> ⇒ ¬<¬∀c: ¬(b+c)=a ⇒ ∀c: ¬(a+c)=b>> | |||||||||
| (70) | Kontraposition (69) | <¬¬<¬∀c: ¬(b+c)=a ⇒ ∀c: ¬(a+c)=b> ⇒ ¬<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b>> | |||||||||
| (71) | Doppelte Negation (59) | ¬¬<¬∀c: ¬(b+c)=a ⇒ ∀c: ¬(a+c)=b> | |||||||||
| (72) | Modus ponens (70), (71) | ¬<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> | |||||||||
| (73) | Konklusion (37), (72) | <¬a=b ⇒ ¬<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b>> | |||||||||
| (74) | Kontraposition (73) | <¬¬<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> ⇒ ¬¬a=b> | |||||||||
| (75) | Hypothese | <¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> | |||||||||
| (76) | Doppelte Negation (75) | ¬¬<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> | |||||||||
| (77) | Übernahme (74) | <¬¬<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> ⇒ ¬¬a=b> | |||||||||
| (78) | Modus ponens (77), (76) | ¬¬a=b | |||||||||
| (79) | Doppelte Negation (78) | a=b | |||||||||
| (80) | Konklusion (75), (79) | <<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> ⇒ a=b> | |||||||||
| (81) | Verallgemeinerung (80) nach b | ∀b: <<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> ⇒ a=b> | |||||||||
| (82) | Verallgemeinerung (81) nach a | ∀a: ∀b: <<¬∀c: ¬(b+c)=a∧¬∀c: ¬(a+c)=b> ⇒ a=b> | |||||||||
Interpretation:
≤ ist eine Ordnungsrelation