Prädikatenlogik, rekursive Funktion

17.04.2012, 16:02

LiGo

Prädikatenlogik, rekursive Funktion

Ich steh komplett auf dem schlauch:

Es soll eine Funktion rekursiv definiert werden, die für jede beliebige Formel, die Variable x in y umbenennt.

Wie man eine Funktion rekursiv definiert ist mir soweit klar, aber für dieses Problem fehlt mir irgendwie komplett der Ansatz, wie ich es angehen soll.

Ich bin für jeden Wink mit dem Zaunpfahl dankbar!

17.04.2012, 21:43

pseudo-nym

Auf diesen Beitrag antworten »

Beginne damit deine Funktion nur für die Terme zu definieren.

Mit welchen Objekten fängt man bei einer Termrekursion an?

17.04.2012, 21:59

LiGo

Auf diesen Beitrag antworten »

Wenn ich es richtig verstehe, dann meinst du so:

$\begin{eqnarray*} \mathrm{VU}_y^z(y) = \{z\}\ \end{eqnarray*}$

Aber wie weiter?

17.04.2012, 22:02

pseudo-nym

Auf diesen Beitrag antworten »

Was ist $\begin{eqnarray*} \mathrm{VU}_y^z(y) \end{eqnarray*}$ ?

17.04.2012, 22:05

LiGo

Auf diesen Beitrag antworten »

Na das soll die Formel werden, die die Variablen umbenennt

17.04.2012, 22:26

pseudo-nym

Auf diesen Beitrag antworten »

Ich habe leider keine Ahnung was du sagen willst.

Nennen wir die Funktion, die du definieren willst einmal f.
Will man eine Funktion auf den Termen durch Rekursion definieren, muss man erst auf den Variablen festlegen.
Wähle also $\begin{eqnarray*} f(z) \end{eqnarray*}$ für jede Variable z deiner Sprache.

17.04.2012, 22:31

LiGo

Auf diesen Beitrag antworten »

Ich hatte beim verfassen die Aufgabe nicht vorliegen:

Definieren Sie rekursiv eine Funktion $\begin{eqnarray*} \mathrm{VU}:PF \to PF\ \end{eqnarray*}$ welche in einer beliebigen Formel $\begin{eqnarray*} \alpha \in PF \end{eqnarray*}$ die Variable y in die Variable z umbenennt.

PF ist dabei die Menge der Prädikatenformeln.

Ich kenne Rekursion selbstverständlich aus der Progrmmierung und mir ist irgendwie auch klar, wie das hier funktionieren soll. Mir fehlt nur komplett der Ansatz und die Unterlagen die ich habe sind übel schlecht smile

$\begin{eqnarray*} \mathrm{VU}_y^z(y) \end{eqnarray*}$ sollte dann wohl dein $\begin{eqnarray*} f(z) \end{eqnarray*}$ sein

17.04.2012, 22:43

pseudo-nym

Auf diesen Beitrag antworten »

Nun wie ich schon sagte, als erstes muss du geeignete Bilder unter den Variablen der Sprache finden.

Das ist der erste Schritt in einer rekursiven Definition über Terme.

17.04.2012, 23:14

LiGo

Auf diesen Beitrag antworten »

$\begin{eqnarray*} \mathrm{VU}_y^z(\gamma) = \{z \in V \mid z\; kommt\; in\; \gamma\; vor \} \end{eqnarray*}$

als erste Stufe,

wobei V die Menge der Variablen der Sprachte.

Gamma ein Term

18.04.2012, 01:09

pseudo-nym

Auf diesen Beitrag antworten »

Dein Beitrag schon deshalb haarsträubend weil du keine ganzen Sätze formulierst, sondern es mir überlässt aus ein paar Begriffen und Formeln einen Sinnzusammenhang herauszufiltern.

Was ist V?

Da du es jetzt zum wiederholten Male erwähnst, muss ich wissen was $\begin{eqnarray*} VU_y^z \end{eqnarray*}$ bedeuten soll. $\begin{eqnarray*} VU \end{eqnarray*}$ und $\begin{eqnarray*} VU_y^z \end{eqnarray*}$ scheinen jedenfalls nicht gleich zu sein, da das eine in PF und das andere in $\begin{eqnarray*} \mathcal P (V) \end{eqnarray*}$ abbildet.

