matheraum.de
Raum für Mathematik
Offene Informations- und Nachhilfegemeinschaft

Für Schüler, Studenten, Lehrer, Mathematik-Interessierte.
Hallo Gast!einloggen | registrieren ]
Startseite · Forum · Wissen · Kurse · Mitglieder · Team · Impressum
Forenbaum
^ Forenbaum
Status Mathe
  Status Schulmathe
    Status Primarstufe
    Status Mathe Klassen 5-7
    Status Mathe Klassen 8-10
    Status Oberstufenmathe
    Status Mathe-Wettbewerbe
    Status Sonstiges
  Status Hochschulmathe
    Status Uni-Analysis
    Status Uni-Lin. Algebra
    Status Algebra+Zahlentheo.
    Status Diskrete Mathematik
    Status Fachdidaktik
    Status Finanz+Versicherung
    Status Logik+Mengenlehre
    Status Numerik
    Status Uni-Stochastik
    Status Topologie+Geometrie
    Status Uni-Sonstiges
  Status Mathe-Vorkurse
    Status Organisatorisches
    Status Schule
    Status Universität
  Status Mathe-Software
    Status Derive
    Status DynaGeo
    Status FunkyPlot
    Status GeoGebra
    Status LaTeX
    Status Maple
    Status MathCad
    Status Mathematica
    Status Matlab
    Status Maxima
    Status MuPad
    Status Taschenrechner

Gezeigt werden alle Foren bis zur Tiefe 2

Navigation
 Startseite...
 Neuerdings beta neu
 Forum...
 vorwissen...
 vorkurse...
 Werkzeuge...
 Nachhilfevermittlung beta...
 Online-Spiele beta
 Suchen
 Verein...
 Impressum
Das Projekt
Server und Internetanbindung werden durch Spenden finanziert.
Organisiert wird das Projekt von unserem Koordinatorenteam.
Hunderte Mitglieder helfen ehrenamtlich in unseren moderierten Foren.
Anbieter der Seite ist der gemeinnützige Verein "Vorhilfe.de e.V.".
Partnerseiten
Dt. Schulen im Ausland: Mathe-Seiten:Weitere Fächer:

Open Source FunktionenplotterFunkyPlot: Kostenloser und quelloffener Funktionenplotter für Linux und andere Betriebssysteme
StartseiteMatheForenLogikHilbertkalkül
Foren für weitere Schulfächer findest Du auf www.vorhilfe.de z.B. Deutsch • Englisch • Französisch • Latein • Spanisch • Russisch • Griechisch
Forum "Logik" - Hilbertkalkül
Hilbertkalkül < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
Ansicht: [ geschachtelt ] | ^ Forum "Logik"  | ^^ Alle Foren  | ^ Forenbaum  | Materialien

Hilbertkalkül: Frage (beantwortet)
Status: (Frage) beantwortet Status 
Datum: 23:56 Sa 09.05.2015
Autor: impliziteFunktion

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.


        
Bezug
Hilbertkalkül: Mitteilung
Status: (Mitteilung) Reaktion unnötig Status 
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

Bezug
                
Bezug
Hilbertkalkül: Mitteilung
Status: (Mitteilung) Reaktion unnötig Status 
Datum: 19:09 So 10.05.2015
Autor: impliziteFunktion

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.

Bezug
                        
Bezug
Hilbertkalkül: Mitteilung
Status: (Mitteilung) Reaktion unnötig Status 
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 []diesem Skript hier?

Bezug
                                
Bezug
Hilbertkalkül: Mitteilung
Status: (Mitteilung) Reaktion unnötig Status 
Datum: 20:50 So 10.05.2015
Autor: impliziteFunktion

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.

Bezug
        
Bezug
Hilbertkalkül: Antwort
Status: (Antwort) fertig Status 
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] 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.

Bezug
        
Bezug
Hilbertkalkül: Antwort
Status: (Antwort) fertig Status 
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]

Bezug
Ansicht: [ geschachtelt ] | ^ Forum "Logik"  | ^^ Alle Foren  | ^ Forenbaum  | Materialien


^ Seitenanfang ^
www.matheraum.de
[ Startseite | Forum | Wissen | Kurse | Mitglieder | Team | Impressum ]