Es gelten die allgemeinen Vorbemerkungen.
(1) | Axiom 2 | ∀a: (a+0)=a | |||||||||
(2) | Spezialisierung (1) a ← a | (a+0)=a | |||||||||
(3) | Symmetrie (2) | a=(a+0) | |||||||||
(4) | Theorem 1 | ∀a: a=a | |||||||||
(5) | Spezialisierung (4) a ← 0 | 0=0 | |||||||||
(6) | Hypothese | (a+0)=0 | |||||||||
(7) | Übernahme (3) | a=(a+0) | |||||||||
(8) | Transitivität (7), (6) | a=0 | |||||||||
(9) | Übernahme (5) | 0=0 | |||||||||
(10) | Konjunktion (8), (9) | <a=0∧0=0> | |||||||||
(11) | Konklusion (6), (10) | <(a+0)=0 ⇒ <a=0∧0=0>> | |||||||||
(12) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
(13) | Spezialisierung (12) a ← a | ∀b: (a+Sb)=S(a+b) | |||||||||
(14) | Spezialisierung (13) b ← b | (a+Sb)=S(a+b) | |||||||||
(15) | Symmetrie (14) | S(a+b)=(a+Sb) | |||||||||
(16) | Axiom 1 | ∀a: ¬Sa=0 | |||||||||
(17) | Spezialisierung (16) a ← (a+b) | ¬S(a+b)=0 | |||||||||
(18) | Hypothese | (a+Sb)=0 | |||||||||
(19) | Übernahme (15) | S(a+b)=(a+Sb) | |||||||||
(20) | Transitivität (19), (18) | S(a+b)=0 | |||||||||
(21) | Konklusion (18), (20) | <(a+Sb)=0 ⇒ S(a+b)=0> | |||||||||
(22) | Kontraposition (21) | <¬S(a+b)=0 ⇒ ¬(a+Sb)=0> | |||||||||
(23) | Modus ponens (22), (17) | ¬(a+Sb)=0 | |||||||||
(24) | Hypothese | <(a+b)=0 ⇒ <a=0∧b=0>> | |||||||||
(25) | Hypothese | ¬<a=0∧Sb=0> | |||||||||
(26) | Übernahme (23) | ¬(a+Sb)=0 | |||||||||
(27) | Konklusion (25), (26) | <¬<a=0∧Sb=0> ⇒ ¬(a+Sb)=0> | |||||||||
(28) | Kontraposition (27) | <¬¬(a+Sb)=0 ⇒ ¬¬<a=0∧Sb=0>> | |||||||||
(29) | Hypothese | (a+Sb)=0 | |||||||||
(30) | Doppelte Negation (29) | ¬¬(a+Sb)=0 | |||||||||
(31) | Übernahme (28) | <¬¬(a+Sb)=0 ⇒ ¬¬<a=0∧Sb=0>> | |||||||||
(32) | Modus ponens (31), (30) | ¬¬<a=0∧Sb=0> | |||||||||
(33) | Doppelte Negation (32) | <a=0∧Sb=0> | |||||||||
(34) | Konklusion (29), (33) | <(a+Sb)=0 ⇒ <a=0∧Sb=0>> | |||||||||
(35) | Konklusion (24), (34) | <<(a+b)=0 ⇒ <a=0∧b=0>> ⇒ <(a+Sb)=0 ⇒ <a=0∧Sb=0>>> | |||||||||
(36) | Verallgemeinerung (35) nach b | ∀b: <<(a+b)=0 ⇒ <a=0∧b=0>> ⇒ <(a+Sb)=0 ⇒ <a=0∧Sb=0>>> | |||||||||
(37) | Induktion (11), (36) | ∀b: <(a+b)=0 ⇒ <a=0∧b=0>> | |||||||||
(38) | Verallgemeinerung (37) nach a | ∀a: ∀b: <(a+b)=0 ⇒ <a=0∧b=0>> |
Interpretation:
Eine Summe ist nur dann 0, wenn beide Summanden 0 sind