Prädikatenlogik, rekursive Funktion - Seite 2

22.04.2012, 21:58

LiGo

Ok. Ich versuche mal die ersten Fälle des Formelbeweises.
Dann lohnt sichs wenigstens smile

$\begin{eqnarray*} \beta, \gamma \end{eqnarray*}$ , seien Formeln

Fall: $\begin{eqnarray*} \alpha = \neg \beta \end{eqnarray*}$

$\begin{eqnarray*} \mathcal S \models VU(\neg \beta)[\mathfrak{b}] \end{eqnarray*}$
$\begin{eqnarray*} = \mathcal S \models \neg VU(\beta)[\mathfrak{b}] \end{eqnarray*}$
IV:
$\begin{eqnarray*} = \mathcal S \models \neg \beta( b [ y / \mathfrak b (z) ]) \end{eqnarray*}$

Damit wäre der Fall bewiesen.

Fall: $\begin{eqnarray*} \alpha = \beta \land \gamma \end{eqnarray*}$

$\begin{eqnarray*} \mathcal S \models VU(\beta \land \gamma)[\mathfrak{b}] \end{eqnarray*}$
$\begin{eqnarray*} = \mathcal S \models VU(\beta) \land VU(\gamma)[\mathfrak{b}] \end{eqnarray*}$

IV:
$\begin{eqnarray*} = \mathcal S \models \beta \land \gamma( b [ y / \mathfrak b (z) ]) \end{eqnarray*}$
$\begin{eqnarray*} = \mathcal S \models (\beta( b [ y / \mathfrak b (z) ]) \land \gamma( b [ y / \mathfrak b (z) ])) \end{eqnarray*}$

Damit wäre auch dieser Fall bewiesen.

Fall: $\begin{eqnarray*} \alpha = \beta \lor \gamma \end{eqnarray*}$ analog zu $\begin{eqnarray*} \alpha = \beta \land \gamma \end{eqnarray*}$

Soweit der Versuch...

23.04.2012, 20:11

pseudo-nym

Auf diesen Beitrag antworten »

Zitat:

Original von LiGo
Für eine Variable muss ich das nicht beweisen?

Hier also für die Terme:

Hm, also das ist so wie bei einer Induktion über N zu sagen:
"Für die 1 muss ich nichts beweisen? Hier also für die natürlichen Zahlen."
(Jede Variable ist ein Term genauso wie die 1 eine natürliche Zahl ist.)

In deinen Beweisen fehlen die Induktionsanfänge, also die Beweise für die Variablen und die atomaren Formeln.

Hier hast du hast du falsch interpretiert:

Zitat:

$\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*}$

Nach dem Gleichheitszeichen muss das Funktionszeichen f interpretiert werden.

Zitat:

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

$\begin{eqnarray*} \mathcal S \models VU(\neg \beta)[\mathfrak{b}] \end{eqnarray*}$ und $\begin{eqnarray*} \mathcal S \models \neg VU(\beta)[\mathfrak{b}] \end{eqnarray*}$ sind äquivalent, aber nicht gleich. Sinnvoller ist es, wenn du $\begin{eqnarray*} \Leftrightarrow \end{eqnarray*}$ verwendest.

Die Klammerung passt schon. Du hast sie in einem vorherigen Post nur ungeschickt zitiert.

23.04.2012, 20:25

LiGo

Auf diesen Beitrag antworten »

Ich scheine mich langsam zumindest in die richtige Richtung zu bewegen.

Zitat:

Nach dem Gleichheitszeichen muss das Funktionszeichen f interpretiert werden.

Kannst du mr das noch ein wenig näher erleutern?
Ich verstehe die Aussage nicht so richtig. Den rest werde ich versuchen.

Ein wenig schwer tue ich mir auch noch mit dem Ansatz für den beweis für den fall $\begin{eqnarray*} \forall x \beta \end{eqnarray*}$

23.04.2012, 21:37

LiGo

Auf diesen Beitrag antworten »

Versuchen wir also mal den Induktionsanfang:

Sei $\begin{eqnarray*} \beta \end{eqnarray*}$ eine atomare Formel, also eine Aussagenvariable $\begin{eqnarray*} \alpha \end{eqnarray*}$ oder die Aussagekonstante $\begin{eqnarray*} \perp \end{eqnarray*}$ , so gilt:

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

was ganz offensichtlich

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

entspricht.

Also gilt:

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

für alle atomaren Formeln.

Kann man das so schreiben?

24.04.2012, 02:24

pseudo-nym

Auf diesen Beitrag antworten »

Zitat:

Original von LiGo
Sei $\begin{eqnarray*} \beta \end{eqnarray*}$ eine atomare Formel, also eine Aussagenvariable $\begin{eqnarray*} \alpha \end{eqnarray*}$ oder die Aussagekonstante $\begin{eqnarray*} \perp \end{eqnarray*}$ , so gilt:

Es wäre mir neu, dass das die Definition einer atomaren Formel ist.

Was die Interpretation des Funktionszeichens angeht, kann du z.B. auf der Wikipediaseite der Pädikatenlogik erster Stufe, nachlesen wie man ein Funktionszeichen interpretiert. Man muss dabei insbesondere das Zeichen $\begin{eqnarray*} f \end{eqnarray*}$ durch seine Interpretation $\begin{eqnarray*} f^{\mathcal A} \end{eqnarray*}$ austauschen.

Der Ansatz für die Quantoren ist außerdem der selbe wie für $\begin{eqnarray*} \neg, \wedge \end{eqnarray*}$ .

25.04.2012, 14:56

LiGo

Auf diesen Beitrag antworten »

Definition atomare Formel.

Ist p ein n-stelliges Prädikat und sind t1, …, tn Terme, dann ist p(t1, …, tn) eine atomare Formel

Prädikate enthalten keine Veriablen, also ist die Aussage für Prädikate offensichtlich. Ist der Beweis für Terme nicht bereits erbracht?

25.04.2012, 19:52

LiGo

Auf diesen Beitrag antworten »

Hier nochmal der Beweis für

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_f(VU(t_1,.....,t_m))[\mathfrak{b}] \end{eqnarray*}$
$\begin{eqnarray*} = F_f(VU(t_1)[\mathfrak{b}],.....,VU(t_m)[\mathfrak{b}]) \end{eqnarray*}$

Induktionsvoraussetzung:
$\begin{eqnarray*} = F_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*}$

29.04.2012, 14:11

pseudo-nym

Auf diesen Beitrag antworten »

Dein Beweis für die Funktionen passt jetzt.

Wenn du mit Prädikaten Relationszeichen meinst, dann verstehe ich dein Argument nicht. Was willst du sagen, wenn du sagst, dass Relationszeichen keine Variablen haben?

An welcher Stelle in deinem Beweis werden außerdem Formeln der Form $\begin{eqnarray*} t_1 \dot{=} t_2 \end{eqnarray*}$ behandelt ( $\begin{eqnarray*} t_1, t_2 \end{eqnarray*}$ sind Terme.)?

« vorherige Seite 12

Neue Frage »

Antworten »

Prädikatenlogik, rekursive Funktion - Seite 2

Verwandte Themen