Seite 1 von 1

Nachweis einer Sequenzregel

Verfasst: 16. Aug 2011 08:38
von Kineese
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?

Re: Nachweis einer Sequenzregel

Verfasst: 16. Aug 2011 09:00
von Domac
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

Re: Nachweis einer Sequenzregel

Verfasst: 24. Aug 2011 12:50
von kain
\(\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?

Re: Nachweis einer Sequenzregel

Verfasst: 24. Aug 2011 15:10
von fscheepy
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).

Re: Nachweis einer Sequenzregel

Verfasst: 24. Aug 2011 21:10
von kain
Ich hab zu erst die Quantorenregeln angewendet. Die dann entsprechend weiter "auseinander" genommen.

Re: Nachweis einer Sequenzregel

Verfasst: 24. Aug 2011 22:49
von dschneid
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.

Re: Nachweis einer Sequenzregel

Verfasst: 1. Sep 2011 12:50
von kain
\(\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)\)

Re: Nachweis einer Sequenzregel

Verfasst: 1. Sep 2011 16:38
von fscheepy
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

Re: Nachweis einer Sequenzregel

Verfasst: 1. Sep 2011 19:17
von arne.lottmann
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

Re: Nachweis einer Sequenzregel

Verfasst: 1. Sep 2011 20:20
von kain
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.