2.6 Natürliches Schließen in AL

2.6 Natürliches Schließen in AL
Bisher wurde bei der Überprüfung der Gültigkeit von Schlüssen oder
Schlussschemata insofern ein semantisches Herangehen verfolgt, als wir auf die
Bewertung von Formeln mit Wahrheitswerten zurückgegriffen haben.
Eine andere Möglichkeit besteht in einem syntaktischen Herangehen:
Ein Schlussschema φ1 ,..., φn / ψ ist AL-gültig gdw es eine Ableitung von ψ aus
φ1,..., φn in AL gibt.
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
1
Eine Ableitung ist ein rein syntaktisches Verfahren des Operierens mit
Ausdrücken.
Dabei wird nur auf die Gestalt von Formeln Bezug genommen; insbesondere
bleiben die Wahrheitswerte von Formeln unberücksichtigt.
D2.9 Ableitung
Eine Ableitung von ψ aus φ1,..., φn ist eine endliche Folge von Formeln, wobei
die letzte dieser Formeln ψ ist und für jede Formel der Folge gilt: Entweder ist die
jeweilige Formel eine der Annahmen (Voraussetzungen) φ1,..., φn oder aus
vorhergehenden Formeln mit Hilfe von Ableitungsregeln gewonnen.
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
2
D2.10 AL-Ableitbarkeit
Aus φ1,..., φn ist ψ AL-ableitbar gdw es eine Ableitung von ψ aus φ1,..., φn in AL
gibt.
Notation: φ1,..., φn ⊢AL ψ
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
3
D2.11 AL-Beweisbarkeit (AL-Theorem, AL-Gesetz)
Eine Formel ψ ist AL-beweisbar (ein AL-Theorem, AL-Gesetz) gdw es eine
Ableitung von ψ aus der leeren Menge von Annahmen in AL gibt.
Notation: ⊢AL ψ
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
4
Metatheoreme über AL
φ1,..., φn ⊨AL ψ gdw φ1,..., φn ⊢AL ψ
⊨AL ψ gdw ⊢AL ψ
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
5
Zwei Typen von Deduktionssystemen
• Axiomatische Systeme:
Axiome + Ableitungs-(Deduktions-)regeln
• Systeme des natürlichen Schließens:
Ableitungs-(Deduktions-)regeln
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
6
Ein System des natürlichen Schließens für AL
Struktur einer Ableitung im SNSAL
Ableitung von ψ aus Annahmen φ1,..., φn :
φ1
φ2
...
⋮
φn
n.
n + 1. ...
...
⋮
ψ
k.
1.
2.





 Annahmen





