En teoría de la prueba y matemáticas constructivas , el principio de independencia de premisa (IP) 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 φ, mientras que θ puede ser un predicado que depende de ella.
La principal aplicación del principio es en el estudio de la lógica intuicionista , donde el principio no es generalmente válido. Su caso especial equivalente crucial se analiza a continuación. El principio es válido en la lógica clásica .
Como es habitual, se supone que el dominio del discurso está habitado. Es decir, parte de la teoría es al menos algún término. Para la discusión distinguimos uno de esos términos como . En la teoría de los números naturales, este papel lo puede desempeñar el número 7 . A continuación, φ y ψ denotan proposiciones que no dependen de x , mientras que θ es un predicado que puede depender de in.
Se establece fácilmente lo siguiente:
En el primer escenario, algo de x ligado a la premisa se reutiliza en la conclusión y, por lo general, no es el a priori el que lo valida. En el segundo escenario, el valor a en particular valida la conclusión del principio. Entonces, en ambos casos, alguna x valida la conclusión.
En tercer lugar , en contraste con los dos puntos anteriores, consideremos el caso en el que no se sabe cómo probar o rechazar φ. Un caso central es cuando φ es la fórmula ∃ z θ( z ) , en cuyo caso el antecedente φ → ∃ x θ se vuelve trivial: "Si θ es satisfactible, entonces θ es satisfacible". A modo de ilustración, admitamos que θ es un predicado decidible en aritmética, lo que significa que para cualquier número b dado , la proposición θ( b ) puede inspeccionarse fácilmente para determinar su valor de verdad. Más específicamente, θ expresará que x es el índice de una prueba formal de alguna conjetura matemática cuya demostrabilidad se desconoce. Ciertamente aquí, una forma de establecer ∃ x (φ → θ) sería proporcionar un índice particular x para el cual se pueda demostrar (entonces ayudado por el supuesto de que algún valor z satisface θ) que realmente satisface θ. Sin embargo, explicar tal x no es posible (todavía no y posiblemente nunca), ya que tal x codifica exactamente la prueba de una conjetura aún no probada o rechazada.
El ejemplo aritmético anterior proporciona lo que se llama un contraejemplo débil . La afirmación de existencia ∃ x (φ → θ) no puede demostrarse por medios intuicionistas: poder inspeccionar una x que valide φ → θ resolvería la conjetura.
Por ejemplo, consideremos el siguiente argumento clásico: o la conjetura de Goldbach tiene una prueba o no la tiene. Si no tiene una prueba, entonces suponer que tiene una prueba es absurdo y cualquier cosa se sigue; en particular, se sigue que tiene una prueba. Por lo tanto, existe algún índice de números naturales x tal que si se supone que la conjetura de Goldbach tiene una prueba, x es un índice de dicha prueba.
La cuestión también puede abordarse utilizando la interpretación BHK para demostraciones intuicionistas, que debe compararse con el cálculo de demostración clásico. BHK dice que una prueba de φ → ∃ x θ comprende una función que toma una prueba de φ y devuelve una prueba de ∃ x θ . Aquí las pruebas mismas pueden actuar como entrada para funciones y, cuando sea posible, pueden usarse para construir una x . Una prueba de ∃ x (φ → θ) debe entonces demostrar una x particular , junto con una función que convierta una prueba de φ en una prueba de θ en la que x tenga ese valor. En el cálculo de prueba, como en el contraejemplo débil, solo se puede dar una x adecuada utilizando más entradas vinculadas a φ susceptible.
De hecho, utilizando modelos violatorios, se ha establecido que la premisa φ → ∃ x θ no es suficiente para una prueba genérica de existencia tal como la otorga el principio.
Una implicación se fortalece cuando el antecedente puede debilitarse. Aquí son de interés las premisas en forma de enunciados negados, φ := ¬η.
Se ha establecido metateóricamente que si ¬η → ∃ x θ tiene una prueba en aritmética , entonces ∃ x (¬η → θ) también tiene una prueba.
No se sabe si esto también se aplica a las conocidas teorías de conjuntos . [1]
Para φ libre de cuantificadores existenciales, las teorías sobre la lógica intuicionista tienden a comportarse bien con respecto a reglas de esta naturaleza.
Como se señaló, el principio de independencia de la premisa para φ fijo y cualquier θ se deriva tanto de una prueba de φ como de un rechazo de la misma. Por tanto, asumiendo axiomáticamente la ley de la disyunción del tercero excluido , el principio es válido.
Por ejemplo, aquí ∃ x ((∃ y θ) → θ) siempre se cumple. Más concretamente, consideremos la proposición:
Esto es clásicamente demostrable de la siguiente manera: o existe un índice para una prueba de la conjetura de Goldbach, o no existe tal índice. Por un lado, si existe uno, cualquiera que sea ese índice también funciona como una x válida en la proposición anterior. Por otro lado, si no existe tal índice, entonces que tal índice exista también es contradictorio, y entonces por explosión se sigue cualquier cosa - y en particular se sigue que x=7 es un índice de una prueba de la conjetura de Goldbach. En ambos casos existe algún índice que valida la proposición.
Constructivamente, es necesario proporcionar una x tal que se pueda demostrar (luego con la ayuda de φ que se supone válida y también ∃ y θ para alguna y ) que θ se cumple para esa x . Clásicamente, basta sacar la misma conclusión de interés partiendo de dos hipótesis sobre φ. En el último marco, se afirma que existe algo de x en cualquier sentido, y la lógica no exige que se explique.
IP y el más corto ∃ x ((∃ y θ) → θ) tienen análogos en lógica proposicional. En el cálculo intuicionista, la forma finita
puede entenderse como que expresa que no se requiere información en la premisa para establecer qué proposición en un par de conjuntos implica. Porque esto se reduce al llamado principio de Dirk Gfully, más breve pero equivalente . El esquema implica el tercero excluido estrictamente más débil para proposiciones negadas (WLEM) a través de la forma intuicionista de consequentia mirabilis .
La lógica de Kreisel-Putnam , obtenida adoptando este esquema para proposiciones negadas, es decir, con , todavía tiene la propiedad de disyunción . La regla correspondiente es una regla admisible .
