Teorema da dedução

Na lógica matemática, o teorema da dedução é um metateorema da lógica de primeira ordem. É a formalização da comum técnica de prova na qual uma implicação A → B é provada assumindo A e então derivando B a partir da premissa associada a resultados conhecidos. O teorema da dedução explica o porquê de provas de sentenças condicionais na matemática serem logicamente corretas. Embora isto tenha parecido por séculos "óbvio" para os matemáticos literalmente que provar B a partir de A, associado a um conjunto de teoremas era suficiente para provar a implicação A → B baseado nestes teoremas somente, foi deixado a Herbrand e Tarski mostrar (de forma independente entre os dois) que isto era logicamente correto no caso mais geral—outro exemplo,talvez, da lógica moderna "limpando" as práticas matemáticas.

O teorema da dedução afirma que se uma fórmula B é dedutível a partir de um conjunto de premissas $\Delta \cup \{A\}$ , onde A é uma fórmula fechada, então a implicação A → B é dedutível a partir de $\Delta$ . Nos símbolos, $\Delta \cup \{A\}\vdash B$ implica $\Delta \vdash A\to B\,$ . No caso especial, onde $\Delta$ é um conjunto vazio, o teorema da dedução mostra que $\{A\}\vdash B$ implica $\vdash A\to B$ .

O teorema da dedução é seguro para todas as teorias de primeira ordem com o sistema dedutivo para lógica de primeira ordem usual. No entanto, existem outros sistemas de primeira ordem nos quais novas regras de inferência são adicionadas e para o qual o teorema da dedução é falho.

A regra de dedução é uma propriedade importante dos sistemas de Hilbert, pois o uso desde metateorema leva a mais provas curtas do que seria possível sem o mesmo. Embora o teorema da dedução pudesse ser escolhido como uma regra primitiva de inferência em alguns sistemas, essa aproximação não é sempre seguida; ao invés disso, o teorema da dedução é obtido como uma regra admissível usando outros axiomas lógicos e o modus ponens. Em outros sistemas de prova formal, o teorema da dedução é às vezes escolhido como uma primitiva regra de inferência. Por exemplo, na dedução natural, o teorema da dedução é relançado como uma regra de introdução para a "→".

Exemplos de dedução

"Provar" o axioma 1:

- P 1.hipótese

Q 2.hipótese
P 3.Reiteração de 1
Q→P 4. dedução a partir de 2 e 3
P→(Q→P) 5.dedução a partir de 1 e 4, CQD.

"Provar" o axioma 2:

- P→(Q→R) 1. hipótese
P→Q 2. hipótese
P 3. hipótese
Q 4. modus ponens 3,2
Q→R 5. modus ponens 3,1
R 6. modus ponens 4,5
P→R 7. dedução a partir do 3 e do 6
(P→Q)→(P→R) 8. dedução a partir do 2 e do 7
(P→(Q→R))→((P→Q)→(P→R)) 9. dedução a partir do 1 e do 8 CQD

Usando o axioma 1 para mostrar que ((P→(Q→P))→R)→R:

- (P→(Q→P))→R 1. hipótese
P→(Q→P) 2. axioma 1
R 3. modus ponens 2,1
((P→(Q→P))→R)→R 4. dedução a partir do 1 e do 3 CQD

Regras virtuais de inferência

A partir dos exemplos, você pode observar que nós adicionamos 3 regras virtuais (ou extra e temporária) de inferência a nossa lógica axiomática normal. Estas são a "hipótese", a "reiteração" e a "dedução". As regras normais de inferência (ex: "modus ponens" e os vários axiomas) continuam utilizáveis.

1.Hipótese é o passo onde se adiciona uma premissa àquelas já existentes. Logo, se nosso passo anterior S foi deduzido como:

$E_{1},E_{2},...,E_{n-1},E_{n}\vdash S$ ,

então se acrescenta uma premissa H e temos:

$E_{1},E_{2},...,E_{n-1},E_{n},H\vdash H$ .

Isto é simbolizado por mover do n-ésimo nível de identação para o (n+1)-ésimo nível e dizendo:

- - - - S passo anterior
H hipótese

2.Reiteração é o passo onde se reutiliza um passo anterior. Na prática, isto só é necessário quando queremos pegar uma hipótese que não é a mais recente e usá-la como passo final antes do passo dedutivo.

