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 , onde A é uma fórmula fechada, então a implicação A → B é dedutível a partir de . Nos símbolos, implica . No caso especial, onde é um conjunto vazio, o teorema da dedução mostra que implica . 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 "→".