Nachweis einer Sequenzregel

Kineese
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 111
Registriert: 14. Feb 2008 18:33

Nachweis einer Sequenzregel

Beitrag von Kineese » 16. Aug 2011 08:38

Hallo!
Bei Übungsplatt 10 Aufgabe G2 soll man die semantische Korrektheit der Regel nachweisen.
Reicht es denn auch wenn ich zeige dass \((\phi \to \psi) \to \phi \equiv \phi\) ist, oder muss ich dafür mit Beleugngen argumentieren?

Benutzeravatar
Domac
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 160
Registriert: 4. Okt 2010 16:11

Re: Nachweis einer Sequenzregel

Beitrag von Domac » 16. Aug 2011 09:00

Servus,

ich würde hier die Fallunterscheidungen der verschiedenen Belegungen für den Beweis verwenden. Jedoch müsste der Beweis kürzer ausfallen, wenn du in der Annahme bist, dass das Teil allgemeingültig ist (also nur alle allgemeingültigen Belegungen beweisen/betrachten).

Gruß domac
Extend my dropbox space (here).
Thanks!

kain
Mausschubser
Mausschubser
Beiträge: 92
Registriert: 30. Sep 2009 13:49

Re: Nachweis einer Sequenzregel

Beitrag von kain » 24. Aug 2011 12:50

\(\forall x\, (Px \rightarrow\, \varphi (x)) \vdash\, \exists x\, (Px \land\, \varphi (x))\)

Es soll, unabhängig von \(\varphi\), bewiesen werden, dass die Sequenz nicht allgemeingültig ist.

Hab das soweit gemacht und folgende "Blätter" bekommen:

\(\forall x\, (\neg Px \lor\, \varphi(x)), \neg Px \vdash\, Px, \exists x\, (Px \land\, \varphi(x))\)
\(\forall x\, (\neg Px \lor\, \varphi(x)), \varphi(x)) \vdash\, Px, \exists x\, (Px \land\, \varphi(x))\)
\(\forall x\, (\neg Px \lor\, \varphi(x)), \neg Px \vdash\, \varphi(x)), \exists x\, (Px \land\, \varphi(x))\)
\(\forall x\, (\neg Px \lor\, \varphi(x)), \varphi(x)) \vdash\, \varphi(x)), \exists x\, (Px \land\, \varphi(x))\)



Kann das jemand überprüfen, ob es soweit stimmt und auch sagen, wie es jetzt weitergeht?

fscheepy
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 153
Registriert: 14. Dez 2009 21:17

Re: Nachweis einer Sequenzregel

Beitrag von fscheepy » 24. Aug 2011 15:10

kain hat geschrieben:\(\forall x\, (Px \rightarrow\, \varphi (x)) \vdash\, \exists x\, (Px \land\, \varphi (x))\)

Es soll, unabhängig von \(\varphi\), bewiesen werden, dass die Sequenz nicht allgemeingültig ist.

Hab das soweit gemacht und folgende "Blätter" bekommen:

\(\forall x\, (\neg Px \lor\, \varphi(x)), \neg Px \vdash\, Px, \exists x\, (Px \land\, \varphi(x))\)
\(\forall x\, (\neg Px \lor\, \varphi(x)), \varphi(x)) \vdash\, Px, \exists x\, (Px \land\, \varphi(x))\)
\(\forall x\, (\neg Px \lor\, \varphi(x)), \neg Px \vdash\, \varphi(x)), \exists x\, (Px \land\, \varphi(x))\)
\(\forall x\, (\neg Px \lor\, \varphi(x)), \varphi(x)) \vdash\, \varphi(x)), \exists x\, (Px \land\, \varphi(x))\)



Kann das jemand überprüfen, ob es soweit stimmt und auch sagen, wie es jetzt weitergeht?
Kannst du mir sagen, welche Regeln du in welcher Reihenfolge angewendet hast? Ich hätte, ausgehend von deiner Ursprungsformel zuerst (vL) angewendet und auf die beiden Prämissen davon jeweils nochmal (^R).

kain
Mausschubser
Mausschubser
Beiträge: 92
Registriert: 30. Sep 2009 13:49

Re: Nachweis einer Sequenzregel

Beitrag von kain » 24. Aug 2011 21:10

Ich hab zu erst die Quantorenregeln angewendet. Die dann entsprechend weiter "auseinander" genommen.

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Nachweis einer Sequenzregel

