Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 9 | ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (2) | Spezialisierung (1) a ← (a+e) | ∀b: ∀c: <(a+e)=b ⇒ ((a+e)+c)=(b+c)> | |||||||||
| (3) | Spezialisierung (2) b ← b | ∀c: <(a+e)=b ⇒ ((a+e)+c)=(b+c)> | |||||||||
| (4) | Spezialisierung (3) c ← f | <(a+e)=b ⇒ ((a+e)+f)=(b+f)> | |||||||||
| (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 ← e | ∀c: (a+(e+c))=((a+e)+c) | |||||||||
| (8) | Spezialisierung (7) c ← f | (a+(e+f))=((a+e)+f) | |||||||||
| (9) | Hypothese | <(a+e)=b∧(b+f)=c> | |||||||||
| (10) | Abtrennung I (9) | (a+e)=b | |||||||||
| (11) | Übernahme (4) | <(a+e)=b ⇒ ((a+e)+f)=(b+f)> | |||||||||
| (12) | Modus ponens (11), (10) | ((a+e)+f)=(b+f) | |||||||||
| (13) | Abtrennung II (9) | (b+f)=c | |||||||||
| (14) | Transitivität (12), (13) | ((a+e)+f)=c | |||||||||
| (15) | Übernahme (8) | (a+(e+f))=((a+e)+f) | |||||||||
| (16) | Transitivität (15), (14) | (a+(e+f))=c | |||||||||
| (17) | Konklusion (9), (16) | <<(a+e)=b∧(b+f)=c> ⇒ (a+(e+f))=c> | |||||||||
| (18) | Verallgemeinerung (17) nach f | ∀f: <<(a+e)=b∧(b+f)=c> ⇒ (a+(e+f))=c> | |||||||||
| (19) | Verallgemeinerung (18) nach e | ∀e: ∀f: <<(a+e)=b∧(b+f)=c> ⇒ (a+(e+f))=c> | |||||||||
| (20) | 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>> | |||||||||
| (21) | Modus ponens (20), (19) | <¬∀e: ∀f: ¬<(a+e)=b∧(b+f)=c> ⇒ ¬∀e: ∀f: ¬(a+(e+f))=c> | |||||||||
| (22) | Theorem 33 | <<¬∀e: ¬(a+e)=b∧¬∀f: ¬(b+f)=c> ⇒ ¬∀e: ∀f: ¬<(a+e)=b∧(b+f)=c>> | |||||||||
| (23) | Theorem 35 | <¬∀e: ∀f: ¬(a+(e+f))=c ⇒ ¬∀d: ¬(a+d)=c> | |||||||||
| (24) | Hypothese | <¬∀e: ¬(a+e)=b∧¬∀f: ¬(b+f)=c> | |||||||||
| (25) | Übernahme (22) | <<¬∀e: ¬(a+e)=b∧¬∀f: ¬(b+f)=c> ⇒ ¬∀e: ∀f: ¬<(a+e)=b∧(b+f)=c>> | |||||||||
| (26) | Modus ponens (25), (24) | ¬∀e: ∀f: ¬<(a+e)=b∧(b+f)=c> | |||||||||
| (27) | Übernahme (21) | <¬∀e: ∀f: ¬<(a+e)=b∧(b+f)=c> ⇒ ¬∀e: ∀f: ¬(a+(e+f))=c> | |||||||||
| (28) | Modus ponens (27), (26) | ¬∀e: ∀f: ¬(a+(e+f))=c | |||||||||
| (29) | Übernahme (23) | <¬∀e: ∀f: ¬(a+(e+f))=c ⇒ ¬∀d: ¬(a+d)=c> | |||||||||
| (30) | Modus ponens (29), (28) | ¬∀d: ¬(a+d)=c | |||||||||
| (31) | Konklusion (24), (30) | <<¬∀e: ¬(a+e)=b∧¬∀f: ¬(b+f)=c> ⇒ ¬∀d: ¬(a+d)=c> | |||||||||
| (32) | Verallgemeinerung (31) nach c | ∀c: <<¬∀e: ¬(a+e)=b∧¬∀f: ¬(b+f)=c> ⇒ ¬∀d: ¬(a+d)=c> | |||||||||
| (33) | Verallgemeinerung (32) nach b | ∀b: ∀c: <<¬∀e: ¬(a+e)=b∧¬∀f: ¬(b+f)=c> ⇒ ¬∀d: ¬(a+d)=c> | |||||||||
| (34) | Verallgemeinerung (33) nach a | ∀a: ∀b: ∀c: <<¬∀e: ¬(a+e)=b∧¬∀f: ¬(b+f)=c> ⇒ ¬∀d: ¬(a+d)=c> | |||||||||
Interpretation:
≤ ist transitiv