Sitzung 11: Modallogiken 3

Bisher haben wir die Beweismethode der semantischen Bäume behandelt. Auch sehr beliebt im Kontext der Modallogiken sind Hilbert-Beweissysteme. Diese beruhen auf einer Menge von Prinzipien formuliert als Axiome bzw. Axiomenschemata. Etwa, die klassische Aussagenlogik basiert auf den folgenden:

Imp1

\(A \rightarrow (B \rightarrow A)\)

Imp2

\((A \rightarrow (C \rightarrow B)) \rightarrow ((A \rightarrow C) \rightarrow (A \rightarrow B))\)

AndE1

\((A \wedge B) \rightarrow A\)

AndE2

\((A \wedge B) \rightarrow B\)

AndI

\(A \rightarrow (B \rightarrow (A \wedge B))\)

DisI1

\(A \rightarrow (A \vee B)\)

DisI2

\(B \rightarrow (A \vee B)\)

DisE

\((A \rightarrow B) \rightarrow ((C \rightarrow B) \rightarrow ((A \vee C ) \rightarrow B))\)

NegI

\((A \rightarrow C) \rightarrow ((A \rightarrow \neg C) \rightarrow \neg A)\)

NegE

\(A \rightarrow( \neg A \rightarrow B)\)

EM

\(A \vee \neg A\)

Die \(A, B\) und \(C\) sind hierbei Metavariablen. Man spricht von Instanzen dieser Schemata, wenn Metavariablen (uniform und simultan) durch konkrete Formeln in der gegeben formalen Sprache (etwa der der Aussagenlogik) ersetzt werden.

Etwa ist \[ p \rightarrow ( (p \wedge q) \rightarrow p)\] eine Instanz des Axiomenschemas \[A \rightarrow ( B \rightarrow A)\] wobei \(A\) durch \(p\) ersetzt wurde und \(B\) durch \(p \wedge q\).

Neben Axiomen brauchen wir zum Schlußfolgern auch Schlußregeln. Etwa, um \(p\) aus \(p \wedge q\) zu folgern brauchen wir zum einen das Axiom \((p\wedge q) \rightarrow p\) und zum anderen die Schlußregel Modus Ponens:

MP

Falls \(A\) und \(A \rightarrow B\), so auch \(B\).

Ein Hilbert-Beweis der klassischen Aussagenlogik basiert auf obigen Axiomen und der Schlußregel MP. Hier ist ein Beispiel eines sehr einfachen Beweises, dass \(p \rightarrow q\) aus \(q\) folgt:

1.	\(q\)	PREM
2.	\(q \rightarrow (p \rightarrow q)\)	Imp1
3.	\(p \rightarrow q\)	MP; 1,2

Oder ein Beweis von \(p \rightarrow r\) aus \(p \rightarrow q\) und \(q \rightarrow r\):

1.	\(p \rightarrow q\)	PREM
2.	\(q \rightarrow r\)	PREM
3.	\((p \rightarrow (q \rightarrow r)) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))\)	Imp2
4.	\((q \rightarrow r) \rightarrow (p \rightarrow (q \rightarrow r))\)	Imp1
5.	\(p \rightarrow (q \rightarrow r)\)	MP; 2,4
6.	\((p \rightarrow q) \rightarrow (p \rightarrow r)\)	MP; 5,3
7.	\(p \rightarrow r\)	MP; 1,6

Generel sind Hilbert-Beweise (wir nennen sie auch Ableitungen oder Deduktionen) wie folgt definiert.

Gegeben eine

1. Menge von Axiom Schemata \(\mathsf{Ax}\)
2. eine Menge von Schlußregeln \(\mathsf{R}\),
3. und eine Menge von Prämissen \(\Gamma\),

ein Beweis in einem Hilbert Beweissystem basierend auf \(\mathsf{Ax}\) und \(\mathsf{R}\) ist eine Sequenz von Formeln \(\langle A_1, A_2 ,\ldots, A_n \rangle\) wobei jedes \(A_i\) (mit \(1 \le i \le n\))

• eine gegebene Prämisse in \(\Gamma\) ist, oder
• eine Instanz eines gegebenen Axiomenschemas in \(\mathsf{Ax}\) ist, oder
• aus \(A_{i_1}, \ldots, A_{i_m}\) mit Hilfe einer gegebenen Schlußregel in \(\mathsf{R}\) abgeleitet wird (wobei \(i_1, \ldots, i_m < i\)).

Für eine gegeben Logik L, die mit einer Menge von Axiomenschemata \(\mathsf{Ax}\) und einer Menge von Schlußregeln \(\mathsf{R}\) assoziiert ist, schreiben wir

\[\Gamma \vdash_{\mathbf{L}} A\]

falls ein Beweis von \(A\) aus \(\Gamma\) (d.h. mit lediglich Prämissen in \(\Gamma\)) und auf der Grundlage von \(\mathsf{Ax}\) und \(\mathsf{R}\) existiert. Die Relation \(\vdash_{\mathbf{L}}\) wird als Deduktions-, Ableitungs- oder Beweisbarkeitsrelation bezeichnet. Ist die Logik L aus dem Kontext klar, so wird das Subskript meist weggelassen.

