Usuário(a):ArthurJorge97/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 em \Delta \vdash A \to B \ . No caso especial, onde \Delta é um conjunto vazio, o teorema da dedução mostra que \{A\} \vdash B implica em \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 ultilizá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 esboços 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 esboços 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 esboços axiomáticos, podemos deduzir rapidamente o esboço 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 esboço axiomático 2 com P, (Q→P), P 2. P→((Q→P)→P) a partir do esboço 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 esboço 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 esboço 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 esboço 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 esboços de teorema do cálculo proposicional (ou o entendimento de que todas as tautologias do cálculo proposicional são feitas como esboços 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. esboço 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. esboço 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 F and \neg F \vdash \neg E) isso requer a inferência contra-positiva para assegurar somado aos requerimentos do teorema clássico da dedução.

O teorema da resolução

O teorema da resolução é o inverso do teorema da dedução. Ele segue imediatamente do modus ponens, o qual é a regra de eliminação para implicação.

Notas

1. ^ Kleene 1967, p. 39, 112; Shoenfield 1967, p. 33
2. ^ Kohlenbach 2008, p. 148
3. ^ Hewitt 2008

Referências

* Carl Hewitt (2008), "ORGs for Scalable, Robust, Privacy-Friendly Client Cloud Computing", IEEE Internet Computing 12 (5): 96, doi:10.1109/MIC.2008.107. September/October 2008
* Kohlenbach, Ulrich (2008), Applied proof theory: proof interpretations and their use in mathematics, Springer Monographs in Mathematics, Berlin, New York: Springer-Verlag, ISBN 978-3-540-77532-4, MR 2445721
* Kleene, Stephen Cole (2002) [1967], Mathematical logic, New York: Dover Publications, ISBN 978-0-486-42533-7, MR 1950307
* Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic (3rd ed.), New York: Springer Science+Business Media, doi:10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6
* Shoenfield, Joseph R. (2001) [1967], Mathematical Logic (2nd ed.), A K Peters, ISBN 978-1-56881-135-2

Links externos

* Introduction to Mathematical Logic by Vilnis Detlovs and Karlis Podnieks Podnieks é um tutorial compreensível. Veja a Section 1.5.