Dedução Natural Proposicional

$$H⊢p$$

Uma descoberta contra-intuitiva (dos filósofos Gregos).

Algumas deduções resultam apenas da forma (sintaxe, estrutura) das proposições envolvidas; o assunto tratado é irrelevante.

Por exemplo as duas deduções

• "Se está frio então levo o cachecol. Está frio. Portanto, levo o cachecol." e
• "Se o orçamento chumbar então o governo cai. O orçamento chumbou. Portanto, o governo cai."

são sobre assuntos muito diferentes mas partilham a mesma forma (estrutura):

$$\frac{a\to ba}{b}$$

Pretente-se definir e usar regras formais para deduzir consequências, $p$, dadas certas hipóteses, $H$, independentemente do assunto que está a ser tratado.

O que significa $H⊢p$?

• A hipótese, $H$, é um conjunto de proposições: expressões construídas a partir de átomos ligados por conectivos.
• A conclusão, $p$, é uma proposição.
• As regras dizem respeito aos conectivos e são de dois tipos: introdução ou eliminação.
• Uma prova de $p$ com hipóteses $H$ resulta de aplicar as regras linha-a-linha de forma que:
  1. Cada linha ou é uma hipótese de $H$ ou uma proposição que depende das linhas anteriores por aplicação de uma regra.
  2. Na última linha está a proposição $p$.
• A notação $H⊢p$ significa "existe uma prova de $p$ com hipóteses em $H$" ou que "$p$ é consequência (formal) das hipóteses $H$".

As proposições são definidas com conectivos e as regras estão organizadas por esses conectivos.

Existem regras para $\neg$, $\vee$, $\wedge$, etc

Além disso, há regras de introdução, em que a conclusão é formada por um certo conectivo, e regras de eliminação em que o conectivo está numa das hipóteses.