Falls \(\emptyset \vdash_{\mathbf{L}} A\) gilt (also \(A\) ist beweisbar ohne Verwendung von Axiomen), so ist \(A\) ein Theorem von L. Dies wird meist abkürzend \(\vdash_{\mathbf{L}} A\) geschrieben. Etwa ist jede Instanz eines Axiomenschemas in \(\mathsf{Ax}\) ein Theorem.

Eine Axiomatisierung der Modallogik K ist gegeben durch die Schemata der klassischen Prädikatenlogik und

K

\(\Box (A \rightarrow B) \rightarrow ( \Box A \rightarrow \Box B)\)

Zudem wird neben MP folgende Regel benutzt:

N

Falls \(\vdash A\) dann auch \(\vdash \Box A\).

Beachte: N ist nur auf Theoreme anwendbar, nicht auf Prämissen oder Formeln deren Beweis von Prämissen Gebrauch macht. Der Unterschied zwischen Modus Ponens, bei dem es heißt “Falls \(A\) und …” und der Regel N, bei der es heißt “Falls \(\vdash A\) …”, ist zwar unscheinbar, aber entscheidend!

Hier ist ein Beispiel für einen Hilbert-Beweis in der Logik K, der zeigt, dass \(\Box v\) aus der Prämissenmenge \(\lbrace p, q, p \rightarrow \Box (r \rightarrow (v \wedge u)), \Box r \rbrace\) folgt. In Zeichen: \[\lbrace p, q, p \rightarrow \Box (r \rightarrow (v \wedge u)), \Box r \rbrace \vdash_{\mathbf{K}} \Box v\]

1.	\(p\)	PREM
2.	\(q\)	PREM
3.	\(p \rightarrow \Box (r \rightarrow (v \wedge u))\)	PREM
4.	\(\Box (r \rightarrow (v \wedge u))\)	MP, 1,3
5.	\(\Box(r \rightarrow (v \wedge u)) \rightarrow (\Box r \rightarrow \Box (v \wedge u))\)	K
6.	\(\Box r \rightarrow \Box (v \wedge u)\)	MP, 4,5
7.	\((v \wedge u) \rightarrow v\)	ANDE1
8.	\(\Box((v \wedge u) \rightarrow v)\)	N
9.	\(\Box((v \wedge u) \rightarrow v) \rightarrow ( \Box(v \wedge u) \rightarrow \Box v)\)	K
10.	\(\Box(v \wedge u) \rightarrow \Box v\)	MP, 8,9
11.	\(\Box r\)	PREM
12.	\(\Box(v \wedge u)\)	MP, 11,6
13.	\(\Box v\)	MP, 12,10

Folgende Eigenschaften folgen unmittelbar aus der obigen Definition von Beweisbarkeit:

Monotonität

Falls \(\Gamma \vdash A\) so auch \(\Gamma \cup \Gamma^{\prime} \vdash A\).

Kompaktheit

Falls \(\Gamma \vdash A\) so gibt es eine endliche Teilmenge \(\Gamma^{\prime}\) von \(\Gamma\) so dass \(\Gamma^{\prime} \vdash A\).

Transitität

Falls \(\Gamma \vdash A\) und \(\Gamma^{\prime} \cup \lbrace A\rbrace \vdash B\) so auch \(\Gamma \cup \Gamma^{\prime} \vdash B\).

Reflexivität

Falls \(A \in \Gamma\), so \(\Gamma \vdash A\).

Wir nehmen etwa für die Transitivität an, dass \(\Gamma \vdash A\) und \(\Gamma^{\prime} \cup \lbrace A \rbrace \vdash B\). Somit gibt es einen Beweis \(\langle A_{1}, \ldots, A_n (=B) \rangle\) von \(B\) mit Prämissen in \(\Gamma^{\prime} \cup \lbrace A\rbrace\). Ebenso gibt es einen Beweis \(\langle B_{1}, \ldots, B_m (= A) \rangle\) von \(A\) mit Prämissen in \(\Gamma\). Um einen Beweis von \(B\) aus \(\Gamma \cup \Gamma^{\prime}\) zu konstruieren, ersetzen wir jedes \(A_i = A\) im ersten Beweis durch \(B_1, \ldots, B_m\). Der resultierende Beweis macht keinen Gebrauch mehr von der Prämisse \(A\) sondern macht nur noch Gebrauch von Prämissen in \(\Gamma \cup \Gamma^{\prime}\). \(\blacksquare\)

Das Deduktionstheorem hält sofern die Axiome Imp1 und Imp2 gegeben sind:

\(\Gamma \cup \lbrace A\rbrace \vdash B\) gdw \(\Gamma \vdash A \rightarrow B\).

