Lógica
Proposicional
Completude e
Corretude do Sistema
de Tableaux
Semânticos
Relembrando Corretude
e Completude...
Correto

Correto:


Toda sentença deduzida por SD
a partir de um dado conjunto de sentenças S



inclusive o conjunto vazio de sentenças!
Seja realmente dedutível a partir de S!
Se as premissas são válidas, a conclusão
também é válida!
Completo e Consistente

Completo:


Toda sentença realmente dedutível a partir
de S, seja também dedutível através de SD
Consistente:

Não seja possível gerar contradições
usando SD
Teorema da correção



Um sistema de dedução SD é correto se
satisfaz à condição abaixo
Se Γ├SD A, então Γ ⊨ A
SD só deduz fórmulas corretas!!
Teorema da completude



Um sistema de dedução SD é completo se
satisfaz às condições abaixo
Se Γ⊨ A, então Γ├SD A
Toda fórmula dedutível também é
dedutível por SD!!
Conjuntos Saturados

Um conjunto de fórmulas θ em que:

Se existe uma fórmula em θ do tipo α, então α1
e α2 também estão em θ


Se A é do tipo α e A ∈ θ  α1∈ θ e α2 ∈ θ
Se existe uma fórmula em θ do tipo β, então β1
ou β2 também estão em θ

Se A é do tipo β e A ∈ θ  β1∈ θ ou β2 ∈ θ
Conjuntos de Hintikka


ou Conjuntos Descendentemente Saturados
Um conjunto saturado de fórmulas θ em que:

Nenhuma fórmula e sua negação estão em θ

A ∈ θ  ¬A ∉ θ
Conjuntos de Hintikka


ou Conjuntos Descendentemente Saturados
Um conjunto de fórmulas θ em que:

Nenhuma fórmula e sua negação estão em θ


Se existe uma fórmula em θ do tipo α, então α1
e α2 também estão em θ


A ∈ θ  ¬A ∉ θ
Se α ∈ θ  α1∈ θ e α2 ∈ θ
Se existe uma fórmula em θ do tipo β, então β1
ou β2 também estão em θ

Se β ∈ θ  β1∈ θ ou β2 ∈ θ
Lema


Todo ramo saturado e aberto de um
tableaux é descendentemente saturado
Prova:

Se é aberto, satisfaz à 1ª condição


A ∈ θ  ¬A ∉ θ
Se é saturado satisfaz à 2ª condição
Lema



Θ (ainda não saturado) é satisfatível se
para toda fórmula sse para toda ψ∈θ,
existir uma interpretação I tal que
I[ψ]=T
Se θ é satisfatível, então θ U {α1,α2} é
satisfatível tb
Se θ é satisfatível, então θ U {β1} é
satisfatível ou θ U {β2} é satisfatível
Demonstração

Suponha que α∈θ e é da forma A^B.



Suponha que β∈θ e é da forma AvB.



Se θ é satisfatível, então existe I[θ]=T e
I[A^B]=T tb. Então I[A]=I[B]=T e
θ U {A,B} é satisfatível tb
Se θ é satisfatível, então existe I[θ]=T e
I[AvB]=T tb. Então I[A]=T ou I[B]=T e
θ U {A} ou θ U {B} é satisfatível
Provas análogas para AB e ¬A
Lema de Hintikka


Todo conjunto descendentemente
saturado é satisfatível
Prova

Se é descendentemente saturado então


A ∈ θ  ¬A ∉ θ
Se A e ¬A ∉ simultaneamente a θ e é
saturado então A é satisfatível (ramo
aberto) e há uma interpretação I[A]=T
Lema de Hintikka - Prova


Caso básico coberto (A ∈ θ  I[A]=T)
Indução sobre a complexidade de ψ∈θ

Caso α ∈ θ


 α1,α2 ∈ θ
Pela hipótese de indução I[α]=T então I[α1] =
I[α2]=T
Lema de Hintikka - Prova


Caso básico coberto (A ∈ θ  I[A]=T)
Indução sobre a complexidade de ψ∈θ


Caso α ∈ θ
Caso β ∈ θ



 β1∈ θ ou β2 ∈ θ
Pela hipótese de indução I[β]=T então I[β1]
=T ou I[β2]=T
Se I[β1] =T ou I[β2]=T  I[β]=T
Corretude dos Tableaux




Se Γ├TS A, então Γ ⊨ A
Prova pela contrapositiva
Supomos Γ ⊭ A e se chegarmos em
Γ⊬TS A, então está provado
Se Γ ⊭ A então existe uma
interpretação I tal que I[Γ]=T e I[A]=F
Corretude dos Tableaux (cont)




Seja Θ um conjunto de fórmulas ainda
não saturado e que θ├TS A mas por
absurdo θ ⊭ A
Neste caso, existe uma interpretação
I[θ]=T e I[A]=F
Se θ├TS A então I[θ]=T
Chamamos θi a expansão por tableaux
de θ em que foi aplicada apenas uma
regra
Corretude dos Tableaux (cont)


A cada passo de expansão por tableaux
de θ, haverá um ramo θi, em que foi
aplicada apenas uma regra
Se existe uma interpretação I[θ]=T,
nesta interpretação I[θi-1]=T
Corretude dos Tableaux (cont)

Então por lemas anteriores, se θi-1é
satisfatível e há uma expansão :


por α, então

θi= θi-1 U {α1,α2} é satisfatível tb

O ramo continua aberto!
por β, então

θi= θi-1 U {β1 ou β2} é satisfatível

Um dos ramos está aberto!
Corretude dos Tableaux (cont)



Sempre haverá um ramo aberto, que
após as expansões será um conjunto
descendentemente saturado, e que não
fecha
Portanto θ⊬TS A
Não pode haver tableau fechado
quando θ ⊭ A
Completude dos Tableaux






Se Γ ⊨ A então Γ├TS A
Prova pela contrapositiva
Supomos Γ ⊬TS A e se chegarmos em
Γ⊭ A, então está provado
Se Γ ⊬TS A então temos um ramo θ
saturado
Pelo lema de Hintikka, θ é satisfatível
Então existe uma interpretação I tal que
I[Γ]=T e I[A]=F e portanto Γ⊭ A