13 - Dedução Natural

Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original

Clique para editar o estilo do título mestre
Clique para editar o estilo do subtítulo mestre
*
*
*
Lógica Proposicional
Dedução Natural 
*
*
*
Conseqüência lógica
Definição informal:
Uma fórmula é uma conseqüência lógica de um conjunto de fórmulas se sempre que estas forem verdadeiras aquela também seja verdadeira.
Definição formal:
Dada uma fórmula H e um conjunto de hipóteses b, H é conseqüência lógica de b num sistema de dedução, se existir uma prova de H a partir de b
*
*
*
Notação de Conseqüência Lógica e Teorema
Dada uma fórmula H, se H é conseqüência lógica de um conjunto de hipóteses b={H1,H2,...Hn}, diz-se que:
b├ H ou
{H1,H2,...Hn}├ H
Uma fórmula H é um teorema se existe uma prova de H que não usa hipóteses
├ H
*
*
*
Cálculo Proposicional
Cálculo = Lógica + Sistema de Prova (ou dedução)
Um sistema de prova serve para analisar e raciocinar sobre argumentos de uma lógica, de maneira a prová-los válidos ou inválidos.
*
*
*
Sistema de dedução natural
Alfabeto da Lógica Proposicional
Conjunto de fórmulas da Lógica Proposicional
Conjunto de regras de dedução (ou regras de inferência)
*
*
*
Regras de inferência de dedução natural
Servem para inserção e retirada de conectivos lógicos, criando derivações
Regras de Introdução 
Regras de Eliminação
Chama-se dedução natural por estar próxima da maneira como nós raciocinamos quando queremos (informalmente) provar um argumento.
*
*
*
Regras de inferência - conjunção 
Introdução da conjunção (^I):
 H		G		-> derivação
	 H^G
Eliminação da conjunção (^E):
H^G	H^G
	 H	 G
*
*
*
Prova
Dados H uma fórmula e b um conjunto de fórmulas (hipóteses)
Uma prova de H a partir de b é uma derivação onde 
As regras de inferência são aplicadas tendo como premissas fórmulas de b 
A última fórmula da derivação é H
*
*
*
Exemplo de prova
P ^ Q, R |- Q ^ R
P ^ Q	(Premissa)
	 Q (^E)		R (Premissa)
		 Q^R (^I)
Exercícios:
(P^Q) ^ R, S^T |- Q^S
P^Q |- Q^P
(P^Q) ^ R |- P ^ (Q^R)
*
*
*
Regras da Dedução Natural - implicação 
Eliminação da implicação - modus ponens (E)
H H  G
	 	 G
Introdução da implicação (I)
[H] (hipótese eliminada)
		|
	 G . 
 H  G
*
*
*
Exemplo de eliminação da implicação
P^Q, (P (Q R)) ├ (Q R)
P^Q
	 P (^E)	 P (Q R) (premissa)
			 (Q R) (E) 
*
*
*
Exemplo de introdução da implicação
├ (P ((PQ)Q) 
Supor os antecedentes 
Eles não poderão ser usados depois
[P] 		[(PQ)] (hipóteses)
		 Q 		(E) 
(PQ)Q) (I)
(P ((PQ)Q) 	 (I)
*
*
*
Exercício
├ (P(Q P))
├ (P(Q R)) ((P^Q)R))
*
*
*
Exercícios
	
1. {P^Q, (P^Q)(R^P)} |- R^P
2. {P  (Q R), PQ, P} |- R
3. {P (P  Q), P} |- Q
*
*
*
Regras da Dedução Natural
- disjunção
Introdução da disjunção (vI)
 H	 G . 
		 HvG	 HvG
	
Eliminação da disjunção (vE)
 [H] [G] (hipóteses) 		 			D1 D2
 		HvG	 E E
			E
*
*
*
Exemplo de Eliminação da disjunção
{PvQ,Q,P} |- false
 		PvQ .
	[P] 	P (prem.) [Q] Q (prem.) 
		 false				false
					false
*
*
*
Regras da Dedução Natural
- negação
De uma derivação de uma contradição (false) a partir de uma hipótese H, pode-se descartar a hipótese e inferir H e vice-versa
[H]	 (I) 		[H] (E ou RAA) 
	 |				 |
 false			false reductio ad 	 H			 H absurdum
Exercícios: HH e
		 	 H H	
*
*
*
Exercício
Mostre que o seguintes argumento é válido:
Se este argumento for incorreto e válido, então nem todas as suas premissas são verdadeiras. Todas as suas premissas são verdadeiras. Ele é válido. Portanto ele é correto.
*
*
*
Solução
Identificando as Sentenças:
P: as premissas deste argumento são verdadeiras.
S: este argumento é correto.
V: este argumento é válido.
Formalizando:
		{(S ^ V)  P, P, V} ├ S
*
*
*
Exercício
Deus não existe. Pois, se Deus existisse a vida teria significado. Mas a vida não tem significado. Prove isso!
*
*
*
Quando tudo o mais falhar
EFQ: ex falso quodlibet ou regra da contradição
Podemos estar loucos, então qualquer literal é aceitável!
false 
	 H
*
*
*
Prova de EFQ
{P, P} ├ Q
Q .
 P P (prem.) 
 false 
	 Q (E)
*
*
*
Exemplo
Prove o Silogismo Disjuntivo, usando EFQ: {P v Q, P} ├ Q
*
*
*
Lógicas clássicas
Lógica minimal: {^v} x {IE}
Lógica intuicionista = 
	Lógica minimal U EFQ
*
*
*
Exercícios
{P (QR), P, Q} |= R
{P  Q, P} |= Q
{P  (Q ^ R), P} |= P ^ Q
{(P ^ Q)  (R ^ S), P, Q} |= S
{AB, C(DvE), DC, AE} |= (C  B)
{Cv(B  A), A  R, (B  R)  S} |= (C  S)