3.Dedução é o passo onde se remove a hipótese mais recente (ainda ultilizável) e prefixa ela ao passo anterior. Isto é visto desidentando um nível como a seguir:

- - - - H hipótese
........(outros passos)
C (conclusão feita a partir de H)
H→C dedução

Convertendo de provas usando o metateorema da dedução para provas axiomáticas

Nas versões axiomáticas da lógica proposicional, algumas geralmente têm nelas esquemas axiomáticos (onde P,Q, e R são substituídos por quaisquer preposições):

O axioma 1 é: P→(Q→P)
O axioma 2 é : (P→(Q→R))→((P→Q)→(P→R))
O Modus ponens é: de P e P→Q inferimos Q

Estes esquemas axiomáticos são escolhidos para possibilitar que a derivação do teorema da dedução a partir dele seja feito mais facilmente. Logo, pode parecer que estamos pedindo a questão. Entretanto, eles podem ser justificados checando que eles são tautologias, usando as tabelas-verdade e que o modus ponens preserva a validadade deles.

A partir destes esquemas axiomáticos, podemos deduzir rapidamente o esquema do teorema P→P (reflexividade da implicação),o qual é usado abaixo:

1. (P→((Q→P)→P))→((P→(Q→P))→(P→P)) a partir do esquema axiomático 2 com P, (Q→P), P

2. P→((Q→P)→P) a partir do esquema axiomático 1 com P, (Q→P)

3. (P→(Q→P))→(P→P) a partir modus ponens aplicado ao passo 2 e ao passo 1

4. P→(Q→P) a partir do esquema axiomático 1, com P, Q

5. P→P a partir do modus ponens aplicado ao passo 4 e ao passo 3

Suponha que tenhamos Γ e H provando C, e que desejamos mostrar que Γ prova H→C. Para cada passo S na dedução no qual é uma premissa Γ (passo de reiteração) ou um axioma, podemos aplicar modus ponens em 1 e em S→(H→S), para conseguir H→S. Se o passo for H em si ( passo de hipótese), aplicamos o esquema de teorema para conseguir H→H. Se o passo for resultado da aplicação do modus ponens em A e em A→S, precisamos primeiramente nos certificar que estes foram convertidos em H→A e em H→(A→S) e então pegamos o axioma 2, (H→(A→S))→((H→A)→(H→S)) e aplicamos modus ponens para conseguir (H→A)→(H→S) e novamente para chegar em H→S. Ao final da prova, teremos H→C como pedido, porém, depende somente de Γ, e não de H. Logo, o passo dedutivo irá desaparecer, consolidado no passo anterior, o qual foi a conclusão derivada a partir de H.

Para minimizar a complexidade da prova, algum tipo de processamento deve ser feito antes da conversão. Alguns passos (além da conclusão), os quais não dependem de H, devem ser movidos para antes do passo de hipótese e desidentados em um nível. E qualquer outro passo desnecessário (os que não são usados para chegar a conclusão ou podem ser evitados), como as reiterações que não sejam a conclusão, devem ser eliminados.

Durante a conversão, pode ser útil colocar todas as aplicações do modus ponens no axioma 1 no começo da dedução (logo após o passo H→H). Quando se está convertendo o modus ponens, se A estiver fora do escopo de H, então será necessário aplicar ao axioma 1, A→(H→A), e modus ponens para chegar em H→A. De forma similar, se A→S estiver fora do escopo de H, aplica-se o axioma 1, (A→S)→(H→(A→S)), e modus ponens para conseguindo H→(A→S). Não será necessário fazer ambos, a não ser que o modus ponens seja a conclusão, porque, se estiver fora do escopo, então o modus ponens deve ser movido para antes de H e então para fora do escopo também.

Abaixo da correspondência de Curry-Howard, o processo de conversão acima para o metateorema da dedução é análogo ao processo de conversão termo a termo da lógica combinatória em cálculo lambda, onde 1 corresponde ao K combinador, e o axioma 2 corresponde ao S combinador. Perceba que o I combinador corresponde ao esquema de teorema P→P.

O teorema da dedução na lógica de predicados

O teorema da dedução também é válido na lógica de primeira ordem, da seguinte maneira:

Se T for uma teoria e F, G são fórmulas, sendo F fechada e T∪{F}├G, então T├F→G.