Und was hat das alles mit meinem Voschlag zu tun? Ich wollte, dass du dir $\begin{eqnarray*} VU(z) \end{eqnarray*}$ für eine Variable z überlegst. Davon kann ich hier nichts erkennen.

Hilfreich ist es wohl auch wenn du einmal erklärst wie du dir eine Term- bzw. Formelrekursion allgemein vorstellst.

18.04.2012, 08:34

LiGo

Auf diesen Beitrag antworten »

Zitat:

Dein Beitrag schon deshalb haarsträubend weil du keine ganzen Sätze formulierst, sondern es mir überlässt aus ein paar Begriffen und Formeln einen Sinnzusammenhang herauszufiltern.

Entschuldige bitte, ich wollte Dich nicht verärgern.

$\begin{eqnarray*} VU_y^z \end{eqnarray*}$ sollte gleich zu $\begin{eqnarray*} VU \end{eqnarray*}$ sein, meine Abbildung war nur völlig falsch unglücklich

Sie müsste auf mindestens einen Term abbilden und nicht auf eine Variable.

Wenn ich es richtig verstehe, muss bei der rekursiven Definition erst die einfachste Möglichkeit der Funktion definiert werden, dann eine Rekursionsbedingung, die beim wiederholten Anwenden die endgültige Rekursion bildet! Ist das soweit richtig?

Zitat:

$\begin{eqnarray*} VU(z) \end{eqnarray*}$ für eine Variable z überlegst

Das würde ich gerne. Ich habe nur leider keine Idee, wie ich die Umbenennung ausdrücken soll...

Leider scheint mir hierfür wirklich noch ein gewisses Grundverständnis zu fehlen unglücklich

18.04.2012, 18:52

pseudo-nym

Auf diesen Beitrag antworten »

Zitat:

Original von LiGo
Wenn ich es richtig verstehe, muss bei der rekursiven Definition erst die einfachste Möglichkeit der Funktion definiert werden, dann eine Rekursionsbedingung, die beim wiederholten Anwenden die endgültige Rekursion bildet! Ist das soweit richtig?

Das stimmt bis auf die Tatsache, dass es nicht unbedingt nur eine Rekursionsbedingung geben muss. In der Tat braucht man für Formelrekursion mindestens drei solcher Schritte.
In deinem Fall solltest du dir überlegen, was die einfachste Form eines Terms ist, damit du $\begin{eqnarray*} VU \end{eqnarray*}$ auf Objekten dieser Form festlegen kannst.

Zitat:

Original von LiGo
Leider scheint mir hierfür wirklich noch ein gewisses Grundverständnis zu fehlen[.]

Wenn du sagst du kennst Rekursion vom Programmieren, dann meinst du warscheinlich Rekursion auf den natürlichen Zahlen. Rekursion über Terme und Formeln funktioniert ähnlich aber nicht genau gleich.

18.04.2012, 21:32

LiGo

Auf diesen Beitrag antworten »

Ok, also ich denke den ersten Schritt habe ich jetzt. Die gesuchte Umbenennung wird durch die Substitution [y/z] beschrieben.

Der gesuchte einfachste Fall müsste also:

$\begin{eqnarray*} VU(y) = y[y/z] \end{eqnarray*}$

lauten.

Hab ich das jetzt soweit mal geschnallt?

Wie geht es weiter?

18.04.2012, 22:14

LiGo

Auf diesen Beitrag antworten »

Ok... ich habs noch etwas meiter versucht:

$\begin{eqnarray*} VU(y) = y[y/z] \end{eqnarray*}$
$\begin{eqnarray*} VU(\neg \alpha) = \neg VU( \alpha) \end{eqnarray*}$
$\begin{eqnarray*} VU(\alpha \land \beta) = \neg VU( \alpha) \land VU(\beta) \end{eqnarray*}$
$\begin{eqnarray*} VU(\alpha \rightarrow \beta) = \neg VU( \alpha) \rightarrow VU(\beta) \end{eqnarray*}$

