Universidade de Brası́lia
Instituto de Ciências Exatas
Departamento de Ciência da Computação
CIC 117366 Lógica Computacional 1 - 2015/2
Primeira Avaliação
(Gabarito)
Prof. Flávio L. C. de Moura
Nome:
17 de setembro de 2015
Matrı́cula:
1. (2 pontos) O Princı́pio da Indução é fundamental tanto em Matemática e Computação porque
nos permite provar propriedades de estruturas indutivas como, por exemplo, as fórmulas da lógica
proposicional:
ϕ ::= ⊥ | > | p | (¬ϕ) | (ϕ ∧ ϕ) | (ϕ ∨ ϕ) | (ϕ → ϕ)
Um aspecto interessante sobre a gramática acima é que ela pode ser drasticamente simplificada sem
perder o poder de expressividade na lógica clássica proposicional. De fato, em termos de conectivos,
apenas a negação e disjunção já são suficientes para expressar todos os outros conectivos. Outras
combinações de conectivos também são possı́veis para se obter os chamados conjuntos completos
de conectivos. Mostre que {¬, ∨} é um conjunto completo de conectivos, isto é, mostre que para
qualquer fórmula ϕ da lógica clássica proposicional é possı́vel construir uma fórmula
ϕ0 contendo apenas os conectivos ¬ e ∨, e que seja equivalente a ϕ.
Dica: Lembre que ϕ → ψ é equivalente a (¬ϕ) ∨ ψ, e ¬(ϕ ∨ ψ) é equivalente a (¬ϕ) ∧ (¬ψ).
Solução. A prova segue por indução na estrutura de ϕ. Note que se ϕ for ⊥, > ou uma variável
proposicional p então o resultado é imediato porque ϕ neste caso não contém conectivos. Se ϕ for
da forma ¬ψ então por hipótese de indução podemos construir uma fórmula ψ 0 equivalente a ψ e
contendo apenas os conectivos ¬ e ∨. Neste caso, a fórmula ¬ψ 0 é equivalente a ϕ e contém apenas
os conectivos ¬ e ∨. Se ϕ é da forma ψ ∨ γ então por hipótese de indução podemos construir as
fórmulas ψ 0 e γ 0 equivalentes respectivamente a ψ e γ e contendo apenas os conectivos ¬ e ∨. Desta
forma, a fórmula ψ 0 ∨γ 0 é equivalente a ϕ e contém apenas os conectivos ¬ e ∨. Se ϕ é da forma ψ∧γ
então por hipótese de indução podemos construir as fórmulas ψ 0 e γ 0 equivalentes respectivamente a
ψ e γ e contendo apenas os conectivos ¬ e ∨. Desta forma, a fórmula ¬((¬ψ 0 ) ∨ (¬γ 0 )) é equivalente
a ϕ e contém apenas os conectivos ¬ e ∨. Se ϕ é da forma ψ → γ então por hipótese de indução
podemos construir as fórmulas ψ 0 e γ 0 equivalentes respectivamente a ψ e γ e contendo apenas os
conectivos ¬ e ∨. Desta forma, a fórmula ¬ψ 0 ∨ γ 0 é equivalente a ϕ e contém apenas os conectivos
¬ e ∨.
2. A lógica intuicionista é importante para a Ciência da Computação porque fornece provas construtivas de propriedades, isto é, os objetos que satisfazem a propriedade provada podem ser construı́dos
concretamente. Em dedução natural, uma prova intuicionista caracteriza-se pela não utilização da
lei do terceiro excluı́do (LEM), ou de qualquer regra clássica1 . As regras de inferência do sistema
de dedução natural para a LPI são dadas a seguir:
Um resultado interessante em teoria da prova estabelece que provabilidade construtiva e provabilidade em geral são equivalentes no seguinte sentido:
Se `c ϕ, isto é, se ϕ é um teorema da lógica proposicional clássica então
`i ¬¬ϕ, ou seja, ¬¬ϕ é um teorema da lógica proposicional intuicionista.
(2 pontos) Seja p uma variável proposicional. Prove `i ¬¬(p ∨ (¬p)).
1 Além
da LEM, vimos que (PBC) , (¬¬e ) e LP também são regras clássicas.
1
regras de introdução
regras de eliminação
ϕ ψ
(∧i )
ϕ∧ψ
ϕ∧ψ
(∧e )
ψ
ϕ∧ψ
ϕ (∧e )
ϕ
ψ
(∨i )
(∨i )
ϕ∨ψ
ϕ∨ψ
[ϕ]u
..
.
χ
χ
ϕ∨ψ
[ϕ]u
..
.
ψ
(→i ) u
ϕ→ψ
ϕ
(∨e ) u, v
ϕ→ψ
(→e )
ψ
ϕ
[ϕ]u
..
.
⊥ (¬ ) u
i
¬ϕ
[ψ]v
..
.
χ
¬ϕ
(¬e )
⊥
⊥ (⊥ )
e
ϕ
Solução.
[p]2
(∨i )
p ∨ (¬p)
[¬(p ∨ (¬p))]1
(∨i )
⊥
¬p
p ∨ (¬p)
(¬i ) 2
(∨i )
[¬(p ∨ (¬p))]1
⊥
¬¬(p ∨ (¬p))
(¬e )
(¬i ) 1
(2 pontos) Sabemos que a regra de eliminação da dupla negação (¬¬e ) é, em geral, uma regra
clássica, no entanto, um outro resultado interessante da lógica intuicionista é que a eliminação da
dupla negação de fórmulas negativas é um teorema. Uma fórmula ϕ é dita negativa se qualquer
variável proposicional p de ϕ ocorre apenas na forma ¬p em ϕ, e ϕ não contém disjunções. Prove
que ¬¬¬p `i ¬p.
Solução.
[p]1
[¬p]2
⊥
¬¬p
¬¬¬p
⊥
¬p
(¬e )
(¬i ) 2
(¬e )
(¬i ) 1
(2 pontos) A lógica proposicional clássica (LPC) pode ser obtida da tabela acima substituindo-se
2
a regra (⊥e ) por
[¬φ]a
..
.
⊥
φ
(PBC) a
Desta forma, (⊥e ) pode ser vista como uma regra derivada na LPC. Prove que de fato, (⊥e ) é uma
regra derivada na LPC.
Solução.
⊥
[¬φ]1
(∧i )
⊥∧φ
(∧e )
⊥
(PBC) 1
φ
(2 pontos) Alternativamente a LPC também pode ser caracterizada pela Lei de Peirce: ((ϕ →
ψ) → ϕ) → ϕ. Prove ` ((ϕ → ψ) → ϕ) → ϕ.
Solução.
[ϕ]3
[¬ϕ]2
⊥
ψ
ϕ→ψ
[(ϕ → ψ) → ϕ]1
ϕ
⊥
ϕ
((ϕ → ψ) → ϕ) → ϕ
3
(¬e )
(⊥e )
(→i ) 3
(→e )
[¬ϕ]2
(¬e )
(PBC) 2
(→i ) 1