Teorema da dedução - Deduction theorem

Em lógica matemática , um teorema de dedução é um metateorema que justifica fazer provas condicionais - para provar uma implicação A  →  B , assumir A como uma hipótese e então proceder para derivar B - em sistemas que não têm uma regra de inferência explícita para isso. Existem teoremas dedução tanto para lógica proposicional e lógica de primeira ordem . O teorema da dedução é uma ferramenta importante nos sistemas de dedução do estilo de Hilbert porque permite escrever provas mais compreensíveis e geralmente muito mais curtas do que seria possível sem ele. Em certos outros sistemas formais de prova, a mesma conveniência é fornecida por uma regra de inferência explícita; por exemplo, a dedução natural chama isso de introdução de implicação .

Em mais detalhes, o teorema da dedução lógica proposicional afirma que se uma fórmula é dedutível de um conjunto de suposições, então a implicação é dedutível de ; em símbolos, implica . No caso especial em que é o conjunto vazio , a afirmação do teorema da dedução pode ser escrita de forma mais compacta como: implica . O teorema de dedução para a lógica de predicados é semelhante, mas vem com algumas restrições extras (que seriam satisfeitas, por exemplo, se fosse uma fórmula fechada ). Em geral, um teorema de dedução precisa levar em conta todos os detalhes lógicos da teoria em consideração, de modo que cada sistema lógico tecnicamente precisa de seu próprio teorema de dedução, embora as diferenças sejam geralmente menores. ${\ displaystyle B}$${\ displaystyle \ Delta \ cup \ {A \}}$${\ displaystyle A \ a B}$${\ displaystyle \ Delta}$${\ displaystyle \ Delta \ cup \ {A \} \ vdash B}$${\ displaystyle \ Delta \ vdash A \ to B}$${\ displaystyle \ Delta}$${\ displaystyle A \ vdash B}$${\ displaystyle \ vdash A \ to B}$${\ displaystyle A}$

O teorema da dedução vale para todas as teorias de primeira ordem com os sistemas dedutivos usuais para lógica de primeira ordem. No entanto, existem sistemas de primeira ordem nos quais novas regras de inferência são adicionadas para os quais o teorema da dedução falha. Mais notavelmente, o teorema da dedução falha em se sustentar na lógica quântica de Birkhoff-von Neumann , porque os subespaços lineares de um espaço de Hilbert formam uma rede não distributiva .

Exemplos de dedução

1. Axioma 1 "provar":

   • P 1. hipótese
   • Q 2. hipótese
     • P 3. reiteração de 1
   • Q → P 4. dedução de 2 a 3

   P → ( Q → P ) 5. dedução de 1 a 4 QED

2. Axioma 2 de "provar":

   • 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 de 3 a 6
   • ( P → Q ) → ( P → R ) 8. dedução de 2 a 7

   ( P → ( Q → R )) → (( P → Q ) → ( P → R )) 9. dedução de 1 a 8 QED

