Sistema de Dedução Natural

Frank Coelho de Alcantara -2020   

Um pouco de história

O sistema de dedução natural foi desenvolvido por Gehard Gentzen, no final dos anos 1930, em busca de um sistema lógico matemático que fosse similar ao processo de dedução natural. O processo que seguimos quando queremos tomar uma decisão sobre qualquer coisa.

No mesmo trabalho Gentzen também apresentou ao mundo o Cálculo de Sequentes. No Sistema de Dedução Natural, existem regras de introdução e eliminação para cada operador e no cálculo de sequentes, regras de introdução..

O próprio Gentzen, parece ter acreditado que a diferença entre os dois é formal. Então, ao vemos o processo de dedução natural estamos vendo um superconjunto do cálculo de sequentes.

Definições, Alfabeto e Forma

Alfabeto $\Sigma_L=\{\neg, \vee, \wedge, \rightarrow, \vdash, \Rightarrow, \{ P, Q, R, S,...\}, (,)\}$

Representação.

$$\frac{P_1, P_2, ...P_n}{Q}$$

Uma estrutura em forma de fração que não tem nenhuma relação com a divisão. Na parte de cima, equivalente ao numerador, estará um conjunto de premissas, e chamaremos esta parte de contexto $\Gamma$, ou teoria $\Gamma$ e na parte de baixo, equivalente ao denominador, está a conclusão lógica destas premissas

Definições, Significado

Representação.

$$\frac{P_1, P_2, ...P_n}{Q}$$

Não podemos esquecer que tanto premissas, quanto conclusão, são premissas. A diferença é que as premissas serão consideradas como verdadeiras, até prova em contrário.

Lê-mos: dado o contexto $\Gamma$ formado por $P_1, P_2, ...P_n$ podemos concluir $Q$, ou podemos inferir $Q$, ou ainda $Q$ pode ser inferido a partir do contexto $\Gamma$.

Regras de Dedução / Inferência

Introdução da Conjunção

Introdução da Conjunção, ou simplesmente conjunção $(\text{Intro. } \wedge )$. Deduzimos $(P\wedge Q)$ já que $P$ e $Q$ já foram provadas como verdadeiras.

$$\frac{P; Q}{(P\wedge Q)}(\text{Intro. } \wedge)$$

Na dúvida, você pode verificar a tabela verdade e lembre-se que $P$ E $Q$ representam qualquer Fórmula Bem Formada. O ";" é dispensável.

Eliminação da Conjunção

Eliminação da Conjunção, simplificação $(\text{Elim. }\wedge )$. Uma vez que $P$ e $Q$ já foram provadas como verdadeiras Deduzimos $(P\wedge Q)$.

$$\frac{(P\wedge Q)}{P}\ \ \ \ \ \frac{(P\wedge Q)}{Q} (\text{Elim. } \wedge)$$

A regra tem duas formas e permite deduzir tanto $P$ quanto $Q$. Novamente, você pode usar a tabela verdade se preferir.

Exemplo 1

Considere o argumento: $(P\wedge Q); R \vdash (Q\wedge R)$ e prove sua veracidade.

Começamos listando as premissas da Teoria $\Gamma$: no caso $(P\wedge Q), R$.

  1. $(P\wedge Q)$     (premissa)
  2. $R$     (premissa)

Aplicamos a regra da simplificação $\frac{(P\wedge Q)}{Q}$ em 1.

  1. $(P\wedge Q)$    (premissa)
  2. $R$    (premissa)
  3. $Q$   $(\text{Elim. } \wedge)$

$R \equiv \top$ devido a ser uma premissa e provamos $Q \equiv \top$ podemos provar $(Q\wedge R)$ usando a Introdução da Conjunção.

  1. $(P\wedge Q)$    (premissa)
  2. $R$    (premissa)
  3. $Q$    $(\text{Elim. } \wedge)$
  4. $(Q\wedge R)$    $(\text{Intro. } \wedge)$ consequentemente teremos: $\frac{Q \ \ \ R}{(Q\wedge R)}$

Exercício 1

Considere o argumento: $(P \wedge Q) \wedge R, (S \wedge T) \vdash (Q \wedge S)$ e prove sua veracidade.

Lembre-se de começar sempre listando as premissas.

Regras da Negação Dupla

Eliminação da Negação Dupla ($\text{DNE}$): $$\frac{\neg \neg P}{P}$$

Introdução da Negação Dupla ($\text{DNI}$): $$\frac{P}{\neg \neg P}$$

Estas regras têm origem nas regras de equivalência.

Exemplo 2

Considere o argumento: $P;\neg \neg(Q\wedge R) \vdash (\neg \neg P\wedge \neg \neg R)$ e prove sua veracidade.