geht das jetzt etwa in die richtige Richtung oder bin ich wieder völlig auf dem Holzweg?

19.04.2012, 10:56

pseudo-nym

Auf diesen Beitrag antworten »

Zitat:

Original von LiGo
Ok, also ich denke den ersten Schritt habe ich jetzt. Die gesuchte Umbenennung wird durch die Substitution [y/z] beschrieben.

Das ist keine gute Idee denn Substitution und Variablenersetzung sind nicht gleich. So gilt z.B.:
$\begin{eqnarray*} (\exists x : x\, \dot {=}\, x)[x/y] = \exists x : x \, \dot {=}\, x \neq \exists y : y \, \dot {=}\, y = VU(\exists x : x \, \dot {=}\, x) \end{eqnarray*}$

Zitat:

Original von LiGo
Der gesuchte einfachste Fall müsste also:

$\begin{eqnarray*} VU(y) = y[y/z] \end{eqnarray*}$

lauten.

Solange du nicht sagst vorher deine Variablen kommen, ist diese Gleichung (wie auch die im folgenden Post) ziemlich unlesbar. Ist das y ein Term, eine Formel, eine Variable der gegebenen Sprache, oder etwas ganz anderes?

Ich vermute mittlerweile die Probleme sind grundlegenderer Natur. Gib mir doch bitte mal deine Definition von einem Term.

19.04.2012, 11:14

LiGo

Auf diesen Beitrag antworten »

Wenn ich das richtig verstehe ist alles ein Term, was die die folgenden Bedingungen erfüllt:

Jede Variable der Sprache ist Term.
Jede Konstante der Sprache ist ein Term.
Sind t1,...tn -Terme, n >= 1, und ist f Funktionssymbol der Sprache, so ist auch f(t1,...tn) ein Term.

Zitat:

Ich vermute mittlerweile die Probleme sind grundlegenderer Natur. Gib mir doch bitte mal deine Definition von einem Term.

Oh ja... die Befürchtung erschleicht mich langsam auch. Ich dachte ich komme damit besser klar. Hilft nicht.... Backen zusammenkneifen und durch...

19.04.2012, 11:26

pseudo-nym

Auf diesen Beitrag antworten »

Deine Definition ist so okay. Als erstes musst du dir jetzt überlegen wie das Bild einer Variablen der Sprache unter VU aussieht.
Wenn dir das schwerfällt kannst dir VU an ein paar Beispielen explizit überlegen:
$\begin{eqnarray*} VU(x) = ? \\ VU(y) = ? \\ VU(z) = ? \end{eqnarray*}$
( $\begin{eqnarray*} x, y, z \end{eqnarray*}$ sind Variablen der Sprache!)

19.04.2012, 11:31

LiGo

Auf diesen Beitrag antworten »

Ok. Von der Aufgabenstellung her soll ja nur y in z umbenannt werden, das würde auf dein Beispiel bedeuten:

$\begin{eqnarray*} VU(x) = \{x\} \\ VU(y) = \{z\} \\ VU(z) = \{z\} \end{eqnarray*}$
( $\begin{eqnarray*} x, y, z \end{eqnarray*}$ sind Variablen der Sprache!)

Sind die geschweiften Klammern hier richtig?

Danke übrigens für Deine Gedult!

19.04.2012, 11:55

pseudo-nym

Auf diesen Beitrag antworten »

Zitat:

Original von LiGo
Sind die geschweiften Klammern hier richtig?

Nein, die Bilder von VU sollen ja wieder Ausdrücke werden und nicht Mengen von Ausdrücken, so wie es bei dir jetzt steht. Wenn du die Klammern entfernst stimmt es.

Jetzt musst du deine Erkenntnis verallgemeinern und VU(x) für eine beliebige Variable der formalen Sprache formulieren.

19.04.2012, 13:20

LiGo

Auf diesen Beitrag antworten »

Ok... lass es mich mal versuchen ... puh..

$\begin{eqnarray*} \tau \end{eqnarray*}$ sei ein Term.

$\begin{eqnarray*} y, z \end{eqnarray*}$ seien Variablen der Sprache!)

