Tableaux

Logischer Kalkül $\mathcal K$

formales Regelsystem, nimmt nur auf Syntax bezug

zeigt schrittweise die Gültigkeit von Formeln und Konsequenzbehauptungen

$\small F_{1}, \ldots F_{n} \vdash_{\mathcal{K}} G$

Eigenschaften von Kalkülen

Korrektheit (Syntax zu Semantik)

$\small F_{1}, \ldots, F_{n} \vdash_{\mathcal{K}} G \textcolor{grey}{\Longrightarrow} F_{1}, \ldots, F_{n} \models G$

Vollständigkeit (Semantik zu Syntax)

$\small F_{1}, \ldots, F_{n} \vdash_{\mathcal{K}} G \textcolor{grey}{\Longleftarrow} F_{1}, \ldots, F_{n} \models G$

Hilbert-Typ-Kalkül

siehehttps://de.m.wikipedia.org/wiki/Hilbert-Kalkül

Beweissuche schwer zu automatisieren

Ableitungen entsprechen nicht natürlichsprachlichen mathematischen Argumentationsketten

Keine Beziehung zur Semantik

Vollständigkeit ist nicht einfach nachzuweisen (korrektheit schon)

Aussagenlogik

Logische Axiome

$A,B$ und $C$ können gegen jede beliebige atomare Formel ausgetauscht werden

$\small (A \supset(B \supset A))$

$\small ((A \supset(B \supset C)) \supset((A \supset B) \supset(A \supset C)))$

Nur eine Regel: Modus Ponens

$\Large \frac{A \quad A \supset B}{B}$

Beispiel
Wir wollen $A \supset A$ beweisen
Axiom 1: $\small (A \supset(B \supset A))$
Axiom 2: $\small ((A \supset(B \supset C)) \supset((A \supset B) \supset(A \supset C)))$
statt $B$ in Axiom 1 setzen wir in der ersten Zeile $(A\supset A)$ ... usw.

Prädikatenlogik

Frege-Hilbert-Typ-Kalkül für klassische PL

Gleichen Nachteile wie bei AL

Logische Axiome

$A,B$ und $C$ können gegen jede beliebige atomare Formel ausgetauscht werden

$\small (A \supset(B \supset A))$

$\small ((A \supset(B \supset C)) \supset((A \supset B) \supset(A \supset C)))$

$\dots$ 3. bis 9.

$\small A(x / t) \supset \exists x A$
$t$ muss in $A$ frei für $x$ sein

$\small \forall x A \supset A(x / t)$
$t$ muss in $A$ frei für $x$ sein

Regeln

$\Large \frac{A ~~~A \supset B}{B}$ $\Large \frac{B\supset A}{B \supset \forall x A}$ $\Large \frac{A \supset B}{\exists x A \supset B}$

$x$ darf in $B$ nicht frei vorkommen

(außer in der ersten Regel)

Tableau-Kalkül

Variante des Sequentialkalküls

siehehttps://de.m.wikipedia.org/wiki/Baumkalkül

Ein Tableau ist ein Baum von bewerteten Formeln als Tafel.

Sie können von Wahrheitstafeln abgelesen werden.

Grundidee: Beweis durch widerspruch

Wir gehen davon aus es gibt eine mögliche Interpretation für die Konsequenzbehauptung $\small F_{1}, \ldots, F_{n} \models G$ .

Beweis durch Widerspruch, durch Annahme dass

$\small \operatorname{val}_{I}\left(F_{1}\right)=\mathbf{t}, \ldots, \operatorname{val}_{I}\left(F_{n}\right)=\mathbf{t}$

$\small \operatorname{val}_{I}(G)=\mathbf{f}$

für eine Interpretation $I$ gilt (und folgert für Teilformeln.)

Beispiel
Tableau-Beweis von $(A \supset B) \wedge A \models B$
Wir wollen einen Widerspruch zeigen, deshalb:
1. Annahme: $\mathbf{t}:(A \supset B) \wedge A$
2. Annahme: $\mathbf{f}: B$
Wir zerlegen die Annahme $\mathbf{t}:(A \supset B) \wedge A$
$\mathbf{t}: A \supset B$
$\mathbf{t}: A$
Aus $\mathbf{t}: A \supset B$ folgt
$\mathbf{f}: A$
$\mathbf{t}: B$
Das steht im Widerspruch zu den vorherigen Annahmen.

