Hilbertkalkül < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
| Aufgabe | Geben Sie formale Beweise im Hilbertkalkül der folgenden Formeln an:
1) [mm] $((\exists x\phi)\rightarrow\psi)\rightarrow(\forall x(\phi\rightarrow\psi))$ [/mm] wenn x nicht frei in [mm] $\psi$
[/mm]
2) [mm] $\forall x\forall y\forall [/mm] z [mm] (x=y\rightarrow y=z\rightarrow [/mm] x=z)$
3) [mm] $(\forall y(x=y\rightarrow \phi(y)))\rightarrow \phi(x)$ [/mm] |
Hallo,
leider fallen mir formale Beweise im Hilbertkalkül recht schwer und ich würde gerne diese drei Formeln beweisen.
Den Hilbertkalkül haben wir wie folgt definiert.
Eine L-Formel [mm] $\varphi$ [/mm] heißt beweisbar, wenn [mm] $\varphi$
[/mm]
1) Eine Tautologie ist
2) Ein Gleichheitsaxiom ist
3) Ein [mm] $\exists$-Axiom [/mm] ist
4) Durch den Modus Ponens entsteht aus zwei L-Beweisbaren Formeln
5) Durch [mm] $\exists$ [/mm] Einführung aus einer beweisbaren L-Formel entsteht.
Außerdem haben wir in einem Lemma noch ein paar Eigenschaften
Aussagenlogik, [mm] $\forall$-Einführung [/mm] und [mm] $\forall$-Axiom [/mm] aufgezählt.
Wenn ihr fragen zu den einzelnen Axiomen habt, also unserer Formulierung, dann bitte nachfragen. :)
Zu erst ist mir eines noch unklar, weil dies in meinem Skript leider nicht näher kenntlich gemacht ist. Bei dem [mm] $\exist$-Axiom [/mm] handelt es sich doch um folgendes:
Angenommen [mm] $\varphi$ [/mm] ist eine L-Formel, $t$ ist ein L-Term und $x$ eine Variable, die frei für $t$ in [mm] $\varphi$ [/mm] ist. Dann ist die Formel
[mm] $\varphi\frac{t}{x}\rightarrow\exists x\varphi$ [/mm] allgemeingültig.
Nun eine Frage zum Hilbertkalkül und formalen beweisen. Mir ist klar, dass ich nur die Axiome verwenden darf, oder Formeln die aus den Regeln entstehen.
Wie bei einem "üblichen" beweis muss ich daraus aus dem was "links" der Implikation steht, das was "rechts" der Implikation steht, folgern.
Also bei Aufgabe 1) wäre etwa
[mm] $((\exists\phi)\rightarrow\psi)$ [/mm] und, dass $x$ nicht frei in [mm] $\psi$ [/mm] ist, die Voraussetzung und was ich nun aus den Axiomen und Regeln folgern muss ist
[mm] $(\forall x(\phi\rightarrow\psi))$
[/mm]
Denn bei Aufgabe 2) habe ich ja gar keine Implikation wie in 1) oder 3) gegeben.
Was ist hier zu tun?
Am besten fangen wir auch direkt mit Aufgabe 2) an, da sie mir auch am einfachsten vorkommt.
Denn meiner Meinung nach wäre
2) [mm] \forall x\forall y\forall z(x=y\rightarrow y=z\rightarrow [/mm] x=z)
dies einfach das Gleichheitsaxiom der Symmetrie und Transitivität, die denn da lauten:
[mm] $\forall [/mm] x,y [mm] (x=y\rightarrow [/mm] y=x)$ (Symmetrie)
[mm] $\forall [/mm] x,y,z [mm] (x=y\wedge y=z\rightarrow [/mm] x=z)$ (Transitivität)
Ist es hier bei Aufgabe 2) nun so, dass im Grunde meine "Voraussetzung" nur das
[mm] $\forall [/mm] x,y,z $ ist und ich nun formal beweisen muss, dass dann [mm] $(x=y\rightarrow y=z\rightarrow [/mm] x=z)$ gilt?
Anfangen würde ich so:
[mm] $\forall x\forall y\forall [/mm] z [mm] (x=y\wedge y=z\rightarrow [/mm] x=z)$ nach Transitivität
[mm] $\forall x\forall y\forall [/mm] z [mm] ((x=y\wedge y=z)\rightarrow x=y)\wedge ((x=y\wedge y=z)\rightarrow [/mm] y=z)) nach Symmetrie.
Mit dem Modus Ponens ist also $x=z$ und $y=z$ allgemeingültig.
[mm] $\forall x\forall y\forall [/mm] z [mm] (x=z\wedge y=z\rightarrow [/mm] x=y)$ nach Transitität
Wenn ich wieder den Modus Ponens anwende erhalte ich also
[mm] $\forall x\forall y\forall z(x=y\rightarrow y=z\rightarrow [/mm] x=z)$
Wäre dies so im Kern richtig, oder bereits grundlegend falsch?
Bis zum letzten Schritt bin ich mir relativ sicher, dass es bisher passt. Nur fällt für meinen Geschmack dann das was ich zeigen soll einfach vom Himmel, da fehlt mir dann wohl noch ein passendes Argument...
Über Hilfestellung würde ich mich sehr freuen.
Vielen Dank im voraus.
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 19:06 So 10.05.2015 | | Autor: | tobit09 |
Hallo impliziteFunktion!
> Den Hilbertkalkül haben wir wie folgt definiert.
>
> Eine L-Formel [mm]\varphi[/mm] heißt beweisbar, wenn [mm]\varphi[/mm]
>
> 1) Eine Tautologie ist
>
> 2) Ein Gleichheitsaxiom ist
>
> 3) Ein [mm]\exists[/mm]-Axiom ist
>
> 4) Durch den Modus Ponens entsteht aus zwei L-Beweisbaren
> Formeln
>
> 5) Durch [mm]\exists[/mm] Einführung aus einer beweisbaren L-Formel
> entsteht.
>
> Außerdem haben wir in einem Lemma noch ein paar
> Eigenschaften
>
> Aussagenlogik, [mm]\forall[/mm]-Einführung und [mm]\forall[/mm]-Axiom
> aufgezählt.
>
> Wenn ihr fragen zu den einzelnen Axiomen habt, also unserer
> Formulierung, dann bitte nachfragen. :)
Habt ihr ein öffentlich zugängliches Skript, aus dem eure Definitionen und Konventionen im Einzelnen ersichtlich sind?
Viele Grüße
Tobias
|
|
|
| |
|
Nein, so etwas haben wir nicht.
Der Dozent hält sich an das Buch 'Mathematische Logik' von Martin Ziegler, falls du dies besitzt.
Ich habe dort bisher leider nicht reingeschaut, daher kann ich auch hier nicht sagen in wie weit es Deckungsgleich ist.
Ich kann aber auch gerne die Definitionen aufschreiben, wenn du das möchtest.
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig | | Datum: | 19:20 So 10.05.2015 | | Autor: | tobit09 |
Um dir unnötige Schreibarbeit zu ersparen:
Passen eure Formulierungen zu Kapitel 1 Abschnitte 3 und 4 aus ![[]](/images/popup.gif) diesem Skript hier?
|
|
|
| |
|
Ja, das ist tatsächlich in weiten Teilen Deckungsgleich.
An manchen Stellen werden Beweise sogar ausführlich erklärt, so scheint es mir.
Danke für den Link, da werde ich zukünftig bestimmt das ein oder andere mal reinschauen.
|
|
|
| |
|
| Status: |
(Antwort) fertig  | | Datum: | 17:22 Di 12.05.2015 | | Autor: | tobit09 |
So, jetzt komme ich endlich zum antworten... 
> Geben Sie formale Beweise im Hilbertkalkül der folgenden
> Formeln an:
>
> 1) [mm]((\exists x\phi)\rightarrow\psi)\rightarrow(\forall x(\phi\rightarrow\psi))[/mm]
> wenn x nicht frei in [mm]\psi[/mm]
>
> 2) [mm]\forall x\forall y\forall z (x=y\rightarrow y=z\rightarrow x=z)[/mm]
>
> 3) [mm](\forall y(x=y\rightarrow \phi(y)))\rightarrow \phi(x)[/mm]
> Zu erst ist mir eines noch unklar, weil dies in meinem
> Skript leider nicht näher kenntlich gemacht ist. Bei dem
> [mm]\exist[/mm]-Axiom handelt es sich doch um folgendes:
>
> Angenommen [mm]\varphi[/mm] ist eine L-Formel, [mm]t[/mm] ist ein L-Term und
> [mm]x[/mm] eine Variable, die frei für [mm]t[/mm] in [mm]\varphi[/mm] ist. Dann ist
> die Formel
>
> [mm]\varphi\frac{t}{x}\rightarrow\exists x\varphi[/mm]
> allgemeingültig.
Ersetze das Wort "allgemeingültig" am Ende durch "ein [mm] $\exists$-Quantorenaxiom".
[/mm]
Gemäß Definition des Hilbertkalküls sind diese [mm] $\exists$-Quantorenaxiome [/mm] beweisbar.
Sinnvoll ist diese Festlegung natürlich nur, da alle diese [mm] $\exists$-Quantorenaxiome [/mm] allgemeingültig sind.
(Schließlich sollen alle beweisbaren Formeln allgemeingültig sein.
Diese Eigenschaft des Hilbertkalküls nennt man seine Korrektheit.
Darüber hinaus habt ihr nachgewiesen, dass auch die Umkehrung gilt: alle allgemeingültigen Formeln sind beweisbar.
Diese Eigenschaft des Hilbertkalküls nennt man seine Vollständigkeit.)
(Jetzt bin ich aber etwas ins Schwafeln gekommen...  )
> Nun eine Frage zum Hilbertkalkül und formalen beweisen.
> Mir ist klar, dass ich nur die Axiome verwenden darf, oder
> Formeln die aus den Regeln entstehen.
Ja. Ein Beispiel dazu findest du auf Seite 17 im von mir bereits verlinkten Skript.
(Ich gehe davon aus, dass auch ihr die "abgeleiteten" Axiome und Schlussregeln (Aussagenlogik), [mm] ($\forall$-Quantorenaxiome) [/mm] und [mm] ($\forall$-Einführung) [/mm] benutzen dürft.)
> Wie bei einem "üblichen" beweis muss ich daraus aus dem
> was "links" der Implikation steht, das was "rechts" der
> Implikation steht, folgern.
Nein, Aufgabe ist hier eben nicht, einen "herkömmlichen" "inhaltlichen" Beweis zu führen, sondern eine formale Herleitung im Hilbertkalkül anzugeben.
> Also bei Aufgabe 1) wäre etwa
>
> [mm]((\exists\phi)\rightarrow\psi)[/mm] und, dass [mm]x[/mm] nicht frei in
> [mm]\psi[/mm] ist, die Voraussetzung und was ich nun aus den Axiomen
> und Regeln folgern muss ist
>
> [mm](\forall x(\phi\rightarrow\psi))[/mm]
Nein. Im Hilbertkalkül gibt es keine Folgerungen aus (nicht allgemeingültigen) Voraussetzungen, sondern nur formale Axiome und Schlussregeln, die ausschließlich allgemeingültige Formeln produzieren.
> Denn bei Aufgabe 2) habe ich ja gar keine Implikation wie
> in 1) oder 3) gegeben.
> Was ist hier zu tun?
> Am besten fangen wir auch direkt mit Aufgabe 2) an, da sie
> mir auch am einfachsten vorkommt.
> Denn meiner Meinung nach wäre
>
> 2) [mm]\forall x\forall y\forall z(x=y\rightarrow y=z\rightarrow[/mm]
> x=z)
>
> dies einfach das Gleichheitsaxiom der Symmetrie und
> Transitivität, die denn da lauten:
>
> [mm]\forall x,y (x=y\rightarrow y=x)[/mm] (Symmetrie)
>
> [mm]\forall x,y,z (x=y\wedge y=z\rightarrow x=z)[/mm]
> (Transitivität)
"Inhaltlich" hast du völlig Recht damit, dass die Formel aus der Aufgabenstellung eigentlich nur die Transitivität des $=$-Zeichens ausdrückt.
(Um Symmetrie geht es nicht.)
Aber es geht wie gesagt bei dieser Aufgabe nicht um einen "inhaltlichen" Beweis, sondern um eine formale Herleitung im Rahmen des Hilbertkalküls.
> Ist es hier bei Aufgabe 2) nun so, dass im Grunde meine
> "Voraussetzung" nur das
>
> [mm]\forall x,y,z[/mm] ist und ich nun formal beweisen muss, dass
> dann [mm](x=y\rightarrow y=z\rightarrow x=z)[/mm] gilt?
Diese Überlegung hat nichts mit formalen Beweisen im Hilbertkalkül zu tun, hilft uns also leider nicht weiter.
> Anfangen würde ich so:
>
> [mm]\forall x\forall y\forall z (x=y\wedge y=z\rightarrow x=z)[/mm]
> nach Transitivität
![[ok]](/images/smileys/ok.gif "[ok]") Guter erster Schritt!
> [mm]$\forall x\forall y\forall[/mm] z [mm]((x=y\wedge y=z)\rightarrow x=y)\wedge ((x=y\wedge y=z)\rightarrow[/mm]
> y=z)) nach Symmetrie.
"Inhaltlich" erkenne ich keinen Zusammenhang zur Symmetrie des =-Zeichens.
Aber wichtiger: Du hast diese Formel nicht im Hilbertkalkül hergeleitet!
> Mit dem Modus Ponens ist also [mm]x=z[/mm] und [mm]y=z[/mm]
> allgemeingültig.
Weder entstehen diese beiden Formeln durch Modus Ponens aus schon als beweisbar erkannten Formeln, noch sind sie allgemeingültig.
(Allgemeingültigkeit etwa der ersten der beiden Formeln hieße etwas salopp formuliert: In jeder L-Struktur bei jeder Belegung trifft $x=z$ zu. Das ist aber nicht der Fall: Betrachte irgendeine L-Struktur mit mindestens 2 Elementen im Träger und eine Belegung, die x und z unterschiedliche Elemente des Trägers zuordnet.)
> [mm]\forall x\forall y\forall z (x=z\wedge y=z\rightarrow x=y)[/mm]
> nach Transitität
Das kommt darauf an, wie ihr die Gleichheitsaxiome genau eingeführt habt: Soll für alle Variablen x, y und z die Formel
[mm] $\forall x\forall y\forall [/mm] z [mm] (x=y\wedge y=z\rightarrow [/mm] x=z)$
ein Gleichheitsaxiom sein, oder nur für die ausgezeichneten Variablen x, y und z?
> Wenn ich wieder den Modus Ponens anwende erhalte ich also
>
> [mm]\forall x\forall y\forall z(x=y\rightarrow y=z\rightarrow x=z)[/mm]
Nein, auf welche Formeln [mm] $\phi$ [/mm] und [mm] $\psi$, [/mm] für die du bereits die Beweisbarkeit von [mm] $\phi$ [/mm] und [mm] $(\phi\rightarrow\psi)$ [/mm] nachgewiesen hast, möchtest du den Modus Ponens anwenden?
Damit es nicht ganz so unübersichtlich wird, schreibe ich meine Tipps zum Lösen von Teil 2 in eine separate Antwort.
|
|
|
| |
|
| Status: |
(Antwort) fertig | | Datum: | 17:50 Di 12.05.2015 | | Autor: | tobit09 |
> Geben Sie formale Beweise im Hilbertkalkül der folgenden
> Formeln an:
> 2) [mm]\forall x\forall y\forall z (x=y\rightarrow y=z\rightarrow x=z)[/mm]
Mein erster Ansatz zur Lösung war folgender:
Ausgangspunkt ist wie von dir richtig erkannt das Gleichheitsaxiom
[mm] $\forall x\forall y\forall [/mm] z [mm] (x=y\wedge y=z\rightarrow [/mm] x=z)$.
Nun hilft folgende Beobachtung:
Die Formeln
[mm] $\varphi_1:=(x=y\wedge y=z\rightarrow [/mm] x=z)$
und
[mm] $\varphi_2:=(x=y\rightarrow y=z\rightarrow [/mm] x=z)$
scheinen "aussagenlogisch das gleiche auszudrücken", präziser: Wenn [mm] $\varphi_1$ [/mm] beweisbar ist, so auch [mm] $\varphi_2$ [/mm] mittels der Schlussregel (Aussagenlogik).
Mache dir letzteres genau klar: Was sind hier n und [mm] $\phi_1,\ldots,\phi_n$ [/mm] sowie [mm] $\psi$ [/mm] in der Formulierung der Schlussregel (Aussagenlogik) aus dem Skript? Warum ist [mm] $(\phi_1\wedge\ldots\wedge\phi_n)\rightarrow\psi$ [/mm] wirklich eine Tautologie, d.h. aus welcher aussagenlogischen Formel lässt sich die Formel [mm] $(\phi_1\wedge\ldots\wedge\phi_n)\rightarrow\psi$ [/mm] durch Einsetzung erhalten?
(Und [mm] $\varphi_1$ [/mm] wird beweisbar sein, denn sie ist allgemeingültig.)
Versuche nun die Formel [mm] $\varphi_1$ [/mm] mithilfe des obigen Gleichheitsaxioms im Hilbertkalkül herzuleiten.
Es gilt dazu quasi, die Quantoren innerhalb des Gleichheitsaxioms zu "eliminieren".
Jeder einzelne der drei Quantoren lässt sich durch ein [mm] $\forall$-Quantorenaxiom [/mm] und eine Anwendung des Modus Ponens "eliminieren".
Wie im Einzelnen?
Schließlich gilt es noch, mithilfe der Beweisbarkeit von [mm] $\varphi_2$ [/mm] die Beweisbarkeit der Formel aus der Aufgabenstellung herzuleiten.
Mit welcher Regel erhältst du wohl die nötigen [mm] $\forall$-Quantoren?
[/mm]
|
|
|
|