$\begin{eqnarray*} VU(\tau)=\begin{cases}<br /> z, & \text{falls }\tau = y\\<br /> \tau, & \text{sonst}<br /> \end{cases} \end{eqnarray*}$

19.04.2012, 13:38

pseudo-nym

Auf diesen Beitrag antworten »

Jetzt hat du zu stark verallgemeinert. solltest doch VU nur für alle Variablen angeben. Wenn die Sprache L ein einstelliges Funktionszeichen f enthält so gilt mit deiner Defintion
$\begin{eqnarray*} VU(fy) = fy \end{eqnarray*}$ , da $\begin{eqnarray*} fy \neq y \end{eqnarray*}$ .
Dein VU tut nicht was es tun sollte.

19.04.2012, 14:04

LiGo

Auf diesen Beitrag antworten »

Genau da hebt es bei mir wieder mit dem Verständnis unglücklich

Ich kann ja nicht die Menge aller Variablen in die Funktion packen... und mit einem Variablennamen ( für alle z aus der Menge der Variablen ) kann ich nicht arbeiten, da ja eben dieser Name ersetzt werden soll.
Ich komme einfach nicht drauf, wie ich alle Variablen der Sprache bezeichnen soll, wenn ich keinen Namen nennen soll.

EDIT: Deine Erklärung über meinen letzten Ansatz leuchtet übrigens völlig ein smile

19.04.2012, 21:56

LiGo

Auf diesen Beitrag antworten »

Ok. Versuchen wir es nochmal....

$\begin{eqnarray*} m_{1},....,m_{i} \end{eqnarray*}$ seien Variablen

$\begin{eqnarray*} VU(m_{1},....,m_{i})=\begin{cases} z, & \text{falls }m_{i} = y\\ m_{i}, & \text{sonst}\end{cases} \end{eqnarray*}$

Kann man das so ausdrücken?

19.04.2012, 22:16

LiGo

Auf diesen Beitrag antworten »

Noch ein Lösungsansatz, der für mich endlich plausibel wirkt:

( $\begin{eqnarray*} x, y, z \end{eqnarray*}$ sind Variablen der Sprache)

$\begin{eqnarray*} VU_y^z(x) = \begin{cases} z, & \text{falls }x = y\\ x, & \text{sonst}\end{cases} \end{eqnarray*}$

jetzt bin ich ganz guter Dinge, zumindest mal die Variablen erschlagen zu haben. Passt das so? Und wie geht es jetzt weiter?

20.04.2012, 01:18

pseudo-nym

Auf diesen Beitrag antworten »

Du musst unterscheiden zwischen den Variablen der Sprache, welche feste Objekte sind und den metasprachlichen Variablen, die du benutzt um einen Zusammenhang für mehrer Objekte gleichzeitig auszudrücken.

Wenn du x, y, z als Variablen der Sprache festlegst ist
$\begin{eqnarray*} VU(x) = \begin{cases} z, & \text{falls }x = y\\ x, & \text{sonst}\end{cases} = x \end{eqnarray*}$
denn $\begin{eqnarray*} VU(x) \end{eqnarray*}$ ist nichts anderes als das Bild des konkreten Objekts x, (welches ungleich der Sprachvariablen y ist). Dadurch wird deine Fallunterscheidung bedeutungslos.

Wenn du VU für jede Sprachvariable betrachten willst, brauchst du eine Metavariable:
Sei $\begin{eqnarray*} \beta \end{eqnarray*}$ eine beliebige Variable der formalen Sprache.

$\begin{eqnarray*} VU(\beta) = \begin{cases} z, & \text{falls }\beta = y\\ \beta, & \text{sonst}\end{cases} \end{eqnarray*}$
Hier ist $\begin{eqnarray*} \beta \end{eqnarray*}$ lediglich ein Platzhalter für ein anderes Objekt. Intuitiv ist das genau das was man sich unter einer Variable vorstellt, aber die Sprachvariable, die du in deinem Vesuch verwendet hast, ist für diesen Zweck nicht zu gebauchen, denn sie ist ein konkretes Objekt welches wir studieren wollen.

20.04.2012, 08:48

LiGo