Die Links-Rechts Richtung kann man induktiv zeigen. Wir gehen von einem Beweis \(\langle A_{1}, \ldots, A_n (=B) \rangle\) von \(B\) aus Prämissen in \(\Gamma \cup \lbrace A\rbrace\) aus. Wir zeigen nun induktiv, dass für jedes \(i = 1, \ldots, n\), die Formel \(A \rightarrow A_i\) aus \(\Gamma\) ableitbar ist.

• Basis: \(A_1\) ist entweder ein Axiom oder eine Prämisse in \(\Gamma \cup \lbrace A\rbrace\). Im ersten Fall gibt es folgenden Beweis von \(A \rightarrow A_{1}\):

  1.	\(A_1\)	Ax
  2.	\(A_1 \rightarrow ( A \rightarrow A_1)\)	Imp1
  3.	\(A \rightarrow A_1\)	MP; 1,2

  Falls \(A_1 \in \Gamma\) dann verfahren wir analog. Im Fall \(A_1 = A\), können wir zeigen, dass \(\vdash A_1 \rightarrow A_1\). Beweisen Sie dies als Übung! :-)

• Schritt: Es sei \(1 < i \le n\). Als Induktionshypothese gehen wir davon aus, dass für alle \(j < i\) gilt \(\Gamma \vdash A \rightarrow A_j\).

  • Falls \(A_i\) eine Prämisse in \(\Gamma \cup \lbrace A\rbrace\) oder ein Axiom ist, gehen wir genauso vor wie im Basisschritt.
  • Ansonsten wurde \(A_i\) durch MP (oder im Kontext der Modallogiken möglicherweise auch durch N) abgeleitet. Das heißt es gibt \(A_k\) und \(A_l = A_k \rightarrow A_i\) wobei \(k,l < i\). Mit der Induktionshypothese wissen wir, dass es Beweise \(\langle C_{1}, \ldots, C_m (= A \rightarrow A_k)\rangle\) und \(\langle D_{1}, \ldots, D_{m^{\prime}} (= A \rightarrow A_l)\rangle\) aus \(\Gamma\) gibt. Wir verbinden nun diese beiden Beweise zu einem neuen Beweis wie folgt:

    1.	\(C_1\)	…
    …	…	…
    \(m\).	\(C_m (= A \rightarrow A_k)\)	…
    \(m+1\).	\(D_1\)	…
    …	…	…
    \(m+m^{\prime}\).	\(D_{m^{\prime}} (= A \rightarrow A_l = A \rightarrow (A_k \rightarrow A_i))\)	…
    \(m+m^{\prime}+1\).	\((A \rightarrow ( A_k \rightarrow A_i)) \rightarrow ((A \rightarrow A_k)\rightarrow (A \rightarrow A_i))\)	Imp2
    \(m+m^{\prime}+2\).	\((A \rightarrow A_k) \rightarrow (A \rightarrow A_i)\)	MP; \(m+m^{\prime}, m+m^{\prime}+1\)
    \(m+m^{\prime}+3\).	\(A \rightarrow A_i\)	MP; \(m, m+m^{\prime}+2\)

• Der Fall in dem \(A_i\) durch N abgeleitet wurde ist ähnlich und ist ihnen zur Übung überlassen. \(\blacksquare\)

Generell kann man zeigen, dass das Hilbert-Beweissystem für die Logik K korrekt und vollständig ist bzgl. der semantischen Konsequenzrelation. (Dies gilt selbstverständlich auch für das Hilbert-Beweissystem für die klassische Aussagenlogik.) D.h.,

\(\Gamma \Vdash_{\mathbf{K}} A\) gdw \(\Gamma \vdash_{\mathbf{K}} A\).

Die Richtung von rechts nach links ist die Vollständigkeit: alles was semantische Konsequenz ist, kann beweisen werden. Die andere Richtung ist die Korrektheit: alles was beweisen werden kann ist auch semantische Konsequenz (es wird also nichts Falsches beweisen, weshalb das Beweisverfahren korrekt ist).

Der Beweis der Korrektheit ist relativ einfach und wird uns beim nächsten mal beschäftigen. Der Beweis der Vollständigkeit ist trickreicher, aber auch etwas faszinierender :-)

Übungen

Übung 1. Beweisen Sie:

1. \(\lbrace p \rbrace \vdash q \rightarrow p\)
2. \(\lbrace p \rightarrow q, q \rightarrow r\rbrace \vdash p \rightarrow r\)
3. \(\lbrace p \rightarrow q\rbrace \vdash (p \wedge r ) \rightarrow q\)
4. \(\vdash p \rightarrow p\)

Übung 2. Beweisen Sie die Links-nach-Rechts Richtung des Deduktionstheorems.

Übung 3. Beweisen Sie:

1. \(\lbrace \Box p, \Box(p \rightarrow q)\rbrace \vdash_{\mathbf{K}} \Box q\)
2. \(\lbrace \Box p, \Box q\rbrace \vdash_{\mathbf{K}} \Box(p \wedge q)\)