Começamos listando as premissas da Teoria $\Gamma$: no caso $P;\neg \neg(Q\wedge R)$.

  1. $P$ (premissa)
  2. $\neg \neg(Q\wedge R)$ (premissa)
  3. $\neg \neg P$ ($\text{DNI}$ em 1).
  4. $(Q\wedge R)$ ($\text{DNE}$ em 2).
  5. $R$ ($\text{Elim.} \wedge $ em 4).
  6. $\neg \neg R$ ($\text{DBI} \wedge$ em 5).
  7. $(\neg \neg P \wedge \neg \neg R)$ ($\text{Intro. } \wedge$ em 3 e 5).

Esta dedução cria um novo teorema, que pode ser útil, ou não. $$ \frac{$P;\neg \neg(Q\wedge R)}{(\neg \neg P\wedge \neg \neg R)}$$

Exercício 2

Considere o argumento: $P,\neg \neg(P \wedge R) \vdash \neg \neg P \wedge R$ e prove sua veracidade.

Eliminação da Implicação

A primeira eliminação da Implicação ($\text{MP}$) é conhecida como Modus Ponens: $$\frac{P; (P\rightarrow Q)}{Q}$$

A segunda eliminação da Implicação ($\text{MT}$) é conhecida como Modus Tollens: $$\frac{\neg Q; (P\rightarrow Q)}{\neg P}$$

Exemplo 3

Prove o seguinte argumento: $P, (P \rightarrow Q), P \rightarrow (Q\rightarrow R) \vdash R$

1. $P$ (Premissa))
2. $(P \rightarrow Q)$ (Premissa)
3. $P\rightarrow (Q\rightarrow R)$ (Premissa)
4. $Q$ ($\text{MP}$ em 1 e 2)
5. $(Q\rightarrow R))$ ($\text{MP} \wedge$ em 1 e 3)
6. $R$ ($\text{MP} \wedge$ em 4 e 5)

Exemplo 4

Prove o seguinte argumento: $P \rightarrow (Q \rightarrow R),P, \neg R \vdash \neg Q$

1. $P \rightarrow (Q \rightarrow R)$ (Premissa))
2. $P$ (Premissa)
3. $\neg R$ (Premissa)
4. $(Q\rightarrow R))$ ($\text{MP}$ em 2 e 1)
5. $\neg Q$ ($\text{MT} \wedge$ em 4,3)

Inclusão da Implicação

A inclusão da implicação é um processo de avaliação de hipóteses. Incluiremos um conjunto de hipóteses $P = \{P_1, P_2, P_3,...P_n\}$ de tal forma que se todas as hipóteses de $P$ forem verdadeiras. Podermos dizer que $P\rightarrow Q$.

Representaremos este processo na fórmula: $$\begin{smallmatrix} P_1 \\ : \\ \frac{P_n}{Q} \end{smallmatrix}$$

As hipóteses que criaremos para provar um $Q$ qualquer só podem ser usadas até que $Q$ seja provado e apenas para este fim.

Exemplo 5

Prove o argumento: $P \rightarrow Q \vdash \neg Q \rightarrow \neg P$

1. $P \rightarrow Q$ (Premissa)
2.
$\neg Q$ queremos encontrar $\neg Q \rightarrow \neg P$ podemos começar com $\neg Q$, se chegarmos a $\neg P$ poderemos provar $\neg Q \rightarrow \neg P$. Esta é nossa hipótese.
$\neg P$ Já temos o $P\rightarrow Q $ em 1. Como temos a hipótese $\neg Q$ podemos usar o $\text{MT}$ e encontrar o $\neg P$. Nossa hipótese é válida.
(Hipótese)
3. $\neg P \rightarrow \neg Q$ ($\text{MP}$ em 2)

A conclusão é escrita fora da ánálise de hipótese, por que a hipótese é verdadeira o que implica que $\neg Q$ é verdadeiro neste argumento.

Não podemos usar as inferências do conjunto de hipóteses fora da análise mas, podemos usar qualquer fórmula que esteja fora da análise para analisar a hipótese. Desde que esta fórmula não esteja em outra análise de hipótese.

Exemplo 6

Prove o argumento: $\neg B \rightarrow \neg A \vdash A \rightarrow \neg \neg B$

1. $\neg B \rightarrow \neg A$ (Premissa)
2.
a) $A$ queremos encontrar $A \rightarrow \neg \neg B$ podemos começar com $A$.
b) $\neg \neg A$ ($\text{DNI})$ Estamos tentando montar um $\text{MP}$ ou $\text{MT}$. Podemos fazer $P \equiv \neg B$ e $Q \equiv \neg A$ na premissa 1. E já temos o $\neg Q \equiv \neg \neg A$ então $\text{MT}$.
c) $\neg \neg B$ ($\text{MT})$ de 1 e b e encontramos o $\neg P \equiv \neg \neg B$. E nossa hipótese mostra que $A \rightarrow \neg \neg B$
(Hipótese)
3. $A \rightarrow \neg \neg B$ ($\text{MP}$ em a e c)

