Sistemas Dedutíveis Axiomático, Dedução Natural e Tableau

Prévia do material em texto

Lógica para Computação
Lógica para Computação
Davi Romero de Vasconcelos
Universidade Federal do Ceará em Quixadá, Brasil
daviromero@ufc.br
Lógica para Computação
Sumário
Sumário I
Sistema Dedutível
Axiomático
Dedução Natural
Dedução Natural em Fitch
Tableaux
Lógica para Computação
Sistema Dedutível
Sistema Dedutível
Existem diversas formas de definir um sistema dedutível.
Um sistema dedutivo é um mecanismo que permite a construção de argumentos
formais
Um sistema dedutivo é um mecanismo que permite estabelecer conclusões a partir
de hipóteses.
Um sistema dedutivo é um conjunto de regras (as vezes axiomas) que permite
“chegar” a conclusões (sentenças) a partir de hipóteses (sentenças).
Escrevemos Γ `D ϕ para indicar ϕ é provado com o mecanismo de dedução D a partir
de um conjunto de fórmulas Γ
Correção: Γ `D ϕ =⇒ Γ |= ϕ
Completude: Γ |= ϕ =⇒ Γ `D ϕ
Lógica para Computação
Sistema Dedutível
Axiomático
Sistema Axiomático
Existem diversos sistemas axiomáticos.
Sistema de Hilbert e Bernays.
Contém os seguintes esquemas axiomáticos:
Axioma 1: ϕ→ (ψ → ϕ)
Axioma 2: (ϕ→ (ψ → σ))→ ((ϕ→ ψ)→ (ϕ→ σ))
Axioma 3: (¬ψ → ¬ϕ)→ ((¬ψ → ϕ)→ ψ)
Contém apenas uma regra de inferência (Modus Ponens)
ϕ ϕ→ ψ
ψ
Lógica para Computação
Sistema Dedutível
Axiomático
Exemplo
Prove que `Ax A→ A
Aplicando os esquemas axiomáticos abaixo Axioma 1: ϕ → (ψ → ϕ)Axioma 2: (ϕ → (ψ → σ)) → ((ϕ → ψ) → (ϕ → σ))
temos que
Axioma 1: ϕ = A e ψ = B → A A → ((B → A) → A)
Axioma 1: ϕ = A e ψ = B A → (B → A)
Axioma 2: ϕ = A, ψ = B → A e σ = A (A → ((B → A) → A)) → (A → (B → A)) → (A → A)
A → (B → A)
A → ((B → A) → A) (A → ((B → A) → A)) → (A → (B → A)) → (A → A)
(A → (B → A)) → (A → A)
A → A
Lógica para Computação
Sistema Dedutível
Axiomático
Exemplo
Prove que {A→ B,B → C} `Ax A→ C
Aplicando os esquemas axiomáticos abaixo Axioma 1: ϕ → (ψ → ϕ)Axioma 2: (ϕ → (ψ → σ)) → ((ϕ → ψ) → (ϕ → σ))
temos que
Axioma 1: ϕ = B → C e ψ = A (B → C) → (A → (B → C))
Axioma 2: ϕ = A, ψ = B e σ = C (A → (B → C)) → (A → B) → (A → C)
A → B
B → C (B → C) → (A → (B → C))
A → (B → C) (A → (B → C)) → (A → B) → (A → C)
(A → B) → (A → C)
A → C
Lógica para Computação
Sistema Dedutível
Dedução Natural
Regras de Dedução Natural
ϕ ψ
ϕ ∧ ψ ∧I
ϕ ∧ ψ
ϕ ∧E
ϕ ∧ ψ
ψ
∧E
ϕ
ϕ ∨ ψ ∨I
ψ
ϕ ∨ ψ ∨I
ϕ ∨ ψ
[ϕ]i
.
.
.
α
[ψ]i
.
.
.
α
α ∨E
i
[ϕ]i
.
.
.
ψ
ϕ → ψ → I
i
ϕ ϕ → ψ
ψ
→ E
[ϕ]i
.
.
.
⊥
¬ϕ ¬I
i
ϕ ¬ϕ
⊥ ¬E
⊥
ϕ ⊥
[¬ϕ]i
.
.
.
⊥
ϕ RAA
i
Lógica para Computação
Sistema Dedutível
Dedução Natural
Exemplos
Prove que A ∧ (B ∧ C ) `DN (A ∧ B) ∧ C
A ∧ (B ∧ C )
A
A ∧ (B ∧ C )
B ∧ C
B
A ∧ B
A ∧ (B ∧ C )
B ∧ C
C
(A ∧ B) ∧ C
Lógica para Computação
Sistema Dedutível
Dedução Natural
Exemplos
Prove que A ∨ (B ∨ C ) `DN (A ∨ B) ∨ C
A ∨ (B ∨ C )
[A]1
A ∨ B
(A ∨ B) ∨ C
[B ∨ C ]1
[B]2
A ∨ B
(A ∨ B) ∨ C
[C ]2
(A ∨ B) ∨ C
(A ∨ B) ∨ C
2
(A ∨ B) ∨ C
1
Lógica para Computação
Sistema Dedutível
Dedução Natural
Exemplos
Prove que `DN A→ (B → A)
[A]1
(B → A)
A→ (B → A)
1
Prove que `DN (A→ B)→ ((B → C )→ (A→ C ))
[A]3 [(A→ B)]1
B [B → C ]2
C
A→ C
3
(B → C )→ (A→ C )
2
(A→ B)→ ((B → C )→ (A→ C ))
1
Lógica para Computação
Sistema Dedutível
Dedução Natural
Exemplos
Prove que A→ (B → C ) `DN (A ∧ B)→ C
A→ (B → C )
[A ∧ B]1
A
B → C
[A ∧ B]1
B
C
(A ∧ B)→ C
1
Lógica para Computação
Sistema Dedutível
Dedução Natural
Exemplos
Prove que `DN A→ (¬A→ B)
[A]1 [¬A]2
⊥
B
¬A→ B
2
A→ (¬A→ B)
1
Prove que ¬A ∨ B `DN A→ B
¬A ∨ B
[A]2 [¬A]1
⊥
B
A→ B
2
[B]1
A→ B
A→ B
1
Lógica para Computação
Sistema Dedutível
Dedução Natural
Exemplos
Prove que `DN A ∨ ¬A
[A]2
A ∨ ¬A [¬(A ∨ ¬A)]1
⊥
¬A
2
A ∨ ¬A [¬(A ∨ ¬A)]1
⊥
A ∨ ¬A
1
Lógica para Computação
Sistema Dedutível
Dedução Natural
Exemplos
Prove que `DN (A→ B) ∨ (B → A)
[A]2
B → A
(A → B) ∨ (B → A) [¬((A → B) ∨ (B → A))]1
⊥
B
A → B
2
(A → B) ∨ (B → A) [¬((A → B) ∨ (B → A))]1
⊥
(A → B) ∨ (B → A)
1
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
O sistema de Dedução Natural usualmente é apresentado por meio de árvores,
Estilo de Gentzen, ou por meio de caixas, Estilo de Fitch.
No Estilo de Fitch as demonstrações são apresentadas de forma linear e sequencial,
na qual cada uma das linhas da prova é numerada, tem uma afirmação e uma
justificativa.
As justificativas são definidas por serem premissas da prova ou pela aplicação de
uma das regras do sistema dedutível de Dedução Natural.
As subprovas dentro de uma prova maior têm caixas ao redor e servem para
delimitar o escopo de hipóteses temporárias.
Provas podem ter caixas dentro de caixas, ou pode-se abrir outras caixas depois de
fechar outras, obedecendo as regras de demonstração.
Uma fórmula só pode ser utilizada em uma prova em um determinado ponto se
essa fórmula aconteceu anteriormente e se nenhuma caixa que contenha essa
ocorrência da fórmula tenha sido fechada.
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Regra das premissas
1. ϕ premissa
2. ψ premissa
...
...
...
m. α premissa
...
...
...
A,B ` A ∧ B
1. A premissa
2. B premissa
3.
...
...
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Conjunção Introdução (∧i)
...
...
...
m. ϕ
...
...
...
n. ψ
...
...
...
p. ϕ ∧ ψ ∧i m,n
...
...
...
m. ψ
...
...
...
n. ϕ
...
...
...
p. ϕ ∧ ψ ∧i m,n
A,B ` A ∧ B
1. A premissa
2. B premissa
3. A ∧ B ∧i 1,2
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Conjunção Eliminação (∧e)
...
...
...
m. ϕ ∧ ψ
...
...
...
p. ϕ ∧e m
...
...
...
m. ϕ ∧ ψ
...
...
...
p. ψ ∧e m
A ∧ B,C ` A ∧ C
1. A ∧ B premissa
2. C premissa
3. A ∧e 1
4. A ∧ C ∧i 3,2
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Implicação Eliminação (→ e)
...
...
...
m. ϕ→ ψ
...
...
...
n. ϕ
...
...
...
p. ψ →e m,n
...
...
...
m. ϕ
...
...
...
n. ϕ→ ψ
...
...
...
p. ψ →e m,n
A,A ∧ B,B → C ` C
1. A premissa
2. A ∧ B premissa
3. B → C premissa
4. B ∧ e 2
5. C → e 4,3
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Implicação Introdução (→i)
...
...
...
m.
...
n.
ϕ hipótese
...
...
ψ
n+1. ϕ→ ψ →i m-n
A→ B,B → C ` A→ C
1. A→ B premissa
2. B → C premissa
3. A hipótese
4. B → e 3,1
5. C → e 4,2
6. A→ C → i 3-5
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Disjunção Introdução (∨i)
...
...
...
m. ϕ
...
...
...
p. ϕ ∨ ψ ∨i m
...
...
...
m. ψ
...
...
...
p. ϕ ∨ ψ ∨i m
(A ∨ B)→ C ` A→ C
1. (A ∨ B)→ C premissa
2. A hipótese
3. A ∨ B ∨ i 2
4. C → e 3,1
5. A→ C → i 2-4
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Disjunção Eliminação (∨e)
...
...
...
m. ϕ ∨ ψ
m+1.
...
n.
ϕ hipótese
...
...
α
n+1.
...
p.
ψ hipótese
...
...
α
p+1. α ∨e m, (m+1)-n, (n+1)-p
A→ C ,B → C ,A ∨ B ` C
1. A→ C premissa
2. B → C premissa
3. A ∨ B premissa
4. A hipótese
5. C → e 4,1
6. B hipótese
7. C → e 6,2
8. C ∨ e 3, 4-5, 6-7
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Negação Introdução (¬i)
...
...
...
m.
...
n.
ϕ hipótese
...
...
⊥
n+1. ¬ϕ ¬i m-n
¬(A ∨ B) ` ¬A
1. ¬(A ∨ B) premissa
2. A hipótese
3. A ∨ B ∨ i 2
4. ⊥ ¬ e 1,3
5. ¬A ¬ i 2-4
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Negação Eliminação (¬e)
...
...
...
m. ϕ
...
...
...
n. ¬ϕ
...
...
...
p. ⊥ ¬e m,n
...
...
...
m. ¬ϕ
...
...
...
n. ϕ
...
...
...
p. ⊥ ¬e m,n
A,¬A ` ⊥
1. A premissa
2. ¬A premissa
3. ⊥ ¬ e 1,2
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Contradição Eliminação (⊥e)
...
...
...
m. ⊥
...
...
...
p. ψ ⊥e m
` A→ (¬A→ B)
1. A hipótese
2. ¬A hipótese
3. ⊥¬ e 1,2
4. B ⊥e 3
5. ¬A→ B → i 2-4
6. A→ (¬A→ B) → i 1-5
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Redução Ao Absurdo (raa)
...
...
...
m.
...
n.
¬ϕ hipótese
...
...
⊥
n+1. ϕ raa m-n
` A ∨ ¬A
1. ¬(A ∨ ¬A) hipótese
2. ¬A hipótese
3. A ∨ ¬A ∨ i 2
4. ⊥ ¬ e 3,1
5. A raa 2-4
6. A ∨ ¬A ∨ i 5
7. ⊥ ¬ e 6,1
8. A ∨ ¬A raa 1-7
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch)
Copie
...
...
...
m. ϕ
...
...
...
...
n.
...
...
...
ϕ copie m
...
...
...
...
...
¬A ∨ B ` A→ B
1. ¬A ∨ B premissa
2. ¬A hipótese
3. A hipótese
4. ⊥ ¬ e 2,3
5. B ⊥ e 4
6. A→ B → i 3-5
7. B hipótese
8. A hipótese
9. B copie 7
10. A→ B → i 8-9
11. A→ B ∨ e 1, 2-6, 7-10
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch vs. Gentzen)
` A→ (¬A→ B)
1. A hipótese
2. ¬A hipótese
3. ⊥ ¬ e 1,2
4. B ⊥e 3
5. ¬A→ B → i 2-4
6. A→ (¬A→ B) → i 1-5
[
A
]
1
[
¬A
]
2
⊥ ¬e
B
⊥ e
¬A→ B→ i, 2
A→ (¬A→ B)→ i, 1
Lógica para Computação
Sistema Dedutível
Dedução Natural
Sistema de Dedução Natural (Estilo Fitch vs. Gentzen)
A ∨ B,A→ C ,B → C ` C
1. A→ C premissa
2. B → C premissa
3. A ∨ B premissa
4. A hipótese
5. C → e 4,1
6. B hipótese
7. C → e 6,2
8. C ∨e 3, 4-5, 6-7
A ∨ B
[
A
]
1 A→ C
C
→ e
[
B
]
2 B → C
C
→ e
C
∨e, 1, 2
Lógica para Computação
Sistema Dedutível
Tableaux
Sistema Tableau
Os sistemas Axiomático e Dedução Natural permitem demonstrar quando uma
fórmula é derivada de um conjunto de fórmulas (Γ ` ϕ). Contudo, nenhum desses
métodos nos permite inferir que Γ 6` ϕ.
Note que Γ 6` ϕ não implica em Γ ` ¬ϕ.
O método da Tabela da Verdade é um procedimento de decisão que nos permite
Γ ` ϕ e Γ 6` ϕ. Contudo, esse procedimento tem um crescimento no número de
linhas exponencial em relação ao número de símbolos proposicionais.
O sistema de inferência de Tableau Analítico (Semântico) é um método de decisão
que não necessariamente gera provas de tamanho exponencial.
Lógica para Computação
Sistema Dedutível
Tableaux
Sistema Tableau
Tableau é um método de inferência baseado em refutação: para provarmos Γ ` ϕ,
afirmamos a veracidade de Γ e a falsidade de ϕ, na esperança de derivarmos uma
contradição. Por outro lado, se não for obtida uma contradição, então teremos
construído um contra-exemplo, i.e., uma valoração que satisfaz Γ e não satisfaz ϕ.
Para afirmar a veracidade ou falsidade de uma fórmula, o método dos tableaux
analíticos marca as fórmulas com os símbolos 1 para verdade e 0 para falsidade.
O passo inicial na criação de um tableau é marcar todas as fórmulas de Γ com 1 e
a fórmula ϕ com 0.
Lógica para Computação
Sistema Dedutível
Tableaux
Sistema Tableau
A partir do tableau inicial, utiliza-se regras de expansão do tableau que adicionam
novas fórmulas ao final de um ramo (regras do tipo α) ou que bifurcam um ramo
em dois (regras do tipo β).
Tipo α 1ϕ ∧ ψ
1ϕ
1ψ
0ϕ ∨ ψ
0ϕ
0ψ
0ϕ→ ψ
1ϕ
0ψ
1¬ϕ
0ϕ
Tipo β 0ϕ ∧ ψ
0ϕ 0ψ
1ϕ ∨ ψ
1ϕ 1ψ
1ϕ→ ψ
0ϕ 1ψ
0¬ϕ
1ϕ
Note que as regras α e β não são aplicadas aos átomos.
Lógica para Computação
Sistema Dedutível
Tableaux
Sistema Tableau
Em cada ramo, uma fórmula só pode ser expandida uma única vez.
Um ramo que não possui mais fórmulas para expandir é dito saturado.
Um ramo que possui uma par de fórmulas 1ϕ e 0ϕ é dito fechado. Um ramo
fechado não precisa mais ser expandido.
Um tableau que tem todos os seus ramos fechados é dito fechado, ou seja, Γ ` ϕ.
Um ramo saturado e não fechado nos fornece um contra-exemplo, ou seja, Γ 6` ϕ.
Lógica para Computação
Sistema Dedutível
Tableaux
Exemplos de Provas em Tableaux Semânticos
`TA A ∨ ¬A
0A ∨ ¬A
0A
0¬A
1A
×
Lógica para Computação
Sistema Dedutível
Tableaux
Exemplos de Provas em Tableaux Semânticos
A→ B,B → C `TA A→ C
1A→ B
1B → C
0A→ C
1A
0C
0A
×
1B
0B
×
1C
×
Lógica para Computação
Sistema Dedutível
Tableaux
Exemplos de Provas em Tableaux Semânticos
A,A ∧ B → C 6`TA C
1A
1A ∧ B → C
0C
0A ∧ B
0A
×
0B
1C
×
A valoração v(A) = 1 e v(B) = v(C ) = 0 (contra-exemplo) demonstra que
A,A ∧ B → C 6`TA C .
	Sistema Dedutível
	Axiomático
	Dedução Natural
	Tableaux