Entscheidungsverfahren

Beweisversuch terminiert immer und vollständige Expansion liefert Beweis oder Gegenbeispiel.

Beweis = geschlossenes Tableau

Gegenbeispiel = offener Ast

Don't care Indeterminismus

Ergebnis ist unabhängig von Auswertungsreihenfolge.

Geschlossenheit von Ästen

(Hat nichts mit geschlossenen Formeln zu tun)

Wenn sowohl $\small \mathbf{t}: F$ als auch $\small \mathbf{f}: F$ vorkommen heißt der Tableau-Ast geschlossen, sonst offen.

Abschlussregel

Gelungenes Tableau-Beweis von einer Konsequenzbehauptung $\small F_{1}, \ldots, F_{n} \models G$ ist ein geschlossenes Tableau, mit Annahmen: $\small \mathbf{t}: F_{1}, \ldots, \mathbf{t}: F_{n}, \mathbf{f}: G$ .

Beweis von $F$ ist ein geschlossenes Tableau mit Wurzel $\small \mathbf{f}: F$

Vollständigkeit

Tableau-Beweis $\textcolor{grey}{\Longrightarrow} \small F_{1}, \ldots, F_{n} \models G$

Beweis
Lemma
Für $\vee$ Operator gilt:
$\small \operatorname{val}_{I}(A \vee B)=\mathbf{f} \Longleftrightarrow \operatorname{val}_{I}(A)=\mathbf{f} \text { und } \operatorname{val}_{I}(B)=\mathbf{f}$
$\small \operatorname{val}_{I}(A \vee B)=\mathbf{t} \Longleftrightarrow \operatorname{val}_{I}(A)=\mathbf{t} \text { oder } \operatorname{val}_{I}(B)=\mathbf{t}$
Analog für alle anderen Operatoren
Beweis der Vollständigkeit durch Widerspruch
Angenommen es stimmt nicht, dass "Tableau-Beweis ${\implies} \small F_{1}, \ldots, F_{n} \models G$ ".
Also der Tableau-Beweis gelingt nicht aber die Konsequenzbehauptung stimmt.
Wenn ein vollständig expandiertes Tableau offen ist heißt das der Tableau-Beweis von $\small F_{1}, \ldots, F_{n} \models G$ gelingt nicht.
Das bedeutet es gibt kein Gegenbeispiel $I$ für die Konsequenzbehauptung.
Das bedeutet alle Äste sind offen.
Sei $\Gamma$ ein offener , vollständig expandierter Ast.
Eine Aussagenvariable $A$ kann für in diesem Ast nicht gleichzeitig wahr $\small \mathbf{t}: A$ und falsch $\small \mathbf{f}: A$ sein.
$\small I(A)=\mathbf{t}$ falls $\small \mathbf{t}: A$
$\small I(A)=\mathbf{f}$ falls $\small \mathbf{f}: A$
Durch das Lemma gilt das auch für Formeln. (Induktion)
$\small \text{val}_I(F)=\mathbf{t}$ falls $\small \mathbf{t}: F$
$\small \text{val}_I(F)=\mathbf{f}$ falls $\small \mathbf{f}: F$
Und dadurch dass die wir eine eindeutige Interpretation haben, folgt daraus
$\small \operatorname{val}_{I}\left(F_{1}\right)=\mathbf{t}, \ldots, \operatorname{val}_{I}\left(F_{n}\right)=\mathbf{t}$
$\small \text{val}_{I}(G)=\mathbf{f}$
Das ist das Gegenbeispiel, von der wir behauptet haben, dass sie nicht existiert. ↯

Korrektheit

Tableau-Beweis $\textcolor{grey}{\Longleftarrow} \small F_{1}, \ldots, F_{n} \models G$

