Indepêndencia de premissas
 | As referências deste artigo necessitam de formatação. (Julho de 2015) |
Na teoria da prova e matemática construtiva, o princípio da independência de premissas afirma que, se φ e ∃ x θ são sentenças em uma teoria formal e φ → ∃ x θ é demonstrável, então ∃ x (φ → θ) é demonstrável. Neste caso x não pode ser uma variável livre de φ.
A sua principal aplicação é no estudo da lógica intuicionística, onde o princípio nem sempre é válido.
Na Lógica Clássica[editar | editar código-fonte]
O princípio da independência de premissas é valido na lógica clássica devido à lei do terceiro excluído. Suponha que φ → ∃ x θ é demonstrável. Então, se φ se verifica, há um x satisfazendo φ → θ mas se φ não se verifica, então, qualquer x satisfaz φ → θ. Em qualquer um dos casos, há algum x tal que φ → θ. Assim ∃ x (φ → θ) é demonstrável.
Na Lógica Intuicionística[editar | editar código-fonte]
O princípio da independência de premissas geralmente não é válido na lógica intuicionística (Avigad e Feferman 1999). Isto pode ser ilustrado pela interpretação BHK, que diz que, a fim de provar φ → ∃ x θ intuicionisticamente, é preciso criar uma função que pega uma prova de φ e retorna uma prova de ∃ x θ. Aqui a própria prova é uma entrada para a função e pode ser utilizada para construir x. Por outro lado, uma prova de ∃ x (φ → θ) deve primeiramente demonstrar um x especial, e em seguida, proporcionar uma função que converte uma prova de φ numa prova de θ em que x tem esse valor especial.
Como um contraexemplo fraco, suponha θ (x) é algum predicado decidível de um número natural de forma que não se sabe se algum x satisfaz θ. Por exemplo, θ pode dizer que x é uma prova formal de alguma conjectura matemática cuja prova não é conhecida. Se φ é a fórmula ∃ z θ(z). Então φ → ∃ x θ é demonstrável de forma trivial. No entanto, para provar ∃ x (φ → θ), deve ser demonstrado um valor especial de x, tal que, se qualquer valor de x satisfaz θ, então o valor que foi escolhido satisfaz θ. Isso não pode ser feito sem o prévio conhecimento de que saibamos ∃ x θ, assim, ∃ x (φ → θ) não é intuicionisticamente demonstrável nesta situação.
Referências[editar | editar código-fonte]
- Jeremy Avigad and Solomon Feferman (1999). Gödel's functional ("Dialectica") interpretation (PDF). [S.l.]: in S. Buss ed., The Handbook of Proof Theory, North-Holland. pp. 337–405