Independencia de premisa

En teoría de la prueba y matemáticas constructivas , el principio de independencia de premisa establece que si φ y ∃ x θ son oraciones en una teoría formal y φ → ∃ x θ es demostrable, entonces ∃ x (φ → θ) es demostrable. Aquí x no puede ser una variable libre de φ.

El principio es válido en lógica clásica. Su principal aplicación está en el estudio de la lógica intuicionista, donde el principio no siempre es válido.

En la lógica clásica

El principio de independencia de premisa es válido en la lógica clásica debido a la ley del medio excluido . Suponga que φ → ∃ x θ es demostrable. Entonces, si φ se cumple, hay una x que satisface φ → θ pero si φ no se cumple, entonces cualquier x satisface φ → θ . En cualquier caso, hay una x tal que φ → θ. Por tanto, ∃ x (φ → θ) es demostrable.

En lógica intuicionista

El principio de independencia de premisa no es generalmente válido en la lógica intuicionista (Avigad y Feferman 1999). Esto se puede ilustrar con la interpretación de BHK , que dice que para probar φ → ∃ x θ intuicionísticamente, se debe crear una función que tome una prueba de φ y devuelva una prueba de ∃ x θ . Aquí, la demostración en sí es una entrada a la función y puede usarse para construir x . Por otro lado, una prueba de ∃ x (φ → θ) primero debe demostrar una x particular , y luego proporcionar una función que convierta una prueba de φ en una prueba de θ en la que x tiene ese valor particular.

Como contraejemplo débil , suponga que θ ( x ) es un predicado decidible de un número natural tal que no se sabe si cualquier x satisface θ. Por ejemplo, θ puede decir que x es una prueba formal de alguna conjetura matemática cuya demostrabilidad se desconoce. Sea φ la fórmula ∃ z θ ( z ) . Entonces φ → ∃ x θ es trivialmente demostrable. Sin embargo, para demostrar ∃ x (φ → θ) , uno debe demostrar un valor particular de x tal que, si cualquier valor de xsatisface θ, entonces el elegido satisface θ. Esto no se puede hacer sin saber si ∃ x θ se cumple y, por lo tanto, ∃ x (φ → θ) no es demostrable intuicionísticamente en esta situación.

Referencias

• Jeremy Avigad y Solomon Feferman (1999). Interpretación funcional ("Dialectica") de Gödel (PDF) . en S. Buss ed., The Handbook of Proof Theory, Holanda Septentrional. págs. 337–405.