Introdução da Disjunção

Introdução da Disjunção, ou simplesmente adição $(\text{Intro. } \vee )$. Deduzimos $P\vee Q$ já que na disjunção basta que $P$ ou $Q$ sejam provadas como verdadeiras.

$$\frac{P}{(P\vee Q)} \ \ \ \ \ \frac{Q}{(P\vee Q)} (\text{Intro. } \vee)$$

O nome adição é antigo e remonta a época em que a disjunção era chamada de adição lógica e, neste caso a regra de inferência indica que você pode somar logicamente qualquer proposição verdadeira a qualquer Fórmulas Bem Formadas sem alterar a verdade desta fórmula.

Eliminação da Disjunção

Para eliminar $P\vee Q$, temos um problema. Não há como definir qual premissa é verdadeira, então precisamos utilizar a técnica da análise de hipóteses. E teremos que analisar as hipóteses para os dois operandos da disjunção.

A Eliminação da Disjunção ($\text{Elim. } \vee$) tem a forma:$$\frac{\begin{smallmatrix} & P_1 & Q_1 \\ & : & :\\ (P\vee Q) & R & R \end{smallmatrix}}{R}$$

Isto quer dizer que se encontramos uma $P\vee Q$ e conseguimos derivar $P$ em $R$ e $Q$ em $R$, então, podemos substituir $P\vee Q$ por $R$ na próxima linha.

Exemplo 7

Prove o argumento: $P \vee Q \vdash Q \vee P$

1. $P \vee Q$ (Premissa)
2.
a) $P$ queremos encontrar $Q \vee P$ E teremos que derivar tanto $P$ quanto $Q$.
b) $Q \vee P$ ($\text{Intro.} \vee)$ em (a) e derivamos $Q \vee P$ a partir de $P$.
(Hipótese $P$)
3.
c) $Q$ queremos encontrar $Q \vee P$ E teremos que derivar tanto $P$ quanto $Q$.
d) $Q \vee P$ ($\text{Intro.} \vee)$ em (c) e derivamos $Q \vee P$ a partir de $Q$.
(Hipótese $Q$)
3. $Q \vee P$ CQD

O que, felizmente é verdade, caso contrário teríamos que rever as propriedades da disjunção!

Exercício 3

Prove o argumento: $Q \rightarrow R\vdash (P\vee Q)\rightarrow (P\vee R)$

Exercício 4

Prove o argumento: $(P\vee Q) \vee R \vdash P \vee (Q \vee R)$

Fixação

Prove os seguintes argumentos:

permite otimização utilizando as características da linguagem.

Respostas dos Exercícios

Exercício 1

Considere o argumento: $(P \wedge Q) \wedge R, (S \wedge T) \vdash (Q \wedge S)$ e prove sua veracidade.

  1. $(P \wedge Q) \wedge R$(premissa)
  2. $(S \wedge T)$ (premissa)
  3. $(P\wedge Q)$ $(\text{Elim. } \wedge)$ aplicado em 1
  4. $Q$ $(\text{Elim. } \wedge)$ aplicado em 3
  5. $S$ $(\text{Elim. } \wedge)$ aplicada em 2
  6. $(Q\wedge S))$ $(\text{Intro. } \wedge)$ aplicada em 4 e 5

Exercício 2

Considere o argumento: $P,\neg \neg(P \wedge R) \vdash \neg \neg P \wedge R$ e prove sua veracidade.

Começamos listando as premissas da Teoria $\Gamma$: no caso $P,\neg \neg(P \wedge R)$.

1. $P$ (Premissa))
2. $\neg \neg(P \wedge R)$ (Premissa)
3. $\neg \neg P$ ($\text{DBI.}$ em 1)
4. $(P \wedge R)$ ($\text{DBE.}$ em 2)
5. $R$ ($\text{Elim.} \wedge$ em 4)
6. $\neg \neg P \wedge R$ ($\text{Intro.} \wedge$ em 3 e 5)

Esta dedução cria um novo teorema, que pode ser útil, ou não. $$ \frac{$P;\neg \neg(Q\wedge R)}{(\neg \neg P\wedge \neg \neg R)}$$

Exercício 3

Prove o argumento: $Q \rightarrow R\vdash (P\vee Q)\rightarrow (P\vee R)$

permite otimização utilizando as características da linguagem.

Material de apoio

Você pode baixar o material de apoio clicando aqui

Obras Citadas

AHO, A. V. et al. Compiladores: princípios, técnicas e ferramentas. 2º. ed. Boston, MA, USA: Pearson Education Inc. , 2007.
CASS, S. The 2016 Top Programming Languages. IEEE Spectrum, 2016. Disponível em: http://spectrum.ieee.org/computing/software/the-2016-top-programming-languages. Acesso em: 22 Set. 2016.