BCC101
Matemática Discreta I
Lógica Proposicional
Dedução
1
{I}: como encontrar a hipótese a
ser descarregada?
Case as partes da regra com a prova
Case o b da regra com parte da prova
E case a procurando nas folhas pelo lado esquerdo da  da raiz
Descarregue todas as ocorrências de a nas folhas
a
{I1}
a  b
[a] |– b
{I}
ab
(a  b)  False
{E}
False
{I}
a  False
2
O que descarregar em {I}, {E}, e {RAA}
[a] |– b
 {I}
ab
I
a hipótese a ser descarregada
na subárvore a |– b deve ser
correspondente à fórmula a
da conclusão ab
Introdução da
Implicação
a  b [a] |– c [b] |– c
{E}
c
Ou Eliminação
[a] |– False
{RAA}
a
Reducão ao Absurdo
a hipótese a ser descarregada
na subárvore a |– c deve ser
correspondente à fórmula a
da hipótese ab
de modo similar para
a subárvore b |– c,
mas casando o b de ab
a hipótese a ser descarregada na
subárvore a |– False deve ser
correspondente à fórmula a
onde a é a fórmula abaixo da 3linha
Nor Comuta
(a  b) |-
Plano
• Prove (b  a)  (a  b)
• Use Modus Tollens
x  y y
{mod tol}
x
[x] |– y
x  y {I}
(b  a)
(x  y)
{ com}
(y  x)
Nor Comuta como regra
Usando o Teorema Ou-Comuta
[ b  a]
Usando Modus Tollens
{Com}
ab
 {I}
(b  a)(a  b)
(a  b)
 {mod tol}
(b  a)
decarregada
em I
conclusão
hipótese
restante
4
Isto NÃO é uma prova
o conectivo principal é “”
(a  b)
{ com}
(b  a)
conectivo principal é “”
O que há de errado nisso?
o conectivo principal deve
casar com a regra de inferência
em uma prova por dedução natural
x  y
{ com}
y  x
Ou Comuta como regra
5
Prova Incorreta de um Teorema
Teorema ( Comuta)
 a  b |– b  a
O que há de errado com esta prova?
ab
ab
{E1}
{E2}
a
b
 {I}
ba
x
y
 {I}
xy
regra I
6
Nor Eliminação
O que falta aqui?
Plano
• Suponha a
• Derive False
• Use {I}
[x] |– False
{I}
x
(a  b) |– a
(x  y)
x x
False {E}
[a]
{E1}
x
Nor Eliminação-1 como regra
(a  b)
(hipótese do teorema)
{I1}
Que regra usar?
ab
 (a  b)
{E}
E agora?
False
{I}
a
descarregada em I
conclusão do teorema
7
Nor Eliminação – outro lado
(a  b) |– b
(x  y)
Plano
• Comute usando { com}
• Use {E1}
{E2}
y
Nor Eliminação-2 como regra
(a  b)
{ com}
(b  a)
 {E1}
b
Que regra usar aqui?
8
Lei de DeMorgan - Ou
(Deduzindo um lado)
(a  b)
Plano
• Derive as 2 partes da conclusão
• separadamente
• Use {I}
(a  b)
|– (a)  (b)
(x  y)
{deMF}
(x)(y)
DeMorgan Ou 1
(a  b)
{E1}
{E2}
a
b
{I}
(a)  (b)
Que regra usar aqui?
9
Lei de DeMorgan - Ou
(Deduzindo o outro lado)
(a)  (b) |–
Plano
• Use {E} para derivar False de a  b
• Use {I} para concluir (a  b)
[x] |– False
{I}
x
x  y [x] |– z
z
descarregada
em {I}
[y] |– z
{E}
(a  b)
Atenção: esta prova
é complicada
x
x
{E}
False
(a)  (b)
(a)  (b)
 {E1}
{E2}
b
a
[ a]
[b]
{E}
{E}
a

b
[
]
False
False
{E}
False
{I}
 (a  b)
Descarregadas em {E}
Descarregada em {I}
10
Uma Prova Usando Contradição
a  b, a |–
b
Plano
 Use E
 Depois  E
 Depois CTR
[a]
a
{E}
{silogismo disjuntivo}
a a
{E}
False
False
{CTR}
a
a  b [a] |– c [b] |– c
{E}
c
o que
[ b]
False
 {CTR}
 {ID} descarregar?
ab
b
b
{E}
b conclusão
hipóteses
restantes
11
Dedução Natural
regras de inferência e alguns teoremas
Teoremas
Regras de Inferência
x
xy
{E}
y
False
{CTR}
x
xy
{E1}
x
x
x
xy
{E2}
y
xy
[x] |– z
z
[y] |– z
{E}
{ID}
[x] |– y
x  y {I}
x y
x  y {I}
[x] |– False
{RAA}
x
x
x  y {I1}
[x] |– False
{I}
x
x x
{E}
False
y
x  y {I2}
x  y |– y  x { comm}
(x  y) |– (y  x)
{ com}
x  y |– y  x { comm}
(x  y) |– x
{ E1}
xy, yz |– xz {chain}
(x  y) |– y
{ E2}
xy, y |– x
{mod tol}
x  y, x |– y
{disj syl}
(x  y) |– (x)(y) { deMF}
(x)(y) |– (x  y)
{ deMB}
12
Exercício
Prove o sequente: a  (b  c) |– a  b
Regras de Inferência
x
xy
{E}
y
False
{CTR}
x
xy
{E1}
x
x
x
xy
{E2}
y
xy
[x] |– z
z
[y] |– z
{E}
{ID}
[x] |– y
x  y {I}
x y
x  y {I}
[x] |– False
{RAA}
x
x
x  y {I1}
[x] |– False
{I}
x
x x
{E}
False
y
x  y {I2}
13
Exercício
Prove o sequente: a  (b  c) |– a  b
Regras de Inferência
x
xy
{E}
y
False
{CTR}
x
xy
{E1}
x
x
x
xy
{E2}
y
xy
[x] |– z
z
[y] |– z
a  (b  c)
{E}
[a]
[x] |– y
x  y {I}
x y
x  y {I}
{ID}
[x] |– False
{RAA}
x
x
x  y {I1}
[x] |– False
{I}
x
x x
{E}
False
y
x  y {I2}
ab
ab
[ b  c]
{I1}
Que hipóteses devem ser descarregadas?
{E1}
b
{I2}
ab
{E}
14