sl-cap2-8-3-4p

Prévia do material em texto

✬ ✩
2.8.3 SISTEMAS DEDUTIVOS DO TIPO GENTZEN
Newton José Vieira
UFMG
18 de setembro de 2008
✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Voltando à “regra” i→
A regra i→ não satisfaz a definição de regra de derivação vista no Caṕıtulo 1:
A conclusão depende da existência de uma subdedução a partir de uma
suposição.
Como obter um sistema formal em que haja uma regra correspondente a i→?
Seria a correspondente formal da “regra”:
Γ ∪ {α} |= β
Γ |= α→β
A idéia: “enriquecer” a linguagem com o śımbolo ⊢ (|= é promovido da
metalinguagem para a linguagem básica).
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
A linguagem do sistema formal
O conjunto de sequentes, S, é o das palavras da forma Ψ1⊢Ψ2 em que Ψ1 e Ψ2 são
sequências de fórmulas separadas por v́ırgulas.
• c(Ψ): conjunto das fórmulas em Ψ.
• Um sequente Ψ1⊢Ψ2 é interpretado no presente contexto como dizendo:
toda interpretação que satisfaz todas as fórmulas de c(Ψ1)
satisfaz alguma fórmula de c(Ψ2)
ou ainda,
conjunção das fórmulas de Ψ1 |= disjunção das fórmulas de Ψ2.
Sequência vazia no lado esquerdo: equivale a ⊤; no lado direito: equivale a ⊥.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Exemplos de sequentes e seus significados
• ⊢: diz que ∅ |= ⊥, ou seja, que ⊥ é tautológica (um absurdo);
• ⊢ p: diz que p é tautológica (o que não é verdade, evidentemente);
• ⊢ p → p,¬p: diz que (p → p) ∨ ¬p é tautológica;
• p ⊢: diz que p é contraditória;
• p → p,¬p ⊢: diz que (p → p) ∧ ¬p é contraditória;
• p → q, p ⊢ q: diz que {p → q, p} |= q;
• p → q, p,¬q ⊢ q, r: diz que {p → q, p,¬q} |= q ∨ r.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Sequentes válidos
Objetivos do sistema formal:
• derivar apenas sequentes válidos (correção); e
• derivar todos os sequentes válidos (completude).
Um sequente Ψ1 ⊢ Ψ2 é válido se, e somente se, toda interpretação que satisfaz
c(Ψ1), também satisfaz alguma fórmula de c(Ψ2).
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Exemplos de sequentes válidos e não válidos
• ⊢ não é válido: ∅ 6|= ⊥;
• ⊢ p não é válido: ∅ 6|= p;
• ⊢ p → p,¬p é válido: ∅ |= (p → p) ∨ ¬p;
• p ⊢: não é válido: {p} 6|= ⊥;
• p → p,¬p ⊢ não é válido: {p → p,¬p} 6|= ⊥;
• p → q, p ⊢ q é válido: {p → q, p} |= q;
• p → q, p,¬q ⊢ q, r é válido: {p → q, p,¬q} |= q ∨ r.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Os sistemas formais SI e ST são do tipo Gentzen
• Em SI: o lado direito de cada sequente é sempre λ:
c(Ψ) é insatisfat́ıvel se e somente se Ψ⊢ é válido.
• Em ST : o lado esquerdo de cada sequente é sempre λ.
toda interpretação satisfaz alguma fórmula de c(Ψ) se e somente se ⊢Ψ é
válido.
Ψ′: resultado de substituir em Ψ cada fórmula por uma complementar.
Lema que conecta os três sistemas formais:
Ψ1⊢Ψ2 é válido sse Ψ1,Ψ
′
2⊢ é válido sse ⊢Ψ
′
1,Ψ2 é válido.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Os axiomas do sistema formal SG
No sistema SG, em vez de usar ⊢Ψ,ν,¬ν ou Ψ,ν,¬ν⊢ como esquema de axioma,
será usado:
Ax : Ψ1,ν⊢Ψ2,ν
em que ν ∈ V.
Note: ⊢Ψ,ν,¬ν é válido sse Ψ′,ν,¬ν⊢ é válido sse Ψ1,ν⊢Ψ2,ν é válido,
onde:
• c(Ψ′1) ∪ c(Ψ2) = c(Ψ) e
• c(Ψ1) ∪ c(Ψ
′
2) = c(Ψ
′).
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
As regras de troca do sistema formal SG
As regras vêm aos pares:
• tipo e: lida com lado esquerdo (de ⊢);
• tipo d: lida com lado direito.
Regras estruturais de troca:
tre : Ψ1,α,β,Ψ
′
1⊢Ψ2
Ψ1,β,α,Ψ
′
1⊢Ψ2
trd : Ψ1⊢Ψ2,α,β,Ψ
′
2
Ψ1⊢Ψ2,β,α,Ψ
′
2
Daqui prá frente será suposto que os lados direito e esquerdo são multiconjuntos.
Não serão usadas as regras de troca.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Como obter as regras lógicas do sistema formal SG
As regras podem ser obtidas das de SI ou de ST .
• SI: as regras de sufixo p levam a regras de sufixo e e as de sufixo n levam a
regras de sufixo d (ou seja, fórmulas negativas “trocam de lado”).
• ST : o inverso.
Por exemplo, para falsum a regra de SI é:
falp :
Ψ,⊥
o que leva à regra de introdução de ⊥ à esquerda:
fale :
Ψ1,⊥ ⊢Ψ2
O que seria Ψ na regra de SI agora pode estar espalhado em ambos os lados do
sequente em SG.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
As regras lógicas para verum
Para verum a regra de SI é:
vern :
Ψ,¬⊤
o que leva à regra de introdução de ⊤ à direita:
verp :
Ψ1⊢ ⊤,Ψ2
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
As regras lógicas para a conjunção
A partir das regras de SI para a conjunção:
conjp : Ψ,α,β
Ψ,α∧β
conjn : Ψ,¬α Ψ,¬β
Ψ,¬(α∧β)
chega-se às regras da conjunção para SG
conje : Ψ1,α,β⊢Ψ2
Ψ1,α∧β⊢Ψ2
conjd : Ψ1⊢α,Ψ2 Ψ1⊢β,Ψ2
Ψ1⊢α∧β,Ψ2
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
As regras lógicas do sistema formal SG
Verum
vere : Ψ1⊢Ψ2 verd :
Ψ1,⊤ ⊢Ψ2 Ψ1⊢ ⊤,Ψ2
Falsum
fale : fald : Ψ1⊢Ψ2
Ψ1,⊥ ⊢Ψ2 Ψ1⊢ ⊥,Ψ2
Negação
nege : Ψ1⊢α,Ψ2 negd : Ψ1,α⊢Ψ2
Ψ1,¬α⊢Ψ2 Ψ1⊢ ¬α,Ψ2
• As regras vere e fald não são necessárias; estão presentes apenas para facilitar a
demonstração de completude.
• A negação de uma fórmula é introduzida à esquerda se a fórmula ocorre à direita,
e vice-versa.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
As regras lógicas do sistema formal SG (cont.)
Conjunção
conje : Ψ1,α,β⊢Ψ2 conjd : Ψ1⊢α,Ψ2 Ψ1⊢β,Ψ2
Ψ1,α∧β⊢Ψ2 Ψ1⊢α∧β,Ψ2
Disjunção
disje : Ψ1,α⊢Ψ2 Ψ1,β⊢Ψ2 disjd : Ψ1⊢α,β,Ψ2
Ψ1,α∨β⊢Ψ2 Ψ1⊢α∨β,Ψ2
Condicional
conde : Ψ1⊢α,Ψ2 Ψ1,β⊢Ψ2 condd : Ψ1,α⊢β,Ψ2
Ψ1,α→β⊢Ψ2 Ψ1⊢α→β,Ψ2
Bicondicional
bice : Ψ1,α,β⊢Ψ2 Ψ1⊢α,β,Ψ2 bicd : Ψ1,α⊢β,Ψ2 Ψ1,β⊢α,Ψ2
Ψ1,α↔β⊢Ψ2 Ψ1⊢α↔β,Ψ2
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Como determinar se H |= α em SG?
• Cada regra, se aplicada de trás para frente, elimina um conectivo.
• Assim, para determinar se H |= α, pode-se construir uma dedução de trás para
frente começando com o sequente Ψ⊢α, em que Ψ é uma sequência com as
fórmulas de H;
• Produzir premissas cada vez menores até atingir axiomas.
• Caso seja produzido um sequente sem conectivos que não seja axioma: não há
dedução do sequente H⊢α; portanto, H 6|= α.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Algoritmo para determinar se há dedução de Ψ1 ⊢ Ψ2 em SG
proc Gentzen(sequente Ψ1⊢Ψ2): retorna dedução
conjunto de sequentes CS;
nome de regra regra;
dedução D;
fórmula α, β, γ;
{e, d} lado;
CS := {Ψ1⊢Ψ2}; D := vazia;
repita
Ψ1⊢Ψ2 := escolha(CS); { escolhe próximo sequente } CS := CS − {Ψ1⊢Ψ2};
se Ψ1 ∩ Ψ2 6= ∅ então
regra := Ax
senãose Ψ1⊢Ψ2 contém fórmula que não é literal então
(γ, lado) := escolhanl(Ψ1⊢Ψ2); { escolhe não literal };
se lado = e então Ψ1 := Ψ1 − {γ} senão Ψ2 := Ψ2 − {γ} fimse;
caso (lado, γ) seja
(e,⊤): CS := CS ∪ {Ψ1⊢Ψ2}; regra := vere
(d,⊤): { continue } regra := verd
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
(e,⊥): { continue } regra := fale
(d,⊥): CS := CS ∪ {Ψ1⊢Ψ2}; regra := fald
(e,¬α): CS := CS ∪ {Ψ1⊢α,Ψ2}; regra := nege
(d,¬α): CS := CS ∪ {Ψ1,α⊢Ψ2}; regra := negd
(e, α∧β): CS := CS{Ψ1,α,β⊢Ψ2}; regra := conje
(d, α∧β): CS := CS ∪ {Ψ1⊢α,Ψ2,Ψ1⊢β,Ψ2}; regra := conjd
(e, α∨β): CS := CS ∪ {Ψ1,α⊢Ψ2,Ψ1,β⊢Ψ2}; regra := disje
(d, α∨β): CS := CS ∪ {Ψ1⊢α,β,Ψ2}; regra := disjd
(e, α→β):CS :=CS ∪ {Ψ1⊢α,Ψ2,Ψ1,β⊢Ψ2}; regra := conde
(d, α→β):CS := CS ∪ {Ψ1,α⊢β,Ψ2}; regra := condd
(e, α↔β):CS := LS ∪ {Ψ1,α,β⊢Ψ2,Ψ1⊢α,β,Ψ2}; regra := bice
(d, α↔β):CS := CS ∪ {Ψ1,α⊢β,Ψ2,Ψ1,β⊢α,Ψ2}; regra := bicd
fimcaso
senão { Ψ1 contém literais e/ou ⊥ e Ψ2 contém literais e/ou ⊤ e Ψ1⊢Ψ2 não é axioma}
retorne vazia
fimse;
D := D+(Ψ1⊢Ψ2, regra)
até LS = ∅;
retorne D
fim Gentzen
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Algumas observações sobre o algoritmo
• Não determinismo: apenas o provocado pelas escolhas do pseudocomando
escolhanl; não levam a computações de fracasso.
• São duas escolhas em escolhanl: a do lado do sequente e a da fórmula.
• Uma posśıvel heuŕıstica: preferir regra com menor número de premissas.
• Assim, as regras seriam divididas nas três classes (por ordem de preferência):
1. fale e verd; (vere e fald são supérfluas.)
2. nege, negd, conje, disjd, condd;
3. conjd, disje, conde, bice, bicd.
• Assim como para SI e ST , um comportamento exponencial do algoritmo é
provocado por regras com duas premissas (grupo 3 acima).
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Exemplo
Para mostrar que ∅ |= p → p, deve-se encontrar uma dedução de ⊢ p → p. Existe
uma única regra que permite concluir tal sequente, a regra condd com
Ψ1 = Ψ2 = vazio, o que leva à dedução:
1. p ⊢ p (Ax)
2. ⊢ p → p (condd 1)
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Exemplo
Mostrando que {p → (q → r), q} |= p → r:
1. q, p ⊢ q, r (Ax)
2. q, p, r ⊢ r (Ax)
3. q → r, q, p ⊢ r (conde 1,2)
4. q, p ⊢ p, r (Ax)
5. p → (q → r), q, p ⊢ r (conde 3,4)
6. p → (q → r), q ⊢ p → r (condd 5)
• A dedução não é muito clara, mas sua obtenção pelo uso de SG é trivial.
• É muito mais fácil obtê-la do que uma utilizando um sistema do tipo Hilbert.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Correção e completude
Usando-se o lema
Para cada regra de SG, suas premissas são válidas (todas) se, e somente se,
sua conclusão é válida.
prova-se a correção de SG:
Todo sequente dedut́ıvel é válido.
e a completude de SG:
Todo sequente válido é dedut́ıvel.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
FIM
c©2007 Newton José Vieira UFMG✫ ✪