Hoofdstuk 9: Predikaatlogica: semantische tableaus

Hoofdstuk 9: Predikaatlogica: semantische
tableaus
L. Storme
Toepassingsgerichte formele logica II
academiejaar 2006-2007
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Semantische tableaus
I
Ook in predikaatlogica worden semantische tableaus gebruikt
om geldigheid van een gevolgtrekking te testen.
I
Hoofdidee tableau: systematisch zoeken naar tegenvoorbeeld
voor ϕ1 , . . . , ϕn ◦ ψ.
I
Gesloten tableau: geen tegenvoorbeeld, en dan geldt:
ϕ1 , . . . , ϕn |= ψ.
I
Open tableau: wel een tegenvoorbeeld, en dan geldt:
ϕ1 , . . . , ϕn 6|= ψ.
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Tegenvoorbeeld in propositie- en predikaatlogica
I
Tegenvoorbeeld in propositielogica = waardering die
ϕ1 , . . . , ϕn waar maakt en ψ onwaar.
I
Tegenvoorbeeld in predikaatlogica = predikaatlogisch model
M plus bedeling b die ϕ1 , . . . , ϕn waar maakt en ψ onwaar
(uit definitie M, b |= ψ).
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Extra benodigheden in tableaumethode
I
Reductieregels voor kwantoren ∀ en ∃.
I
Gaandeweg construeren van domein D.
I
Bijhouden van interpretatiefunctie I en bedeling b.
Beperkingen op taal:
I
taal zonder functieletters,
I
gevolgtrekkingen zonder individuele constanten en zonder vrije
variabelen.
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Voorbeeld 9.1
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Vervolg voorbeeld 9.1
Tableau is gesloten!
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Reductieregels
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Reductieregels 2
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
∀L blijft actief
Belangrijke opmerking:
I
in
Φ, ∀x ϕ ◦ Ψ,
bij uitbreiden van domein D in tableaumethode met nieuw
object dk+1 moet ϕ ook waar zijn voor nieuw object dk+1 !
I
Universele kwantor links is nooit uitgewerkt!
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Voorbeeld 9.2
ϕ = Ax → ∀yBy
Dit tableau sluit.
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
∃R blijft actief
Belangrijke opmerking:
I
in
Φ ◦ ∃x ϕ, Ψ,
bij uitbreiden van domein D in tableaumethode met nieuw
object dk+1 moet ϕ ook vals zijn voor nieuw object dk+1 !
I
Existenti¨ele kwantor rechts is nooit uitgewerkt!
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Voorbeeld 9.4
ϕ1 = Ax ∧ Bx en ϕ2 = Bx ∧ Cx
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Voorbeeld 9.4: betekenis * en **
* :
(1) D = {d1 }
(2) ∃ϕ1 : {d1 }
** :
(1) D = {d1 }
(2) ∃ϕ1 : {d1 }
∃ϕ2 : {d1 }
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Voorbeeld 9.5
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Voorbeeld 9.6
Oneindig voortlopende tak in tableau geeft tegenvoorbeeld!
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Probeerregels ∃∗L en ∀∗R
I
Poging om eindig tegenvoorbeeld te vinden.
I
Voorbeeld: Φ ◦ ∀x ϕ, Ψ.
Om tegenvoorbeeld te vinden,
I
I
I
I
I
niet meteen nieuw object invoeren.
Kijk of [d1 /x]ϕ tegenvoorbeeld geeft, en stop als dit het geval
is.
Indien niet, probeer [d2 /x]ϕ.
Pas als volledige domein D gecontroleerd is, voer nieuw object
in D in.
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Opmerkingen probeerregels
I
Probeerregels gebruiken bij ∀R en/of ∃L .
I
Probeerregels nuttig bij eindige tegenvoorbeelden.
I
Bestaan er geen eindige tegenvoorbeelden, dan bij sluiten van
tableau waarin probeerregels toegepast zijn, kan geen
algemene conclusie getrokken worden over de geldigheid van
de corresponderende gevolgtrekking (sequent).
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Semantisch tableau in predikaatlogica
Semantisch tableau in predikaatlogica: twee mogelijkheden.
I
I
Tableau sluit. Dan tableau eindig en gevolgtrekking geldig.
Er is een niet-sluitende tak. Deze kan:
I
I
eindig afbreken, of
oneindig doorlopen.
In beide gevallen: tegenvoorbeeld, gevolgtrekking niet geldig.
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Onbeslisbaarheid van de predikaatlogica
I
Essentieel verschil tussen propositielogica en predikaatlogica.
I
I
Propositielogica is beslisbaar.
Predikaatlogica is onbeslisbaar. (Stelling van Church (1936))
I
Onbeslisbaarheid bij predikaatlogica: bijvoorbeeld als in
tableaumethode niet bepaald kan worden of een oneindige tak
in wording is.
I
Sommige fragmenten van predikaatlogica wel beslisbaar:
bijvoorbeeld de monadische predikaatlogica.
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus
Adequaatheid van de predikaatlogica
I
Predikaatlogica is niet beslisbaar: geen algoritme om te
bepalen voor iedere willekeurige formule of deze geldig is of
niet.
I
Tableaumethode wel adequaat:
Sequent in predikaatlogica heeft gesloten tableau als en
slechts als corresponderende gevolgtrekking geldig is.
I
Voor een open tableau vind je enkel een tegenvoorbeeld als je
zorgt voor fair scheduling van de reductieregels.
L. Storme
Hoofdstuk 9: Predikaatlogica: semantische tableaus

Download Report