PL Eigenschaften

Eigenschaften der PL

Wichtige Eigenschaften der klassichen Prädikatenlogik

(Abstrakte) Vollständigkeit

Es gibt (nicht terminierende) Algorithmen, die genau die gültigen PL-Formeln aufzählen.

= Die Menge der gültigen PL-Formeln ist rekursiv aufzählbar.

= Es gibt Kalküle für die PL, die korrekt und vollständig sind.

Unvollständigkeit der formalen Arithmetik

Es gibt keinen Algorithmus der genau die in N\small \N gültigen PL-Formeln Th(N)\small Th(\N) aufzählt.

= Es gibt keinen korrekten und vollständigen Kalkül der formalen Arithmetik.

Satz von Löwenheim-Skolen

Jede erfüllbare Formel hat ein Modell dessen Gegenstandsbereich aus (allen oder eventuell nur endlich vielen) natürlichen Zahlen besteht.

Unentscheidbarkeit

Es gibt keinen Algorithmus mit dem man die Gültigkeit beliebiger PL-Formeln entscheiden könnte.

Unentscheidbarkeit der PL

Eine Sprache heißt entscheidbar (rekursiv) wenn sie von einer deterministischen TM akzeptiert wird die immer hält.

Unentscheidbarkeit prädikatenlogischer Gültigkeit

Die Menge der gültigen PL-Formeln ist keine entscheidbare Sprache

Unentscheidbarkeit prädikatenlogischer Konsequenz

(siehe Dedeuktionstheorem und Chuch-Turing-These)

Es gibt kein Verfahren, das für beliebige PL-Formeln F1,…Fn,G\small F_{1}, \ldots F_{n}, G feststellen kann ob F1,…Fn⊨G\small F_{1}, \ldots F_{n} \models G gilt oder nicht.

Reduktion Lu≤LPLG\small L_{u} \leq L_{P L G}

Um von der Unentscheidbarkeit vom Halteproblem Lu\small L_u auf Unentscheidbarkeit von PL zu gelangen

Lu\small L_u={(M,w)∣M ist eine TM die w∈{0,1}∗ akzeptiert } \small = \left\{(M, w) \mid M \text { ist eine TM die } w \in\{0,1\}^{*} \text { akzeptiert }\right\} 

LPLG\small L_{PLG} (Sprache) Menge aller gültiger PL-Formeln

Wir wollen aus jeder (M,w)\small (M, w) eine PL-Formel F1,…,Fn,G\small F_{1}, \ldots, F_{n}, G konstruieren, sodass:

M\small M akzeptiert w\small w⟺\LongleftrightarrowF1,…,Fn⊨G\small F_{1}, \ldots, F_{n} \models G

Dann nutzen wir die Lu\small L_u um zu bestimmen ob eine PL-Formel gültig ist.

Die Folge von Konfigurationen (Zustände der TM) wie

q0b1…bn⇒…⇒X1X2…Xi−1qXi….Xn−1Xn \small q_{0} b_{1} \ldots b_{n} \Rightarrow \ldots \Rightarrow X_{1} X_{2} \ldots X_{i-1} q X_{i} \ldots . X_{n-1} X_{n} 

heißt Berechnung von M=(Q,{0,1},Γ,δM,q0,B,F) \small M=\left(Q,\{0,1\}, \Gamma, \delta_{M}, q_{0}, B, F\right) 

mit der Eingabe w=b1…bn(bi∈{0,1})\small w=b_{1} \ldots b_{n}\left(b_{i} \in\{0,1\}\right)

M\small M akzeptiert w\small w genau dann wenn Endzustand q∈F\small q \in F erreicht wird.

Prädikatenlogische Repräsentation von Konfigurationen

Syntax

Signatur ΣM=⟨PS,KS,FS⟩\small \Sigma_{M}=\langle P S, K S, F S\rangle

PS2={Pq∣q∈Q}\small P S_{2}=\left\{P_{q} \mid q \in Q\right\} Prädikaten sind Zustände

FS1={fX∣X∈Γ}\small F S_{1}=\left\{f_{X} \mid X \in \Gamma\right\} Funktionen sind Bandsymbole

