Logik
Vorlesung Wintersemester 2016
Ludwig-Maximilians-Universität München
Josef Berger
7. November 2016
Inhaltsverzeichnis
I
Der Gödelsche Vollständigkeitssatz
2
1 Terme und Formeln
2
2 Herleitungen
7
3 Intuituionistische Logik und Minimallogik
19
Teil I
Der Gödelsche
Vollständigkeitssatz
1
Terme und Formeln
Definition. Eine Sprache L besteht aus folgenden Zeichen:
1. abzählbar viele freie Variablen v0 , v1 , v2 , , . . .
2. abzählbar viele gebundene Variablen x0 , x1 , x2 , . . .
3. beliebig viele Konstantensymbole c , d , e , . . .
4. endlich viele Funktionszeichen f , g , h , . . .
5. endlich viele Relationszeichen P , Q , R , . . .
.
6. die logischen Zeichen = , ⊥ , ∧ , ∨ , → , ∀ , ∃
7. die Hilfszeichen (
, )
,
,
Jedem Funktionszeichen f (und jedem Relationszeichen R ) ist eine positive
natürliche Zahl n zugeordnet. Man nennt n die Stelligkeit von f (bzw. von
R ).
Sprechweise:
.
= ist gleich
Junktoren: ∧ und
∨ oder
→ impliziert
Quantoren: ∀ für alle (Allquantor)
∃ es gibt (Existenzquantor)
⊥ Falsum
Sei L∗ die Menge der endlichen Wörter oder Zeichenketten (der Sprache L).
Zum Beispiel ist
(((, , , , , , x0 v222 ∀, , x0 ∀
ein Wort. Sei FV = { vi | i ∈ N} die Menge der freien Variablen. Für ein
Wort Ω sei
FV( Ω ) = { v ∈ FV | v kommt in Ω vor} .
2
Für Ω , ∆ ∈ L∗ und z ∈ L sei
Ω [∆/z]
das Wort, das entsteht, indem man jedes z in Ω durch ∆ ersetzt.
Lemma 1. Seien Ω , ∆ , ∆0 Wörter und z , z 0 verschiedene Zeichen. Das
Zeichen z 0 komme nicht in ∆ vor und z komme nicht in ∆0 vor. Dann gilt
Ω [ ∆ / z ] [ ∆0 / z 0 ] = Ω [ ∆ 0 / z 0 ] [ ∆ / z ] .
Definition. Die Menge T der Terme der Sprache L ist die kleinste Teilmenge von L∗ mit folgenden Eigenschaften:
t1 ) die freien Variablen sind Terme
t2 ) die Konstantensymbole sind Terme
t3 ) ist f ein n-stelliges Funktionszeichen und sind t1 , . . . , tn ∈ T , so ist
auch f ( t1 , . . . , tn ) ∈ T
Die Komplexität eines Terms t ist die Anzahl der Vorkommen von Funktionszeichen in t . Ist zum Beispiel f ein zweistelliges Funktionszeichen und
c ein Konstantensymbol, so hat der Term
f (f (v9 , c), v0 )
die Komplexität 2.
Lemma 2. (Induktion über die Komplexität der Terme)
Sei E eine Eigenschaft und sei E( t ) die Aussage
“der Term t erfüllt die Eigenschaft E”.
Für n ∈ N sei A(n) die Aussage
“für alle Terme t der Komplexität ≤ n gilt E( t )”.
Gelten weiter
• A(0)
• für alle n ∈ N gilt: aus A(n) folgt A(n + 1)
Dann gilt A(n) für alle n ∈ N. Somit gilt E( t ) für alle Terme t .
Beweis. Vollständige Induktion über n.
3
Lemma 3. (Induktion über den Aufbau der Terme)
Sei E eine Eigenschaft und sei E( t ) die Aussage
“der Term t erfüllt die Eigenschaft E”.
Gelten
• E( v ) für alle freien Variablen v
• E( c ) für alle Konstantensymbole c
• ist f ein n-stelliges Funktionszeichen und gelte E( ti ) für alle 1 ≤ i ≤
n, so gilt auch E( f ( t1 , . . . , tn ) ).
Dann gilt E( t ) für alle Terme t .
Beweis. Rückführung auf Lemma 15 oder direkt.
Lemma 4. Für Terme s , t und eine freie Variable v ist t [ s / v ] ein Term.
Definition. Die Menge F der Formeln der Sprache L ist die kleinste Teilmenge von L∗ mit folgenden Eigenschaften:
i) ⊥ ist eine Formel
ii) ist R ein m-stelliges Relationszeichen und sind t1 , . . . , tm Terme, so ist
R( t1 , . . . , tm )
eine Formel
.
iii) sind s , t Terme, so ist ( s = t ) eine Formel
iv) sind σ , ψ Formeln, so sind
( σ ∧ ψ ),
(σ∨ψ)
und
(σ→ψ)
Formeln
v) ist ψ eine Formel, v eine freie Variable und x eine gebundene Variable,
die nicht in ψ vorkommt, so sind auch
(∃x ψ [ x / v ] )
und
(∀x ψ [ x / v ] )
Formeln
.
Formeln der Form ⊥ , R( t1 , . . . , tm ) oder ( s = t ) heißen Primformeln
oder atomare Formeln.
4
Die Komplexität einer Formel ϕ ist die Anzahl der Vorkommen der Zeichen
∧ , ∨ , → , ∀ , ∃ in ϕ . Ist zum Beispiel f ein zweistelliges Funktionszeichen
und c ein Konstantensymbol, so hat die Formel
.
.
∃z∃x∀y (f (f (x, y), v) = x → f (z, y) = f (c, x))
die Komplexität 4.
Lemma 5. (Induktion über die Komplexität der Formeln)
Sei E eine Eigenschaft und sei E( ϕ ) die Aussage
“die Formel ϕ erfüllt die Eigenschaft E”.
Für n ∈ N sei A(n) die Aussage
“für alle Formeln ϕ der Komplexität ≤ n gilt E( ϕ )”.
Gelten weiter
• A(0)
• aus A(n) folgt A(n + 1), für alle n ∈ N.
Dann gilt A(n) für alle n ∈ N. Somit gilt auch E( ϕ ) für alle Formeln ϕ .
Beweis. Vollstängige Induktion über n.
Lemma 6. (Induktion über den Aufbau der Formeln)
Sei E eine Eigenschaft und sei E( ϕ ) die Aussage
“die Formel ϕ erfüllt die Eigenschaft E”.
Gelte
• E( ϕ ) für die Primformeln ϕ
• aus E( σ ) und E( ψ ) folgt E( ( σ ∧ ψ ) ) (genauso für ∨ und → )
• aus E( ψ) folgt E( (∃x ψ [ x / v ] ) ) (genauso für ∀ )
Dann gilt E( ϕ ) für alle Formeln ϕ .
Beweis. Rückführung auf Lemma 5 oder direkt.
Lemma 7. Sei ϕ eine Formel, t ein Term und v eine freie Variable. Dann
ist ϕ [ t / v ] wieder eine Formel.
5
Wir schreiben oft ( ¬ ϕ ) für ( ϕ → ⊥) und ( σ ↔ ψ ) für
(( σ → ψ ) ∧ ( ψ → σ )) .
Wir lassen oft Klammern weg. Dabei verwenden wir die Regel, dass ¬ und
die Quantore stärker binden als ∧ , ∨ und dass ∧ , ∨ stärker binden als → .
Wir können anstatt
(((∃x ψ [ x / v ] ) ∧ ϕ ) → ( σ ∨ ψ ))
also auch
∃x ψ [ x / v ] ∧ ϕ → σ ∨ ψ
schreiben.
6
2
Herleitungen
Definition. Für eine Formel ϕ und eine Formelmenge ∆ sei
H (D, ϕ, ∆)
eine Abkürzung für
“D ist eine Herleitung von ϕ mit Annahmenmenge ∆”.
Zunächst definieren wir diesen Begriff induktiv.
Danach setzen wir:
def
Σ`ϕ ⇔
es gibt eine Herleitung D von ϕ mit Annahmemenge ∆ ⊆ Σ
Sprechweise: “ϕ ist aus Σ herleitbar”, “D ist eine Zeuge für Σ ` ϕ”
Weiter setzen wir
def
` ϕ ⇔ ∅ ` ϕ.
In diesem Fall sagen wir: ϕ ist ein Theorem
ax: H (ϕ, ϕ, {ϕ})
∧-einf: H (D, σ, ∆) und H (D0 , ψ, ∆0 ) ⇒
D D0
0
H
, σ ∧ ψ, ∆ ∪ ∆
σ∧ψ
∧-elim: H (D, σ ∧ ψ, ∆) ⇒
D
D
, σ, ∆ und H
, ψ, ∆
H
σ
ψ
→-einf: H (D, ψ, ∆) ⇒
H
D
, σ → ψ, ∆ \ {σ}
σ→ψ
→-elim: H (D, ψ, ∆) und H (D0 , ψ → ϕ, ∆0 ) ⇒
D D0
0
, ϕ, ∆ ∪ ∆
H
ϕ
7
∀-einf: H (D, ψ, ∆) ⇒
H
D
, ∀x ψ [x/v] , ∆
∀x ψ [x/v]
Variablenbedingung:
def
v∈
/ FV(∆) = {v | es gibt ein σ ∈ ∆, so dass v in σ vorkommt }
∀-elim: H (D, ∀x ϕ [x/v] , ∆)
⇒
H
D
, ϕ [t/v] , ∆
ϕ [t/v]
∨-einf: H (D, σ, ∆) oder H (D, ψ, ∆) ⇒
D
H
, σ ∨ ψ, ∆
σ∨ψ
∨-elim:
H (D, σ ∨ ψ, ∆) und
H (D0 , ϕ, ∆0 ∪ {σ}) und
H (D00 , ϕ, ∆00 ∪ {ψ})
⇒
D D0 D00
0
00
H
, ϕ, ∆ ∪ ∆ ∪ ∆
ϕ
∃-einf: H (D, ψ, ∆) ⇒
H
D
, ∃x ψ [x/v] , ∆
∃x ψ [x/v]
∃-elim: H (D, ∃x ψ [x/v] , ∆) und H (D0 , ϕ, ∆0 ∪ {ψ}) ⇒
D D0
0
H
, ϕ, ∆ ∪ ∆
ϕ
Variablenbedingung: v ∈
/ FV(∆0 ∪ {ϕ})
⊥: H (D, ⊥, ∆) ⇒
H
D
, ϕ, ∆ \ {¬ϕ}
ϕ
8
.
.
.
=1 : H (t = t, t = t, ∅)
.
.
=2 : H (D, s = t, ∆) ⇒
D
.
H
. , t = s, ∆
t=s
.
.
.
=3 : H (D, r = s, ∆) und H (D0 , s = t, ∆0 ) ⇒
D D0
.
0
H
. , r = t, ∆ ∪ ∆
r=t
.
.
=4 : H (D, s = t, ∆) ⇒
H
D
.
, r [s/v] = r [t/v] , ∆
.
r [s/v] = r [t/v]
.
.
=5 : H (D, s = t, ∆) und H (D0 , ϕ [s/v] , ∆0 ) ⇒
D D0
0
H
, ϕ [t/v] , ∆ ∪ ∆
ϕ [t/v]
In den folgenden Lemmas ist eine Aussage der Art
`σ∧ψ → ψ∧σ
ist so zu verstehe: für alle Formeln σ und ψ gilt
`σ∧ψ → ψ∧σ
Lemma 8 (Anwendungsbeispiele für →-elim, →-einf, ∧-elim, ∧-einf ).
a) ` (σ → ψ) ∧ (ψ → ϕ) → (σ → ϕ)
b) ` σ ∧ ψ → ψ ∧ σ
c) ` (σ → (ψ → ϕ)) ↔ ((σ ∧ ψ) → ϕ)
d) ` ϕ → ¬¬ϕ
e) ` ¬(ϕ ↔ ¬ϕ)
f ) ` (σ → ψ) → ((ψ → ϕ) → (σ → ϕ))
g) ` σ ∧ (ψ ∧ ϕ) ↔ (σ ∧ ψ) ∧ ϕ
Beweis. a)
σ
(σ → ψ) ∧ (ψ → ϕ)
(σ → ψ) ∧ (ψ → ϕ)
σ→ψ
ψ
ψ→ϕ
ϕ
σ→ϕ
(σ → ψ) ∧ (ψ → ϕ) → (σ → ϕ)
9
b)
σ∧ψ σ∧ψ
ψ
σ
ψ∧σ
σ∧ψ → ψ∧σ
c)
σ ψ
σ∧ψ
σ∧ψ →ϕ
ϕ
ψ→ϕ
σ → (ψ → ϕ)
(σ ∧ ψ → ϕ) → (σ → (ψ → ϕ))
d)
e)
ϕ ¬ϕ
⊥
¬¬ϕ
ϕ → ¬¬ϕ
ϕ ↔ ¬ϕ
ϕ ↔ ¬ϕ
ϕ ϕ → ¬ϕ ¬ϕ ¬ϕ → ϕ
ϕ
¬ϕ
ϕ
¬ϕ
⊥
⊥
¬ϕ
¬¬ϕ
⊥
¬(ϕ ↔ ¬ϕ)
Lemma 9 (Anwendungsbeispiele für ⊥).
a) ` ¬σ → (σ → ψ)
b) ` ϕ ↔ ¬¬ϕ
c) ` (σ → ψ) ↔ (¬ψ → ¬σ)
d) ` (ϕ → ψ) → ϕ) → ϕ (Peirce Formel)
Beweis. a)
¬σ
⊥
ψ
σ→ψ
¬σ → (σ → ψ)
σ
10
b)
¬ϕ ¬¬p
ϕ ¬p
⊥
⊥
¬¬ϕ
ϕ
ϕ → ¬¬ϕ ¬¬ϕ → ϕ
ϕ ↔ ¬¬ϕ
c)
σ→ψ
¬ψ ¬ψ → ¬σ
σ
¬σ
ψ
¬ψ
⊥
⊥
ψ
¬σ
¬ψ → ¬σ
σ→ψ
(σ → ψ) → (¬ψ → ¬σ) (¬ψ → ¬σ) → (σ → ψ)
(σ → ψ) ↔ (¬ψ → ¬σ)
σ
d)
ϕ ¬ϕ
⊥
ψ
ϕ → ψ (ϕ → ψ) → ϕ
ϕ
¬ϕ
⊥
ϕ
((ϕ → ψ) → ϕ) → ϕ
Lemma 10 (Anwendungsbeispiele für ∀-elim und ∀-einf ).
a) ` ∀x ϕ [x/v] → ϕ
b) ` ∀x ϕ [x/v] → ∀y ϕ [y/v]
c) ` ∀x (σ → ψ) [x/v] ↔ (σ → ∀x ψ [x/v])
(wobei v ∈
/ FV(σ))
d) ` ∀x (σ → ψ) [x/v] → (∀x σ [x/v] → ∀x ψ [x/v])
e) ` ∀x ϕ [x/v] → ∀x ¬¬ϕ [x/v]
f ) ` ¬∀x ¬¬ϕ [x/v] → ¬∀x ϕ [x/v]
g) ` ∀x ∀y ϕ [y/w] [x/v] ↔ ∀y ∀x ϕ [x/v] [y/w]
h) ` ∀x (σ ∧ ψ) [x/v] ↔ ∀x σ [x/v] ∧ ∀x ψ [x/v]
i) (¬∀x ϕ [x/v] → ψ) → ∀x (¬ϕ → ψ) [x/v]
(wobei v ∈
/ FV(σ))
Beweis. a)
∀x ϕ [x/v]
ϕ
∀x ϕ [x/v] → ϕ
11
b)
∀x ϕ [x/v]
ϕ
∀y ϕ [y/v]
∀x ϕ [x/v] → ∀y ϕ [y/v]
c)
∀x (σ → ψ) [x/v]
σ
σ→ψ
ψ
∀x ψ [x/v]
σ → ∀x ψ [x/v]
∀x (σ → ψ) [x/v] → (σ → ∀x ψ [x/v])
σ → ∀x ψ [x/v]
∀x ψ [x/v]
ψ
σ→ψ
∀x (σ → ψ) [x/v]
(σ → ∀x ψ [x/v]) → ∀x (σ → ψ) [x/v]
σ
d)
∀x σ [x/v] ∀x (σ → ψ) [x/v]
σ
σ→ψ
ψ
∀x ψ [x/v]
∀x σ [x/v] → ∀x ψ [x/v]
∀x (σ → ψ) [x/v] → (∀x σ [x/v] → ∀x ψ [x/v])
i) Hausaufgabe
Lemma 11 (Anwendungsbeispiele für ∨-elim und ∨-einf ).
a) ` ((σ → ϕ) ∧ (ψ → ϕ)) ↔ ((σ ∨ ψ) → ϕ)
b) ` ψ ∨ ¬ψ
c) ` ¬(σ ∧ ψ) → ¬σ ∨ ¬ψ
d) ` (σ → ψ) ∨ (ψ → σ)
e) ` (σ ∧ ψ) ↔ ¬(¬σ ∨ ¬ψ)
f ) ` σ ∨ ψ ↔ (¬σ → ψ)
g) ` (σ ∨ ψ) ∧ (σ → ϕ) ∧ (ψ → ϕ) → ϕ
12
h)
i)
j)
k)
` σ ∨ ψ ↔ ¬ (¬σ ∧ ¬ψ)
` ¬(σ ∨ ψ) ↔ ¬σ ∧ ¬ψ
` σ ∨ (ψ ∨ ϕ) ↔ (σ ∨ ψ) ∨ ϕ
` (ϕ ∧ ψ) ∨ σ) ↔ (ϕ ∨ σ) ∧ (ψ ∨ σ)
Beweis.
a)
b) Hausaufgabe
c)
¬σ
¬σ ∨ ¬ψ
¬ψ
¬(¬σ ∨ ¬ψ) ¬σ ∨ ¬ψ ¬(¬σ ∨ ¬ψ)
⊥
⊥
σ
ψ
σ∧ψ
¬(σ ∧ ψ)
⊥
¬σ ∨ ¬ψ
¬(σ ∧ ψ) → ¬σ ∨ ¬ψ
d)
¬σ
σ
ψ→σ
σ→ψ
(σ → ψ) ∨ (ψ → σ) (σ → ψ) ∨ (ψ → σ)
(σ → ψ) ∨ (ψ → σ)
σ ∨ ¬σ
e) Hausaufgabe
f)
σ
¬σ
¬σ
⊥
ψ
¬σ → ψ
ψ
σ∨ψ
σ
σ∨ψ
ψ σ ∨ ¬σ σ ∨ ψ
ψ
σ∨ψ
σ ∨ ψ → (¬σ → ψ)
(¬σ → ψ) → σ ∨ ψ
σ ∨ ψ ↔ (¬σ → ψ)
g)
¬σ ∧ ¬ψ
¬σ ∧ ¬ψ
ψ
¬ψ
σ
¬σ
σ∨ψ
⊥
⊥
⊥
¬ (¬σ ∧ ¬ψ)
σ ∨ ψ → ¬ (¬σ ∧ ¬ψ)
13
¬(σ ∨ ψ)
¬(σ ∨ ψ)
¬σ
¬ψ
¬σ ∧ ¬ψ
¬ (¬σ ∧ ¬ψ)
⊥
σ∨ψ
¬ (¬σ ∧ ¬ψ) → σ ∨ ψ
h)
i)
j)
ψ
σ
∨
ψ
ϕ
σ
ψ ∨ ϕ (σ ∨ ψ) ∨ ϕ (σ ∨ ψ) ∨ ϕ
σ∨ψ
(σ ∨ ψ) ∨ ϕ
σ ∨ (ψ ∨ ϕ) (σ ∨ ψ) ∨ ϕ
(σ ∨ ψ) ∨ ϕ
σ ∨ (ψ ∨ ϕ) → (σ ∨ ψ) ∨ ϕ
k)
ϕ∧ψ
ψ
σ
(ϕ
∧
ψ)
∨
σ
ψ
∨σ
ϕ∨σ
ψ∨σ
(ϕ ∨ σ) ∧ (ψ ∨ σ)
(ϕ ∧ ψ) ∨ σ → (ϕ ∨ σ) ∧ (ψ ∨ σ)
ϕ∧ψ
ϕ
(ϕ ∧ ψ) ∨ σ ϕ ∨ σ
ϕ∨σ
σ
ψ∨σ
ϕ ψ
(ϕ ∨ σ) ∧ (ψ ∨ σ)
ϕ∧ψ
σ
ψ
∨
σ
(ϕ
∧
ψ)
∨
σ
(ϕ
∧
ψ)
∨σ
(ϕ ∨ σ) ∧ (ψ ∨ σ)
ϕ∨σ
(ϕ ∧ ψ) ∨ σ
(ϕ ∧ ψ) ∨ σ
(ϕ ∨ σ) ∧ (ψ ∨ σ) → (ϕ ∧ ψ) ∨ σ
Lemma 12 (Anwendungsbeispiele für ∃-elim und ∃-einf ).
14
σ
(ϕ ∧ ψ) ∨ σ
a)
b)
c)
d)
e)
f)
g)
` ∃x ψ [x/v] ↔ ¬ ∀x ¬ψ [x/v]
` ∃x ψ [x/v] ∨ ∀x ¬ψ [x/v]
` ¬∃x ψ [x/v] → ∀x ¬ψ [x/v]
` ∃x ψ [x/v] → ∃x (σ → ψ) [x/v]
` (σ → ∃x ψ [x/v]) ↔ ∃x (σ → ψ) [x/v]
` (∃x σ [x/v] → ψ) ↔ ∀x (σ → ψ) [x/v] (wobei v ∈
/ FV(ψ))
Sei P ein einstelliges Relationszeichen. Dann gilt
` ∃x ∀y (P (y) → P (x)) .
Beweis.
a) Hausaufgabe
b) mit a) und Lemma 11b)
c)
ψ
∃x ψ [x/v] ¬∃x ψ [x/v]
⊥
¬ψ
∀x ¬ψ [x/v]
¬∃x ψ [x/v] → ∀x ¬ψ [x/v]
Lemma 13.
.
a) ` ∃x (t = x)
.
.
.
b) ` ∀x, y, z (x =
6 y→x=
6 z∨y =
6 z)
.
.
.
c) ` s1 = t1 ∧ . . . ∧ sn = tn → f (s1 , . . . , sn ) = f (t1 , . . . , tn )
.
.
d) ` s1 = t1 ∧ . . . ∧ sm = tm → (R(s1 , . . . , sm ) ↔ R(t1 , . . . , tm ))
Beweis. a)
.
.
.
6 x)
¬∃x (t = x) ¬∃x (t = x) → ∀x (t =
.
∀x (t =
6 x)
.
.
t=
6 t
t=t
⊥
.
∃x (t = x)
15
b)
.
v=
6 w
.
.
u=
6 w∨v =
6 w
.
u 6= w
.
.
u 6= w ∨ v =
6 w
.
.
¬(u 6= w ∨ v =
6 w)
.
v 6= w
⊥
.
¬(u 6= w)
.
u 6= w
.
.
¬(u 6= w ∨ v =
6 w)
⊥
.
¬(v =
6 w)
⊥
.
v=w
.
w=v
⊥
.
u=w
.
u=v
.
u 6= v
⊥
.
.
u 6= w ∨ v =
6 w
.
.
.
u=
6 v→u=
6 w∨v =
6 w
.
.
.
∀z (u 6= v → u =
6 z∨v =
6 z)
.
.
.
∀y ∀z (u =
6 y→u=
6 z∨y =
6 z)
.
.
.
∀x ∀y ∀z (x =
6 y→x=
6 z∨y =
6 z)
.
v=w
.
.
u=w w=v
.
.
u=v
u=
6 v
⊥
.
.
v=
6 w
u=
6 w
.
.
.
.
.
.
u=w∨u=
6 w
u=
6 w∨v =
6 w
u=
6 w∨v =
6 w
.
.
u=
6 w∨v =
6 w
.
.
.
u 6= v → u =
6 w∨v =
6 w)
.
.
.
∀z (u =
6 v→u=
6 z∨v =
6 z)
.
.
.
∀y ∀z (u =
6 y→u=
6 z∨y =
6 z)
.
.
.
∀x ∀y ∀z (x =
6 y→x=
6 z∨y =
6 z)
Lemma 14.
a) Σ ∪ {σ} ` ψ ⇔ Σ ` σ → ψ
b) {ϕ1 , . . . , ϕn } ` ϕ ⇔ ` ϕ1 ∧ . . . ∧ ϕn → ϕ
Beweis.
a) “⇒” Es gebe eine Herleitung von ψ mit Annahmemenge ∆ ⊆ Σ ∪ {σ}.
Nach der Regel →-einf gibt es damit eine Herleitung von σ → ψ mit
Annahmemenge ∆ \ {σ}. Aus ∆ \ {σ} ⊆ Σ folgt Σ ` σ → ψ.
“⇐” Dies folgt unmittelbar mit der Regel →-elim.
b) Die Aussage folgt aus a) und Lemma 8c).
16
Bemerkung 1. Gilt H (D, ϕ, ∆), so sind ϕ und ∆ eindeutig durch den ‘Herleitungsbaum’ D bestimmt. Die Menge ∆ ist immer endlich.
Definition. Für eine Herleitung D sei die Komplexität von D definiert als
die Anzahl der ‘Balken’ in D.
Zum Beispiel hat die Herleitung
(σ → ϕ) ∧ (ψ → ϕ)
(σ → ϕ) ∧ (ψ → ϕ)
σ
σ→ϕ
ψ
ψ→ϕ
σ∨ψ
ϕ
ϕ
ϕ
(σ ∨ ψ) → ϕ
((σ → ϕ) ∧ (ψ → ϕ)) → ((σ ∨ ψ) → ϕ)
die Komplexität 7.
Lemma 15. (Induktion über die Komplexität der Herleitungen)
Sei E eine Eigenschaft und sei E(D) die Aussage
“die Herleitung D erfüllt die Eigenschaft E”.
Für n ∈ N sei A(n) die Aussage
“für alle Herleitungen D der Komplexität ≤ n gilt E(D)”.
Gelten weiter
• A(0)
• für alle n ∈ N gilt: aus A(n) folgt A(n + 1)
Dann gilt A(n) für alle n ∈ N. Somit gilt E(D) für alle Herleitungen D.
Bemerkung: Ein alternativer Ansatz bestünde darin, die Formeln ohne die
Zeichen ∨ und ∃ zu definieren und die Abkürzungen
def
σ ∨ ψ = ¬(¬σ ∧ ¬ψ)
und
def
∃x ψ [x/v] = ¬∀x ¬ψ [x/v]
17
zu verwenden. Und bei der Definition der Herleitungen auf die Regeln ∨-einf,
∨-elim, ∃-einf, ∃-elim zu verzichten. Dieser Ansatz führt zum selben Herleitungsbegriff! Wir deuten als Beispiel an, wie die ∃-elim Regel ‘hergeleitet’
werden kann.
ϕ ¬ϕ
⊥
¬ψ
¬∀x ¬ψ [x/v] ∀x ¬ψ [x/v]
⊥
ϕ
Dieser alternative Ansatz wäre weniger aufwändig gewesen. Warum haben
wir ihn nicht gewählt?
Erstens ist es gut, die üblichen Junktoren und Quantoren ausführlich und
gleichberechtigt zu behandeln.
Zweitens wollen wir auch über intuitionistische Logik sowie über Minimallogik reden.
18
3
Intuituionistische Logik und Minimallogik
Definition. “ϕ ist intuitionistisch aus Σ herleitbar”,
def
Σ `i ϕ ⇔
es gibt eine Herleitung von ϕ mit Annahmemenge ∆ ⊆ Σ, wobei die ⊥-Regel
ersetzt wird durch
D
, ϕ, ∆ .
int-⊥: H (D, ⊥, ∆) ⇒ H
ϕ
“ϕ ist minimallogisch aus Σ herleitbar”,
def
Σ `m ϕ ⇔
es gibt eine Herleitung von ϕ mit Annahmenmenge ∆ ⊆ Σ, ganz ohne Verwendung der ⊥-Regel.
Lemma 16.
a) `m ¬ϕ ↔ ¬¬¬ϕ
b) `m σ ∧ ¬ψ → ¬(σ → ψ)
c) `m (σ → ψ) → (¬ψ → ¬σ)
d) `m (σ → ψ) → (¬¬σ → ¬¬ψ)
e) `m ¬¬(σ → ψ) → (¬¬σ → ¬¬ψ)
f ) `i (¬¬σ → ¬¬ψ) → ¬¬(σ → ψ)
g) `m ¬¬(σ ∧ ψ) ↔ (¬¬σ ∧ ¬¬ψ)
h) `m ¬¬∀x ψ [x/v] → ∀x ¬¬ψ [x/v]
i) `m (σ ∧ ψ → ϕ) → (¬¬σ ∧ ψ → ¬¬ϕ)
j) `m (σ ∧ ψ → ϕ) → (¬¬σ ∧ ¬¬ψ → ¬¬ϕ)
k) `m (¬(σ ∨ ψ) → ϕ) → (((¬σ → ϕ) ∨ (¬ψ → ϕ) → ϕ) → ϕ)
Definition. Die Abbildung
◦
: F → F sei definiert durch
1. ⊥◦ = ⊥
2. ϕ◦ = ¬¬ϕ für Primformeln verschieden von ⊥
3. (σ ∧ ψ)◦ = σ ◦ ∧ ψ ◦
4. (σ ∨ ψ)◦ = ¬(¬σ ◦ ∧ ¬ψ ◦ )
5. (σ → ψ)◦ = σ ◦ → ψ ◦
6. (∀x ψ [x/v])◦ = ∀x ψ ◦ [x/v]
19
7. (∃x ψ [x/v])◦ = ¬∀x ¬ψ ◦ [x/v]
Diese Abbildung nennt man Gödel-Übersetzung.
Wir legen fest:
menge ∆ sei
◦
bindet stärker als ¬ und die Quantoren. Für eine Formel∆◦ = {ψ ◦ | ψ ∈ ∆} .
Lemma 17. Für alle Formeln ϕ gilt
`m ¬¬ϕ◦ ↔ ϕ◦ .
Lemma 18. Für alle Formeln ϕ gilt
ϕ [t/v]◦ = ϕ◦ [t/v] .
Lemma 19. Für alle Formeln ϕ gilt
` ϕ ↔ ϕ◦ .
Proposition 1.
Γ`ϕ ⇔
20
Γ◦ `i ϕ◦
© Copyright 2024 ExpyDoc
