PDF downloaden

Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Hoofdstuk 3: Propositielogica: geldig gevolg
L. Storme
Toepassingsgerichte formele logica II
Academiejaar 2006-2007
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Geldig gevolg
I
Formule ψ is geldig gevolg van verzameling/rij formules Σ als
elk model van Σ ook model is van ψ.
I
Notatie: Σ |= ψ:
ψ is geldig gevolg van Σ; gevolgtrekking Σ/ψ is geldig.
I
p, p → q |= q
p, p → q, q → r |= r
I
|= ψ: ψ is een tautologie.
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Tautologie
I
Notatie: Σ 6|= ψ:
ψ is geen geldig gevolg van Σ; gevolgtrekking Σ/ψ is niet
geldig.
I
Tegenvoorbeeld van de gevolgtrekking Σ/ψ = model van Σ
dat geen model van ψ is.
I
q, p → q 6|= p
Tegenvoorbeeld: model V met V (q) = 1 en V (p) = 0
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Controleren geldig gevolg
I
Verschil tussen geldigheid en waarheid!
I
Controleren geldig gevolg: waarheidstabel
Is ¬q, p → q/¬p geldig?
V1
V2
V3
V4
p
1
1
0
0
q ¬q p → q ¬p
1 0
1
0
0 1
0
0
1 0
1
1
0 1
1
1
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Waarheidstabellen en semantische tableaus
I
Waarheidstabellen: exponentieel in het aantal proposities
I
Effici¨enter zoeken van tegenvoorbeelden met semantische
tableaus
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Semantische tableaus 1
Semantische tableaus:
I
I
sequent = rijtje van de vorm
ϕ1 , . . . , ϕn ◦ ψ1 , . . . , ψm
met ϕ1 , . . . , ψm formules, n ≥ 0, m ≥ 0.
Waardering V heet een tegenvoorbeeld van sequent
ϕ1 , . . . , ϕn ◦ ψ1 , . . . , ψm als
V (ϕ1 ) = · · · = V (ϕn ) = 1
en
V (ψ1 ) = · · · = V (ψm ) = 0.
I
Sequent ϕ1 , . . . , ϕn ◦ ψ1 , . . . , ψm heeft geen tegenvoorbeeld
als i en j bestaan zodat ϕi = ψj .
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Semantische tableaus 2
I
Semantisch tableau = schema waarin op systematische wijze
mogelijk bestaan van tegenvoorbeelden in een sequent
teruggebracht (gereduceerd) wordt tot dat van ´e´en of meer
overzichtelijker sequenten.
I
Om te bepalen of ϕ1 , . . . , ϕn /ψ een tegenvoorbeeld heeft,
maken we een semantisch tableau voor de sequent
ϕ1 , . . . , ϕn ◦ ψ.
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Tableauregels
ΦoΨ
ΦoΨ
Φ0 o Ψ0
Φ0 o Ψ0
Φ00 o Ψ00
I
Linkervorm betekent: Φ ◦ Ψ heeft een tegenvoorbeeld als en
slechts als Φ0 ◦ Ψ0 heeft een tegenvoorbeeld.
I
Rechtervorm betekent: Φ ◦ Ψ heeft een tegenvoorbeeld als en
slechts als Φ0 ◦ Ψ0 heeft een tegenvoorbeeld of Φ00 ◦ Ψ00 heeft
een tegenvoorbeeld.
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Reductieregels 1
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Reductieregels 2
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Voorbeeld redenering semantisch tableau
1. Heeft p ∨ q, ¬q/p een tegenvoorbeeld?
2. Heeft p ∨ q, ¬q ◦ p een tegenvoorbeeld?
3. als en slechts als: heeft p ∨ q ◦ p, q een tegenvoorbeeld?
4. als en slechts als: heeft p ◦ p, q tegenvoorbeeld of heeft
q ◦ p, q tegenvoorbeeld?
5. beide hebben geen tegenvoorbeeld, zijn gesloten.
6. dus p ∨ q, ¬q/p heeft geen tegenvoorbeeld,
7. dus p ∨ q, ¬q |= p.
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Voorbeeld semantisch tableau
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Conclusies voorbeeld
Is p → (q → r )/(p → q) → r geldig?
Drie tegenvoorbeelden
1. V1 (p) = V1 (q) = V1 (r ) = 0
2. V2 (q) = 1, V2 (p) = V2 (r ) = 0
3. V3 (p) = V3 (r ) = 0
Conclusie: p → (q → r )/(p → q) → r niet geldig:
p → (q → r ) 6|= (p → q) → r
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Gesloten en open tableau
I
Sequent is gesloten als en slechts als eenzelfde formule links
en rechts optreedt.
I
Tableau is gesloten als en slechts als al zijn takken gesloten
zijn.
I
Tableau is open als er minstens ´e´en tak niet gesloten kan
worden (hij is niet gesloten en er kunnen geen reductiestappen
meer toegepast worden op die tak).
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
(Semantisch) consistent
I
Formuleverzameling Σ is (semantisch) consistent als Σ een
model heeft (Σ vervulbaar)
I
Σ = {ϕ1 , . . . , ϕn } is consistent als ϕ1 , . . . , ϕn ◦ een
tegenvoorbeeld heeft
I
Σ = {ϕ1 , . . . , ϕn } is consistent als ϕ1 , . . . , ϕn ◦ een open
tableau heeft
I
Formuleverzameling zonder model heet inconsistent.
Corresponderend tableau is gesloten.
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Inconsistente formuleverzameling
Formuleverzameling Σ is inconsistent: afwezigheid van modellen
impliceert dat uit die verzameling iedere formule geldig volgt, dus
elke formule ϕ en zijn negatie ¬ϕ volgt geldig uit Σ.
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Tautologie testen met tableau
◦ϕ
Als deze sequent geen tegenvoorbeeld heeft, dan is ϕ waar in elk
model van de lege verzameling (staat links). Daar elke waardering
model is van lege verzameling, is elke waardering model van ϕ.
Dus ϕ is tautologie als en slechts als tableau van ◦ϕ sluit.
Voorbeeld: ◦¬(p ∧ ¬p)
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg
Geldig gevolg
Semantische tableaus
Consistentie
Adequaatheid
Adequaatheid
Adequaatheidsstelling:
Theorem
1. ϕ1 , . . . , ϕn |= ψ als en slechts als
2. er bestaat een gesloten semantisch tableau voor
ϕ1 , . . . , ϕn ◦ ψ als en slechts als
3. alle semantische tableaus voor ϕ1 , . . . , ϕn ◦ ψ zijn gesloten.
Bewijs.
Hoofdstuk 5
L. Storme
Hoofdstuk 3: Propositielogica: geldig gevolg

Download Report