|} Anwendung von Ableitungsregeln
Konklusion
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
7
Zwei Typen von Ableitungsregeln im SNSAL
• Einführungsregeln für Konnektoren (E)
• Beseitigungsregeln für Konnektoren (B)
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
8
Konjunktion
E∧
m1 .
m2 .
n.
χ1
χ2
χ1 ∧ χ2
E ∧ m1 , m2
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
9
Konjunktion
m.
n.
χ1 ∧ χ2
χ1
B∧ m
B ∧ (ii) m .
n.
χ1 ∧ χ2
χ2
B∧ m
B ∧ (i)
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
10
Beispiel:
p ∧q ⊢ q ∧ p
1.
2.
3.
4.
p ∧q
p
q
q∧p
Annahme
B∧ 1
B∧ 1
E ∧ 3, 2
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
11
Disjunktion
E ∨ (i)
E ∨ (ii)
m.
n.
χ1
χ1 ∨ χ2
E∨ m
m.
n.
χ2
χ1 ∨ χ2
E∨ m
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
12
Disjunktion
B ∨ (i)
B ∨ (ii)
m1 .
m2 .
n.
χ1 ∨ χ2
¬χ2
χ1
B ∨ m1 , m2
m1 .
m2 .
n.
χ1 ∨ χ2
¬χ1
χ2
B ∨ m1 , m2
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
13
Beispiel:
p ∨ q, ¬q ⊢ p ∨ r
1.
2.
3.
4.
p ∨q
¬q
p
p ∨r
Annahme
Annahme
B ∨ 1, 2
E∨3
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
14
Materiale Implikation
E→
χ1
...
⋮
n − 1 . χ2
χ1 → χ2
n.
m.
zusätzliche Annahme (z.A.)
E → m , n −1
χ1 → χ2 gilt gdw χ2 aus χ1 abgeleitet werden kann.
Nur die Zeile n ist eine echte Zeile der Ableitung.
Die Zeilen m bis n − 1 sind eine eingeschobene Ableitung (‚Nebenrechnung’), sie
dienen allein als Beweis der Zeile n und dürfen in der weiteren Ableitung nicht
mehr verwendet werden.
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
15
Materiale Implikation
B→
m1 .
m2 .
n.
χ1 → χ2
χ1
χ2
B → m1 , m2
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
16
Beispiel:
p →q, q → r ⊢ p → r
1.
2.
3.
4.
5.
6.
p →q
q →r
p
q
r
p→r
Annahme
Annahme
z.A.
B → 1, 3
B → 2, 4
E → 3, 5
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
17
?
Zeige, dass r → p ∧ q aus r → p und r → q ableitbar ist.
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
18
Beispiel:
⊢ (p → q ) → (p → q ∨ r )
1.
2.
3.
4.
5.
6.
(p → q )
p
q
q ∨r
p →q ∨r
(p → q ) → (p → q ∨ r )
z.A.
z.A.
B → 1, 2
E∨ 3
E → 2, 4
E → 1, 5
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
19
?
Zeige, dass (p ∨ q ) → (¬q → p) beweisbar ist.
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
20
Materiale Äquivalenz
E↔
m1 .
m2 .
n.
χ1 → χ2
χ2 → χ1
χ1 ↔ χ2
E ↔ m1 , m2
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
21
Materiale Äquivalenz
B ↔ (i) m .
n.
χ1 ↔ χ2
χ1 → χ2
B↔ m
B ↔ (ii) m .
n.
χ1 ↔ χ2
χ2 → χ1
B↔ m
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
22
Negation
E¬
χ1
...
⋮
n − 1 . χ2 ∧ ¬χ2
¬χ1
n.
m.
z.A.
Widerspruch
E¬ m
Die Zeilen m bis n − 1 sind wieder nur ein eingeschobener Beweis für die n .
Zeile und dürfen in der weiteren Ableitung nicht mehr verwendet werden.
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
23
Negation
B¬
¬χ1
...
⋮
n − 1 . χ2 ∧ ¬χ2
χ1
n
m.
z.A.
Widerspruch
B¬ m
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
24
Beispiel:
p → q , ¬q ⊢ ¬p
1.
2.
3.
4.
5.
6.
p →q
¬q
p
q
q ∧ ¬q
¬p
Annahme
Annahme
z.A.
B → 1, 3
E ∧ 4, 2 Widerspruch
E¬ 3
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
25
Beispiel:
¬¬ p ⊢ p
1.
2.
3.
4.
¬¬ p
¬p
¬¬ p ∧ ¬ p
p
Annahme
z.A.
E ∧ 1, 2 Widerspruch
B¬ 2
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
26
?
Zeige, dass ¬¬ p aus q ∧ (q → p) ableitbar ist.
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
27
Ergänzungen zur Struktur einer Ableitung im SNSAL
• Bewiesene AL-Gesetze (AL-Theoreme) dürfen als neue Zeilen in eine
Ableitung eingefügt werden.
• Bewiesene AL-Äquivalenzen dürfen zur äquivalenten Ersetzung von Formeln
in einer Ableitung verwendet werden.
• Bewiesene AL-Schlussschemata dürfen in einer Ableitung verwendet werden.
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
28
Beispiel:
p → q ∨ r , ¬q ∧ ¬r ⊢ ¬p
1.
2.
3.
p →q ∨r
Annahme
¬q ∧ ¬r
Annahme
¬q ∧ ¬r ↔ ¬ (q ∨ r ) de Morgansches Gesetz
4.
¬q ∧ ¬r → ¬ (q ∨ r ) B ↔ 3
5.
¬ (q ∨ r )
6.
¬p
B → 4, 2
(oder äquivalente Ersetzung 2)
modus tollens (MT) 1, 5
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
29
?
Zeige, dass Hans nicht lacht oder Maria nicht lacht, wenn es nicht der Fall ist,
dass beide lachen.
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
30
Hans lacht nicht oder Maria lacht nicht, wenn es nicht der Fall ist, dass beide
lachen.
Symbolisierung:
¬(p ∧ q ) → ¬p ∨ ¬q
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
31
Einfachere Lösung:
¬(p ∧ q ) ⊢ ¬p ∨ ¬q
(Ableitung)
1. ¬(p ∧ q )
Annahme
2. ¬ (¬p ∨ ¬q )
z.A.
4. ¬ (¬p ∨ ¬q ) → p ∧ q Vor.:
ein bewiesenes
de Morgansches Gesetz
5. p ∧ q
B → 2, 4
E ∧ 5, 1 Wid.
6. p ∧ q ∧ ¬(p ∧ q )
B¬ 2
7. ¬p ∨ ¬q
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
32
Voraussetzung zur Ableitung:
⊢ ¬(¬p ∨¬q) → p ∧q
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
(de Morgansches Gesetz)
¬ (¬p ∨ ¬q )
¬p
¬p ∨ ¬q
(¬p ∨ ¬q ) ∧ ¬ (¬p ∨ ¬q )
p
¬q
¬p ∨ ¬q
(¬p ∨ ¬q ) ∧ ¬ (¬p ∨ ¬q )
q
p ∧q
¬(¬p ∨¬q) → p ∧q
z.A.
z.A.
E∨ 2
E ∧ 3, 1 Wid.
B¬ 2
z.A.
E∨ 6
E ∧ 7, 1 Wid.
B¬6
E ∧ 5, 9
E → 1, 10
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
33
Komplexere Lösung:
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.
15.
16.
17.
⊢ ¬(p ∧ q ) → ¬p ∨ ¬q
¬(p ∧ q )
¬ (¬p ∨ ¬q )
¬ (¬p ∨ ¬q )
¬p
¬p ∨ ¬q
(¬p ∨ ¬q ) ∧ ¬ (¬p ∨ ¬q )
p
¬q
¬p ∨ ¬q
(¬p ∨ ¬q ) ∧ ¬ (¬p ∨ ¬q )
q
p ∧q
¬(¬p ∨¬q) → p ∧q
p ∧q
p ∧ q ∧ ¬(p ∧ q )
¬p ∨ ¬q
¬(p ∧ q ) → ¬p ∨ ¬q
 Johannes Dölling: Logik für Linguisten. WiSe 2012/13
(Beweis)
z.A.
z.A.
z.A.
z.A.
E∨ 4
E ∧ 5, 3 Wid.
B¬ 4
z.A.
E∨ 8
E ∧ 9, 3 Wid.
B¬ 8
E ∧ 7, 11
E → 3, 12
B → 2, 13
E ∧ 14, 1 Wid.
B¬ 2
E → 1, 16
34