Consequência Sintática Proposicional
$$\Huge H \vdash p $$
Uma regra, $\mathbf{R}$, especifica como certas hipóteses, $H$, produzem uma determinada conclusão, $p$:
$$\ndrule{H}{p}{\mathbf{R}}.$$
Encadeando várias regras obtém-se uma prova, apresentada numa tabela:
| Linha | Proposição | Regra | Hipóteses |
|---|---|---|---|
| 1 | $p_1$ | $\mathbf{R}_1$ | $L_1$ |
| $\vdots$ | |||
| n | $p_n$ | $\mathbf{R}_n$ | $L_n$ |
em que cada linha depende das anteriores não descartadas, por aplicação de uma regra.
Por fim, a relação entre as hipóteses não descartadas, $H$, e a conclusão na última linha, $p$, é representada por $H \vdash p$ e diz-se que $p$ é consequência sintática de $H$.
Definição (Teorema)
Uma proposição $p$ é um teorema se $\vdash p$, isto é, se $p$ pode ser demonstrada sem hipóteses.
Pode parecer estranho como fazer uma prova sem hipóteses. Mas já vimos como podemos “descartar” hipóteses usando implicações, pela regra $\ndIImpl: \cbr{ \sbr{p \vdash q} } \vdash p \to q$.
A continuação do exemplo da cadeia de implicações serve para ilustrar este ponto.
Exemplo. Cadeia de Implicações IV
$$\vdash p \to q \to \del{\del{q \to r} \to \del{p \to r}}$$
| Linha | Proposição | Regra | Hipóteses |
|---|---|---|---|
| 1 | $p \to q$ | $H$ | (8) |
| 2 | $q \to r$ | $H$ | (7) |
| 3 | $p$ | $H$ | (6) |
| 4 | $q$ | $\ndMP$ | 3, 1 |
| 5 | $r$ | $\ndMP$ | 4, 2 |
| 6 | $p \to r$ | $\ndIImpl$ | 3 - 5 |
| 7 | $(q \to r) \to (p \to r)$ | $\ndIImpl$ | 2 - 6 |
| 8 | $p \to q \to ((q \to r) \to (p \to r))$ | $\ndIImpl$ | 1 - 7 |
Este exemplo mostra uma prova em que todas as hipóteses foram descartadas. Formalmente seria $$ \emptyset \vdash \del{p \to q} \to ((q \to r) \to (p \to r)) $$ para indicar que o conjunto de hipóteses é vazio, $\emptyset$, mas pode ser abreviado para $$ \vdash \del{p \to q} \to ((q \to r) \to (p \to r)) $$
De acordo com a definição de teorema, $$ \del{p \to q} \to ((q \to r) \to (p \to r)) $$ é um teorema porque tem uma prova sem hipóteses “ativas”.