Beispiel für Beweis < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
| Status: |
(Frage) überfällig  | | Datum: | 23:37 Sa 02.12.2006 | | Autor: | senf |
Ich habe diese Frage in keinem Forum auf anderen Internetseiten gestellt.
Sie bezieht sich auf folgendes "Beispiel für einen formalisierten direkten Beweis" aus dem dtv-Atlas Mathematik Bd 1:
Aus den 4 Axiomen
(1) [mm] \forall [/mm] x [mm] \forall [/mm] y (x=y [mm] \Rightarrow [/mm] y=x)
(2) [mm] \forall [/mm] x [mm] \forall [/mm] y (x=y [mm] \Rightarrow [/mm] (A(x) [mm] \Rightarrow [/mm] A(y)))
(3) [mm] \forall [/mm] x [mm] \forall [/mm] y (x+y=y+x)
(4) [mm] \forall [/mm] x (0+x=x)
ist abzuleiten: [mm] \forall [/mm] x (x+0=x)
Beweis:
(5) x=y [mm] \Rightarrow [/mm] y=x
(6) x=y [mm] \Rightarrow [/mm] (A(x) [mm] \Rightarrow [/mm] A(y))
(7) x+y=y+x
(8) 0+x=x
aus (1),(2),(3),(4) durch Beseitigung des Generalisators
(9) z+0=0+z [mm] \Rightarrow [/mm] 0+z=z+0 aus (5) mit x|z+0, y|0+z
(10) 0+z=z+0 [mm] \Rightarrow [/mm] (0+z=z [mm] \Rightarrow [/mm] z+0=z) aus (6) mit A(u)|u=z, x|0+z, y|z+0
(11) z+0=0+z [mm] \Rightarrow [/mm] (0+z=z [mm] \Rightarrow [/mm] z+0=z) aus (9) und (10) durch modus barbara
(12) z+0=0+z aus (7) mit x|z, y|0
(13) 0+z=z aus (8) mit x|z
(14) z+0=z aus (11), (12), (13) durch modus ponens
(15) [mm] \forall [/mm] z (z+0=z) aus (14) durch Generalisierung
(16) [mm] \forall [/mm] x (x+0=x) aus (15) durch gebundene Umbenennung
Meine Frage: Warum kann man es nicht auch einfacher so machen:
Beweis:
(5) x=y [mm] \Rightarrow [/mm] (A(x) [mm] \Rightarrow [/mm] A(y))
(6) x+y=y+x
(7) 0+x=x
aus (2),(3),(4) durch Beseitigung des Generalisators
(8) 0+z=z+0 [mm] \Rightarrow [/mm] (0+z=z [mm] \Rightarrow [/mm] z+0=z) aus (5) mit A(u)|u=z, x|0+z, y|z+0
(9) 0+z=z+0 aus (6) mit x|0, y|z
(10) 0+z=z aus (7) mit x|z
(11) z+0=z aus (8), (9), (10) durch modus ponens
(12) [mm] \forall [/mm] z (z+0=z) aus (14) durch Generalisierung
(13) [mm] \forall [/mm] x (x+0=x) aus (15) durch gebundene Umbenennung
Hier ist sicher ein Fehler drin, aber ich seh ihn einfach nicht.
Viele Grüße,
Senf
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 00:20 Mi 03.01.2007 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
