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 θ A ∈ θ ¬A ∉ θ

Se existe uma fórmula em θ do tipo α, então α1 e α2 também estão em θ

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.

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 Suponha que β∈θ e é da forma AvB.

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 AB 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