Auf diesen Beitrag antworten »

Ok. Ich denke das habe ich soweit verstanden... also sind ide ersten 2 Schritte der Definition:

$\begin{eqnarray*} VU(y) = \{z\} \end{eqnarray*}$
( $\begin{eqnarray*} y, z \end{eqnarray*}$ sind Variablen der Sprache)

Sei $\begin{eqnarray*} \beta \end{eqnarray*}$ eine beliebige Variable der formalen Sprache.

$\begin{eqnarray*} VU(\beta) = \begin{cases} z, & \text{falls }\beta = y\\ \beta, & \text{sonst}\end{cases} \end{eqnarray*}$

Soweit richtig?

Und jetzt muss ich das irgendwie für Terme verallgemeinern?

20.04.2012, 10:37

pseudo-nym

Auf diesen Beitrag antworten »

Diese Definition ist nicht korrekt, denn y hat unter diesem VU zwei verschiedene Bilder.
Wegem dem ersten Schirtt gilt
$\begin{eqnarray*} VU(y) = \{z\} \end{eqnarray*}$
andererseits kann man y für $\begin{eqnarray*} \beta \end{eqnarray*}$ im zweiten Schritt einsetzen und erhält.
$\begin{eqnarray*} VU(y) = z \end{eqnarray*}$

Der erste Schritt deiner Definition ist nicht zielführend, da $\begin{eqnarray*} \{ z \} \end{eqnarray*}$ kein Term ist und überflüssig, da der zweite Schritt bereits ein Bild für y liefert.

20.04.2012, 12:40

LiGo

Auf diesen Beitrag antworten »

Ok. Wir müssen jetzt also einen Term abbilden:

$\begin{eqnarray*} \tau \end{eqnarray*}$ sei ein Term.

$\begin{eqnarray*} VU(\tau)=\begin{cases} VU(\tau), & \text{falls }\tau \text{ eine Variable ist}\\ f(VU(m_{1}),....,VU(m_{i})) & \text{falls } \tau = f(m_{1},....,m_{i})\end{cases} \end{eqnarray*}$

Puh... das klingt für mich relativ plausibel.... wäre das der 2te schritt?

20.04.2012, 18:54

pseudo-nym

Auf diesen Beitrag antworten »

Ja das geht. Jetzt musst du VU noch rekursiv über alle Formeln definieren.

20.04.2012, 20:51

LiGo

Auf diesen Beitrag antworten »

OK. Ich würde sagen, dass ist jetzt aber das hier:

$\begin{eqnarray*} \alpha \text{ und } \beta \text{ seien Funktionen. } \end{eqnarray*}$

$\begin{eqnarray*} VU(\neg \alpha) = \neg VU( \alpha) \end{eqnarray*}$
$\begin{eqnarray*} VU(\alpha \land \beta) = VU( \alpha) \land VU(\beta) \end{eqnarray*}$
$\begin{eqnarray*} VU(\alpha \rightarrow \beta) = VU( \alpha) \rightarrow VU(\beta) \end{eqnarray*}$

Fehlt jetzt noch was? Muss ich die Quantoren noch irgendwie beachten?

$\begin{eqnarray*} y \text{ sei eine Variable} \end{eqnarray*}$

$\begin{eqnarray*} VU(\exists y \alpha) = \{ \exists \} \cup VU(y) \cup VU(\alpha) \end{eqnarray*}$
$\begin{eqnarray*} VU(\forall y \alpha) = \{ \forall \} \cup VU(y) \cup VU(\alpha) \end{eqnarray*}$

Bitte, bitte smile

20.04.2012, 21:20

pseudo-nym

Auf diesen Beitrag antworten »

Zitat:

Original von LiGo
$\begin{eqnarray*} VU(\neg \alpha) = \neg VU( \alpha) \end{eqnarray*}$
$\begin{eqnarray*} VU(\alpha \land \beta) = VU( \alpha) \land VU(\beta) \end{eqnarray*}$
$\begin{eqnarray*} VU(\alpha \rightarrow \beta) = VU( \alpha) \rightarrow VU(\beta) \end{eqnarray*}$