{B,0,1}∈Γ\small \{B, 0,1\} \in \Gamma

deshalb fB,f0,f1∈FS1\small f_{B}, f_{0}, f_{1} \in F S_{1}

KS={b}\small K S=\{b\} Konstanten sind Eingabesymbole

Intendierte Semantik

Codierung von Konfigurationen als PL-Atome

Sei KK eine Konfiguration.

K=X1X2…Xi−1qXi…Xn−1Xn \small K = \textcolor{green}{X_{1} X_{2} \ldots X_{i-1}} \textcolor{pink}q \textcolor{red}{X_{i} \ldots X_{n-1} X_{n}} 

ξ(K)=Pq(fXi−1(…fX2(fX1(b))…),fXi(…fXn−1(fXn(b))…)) \small\xi(K)=P_{\textcolor{pink}q}\left( \textcolor{green}{ f_{X_{i-1}}\left(\ldots f_{X_{2}}\left(f_{X_{1}}(b)\right) \ldots\right)}, \textcolor{red}{ f_{X_{i}}\left(\ldots f_{X_{n-1}}\left(f_{X_{n}}(b)\right) \ldots\right)}\right) 

Dabei beachten:

Das erste Argument von Pq\small P_q berechnet das Wort von rechts nach links ( X1\small X_1 nach Xi−1\small X_{i-1} ) und das zweite Argument von links nach rechts ( Xn\small X_n nach Xi\small X_{i} ).

bb steht nur für "Argument davor" und "Argument danach", dann kommen nur Leersymbole B\small B .

Prädikatenlogische Repräsentation von Befehlen

Befehle β∈δM\small \beta \in \delta_{M}↦\mapsto PL-Formelmengen ξ(β)\small \xi(\beta)

δ(q,Xi)=(p,Y,…) \small\delta\left(q, X_{i}\right)=(p, Y, \textcolor{pink}\dots) 

Die Funktion bildet jeden Zustand und Symbol am Arbeitsband auf einen neuen Zustand, dem Symbol welches geschrieben werden soll und einer Bewegung zu.

a) Kopf bleibt stehen δ(q,Xi)=(p,Y,S) \small \delta\left(q, X_{i}\right)=(p, Y, \textcolor{pink}S) 

X1X2…Xi−1qXiXi+1…Xn⇒X1X2…Xi−1pYXi+1…Xn \small X_{1} X_{2} \ldots X_{i-1} \mathbf{q} X_{i} X_{i+1} \ldots X_{n} \Rightarrow X_{1} X_{2} \ldots X_{i-1} p Y X_{i+1} \ldots X_{n} 

Wichtig:Xi\small X_iund alle Symbole rechts davon am Band können auch Blank seinB\small B.

ξ1(β)=∀u∀v[Pq(u,fXi(v))⊃Pp(u,fY(v))] \small \xi_{1}(\beta)=\forall u \forall v\left[P_{\mathbf{q}}\left(u, f_{\mathbf{X}_{i}}(v)\right) \supset P_{\mathbf{p}}\left(u, f_{\mathbf{Y}}(v)\right)\right] 

ξ2(β)=∀u[Pq(u,b)⊃Pp(u,fY(b))] \small \xi_{2}(\beta)=\forall u\left[P_{\mathbf{q}}(u, b) \supset P_{\mathbf{p}}\left(u, f_{\mathbf{Y}}(b)\right)\right] 

b) Kopf bewegt sich nach rechts δ(q,Xi)=(p,Y,R) \small \delta\left(q, X_{i}\right)=(p, Y, \textcolor{pink}R) 

X1X2…Xi−1qXiXi+1…Xn⇒X1X2…Xi−1YpXi+1…Xn \small X_{1} X_{2} \ldots X_{i-1} q X_{i} X_{i+1} \ldots X_{n} \Rightarrow X_{1} X_{2} \ldots X_{i-1} Y p X_{i+1} \ldots X_{n} 

ξ1(β)=∀u∀v[Pq(u,fXi(v))⊃Pp(fY(u),v)] \small \xi_{1}(\beta)=\forall u \forall v\left[P_{\mathbf{q}}\left(u, f_{\mathbf{X}_{i}}(v)\right) \supset P_{\mathbf{p}}\left( f_{\mathbf{Y}}(u), v\right)\right] 