Beweis
Beweis der Korrektheit durch Widerspruch
Angenommen es stimmt nicht, dass "Tableau-Beweis ${\Longleftarrow} \small F_{1}, \ldots, F_{n} \models G$ ".
Also die Konsequenzbehauptung stimmt nicht aber der Tableau-Beweis gelingt.
Wenn ein vollständig expandiertes Tableau geschlossen ist heißt das der Tableau-Beweis von $\small F_{1}, \ldots, F_{n} \models G$ gelingt.
Wir nehmen an es gibt ein Gegenbeispiel $I$ für $\small F_{1}, \ldots, F_{n} \models G$ wodurch wir wissen, dass sie nicht stimmen kann.
Es gilt
$\small \operatorname{val}_{I}\left(F_{1}\right)=\mathbf{t}, \ldots, \operatorname{val}_{I}\left(F_{n}\right)=\mathbf{t}$
$\small \text{val}_{I}(G)=\mathbf{f}$ .
Wegen dem Lemma gilt für jeden Ast $\Gamma$ des Tableau:
$\small \text{val}_I(F)=\mathbf{t}$ falls $\small \mathbf{t}: F$
$\small \text{val}_I(F)=\mathbf{f}$ falls $\small \mathbf{f}: F$
Dadurch dass das Tableau geschlossen ist, muss auch jeder Ast geschlossen sein, wodurch gleichzeitig $\small \mathbf t:F$ und $\small \mathbf f:F$ auf dem Ast liegen müssen.
Wir müssten im Tableau auf ein Widerspruch stoßen, wodurch der Tableau-Beweis gelingen würde. ↯

Aussagenlogik

Tableau Expansion

(siehe unten)

Typen von Folgerungen:

$\alpha$ -Regeln Konjunktion von kleineren Behauptungen

$\beta$ -Regeln Disjunktion von kleineren Behauptungen

Regeln

Eingeschränkte Syntax, mit nur $\small \vee, \wedge, \supset, \neg$

Prädikatenlogik

💡

Wir beschränken uns auf geschlossene Formeln

F

Es kommen im PL-Tableau nie freie Variablen vor.

Begriffe

“Term $\small t$ ist frei für $\small x$ in $\small F$ ”

wenn $t$ keine Variablen enthält die in $\small \forall xF$ oder $\small \exists xF$ gebunden sind.

“ $\small x$ ist frei in $\small F$ ”

wenn $x$ nicht an einem Quantor gebunden ist, also wenn $\small x \in F V(F)$ .

“geschlossen”

$\small F$ ist geschlossen wenn $\small F V(F)=\{\}$ .

Term $\small t$ ist geschlossen wenn es keine Variablen hat, also $\small F V(t)=V(t)=\{\}$ .

Regeln

Eingeschränkte Syntax, mit nur $\small \vee, \wedge, \supset, \neg$

Tableau Expansion (mit Quantoren)

$\Sigma^{p a r}$ Signatur erweitert mit den Parametern $\small c,d,e$

$\alpha$ -Regeln

$\begin{aligned}&\frac{w:~ F}{w_{1}:~ F_{1}} \\&w_{2}:~ F_{2}\end{aligned}$

$\beta$ -Regeln

$\Large \frac{w:~~ F}{w_{1}:~~ F_{1} ~\mid~ w_{2}:~~ F_{2}}$

$\gamma$ -Regeln

$\Large\frac{\mathbf{t}:~~ \forall x F}{\mathbf{t}:~~F(x / t)}$ $\Large\frac{\mathbf{f}:~~\exists x F}{\mathbf{f}:~~F(x / t)}$

für beliebige geschlossene (ohne Variablen) Terme $t$ über $\Sigma^{p a r}$ .

(muss meistens öfter über die selbe Formel mit verschiedenen $t$ angewendet werden)