Wenn $\begin{eqnarray*} \alpha, \beta \end{eqnarray*}$ wirklich Funktionen sein sollen musst du mir erst erklären wie boolesche Operationen auf denen funktionieren sollen.
Der letzte Schritt ist außerdem überflüssig, denn $\begin{eqnarray*} \alpha \rightarrow \beta \Leftrightarrow \alpha \wedge \neg \beta \end{eqnarray*}$ .

Zitat:

Original von LiGo
$\begin{eqnarray*} VU(\exists y \alpha) = \{ \exists \} \cup VU(y) \cup VU(\alpha) \end{eqnarray*}$
$\begin{eqnarray*} VU(\forall y \alpha) = \{ \forall \} \cup VU(y) \cup VU(\alpha) \end{eqnarray*}$

Das Problem ist hier, dass Formeln keine Mengen sind und man sie dementsprechend a priori nicht vereinigen kann. Eine Fallunterscheidung wie bei den Variablen wird imho mehr Effekt haben.
Auch hier kannst du dir die Definition für den Allquantor sparen, da $\begin{eqnarray*} \forall x \varphi \Leftrightarrow \neg \exists x \neg \varphi \end{eqnarray*}$ .

20.04.2012, 21:41

LiGo

Auf diesen Beitrag antworten »

Zitat:

Wenn $\begin{eqnarray*} \alpha, \beta \end{eqnarray*}$ wirklich Funktionen sein sollen musst du mir erst erklären wie boolesche Operationen auf denen funktionieren sollen. Der letzte Schritt ist außerdem überflüssig, denn $\begin{eqnarray*} \alpha \rightarrow \beta \Leftrightarrow \alpha \wedge \neg \beta \end{eqnarray*}$ .

Du siehst wirklich alles... wahnsinn. In dem Fall war es aber wirklich mal nur ein Tippfehler. es sollte Formeln heissen.

Ok. Also mit Fallunterscheidung:

Sei $\begin{eqnarray*} \beta \end{eqnarray*}$ eine beliebige Variable der formalen Sprache.

$\begin{eqnarray*} VU(\exists \beta \alpha) = \begin{cases}\exists z VU(\alpha), & \text{falls }\beta = y\\ \exists \beta VU(\alpha), & \text{sonst}\end{cases} \end{eqnarray*}$

Zitat:

$\begin{eqnarray*} \alpha \rightarrow \beta \Leftrightarrow \alpha \wedge \neg \beta \end{eqnarray*}$
$\begin{eqnarray*} \forall x \varphi \Leftrightarrow \neg \exists x \neg \varphi \end{eqnarray*}$ .

Leuchtet mir voll ein, beide Fälle werden aber in vergleichbaren definitionen im Skript berücksichtig.

21.04.2012, 10:20

LiGo

Auf diesen Beitrag antworten »

Ich hoffe mal, dass die Definition jetzt stimmt.

Jetzt muss ich noch beweisen, dass für die Funktion für alle $\begin{eqnarray*} \alpha \in PF \end{eqnarray*}$ , jede $\begin{eqnarray*} \tau \end{eqnarray*}$ Struktur $\begin{eqnarray*} \mathcal S \end{eqnarray*}$ und alle Belegungen $\begin{eqnarray*} \mathfrak{b} \in Bel_s \end{eqnarray*}$ folgendes gilt:

$\begin{eqnarray*} ( \mathcal S \models VU( \alpha)[\mathfrak{b}] \Longleftrightarrow \mathcal S \models \alpha \mathfrak{b}[y/\mathfrak{b}(z)])) \end{eqnarray*}$ , sofern $\begin{eqnarray*} z \notin Vk(\alpha) \end{eqnarray*}$ .

Das wird noch ein hartes Stück Arbeit für mich.

Ich vermute mal, dass ich das über eine strukturelle Induktion beweisen muss.

Muss ich dann jetzt für jeden Fall der Funktionsdefinition die Behauptung beweisen?

21.04.2012, 11:29

pseudo-nym

Auf diesen Beitrag antworten »

Die Definition passt jetzt so.

Ich würde die Aussage tatsächlich induktiv über den Aufbau der Formel beweisen.

21.04.2012, 21:43