Aqui, o símbolo ├ significa "é consequência sintática de". Indicamos abaixo como a prova deste teorema da dedução difere daquele teorema da dedução do cálculo proposicional. Entre as versões mais comuns da noção de prova formal, aqui estão, em soma os esquemas de teorema do cálculo proposicional (ou o entendimento de que todas as tautologias do cálculo proposicional são feitas como esquemas de axioma para seu próprio direito), axiomas de quantificador, e, em soma ao modus ponens, uma regra de inferência adicional, conhecida como regra de generalização: "A partir de K, inferimos ∀vK".

Para converter uma prova de G a partir de T∪{F} para uma de F→G a partir de T, onde lida com os passos da prova de G, as quais são axiomas ou resultado da aplicação do modus ponens da mesma forma do que fazemos em provas da lógica proposicional. Passos os quais que resultam da aplicação da regra de generalização são tratados via o o quantificador axiomático (válido quando a variável v não for livre na fórmula H):

(H→K)→(H→∀vK).

Já que no nosso caso F é dita fechada, podemos pegar H para ser F. Este axioma permite deduzir F→∀vK a partir de F→K, o qual só é preciso quando a regra de generalização é aplicada a algum K na prova de G.

Exemplo de conversão

Para ilustrar como podemos converter uma dedução natural para uma forma axiomática de prova, vamos aplicar isto a tautologia Q→((Q→R)→R). Na prática, geralmente é suficiente saber que podemos fazer isso. Usamos normalmente a forma dedutiva-natural no lugar de uma prova axiomática muito mais extensa. Primeiramente, escrevemos a prova usando um método como o da dedução natural:

- Q 1.hipótese
Q→R 2.hipótese
R 3.modus ponens 1,2
(Q→R)→R 4.dedução a partir de 2 e de 3
Q→((Q→R)→R) 5. dedução a partir de 1 e de 4 CQD

Após isto, convertemos o interior da dedução em uma prova axiomática:

(Q→R)→(Q→R) 1. esquema de teorema (A→A)
((Q→R)→(Q→R))→(((Q→R)→Q)→((Q→R)→R)) 2. axioma 2
((Q→R)→Q)→((Q→R)→R) 3. modus ponens 1,2
Q→((Q→R)→Q) 4. axioma 1
Q 5. hipótese
(Q→R)→Q 6. modus ponens 5,4
(Q→R)→R 7. modus ponens 6,3
Q→((Q→R)→R) 8. dedução a partir de 5 e de 7 CQD

Então, convertemos o exterior da dedução em uma prova axiomática:

(Q→R)→(Q→R) 1. esquema de teorema (A→A)
((Q→R)→(Q→R))→(((Q→R)→Q)→((Q→R)→R)) 2. axioma 2
((Q→R)→Q)→((Q→R)→R) 3. modus ponens 1,2
Q→((Q→R)→Q) 4. axioma 1
[((Q→R)→Q)→((Q→R)→R)]→[Q→(((Q→R)→Q)→((Q→R)→R))] 5. axioma 1
Q→(((Q→R)→Q)→((Q→R)→R)) 6. modus ponens 3,5
[Q→(((Q→R)→Q)→((Q→R)→R))]→([Q→((Q→R)→Q)]→[Q→((Q→R)→R))]) 7. axioma 2
[Q→((Q→R)→Q)]→[Q→((Q→R)→R))] 8. modus ponens 6,7
Q→((Q→R)→R)) 9. modus ponens 4,8 CQD

Estes três passos podem ser especificados de forma sucinta usando a correspondência de Curry-Howard:

primeiramente, em cálculo lambda, a função f = λa. λb. b a é do tipo q → (q → r) → r
Após isto, por eliminação lambda em b, f = λa. s i (k a)
Então, por eliminação lambda de a, f = s (k (s i)) k

O teorema paraconsistente da dedução

Em geral, o teorema clássico da dedução é assegurado na lógica paraconsistente. Entretanto, o seguinte "teorema da dedução de duas vias" é assegurado em uma forma da lógica paraconsistente.

$\vdash E\rightarrow F$ se e somente se $(E\vdash Fand\neg F\vdash \neg E)$

isso requer a inferência contra-positiva para assegurar somado aos requerimentos do teorema clássico da dedução.