david.mihola
24-11-2008, 15:55
Thread-Titel ist falsch! Sollte lauten: Ideen für 7.3?
Hat jemand irgendeine Idee, wie man 7.3 angehen könnte? Die Erklärungen zum Hilbert-Kalkül im Skriptum und auf den Folien sind ja ziemlich knapp gehalten...
Von der Idee her ist mir der Hilbert-Kalküĺ schon klar, aber mir fehlt eine Arbeitsanleitung für die Lösung des Beispiels - grundsätzlich scheint es ja so zu funktionieren:
Damit ich unter dem Strich B ⊃ ((A ∨ A) ⊃ A) rauskrieg brauch ich über dem Strich etwas auf diese Art:
linker Teil: [Formel X]
rechter Teil: [Formel X] ⊃ (B ⊃ ((A ∨ A) ⊃ A))
wobei der linke und der rechte Teil entweder selbst Axiome oder wieder das Ergebnis eines Modus Ponens sind.
Dazu aber ein paar Fragen:
* Ich kann die Buchstaben aus den Axiomen ja offenbar beliebig gegen andere Buchstaben oder Formeln ersetzen, oder? (Vgl. Beispiel von den Folien: In A ⊃ (B ⊃ A) wird das B durch A ⊃ A ersetzt). Oder ist das nicht so ganz willkürlich - welche Regeln gelten dann?
* Da es nur den MP als einzige Regel gibt, folgt auch, dass von "über dem Strich" nach "unter den Strich" die Ausdrücke immer kürzer werden - es fällt immer [Formel X] weg, an dem übrigen ändert sich aber durch eine Regelanwendung nie etwas, richtig?
* Das würde für unser Beispiel bedeuten, dass man auf jeden Fall Axiom 5 braucht, denn nur dieses enthält hinten ((A ∨ B) ⊃ C) was man in ((A ∨ A) ⊃ A) überführen könnte (durch ersetzen). Aber wie mach ich dann das (B ⊃ C) zu B?
Kurz gesagt: Bis auf ein paar vage Ideen steh' ich total auf der Leitung und wäre für Hinweise dankbar. (Wurde in der VO vielleicht noch irgendwas dazu gesagt, was im Skriptum nicht drin steht?)
Danke schon mal und LG
David
Hat jemand irgendeine Idee, wie man 7.3 angehen könnte? Die Erklärungen zum Hilbert-Kalkül im Skriptum und auf den Folien sind ja ziemlich knapp gehalten...
Von der Idee her ist mir der Hilbert-Kalküĺ schon klar, aber mir fehlt eine Arbeitsanleitung für die Lösung des Beispiels - grundsätzlich scheint es ja so zu funktionieren:
Damit ich unter dem Strich B ⊃ ((A ∨ A) ⊃ A) rauskrieg brauch ich über dem Strich etwas auf diese Art:
linker Teil: [Formel X]
rechter Teil: [Formel X] ⊃ (B ⊃ ((A ∨ A) ⊃ A))
wobei der linke und der rechte Teil entweder selbst Axiome oder wieder das Ergebnis eines Modus Ponens sind.
Dazu aber ein paar Fragen:
* Ich kann die Buchstaben aus den Axiomen ja offenbar beliebig gegen andere Buchstaben oder Formeln ersetzen, oder? (Vgl. Beispiel von den Folien: In A ⊃ (B ⊃ A) wird das B durch A ⊃ A ersetzt). Oder ist das nicht so ganz willkürlich - welche Regeln gelten dann?
* Da es nur den MP als einzige Regel gibt, folgt auch, dass von "über dem Strich" nach "unter den Strich" die Ausdrücke immer kürzer werden - es fällt immer [Formel X] weg, an dem übrigen ändert sich aber durch eine Regelanwendung nie etwas, richtig?
* Das würde für unser Beispiel bedeuten, dass man auf jeden Fall Axiom 5 braucht, denn nur dieses enthält hinten ((A ∨ B) ⊃ C) was man in ((A ∨ A) ⊃ A) überführen könnte (durch ersetzen). Aber wie mach ich dann das (B ⊃ C) zu B?
Kurz gesagt: Bis auf ein paar vage Ideen steh' ich total auf der Leitung und wäre für Hinweise dankbar. (Wurde in der VO vielleicht noch irgendwas dazu gesagt, was im Skriptum nicht drin steht?)
Danke schon mal und LG
David