3. Usando o axioma 1 para mostrar (( 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 de 1 a 3 QED

Regras virtuais de inferência

A partir dos exemplos, você pode ver que adicionamos três regras de inferência virtuais (ou extras e temporárias) à nossa lógica axiomática normal. Estes são "hipótese", "reiteração" e "dedução". As regras normais de inferência (ou seja, "modus ponens" e os vários axiomas) permanecem disponíveis.

1. Hipótese é uma etapa em que se adiciona uma premissa adicional àquelas já disponíveis. Portanto, se sua etapa anterior S foi deduzida como:

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

em seguida, adiciona-se outra premissa H e obtém:

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

Isso é simbolizado movendo-se do n-ésimo nível de recuo para o n + 1-ésimo nível e dizendo

• S etapa anterior
  • Hipótese H

2. A reiteração é uma etapa em que se reutiliza uma etapa anterior. Na prática, isso só é necessário quando se deseja tomar uma hipótese que não é a hipótese mais recente e usá-la como a etapa final antes de uma etapa de dedução.

3. A dedução é uma etapa em que se remove a hipótese mais recente (ainda disponível) e a prefixa à etapa anterior. Isso é mostrado removendo a indentação de um nível da seguinte forma:

• Hipótese H
• ......... (outras etapas)
• C (conclusão tirada de H )

• Dedução H → C

Conversão da prova usando o metateorema de dedução para prova axiomática

Em versões axiomáticas de lógica proposicional, geralmente temos entre os esquemas de axioma (onde P , Q e R são substituídos por quaisquer proposições):

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

Esses esquemas de axioma são escolhidos para permitir que alguém derive o teorema de dedução deles facilmente. Portanto, pode parecer que estamos implorando por uma questão. No entanto, eles podem ser justificados verificando se são tautologias usando tabelas de verdade e se o modus ponens preserva a verdade.

A partir desses esquemas de axioma, pode-se rapidamente deduzir o esquema de teorema P → P (reflexividade de implicação) que é usado abaixo:

1. ( P → (( Q → P ) → P )) → (( P → ( Q → P )) → ( P → P )) do esquema axioma 2 com P , ( Q → P ), P
2. P → (( Q → P ) → P ) do esquema do axioma 1 com P , ( Q → P )
3. ( P → ( Q → P )) → ( P → P ) do modus ponens aplicado à etapa 2 e etapa 1
4. P → ( Q → P ) do esquema axioma 1 com P , Q
5. P → P do modus ponens aplicado à etapa 4 e etapa 3

Suponha que temos que Γ e H provar C , e queremos mostrar que Γ prova H → C . Para cada etapa S na dedução que é uma premissa em Γ (a passo reiteração) ou um axioma, podemos aplicar modus ponens para o axioma 1, S → ( H → S ), para obter H → S . Se o passo é H si (um passo hipótese), aplica-se o esquema teorema de obter H → H . Se a etapa é o resultado da aplicação do modus ponens a A e A → S , primeiro nos certificamos de que eles foram convertidos em H → A e H → ( A → S ) e, em seguida, tomamos o axioma 2, ( H → ( Um → S )) → (( H → a ) → ( H → S )), e aplicar o ponente modus para obter ( H → a ) → ( H → S ) e, em seguida, novamente para obter H → S . No final da prova, teremos H → C , conforme necessário, exceto que agora só depende de Γ, e não em H . Assim, o passo dedução desaparecerá, consolidados no passo anterior, que foi a conclusão derivado de H .

Para minimizar a complexidade da prova resultante, algum pré-processamento deve ser feito antes da conversão. Quaisquer etapas (exceto a conclusão) que realmente não dependem de H devem ser movidas para cima antes da etapa de hipótese e um nível desindentado. E quaisquer outras etapas desnecessárias (que não são usadas para obter a conclusão ou podem ser contornadas), como reiterações que não são a conclusão, devem ser eliminadas.

Durante a conversão, pode ser útil para colocar todas as aplicações de ponente modus para axioma 1 no início da dedução (direita após o H → H passo).

Quando a conversão de um modus ponente, se A está fora do âmbito de H , então será necessário aplicar um axioma, Um → ( H → Um ponente), e modus para obter H → Uma . Da mesma forma, se A → S está fora do escopo de H , aplique o axioma 1, ( A → S ) → ( H → ( A → S )) e modus ponens para obter H → ( A → S ). Não deve ser necessário fazer ambos, a menos que a etapa do modus ponens seja a conclusão, porque se ambos estiverem fora do escopo, então o modus ponens deve ter sido movido para cima antes de H e, portanto, também estar fora do escopo.

De acordo com a correspondência de Curry-Howard , o processo de conversão acima para o metateorema de dedução é análogo ao processo de conversão de termos de cálculo lambda para termos de lógica combinatória , onde o axioma 1 corresponde ao combinador K, e o axioma 2 corresponde ao combinador S . Note-se que os corresponde I combinadores no esquema teorema P → P .

Teoremas úteis

Se alguém pretende converter uma prova complicada usando o teorema da dedução em uma prova em linha reta sem usar o teorema da dedução, então provavelmente seria útil provar esses teoremas de uma vez por todas no início e, em seguida, usá-los para ajudar na conversão :

${\ displaystyle A \ a A}$

ajuda a converter as etapas da hipótese.

${\ displaystyle (B \ to C) \ to ((A \ to B) \ to (A \ to C))}$

ajuda a converter o modus ponens quando a premissa principal não depende da hipótese, substitui o axioma 2, evitando o uso do axioma 1.

${\ displaystyle (A \ to (B \ to C)) \ to (B \ to (A \ to C))}$

ajuda a converter o modus ponens quando a premissa menor não depende da hipótese, substitui o axioma 2, evitando o uso do axioma 1.

Esses dois teoremas em conjunto podem ser usados ​​no lugar do axioma 2, embora a prova convertida seja mais complicada:

${\ displaystyle (A \ to B) \ to ((B \ to C) \ to (A \ to C))}$

${\ displaystyle (A \ to (A \ to C)) \ to (A \ to C)}$

A lei de Peirce não é uma consequência do teorema da dedução, mas pode ser usada com o teorema da dedução para provar coisas que de outra forma não seria possível provar.

${\ displaystyle ((A \ para B) \ para A) \ para A}$

Também pode ser usado para obter o segundo dos dois teoremas que podem ser usados ​​no lugar do axioma 2.

Prova do teorema da dedução

Provamos o teorema da dedução em um sistema dedutivo de cálculo proposicional ao estilo de Hilbert.

Deixe ser um conjunto de fórmulas e e fórmulas, de tal forma . Queremos provar isso . ${\ displaystyle \ Delta}$${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle \ Delta \ cup \ {A \} \ vdash B}$${\ displaystyle \ Delta \ vdash A \ to B}$

Desde há uma prova de partir . Provamos o teorema por indução no comprimento de prova n ; assim, a hipótese de indução é que para qualquer , e tal que haja uma prova de de de comprimento até n , vale. ${\ displaystyle \ Delta \ cup \ {A \} \ vdash B}$${\ displaystyle B}$${\ displaystyle \ Delta \ cup \ {A \}}$${\ displaystyle \ Delta}$${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle B}$${\ displaystyle \ Delta \ cup \ {A \}}$${\ displaystyle \ Delta \ vdash A \ to B}$

Se n = 1, então é membro do conjunto de fórmulas . Portanto , qualquer um deles, caso em que é simplesmente derivável por substituição de p → p que é derivável dos axiomas, portanto, também ; ou está em , caso em que ; segue-se do axioma p → (q → p) com substituição que e, portanto, por modus ponens isso . ${\ displaystyle B}$${\ displaystyle \ Delta \ cup \ {A \}}$${\ displaystyle B = A}$${\ displaystyle A \ a B}$${\ displaystyle A \ a A}$${\ displaystyle \ Delta \ vdash A \ to B}$${\ displaystyle B}$${\ displaystyle \ Delta}$${\ displaystyle \ Delta \ vdash B}$${\ displaystyle \ Delta \ vdash B \ to (A \ to B)}$${\ displaystyle \ Delta \ vdash A \ to B}$

Agora, vamos assumir a hipótese de indução para provas de comprimento até n , e seja uma fórmula demonstrável com uma prova de comprimento n +1. Então, existem três possibilidades: ${\ displaystyle B}$${\ displaystyle \ Delta \ cup \ {A \}}$

1. ${\ displaystyle B}$é membro do conjunto de fórmulas ; neste caso procedemos como para n = 0.${\ displaystyle \ Delta \ cup \ {A \}}$
2. ${\ displaystyle B}$é obtido por uma substituição em uma fórmula φ. Então φ é provado com no máximo n passos, portanto, pela hipótese de indução , onde podemos escrever A e φ com variáveis ​​diferentes. Mas então podemos chegar a pela mesma substituição que é usada para derivar de φ; assim .${\ displaystyle \ Delta \ cup \ {A \}}$${\ displaystyle \ Delta \ vdash A \ to \ varphi}$${\ displaystyle A \ to \ varphi}$${\ displaystyle A \ a B}$${\ displaystyle B}$${\ displaystyle \ Delta \ vdash A \ to B}$
3. ${\ displaystyle B}$é alcançado usando o modus ponens. Então, há uma fórmula C tal que prova e , e o modus ponens é então usado para provar . As provas de e estão com no máximo n passos, e pela hipótese de indução temos e . Pelo axioma (p → (q → r)) → ((p → q) → (p → r)) com substituição segue-se que , e usando o modus ponens duas vezes temos .${\ displaystyle \ Delta \ cup \ {A \}}$${\ displaystyle C}$${\ displaystyle C \ a B}$${\ displaystyle B}$${\ displaystyle C}$${\ displaystyle C \ a B}$${\ displaystyle \ Delta \ vdash A \ a C}$${\ displaystyle \ Delta \ vdash A \ to (C \ to B)}$${\ displaystyle \ Delta \ vdash (A \ to (C \ to B)) \ to ((A \ to C) \ to (A \ to B))}$${\ displaystyle \ Delta \ vdash A \ to B}$

Assim, em todos os casos, o teorema é válido também para n +1, e por indução o teorema de dedução é provado.

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 na seguinte forma:

• Se T é uma teoria e F , G são fórmulas com F fechado e , então .${\ displaystyle T \ cup \ {F \} \ vdash G}$${\ displaystyle T \ vdash F \ rightarrow G}$

Aqui, o símbolo significa "é uma consequência sintática de." Indicamos a seguir como a prova desse teorema da dedução difere daquela do teorema da dedução no cálculo proposicional. ${\ displaystyle \ vdash}$

Nas versões mais comuns da noção de prova formal, existem, além dos esquemas de axioma do cálculo proposicional (ou o entendimento de que todas as tautologias do cálculo proposicional devem ser tomadas como esquemas de axioma em seu próprio direito), axiomas quantificadores , e, além do modus ponens , uma regra adicional de inferência , conhecida como regra de generalização : "De K , inferir ∀ vK ."

Para converter uma prova de G de T ∪ { F } para uma de F → G de T , trata-se de etapas da prova de G que são axiomas ou resultam da aplicação do modus ponens da mesma forma que para as provas em lógica proposicional. As etapas que resultam da aplicação da regra de generalização são tratadas por meio do seguinte axioma quantificador (válido sempre que a variável v não é livre na fórmula H ):

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

Uma vez que no nosso caso, F é assumida para ser fechado, que pode tomar H para ser F . Este axioma permite deduzir F → ∀ VK de F → K e generalização, que é apenas o que é necessário sempre que a regra de generalização é aplicada a alguns K na prova do G .

Na lógica de primeira ordem, a restrição de que F seja uma fórmula fechada pode ser relaxada, dado que as variáveis ​​livres em F não foram variadas na dedução de G de . No caso de uma variável livre v em F ter sido variada na dedução, escrevemos (o sobrescrito na catraca indicando que v foi variada) e a forma correspondente do teorema da dedução é . ${\ displaystyle T \ cup \ {F \}}$${\ displaystyle T \ cup \ {F \} \ vdash ^ {v} G}$${\ displaystyle T \ vdash (\ forall vF) \ rightarrow G}$

Exemplo de conversão

Para ilustrar como alguém pode converter uma dedução natural para a forma axiomática de prova, nós a aplicamos à tautologia Q → (( Q → R ) → R ). Na prática, geralmente é suficiente saber que podemos fazer isso. Normalmente usamos a forma dedutiva natural no lugar da prova axiomática muito mais longa.

Primeiro, escrevemos uma prova usando um método de dedução natural:

• Q 1. hipótese
  • Q → R 2. hipótese
  • R 3. modus ponens 1,2
• ( Q → R ) → R 4. dedução de 2 a 3

• Q → (( Q → R ) → R ) 5. dedução de 1 a 4 QED

Em segundo lugar, convertemos a dedução interna em uma prova axiomática:

• ( Q → R ) → ( Q → R ) 1. esquema do 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 de 5 a 7 QED

Terceiro, convertemos a dedução externa em uma prova axiomática:

• ( Q → R ) → ( Q → R ) 1. esquema do 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 QED

Essas três etapas podem ser declaradas sucintamente usando a correspondência Curry-Howard :

• primeiro, no cálculo lambda, a função f = λa. λb. ba tem tipo q → ( q → r ) → r
• segundo, por eliminação lambda em b, f = λa. si (ka)
• terceiro, por eliminação lambda em a, f = s (k (si)) k

Veja também

• Teorema de eliminação de corte
• Prova condicional
• Escovando
• Cálculo proposicional
• Lei de Peirce

Notas

Referências

• Carl Hewitt (2008), "ORGs for Scalable, Robust, Privacy-Friendly Client Cloud Computing", IEEE Internet Computing , 12 (5): 96–99, doi : 10.1109 / MIC.2008.107 . Setembro / outubro de 2008
• Kohlenbach, Ulrich (2008), teoria da prova aplicada: interpretações da prova e seu uso em matemática , Springer Monographs in Mathematics, Berlim, Nova 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 (2ª ed.), AK Peters , ISBN 978-1-56881-135-2

links externos

• Introdução à lógica matemática por Vilnis Detlovs e Karlis Podnieks Podnieks é um tutorial abrangente. Consulte a Seção 1.5.
• "Teorema da Dedução"