En la teoría de la demostración y las matemáticas constructivas , el principio de independencia de las premisas (PI) establece que si φ y ∃ x θ son enunciados 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 el estudio de la lógica intuicionista , donde el principio no es válido en general. Su caso especial crucial equivalente 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 un término de este tipo como a . En la teoría de los números naturales, este papel puede ser desempeñado por 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 .
Lo siguiente se establece fácilmente:
En el primer caso, algún valor x de la premisa se reutiliza en la conclusión y, por lo general, no es el valor a priori el que lo valida. En el segundo caso, el valor a en particular valida la conclusión del principio. Por lo tanto, en ambos casos, algún valor x valida la conclusión.
En tercer lugar , ahora en contraste con los dos puntos anteriores, considere 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 satisfacible entonces θ es satisfacible". A modo de ilustración, supongamos que θ es un predicado decidible en aritmética, lo que significa que para cualquier número dado b 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 no se conoce. Ciertamente, en este caso, una manera de establecer ∃ x (φ → θ) sería proporcionar un índice particular x para el cual se pueda demostrar (con la ayuda de la suposición de que algún valor z satisface θ) que genuinamente 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 que aún no ha sido probada o rechazada.
El ejemplo aritmético anterior proporciona lo que se denomina un contraejemplo débil . La afirmación de existencia ∃ x (φ → θ) no se puede demostrar por medios intuicionistas: ser capaz de inspeccionar una x que valide φ → θ resolvería la conjetura.
Por ejemplo, consideremos el siguiente argumento clásico: o bien la conjetura de Goldbach tiene una prueba o bien no la tiene. Si no tiene una prueba, entonces suponer que tiene una prueba es absurdo y se sigue cualquier cosa, en particular, se sigue que tiene una prueba. Por lo tanto, existe algún índice de número natural x tal que si uno 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 pruebas intuicionistas, que deben compararse con el cálculo de pruebas 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 en sí mismas pueden actuar como entrada a 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 convierte una prueba de φ en una prueba de θ en la que x tiene ese valor. En el cálculo de pruebas - como en el contraejemplo débil - una x adecuada solo puede darse usando más entrada vinculada 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 concede 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 teorías de conjuntos conocidas . [1]
En el caso de φ 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 ha señalado, el principio de independencia de premisas para φ fijo y cualquier θ se desprende tanto de una prueba de φ como de un rechazo de la misma. Por lo tanto, suponiendo axiomáticamente la ley de la disyunción del tercio excluido, el principio es válido.
Por ejemplo, aquí siempre se cumple ∃ x ((∃ y θ) → θ) . Más concretamente, consideremos la proposición:
Esto se puede demostrar clásicamente de la siguiente manera: o bien existe un índice para una prueba de la conjetura de Goldbach, o bien no existe tal índice. Por un lado, si existe uno, entonces 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 también exista 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.
De manera constructiva, es necesario proporcionar una x tal que se pueda demostrar (con la ayuda de φ, que se supone válida, y también de ∃ y θ para algún y ) que θ se cumple para ese x . Clásicamente, basta con extraer la misma conclusión de interés cuando se parte de dos hipótesis sobre φ . En el último marco, se afirma que existe algún x de una u otra manera, y la lógica no exige que se lo explique.
IP y la forma más corta ∃ x ((∃ y θ) → θ) tienen análogos en la 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 conjunciones implica. Para , esto se reduce al llamado principio de Dirk Gently, más corto pero de hecho 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 al adoptar este esquema para proposiciones negadas, es decir con , todavía tiene la propiedad de disyunción . La regla correspondiente es una regla admisible .