Beitrag von dschneid » 24. Aug 2011 22:49

Mit dem Sequenzenkalkül kann man nicht nachweisen, dass eine FO-Formel nicht allgemeingültig ist. Man kann nur nachweisen, dass sie allgemeingültig ist. Bei AL-Formeln funktioniert das erste auch noch, weil die Art, wie man die Regeln rückwärts anwendet, um die Sequenzen auseinanderzunehmen, bis man entweder auf Axiome kommt oder eben nicht, deterministisch ist. Bei FO-Formeln gibt es aber wegen der beliebigen Ersetzung von Termen oder Konstanten für die quantifizierten Variablen in den entsprechenden Regeln unendlich viele Möglichkeiten, wie man einen Quantor entfernen könnte. Die müsste man alle erstmal durchprobieren, um zu einer definitiven Antwort zu gelangen, aber das geht natürlich nicht.

Man muss also auch semantisch argumentieren: Die Sequenz ist per Definition allgemeingültig, wenn \(\forall x (Px \rightarrow \varphi(x)) \models \exists x (Px \wedge \varphi(x))\), also müssen alle Strukturen, welche ein Modell der ersten Formel sind, auch die zweite Formel erfüllen. Wählt man jetzt aber eine Struktur, die beliebig ist bis auf die Festlegung, dass Px für alle x falsch ist, dann wird die erste Formel davon erfüllt (denn \(Px \rightarrow \varphi(x)\) ist dann für alle \(x\) wahr), aber die zweite nicht (denn es gibt schon kein \(x\), so dass \(Px\) wahr sein könnte). Ergo gilt die geforderte Folgerungsbeziehung nicht, und die Sequenz ist damit nicht allgemeingültig.

kain
Mausschubser
Mausschubser
Beiträge: 92
Registriert: 30. Sep 2009 13:49

Re: Nachweis einer Sequenzregel

Beitrag von kain » 1. Sep 2011 12:50

\(\forall x(Px \rightarrow \varphi ((x)) \models \exists x(Px \land \varphi (x))\)

Wie würde eine Quantifizierung aussehn?

So etwa?

\(\neg Pc \lor \varphi (c) \models Pc \land \varphi (c)\)

oder

\(\neg Pc \lor \varphi (c/x) \models Pc \land \varphi (c)\)

Das wäre falsch?

\(\neg Pc \lor \varphi (c/x) \models Pc \land \varphi (c/x)\)

fscheepy
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 153
Registriert: 14. Dez 2009 21:17

Re: Nachweis einer Sequenzregel

Beitrag von fscheepy » 1. Sep 2011 16:38

kain hat geschrieben:\(\forall x(Px \rightarrow \varphi ((x)) \models \exists x(Px \land \varphi (x))\)

Wie würde eine Quantifizierung aussehn?

So etwa?

\(\neg Pc \lor \varphi (c) \models Pc \land \varphi (c)\)

oder

\(\neg Pc \lor \varphi (c/x) \models Pc \land \varphi (c)\)

Das wäre falsch?

\(\neg Pc \lor \varphi (c/x) \models Pc \land \varphi (c/x)\)
Würde auf ersteres tippen, bei zweiterem müsste doch wenn überhaupt in beiden klammern (c/x) stehen, also wie bei dritterem...das könnte auch richtig sein, keine Ahnung :P

arne.lottmann
Mausschubser
Mausschubser
Beiträge: 99
Registriert: 4. Okt 2010 16:25

Re: Nachweis einer Sequenzregel

Beitrag von arne.lottmann » 1. Sep 2011 19:17

Wenn man sich die Lösung zu Übung 14 anschaut, sieht man da beide Formen auftauchen; von daher scheint es mir, als würden beide zumindest akzeptiert werden. Welche nun die "wirklich richtige Form" ist, bleibt Sache der fanatischen Formalisten :D

kain
Mausschubser
Mausschubser
Beiträge: 92
Registriert: 30. Sep 2009 13:49

Re: Nachweis einer Sequenzregel

Beitrag von kain » 1. Sep 2011 20:20

Falls ich die Regeln richtig verstanden habe:

\(\forall L \exists R\) setzt man \(\varphi(t/x)\) (für die anderen beiden Fälle dann (c/x))

Das t steht dabei für z.B. eine Funktion, demnach ist c (Funktion^0) und c/x (Funktion^1) erlaubt.

Antworten

Zurück zu „Archiv“