ξ2(β)=∀u[Pq(u,b)⊃Pp(fY(u),b)] \small \xi_{2}(\beta)=\forall u\left[P_{\mathbf{q}}(u, b) \supset P_{\mathbf{p}}\left(f_{\mathbf{Y}}(u), b\right)\right] 

c) Kopf bewegt sich nach links δ(q,Xi)=(p,Y,L) \small \delta\left(q, X_{i}\right)=(p, Y, \textcolor{pink}L) 

X1X2…Xi−1qXiXi+1…Xn⇒X1X2…pXi−1YXi+1…Xn \small X_{1} X_{2} \ldots X_{i-1} q X_{i} X_{i+1} \ldots X_{n} \Rightarrow X_{1} X_{2} \ldots pX_{i-1} Y X_{i+1} \ldots X_{n} 

Konfigurations-Übergänge entsprechen PL-Inferenzen

K⇒β[∗]K′K \Rightarrow_{\beta}^{[*]} K^{\prime}

wobei β∈δM\small \beta \in \delta_{M} beliebig oft angewendet

Lemma

K⇒βK′\small K \Rightarrow_\beta K^{\prime}⟹\impliesξ(K),ξ1(β),ξ2(β)⊨ξ(K′) \small \xi(K), \xi_{1}(\beta), \xi_{2}(\beta) \models \xi\left(K^{\prime}\right) 

K⇒β∗K′\small K \Rightarrow_\beta ^*K^{\prime} * ⟸\Longleftarrowξ(K),ξ1(β),ξ2(β)⊨ξ(K′) \small \xi(K), \xi_{1}(\beta), \xi_{2}(\beta) \models \xi\left(K^{\prime}\right) 

Akzeptieren (Halten) einer MaschineM\small M

Akzept(M)=∃x∃y[Pp1(x,y)∨…∨Ppn(x,y)] \small A k z e p t(M)=\exists x \exists y\left[P_{p_{1}}(x, y) \vee \ldots \vee P_{p_{n}}(x, y)\right] 

Dabei ist {p1,…,pn}\small \left\{p_{1}, \ldots, p_{n}\right\} die Menge der Endzustände der Maschine.

Satz: Reduktion des Halteproblems auf PL-Konsequenz

Für alle w∈{0,1}∗\small w \in\{0,1\}^{*} und Turingmaschinen M\small M mit δ={β1,…,βn}\small \delta=\left\{\beta_{1}, \ldots, \beta_{n}\right\} gilt:

Die TM akzeptiert das Wort w\small w genau dann, wenn

ξ(K0(M,w)),ξ1(β1),ξ2(β1),…,ξ1(βn),ξ2(βn)⊨Akzept⁡(M) \small \xi\left(K_{0}(M, w)\right), \xi_{1}\left(\beta_{1}\right), \xi_{2}\left(\beta_{1}\right), \ldots, \xi_{1}\left(\beta_{n}\right), \xi_{2}\left(\beta_{n}\right) \models \operatorname{Akzept}(M) 

Aus diesem Satz und dem Deduktionstheorem folgt Lu≤LPLG\small L_{u} \leq L_{P L G} .

Dadurch ist die Unentscheidbarkeit der PL (Gültigkeit und Konsequenz) bewiesen.

Bedeutung der Reduktion

Für "Leibniz und Hilberts" Traum bedeutet das:

Probleme lassen sich meist in PL ausdrücken.

Vollständigkeit

Wenn es eine Lösung gibt, so lässt sich diese (als formaler PL-Beweis) prinzipiell auch finden.

Unentscheidbarkeit

Es gibt kein Verfahren, dass in jedem Fall feststellen kann, ob eine Lösung existiert.

Satz (Konsequenz für die Beweissuche)

Es gibt keine berechenbare Funktion g\small g , so dass:

Wenn FF eine gültige PL-Formel ist, dann gibt es einen Tableau-Beweis von F\small F in der Größe g(∣F∣)\small g(|F|) wobei ∣F∣\small |F| die Länge von F\small F bezeichnet.