Erklärung
$\small \operatorname{val}_{\mathcal{I}}(\textcolor{pink}{\forall x F})=\textcolor{pink}{\mathbf{t}}$ für alle Interpretationen $\small \mathcal{I}^{\prime} \stackrel{x}{\sim} \mathcal{I}$ .
Daher auch in $\small \operatorname{val}_{\mathcal{I}}(\textcolor{pink}{F(x / t)})=\textcolor{pink}{\mathbf{t}}$ für alle variablenfreien $\small t$ .
(Eigentlich sogar auch für alle $\small t$ die frei für $\small x$ in $F$ sind → keine gebundenen Variablen aus $F$ beinhalten)
Analog für $\small \operatorname{val}_{\mathcal{I}}({\exists x F})={\mathbf{f}}$

Problem
Wir können nicht garantieren, dass alle Elemente der Domäne durch einen Term repräsentiert werden.

$\delta$ -Regeln

$\Large\frac{\mathbf{f}:~~ \forall x F}{\mathbf{f}:~~ F(x / c)}$ $\Large\frac{\mathbf{t}:~~ \exists x F}{\mathbf{t}:~~ F(x / c)}$

für Parameter $c \in \Sigma^{p a r}$ der bisher nicht vorgekommen ist

Erklärung
$\small \operatorname{val}_{\mathcal{I}}(\textcolor{pink}{\exists x F})=\textcolor{pink}{\mathbf{f}}$ für mindestens eine der Interpretationen $\small \mathcal{I}^{\prime} \stackrel{x}{\sim} \mathcal{I}$ .
Analog für $\small \operatorname{val}_{\mathcal{I}}({\forall x F})={\mathbf{f}}$

Problem
Wir wissen nicht welche Terme $\small t$ wir für $\small x$ substituieren dürfen und welche nicht.
Wir wissen nicht ob es einen variablenfreien Term gibt der einen "Zeugen" für $\small {\exists x F}$ repräsentiert.

Satz von Löwenheim-Skolen

Lösung für Probleme die mit $\gamma$ -Regeln entstehen:

$\Sigma^{p a r}$ Parameter: Erweiterung der Sprache um unendlich viele zusätzliche Konstanten

Lösung für Probleme die mit $\delta$ -Regeln entstehen:

Bei der Zerlegung von $\small \textcolor{pink}{\mathbf{f}: \forall x F}$ und $\small \textcolor{pink}{\mathbf{t}:\exists x F}$ muss der "Zeuge" für $\small F$ neu sein (also nicht im Tableau bisher vorgekommen sein).

Mit Gleichheits-Operator

💡

Wir beschränken uns auf geschlossene Formeln

F

Es kommen im PL-Tableau nie freie Variablen vor

Atomare Formeln, können nur variablenfreie Terme enthalten.

Für die Terme $\small s,t$ die in den folgenden Formeln vorkommen gilt $\small V(s)=V(t)=\{\}$ .

$\small \mathbf{t}: s=t$

$\small \mathbf{f}: s=t$

Abschlussregel für Gleichheitsatome $\small AB^=$

(Abschlussregel für Tableaux siehe oben)

Wenn ein Ast die Formel $\small \mathbf{f}: t=t$ enthält, wird er geschlossen.

Substitutionssregel für Gleichheitsatome $\small S^=$

$\small \begin{gathered}\mathbf{t}: s=t \\\frac{\textcolor{pink}{\mathbf{t}}: A[s]}{\textcolor{pink}{\mathbf{t}}: A[\textcolor{pink}{s / t}] }\end{gathered}$ $\small \begin{gathered} \mathbf{t}: s=t \\ \frac{\textcolor{pink}{\mathbf{f}}: A[s]}{\textcolor{pink}{\mathbf{f}}: A[\textcolor{pink}{s / t}] } \end{gathered}$ $\small \begin{gathered}\mathbf{t}: s=t \\\textcolor{pink}{\mathbf{t}}: A[t] \\\hline \textcolor{pink}{\mathbf{t}}: A[\textcolor{pink}{t / s}] \end{gathered}$ $\small\begin{gathered}\mathbf{t}: s=t \\\frac{\textcolor{pink}{\mathbf{f}}: A[t]}{\textcolor{pink}{\mathbf{f}}: A[\textcolor{pink}{t / s}] }\end{gathered}$

$\small A[s]$ Atom $A$ enthält Term $s$ (beliebig tief)

$\small A[s/t]$ Term $s$ wird durch $t$ ersetzt