LiGo

Auf diesen Beitrag antworten »

Nach langem hin und herüberlegen versuche ich es mal mit Fall 1:

Sei $\begin{eqnarray*} \alpha \end{eqnarray*}$ eine beliebige Variable.

Dann gilt laut Definition:

$\begin{eqnarray*} VU(\alpha) = \begin{cases} z, & \text{falls }\alpha = y\\ \beta, & \text{sonst}\end{cases} \end{eqnarray*}$

$\begin{eqnarray*} \alpha \end{eqnarray*}$ = y:

$\begin{eqnarray*} ( \mathcal S \models z[\mathfrak{b}] \Longleftrightarrow \mathcal S \models y (\mathfrak{b}[y/\mathfrak{b}(z)])) \end{eqnarray*}$
daraus folgt:
$\begin{eqnarray*} ( \mathcal S \models z[\mathfrak{b}] \Longleftrightarrow \mathcal S \models z[\mathfrak{b}]) \end{eqnarray*}$

$\begin{eqnarray*} \alpha \end{eqnarray*}$ ungleich y:

$\begin{eqnarray*} ( \mathcal S \models \alpha[\mathfrak{b}] \Longleftrightarrow \mathcal S \models \alpha( \mathfrak{b}[y/\mathfrak{b}(z)])) \end{eqnarray*}$
daraus folgt:
$\begin{eqnarray*} ( \mathcal S \models \alpha[\mathfrak{b}] \Longleftrightarrow \mathcal S \models \alpha[\mathfrak{b}]) \end{eqnarray*}$

Damit wäre der erste Fall bewiesen. Stimmt das so?

21.04.2012, 22:27

pseudo-nym

Auf diesen Beitrag antworten »

$\begin{eqnarray*} \mathcal S \models z[\mathfrak{b}] \end{eqnarray*}$

Beschreibe mir bitte in Worten so ausführlich wie du kannst, was dieser Ausdruck bedeutet.

21.04.2012, 22:35

LiGo

Auf diesen Beitrag antworten »

Autsch.... ich sehe... und höre an deiner Antwort, dass ich wieder komplett daneben liege.

Ich kann deine Frage leider nicht beantworten, da ich die Antwort nicht kenne.

$\begin{eqnarray*} ( \mathcal S \models VU( \alpha)[\mathfrak{b}] \Longleftrightarrow \mathcal S \models \alpha \mathfrak{b}[y/\mathfrak{b}(z)])) \end{eqnarray*}$ , sofern $\begin{eqnarray*} z \notin Vk(\alpha) \end{eqnarray*}$ .

Es war das, was übrig geblieben ist, wenn ich die VU funktion mit einer Variablen befüllt habe.

