Consequência Sintática Proposicional

$H ⊢ p$

Uma regra, $R$ , especifica como certas hipóteses, $H$ , produzem uma determinada conclusão, $p$ :

$\frac{H}{p} (R) .$

Encadeando várias regras obtém-se uma prova, apresentada numa tabela:

Linha	Proposição	Regra	Hipóteses
1	$p_{1}$	$R_{1}$	$L_{1}$
	$⋮$
n	$p_{n}$	$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 ⊢ p$ e diz-se que $p$ é consequência sintática de $H$ .

Definição (Teorema)

Uma proposição $p$ é um teorema se $⊢ 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 $\to^{+} : {[p ⊢ q]} ⊢ p \to q$ .

A continuação do exemplo da cadeia de implicações serve para ilustrar este ponto.

Exemplo. Cadeia de Implicações IV

$⊢ p \to q \to ((q \to r) \to (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$	$MP$	3, 1
5	$r$	$MP$	4, 2
6	$p \to r$	$\to^{+}$	3 - 5
7	$(q \to r) \to (p \to r)$	$\to^{+}$	2 - 6
8	$p \to q \to ((q \to r) \to (p \to r))$	$\to^{+}$	1 - 7

Este exemplo mostra uma prova em que todas as hipóteses foram descartadas. Formalmente seria $\emptyset ⊢ (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 $⊢ (p \to q) \to ((q \to r) \to (p \to r))$

De acordo com a definição de teorema, $(p \to q) \to ((q \to r) \to (p \to r))$ é um teorema porque tem uma prova sem hipóteses "ativas".

Lógica e Computação

Consequência Sintática Proposicional