$\begin{eqnarray*} ( \mathcal S \models VU( \alpha)[\mathfrak{b}] \end{eqnarray*}$

Ich verstehe bereits in diesem Ausdruck nicht, was ich mit dem alleine stehenden $\begin{eqnarray*} [\mathfrak{b}] \end{eqnarray*}$ anfangen soll.

Ich versuche jetzt seit Tagen mit harter arbeit an dieses Zeugs ranzukommen, was echt nicht einfach ist. So langsam wird es frustrierend. Ich habe den ganzen Abend versucht eine Quelle zu finden, die mir wenigstens diesen ersten Schritt der Induktion klar erleutert

21.04.2012, 23:38

pseudo-nym

Auf diesen Beitrag antworten »

Zitat:

Original von LiGo
$\begin{eqnarray*} ( \mathcal S \models VU( \alpha)[\mathfrak{b}] \end{eqnarray*}$

Ich verstehe bereits in diesem Ausdruck nicht, was ich mit dem alleine stehenden $\begin{eqnarray*} [\mathfrak{b}] \end{eqnarray*}$ anfangen soll.

Dieser Ausdruck ist seltsam geklammert. Er muss
$\begin{eqnarray*} \mathcal S \models (VU( \alpha)[\mathfrak{b}]) \end{eqnarray*}$
heißen.

Jedenfalls wirst du sehen, dass die Erfüllungsrelation $\begin{eqnarray*} \models \end{eqnarray*}$ nicht für Strukturen und Terme definiert ist. Dementsprechend macht
$\begin{eqnarray*} \mathcal S \models z[\mathfrak{b}] \end{eqnarray*}$
oder in Worten: "Die Struktur $\begin{eqnarray*} \mathcal S \end{eqnarray*}$ erfüllt den Term $\begin{eqnarray*} z[\mathfrak{b}] \end{eqnarray*}$ " keinen Sinn.

Bevor du mit dem Beweis der eigentlichen Aussage, welche für Formeln gilt, anfangen kannst, musst du erst noch für alle Terme t $\begin{eqnarray*} VU(t)[\mathfrak b ] = t \mathfrak b [ y / \mathfrak b (z) ] \end{eqnarray*}$ zeigen.

Was ist eigentlich Vk?

22.04.2012, 20:04

LiGo

Auf diesen Beitrag antworten »

Zitat:

Dieser Ausdruck ist seltsam geklammert. Er muss $\begin{eqnarray*} \mathcal S \models (VU( \alpha)[\mathfrak{b}]) \end{eqnarray*}$ heißen.

Die original Aufgabe ist exakt so geklammert:

$\begin{eqnarray*} ( \mathcal S \models VU( \alpha)[\mathfrak{b}] \Longleftrightarrow \mathcal S \models \alpha( \mathfrak{b}[y/\mathfrak{b}(z)])) \end{eqnarray*}$ , sofern $\begin{eqnarray*} z \notin Vk(\alpha) \end{eqnarray*}$

Du sagst, das passt so nicht?

Zitat:

Jedenfalls wirst du sehen, dass die Erfüllungsrelation $\begin{eqnarray*} \models \end{eqnarray*}$ nicht für Strukturen und Terme definiert ist.

Leider war die Erfülllungsrelation für Strukturen in dem mir vorliegenden Skript überhaupt nicht definiert, sie wurde einfach ab einem gewissen Punkt verwendet. Nach deiner Aussage habe ich mir das nochmal anesehen, und du hast recht, sie wird nur für Formeln verwendet.

Zitat:

Was ist eigentlich Vk?

Nach längerem Suchen habe ich hier eine Definition gefunden:
"Die Mengen $\begin{eqnarray*} Vk(t) \end{eqnarray*}$ bzw. $\begin{eqnarray*} Vk(\alpha) \end{eqnarray*}$ der in einem Term t bzw. einer Formel $\begin{eqnarray*} \alpha \end{eqnarray*}$ vorkommenden Variablen.

Ok. Dann werd ich mich jetzt daran mal versuchen

22.04.2012, 20:41

LiGo

Auf diesen Beitrag antworten »

$\begin{eqnarray*} VU(t)[\mathfrak b ] = t (\mathfrak b [ y / \mathfrak b (z) ]) \end{eqnarray*}$

Für eine Variable muss ich das nicht beweisen?

Hier also für die Terme:

Fall $\begin{eqnarray*} t = f(t_1,....,t_m) \end{eqnarray*}$

$\begin{eqnarray*} VU(f(t_1,.....,t_m))[\mathfrak{b}] \end{eqnarray*}$
$\begin{eqnarray*} = f(VU(t_1,.....,t_m))[\mathfrak{b}] \end{eqnarray*}$ --> muss ich das noch in die Formeldefinition aufnehmen?
$\begin{eqnarray*} = f(VU(t_1)[\mathfrak{b}],.....,VU(t_m)[\mathfrak{b}]) \end{eqnarray*}$

Induktionsvoraussetzung:
$\begin{eqnarray*} = f(t_1( b [ y / \mathfrak b (z) ]),.....,t_m( b [ y / \mathfrak b (z) ])) \end{eqnarray*}$
$\begin{eqnarray*} = f(t_1,.....,t_m)( b [ y / \mathfrak b (z) ]) \end{eqnarray*}$

Insgesamt sollte doch die Behauptung damit gezeigt sein?

Und wie mache ich jetzt mit den Formeln weiter?

12 nächste Seite »

Neue Frage »

Antworten »

Prädikatenlogik, rekursive Funktion

Verwandte Themen