La paradoja de Curry es una paradoja en la que se prueba una afirmación arbitraria F a partir de la mera existencia de una oración C que dice de sí misma "Si C , entonces F ", requiriendo sólo unas pocas reglas de deducción lógica aparentemente inocuas. Dado que F es arbitrario, cualquier lógica que tenga estas reglas permite probar todo. La paradoja puede expresarse en lenguaje natural y en diversas lógicas , incluidas ciertas formas de teoría de conjuntos , cálculo lambda y lógica combinatoria .
La paradoja lleva el nombre del lógico Haskell Curry . También se le ha llamado la paradoja de Löb en honor a Martin Hugo Löb , [1] debido a su relación con el teorema de Löb .
En lenguaje natural
Las afirmaciones de la forma "si A, entonces B" se denominan reclamaciones condicionales . La paradoja de Curry usa un tipo particular de oración condicional autorreferencial, como se demuestra en este ejemplo:
Aunque Alemania no tiene fronteras con China , la oración de ejemplo ciertamente es una oración en lenguaje natural, por lo que se puede analizar la verdad de esa oración. La paradoja se deriva de este análisis. El análisis consta de dos pasos.
- Primero, se pueden usar técnicas comunes de prueba en lenguaje natural para demostrar que la oración de ejemplo es verdadera.
- En segundo lugar, la veracidad de la oración del ejemplo se puede utilizar para demostrar que Alemania limita con China. Debido a que Alemania no tiene fronteras con China, esto sugiere que ha habido un error en una de las pruebas.
La afirmación "Alemania limita con China" podría sustituirse por cualquier otra afirmación, y la frase aún podría demostrarse. Por tanto, cada frase parece demostrable. Debido a que la demostración usa solo métodos de deducción bien aceptados, y debido a que ninguno de estos métodos parece ser incorrecto, esta situación es paradójica. [2]
Prueba informal
El método estándar para probar oraciones condicionales (oraciones de la forma "si A, entonces B") se llama " prueba condicional ". En este método, para probar "si A, entonces B", primero se supone A y luego con esa suposición B se demuestra que es verdadera.
Para producir la paradoja de Curry, como se describe en los dos pasos anteriores, aplique este método a la oración "si esta oración es verdadera, entonces Alemania limita con China". Aquí A, "esta oración es verdadera", se refiere a la oración general, mientras que B es "Alemania limita con China". Entonces, asumir A es lo mismo que asumir "Si A, entonces B". Por lo tanto, al suponer A, hemos asumido tanto A como "Si A, entonces B". Por lo tanto, B es verdadera, por modus ponens , y hemos probado "Si esta oración es verdadera, entonces 'Alemania limita con China' es verdadera". de la forma habitual, asumiendo la hipótesis y derivando la conclusión.
Ahora, debido a que hemos probado "Si esta oración es verdadera, entonces 'Alemania limita con China' es verdadera", entonces podemos aplicar nuevamente el modus ponens, porque sabemos que la afirmación "esta oración es verdadera" es correcta. De esta forma, podemos deducir que Alemania limita con China.
Prueba formal
Lógica oracional
El ejemplo de la sección anterior utilizó un razonamiento en lenguaje natural no formalizado. La paradoja de Curry también ocurre en algunas variedades de lógica formal . En este contexto, muestra que si asumimos que hay una oración formal (X → Y), donde X en sí es equivalente a (X → Y), entonces podemos probar Y con una prueba formal. Un ejemplo de tal prueba formal es el siguiente. Para obtener una explicación de la notación lógica utilizada en esta sección, consulte la lista de símbolos lógicos .
- X: = (X → Y)suposición , el punto de partida, equivalente a "Si esta oración es verdadera, entonces Y"
- X → X
- X → (X → Y)sustituya el lado derecho de 2 , ya que X es equivalente a X → Y por 1
- X → Yde 3 por contracción
- Xsustituir 4 , por 1
- Yde 5 y 4 por modus ponens
Una prueba alternativa es a través de la ley de Peirce . Si X = X → Y entonces (X → Y) → X. Esto junto con la ley de Peirce ((X → Y) → X) → X y modus ponens implica X y posteriormente Y (como en la prueba anterior).
Por lo tanto, si Y es un enunciado indemostrable en un sistema formal, no hay un enunciado X en ese sistema tal que X sea equivalente a la implicación (X → Y). Por el contrario, la sección anterior muestra que en el lenguaje natural (no formalizado), para cada enunciado de lenguaje natural Y hay un enunciado de lenguaje natural Z tal que Z es equivalente a (Z → Y) en lenguaje natural. Es decir, Z es "Si esta oración es verdadera, entonces Y".
En casos específicos donde ya se conoce la clasificación de Y, se necesitan pocos pasos para revelar la contradicción. Por ejemplo, cuando Y es "Alemania limita con China", se sabe que Y es falso.
- X = (X → Y)suposición
- X = (X → falso)sustituir el valor conocido de Y
- X = (¬X ∨ falso)
- X = ¬Xidentidad
Teoría de conjuntos ingenua
Incluso si la lógica matemática subyacente no admite oraciones autorreferenciales, ciertas formas de teoría de conjuntos ingenua siguen siendo vulnerables a la paradoja de Curry. En las teorías de conjuntos que permiten una comprensión sin restricciones , podemos, no obstante, probar cualquier enunciado lógico Y examinando el conjunto
Asumiendo que tiene prioridad sobre ambos y , la prueba procede de la siguiente manera:
- Definición de X
- Sustitución de conjuntos iguales en membresía
- Adición de un consecuente a ambos lados de un bicondicional (de 2)
- Ley de concreción (de 1 y 3)
- Eliminación bicondicional (de 4)
- Contracción (de 5)
- Eliminación bicondicional (de 4)
- Modus ponens (a partir de 6 y 7)
- Modus ponens (a partir de 8 y 6)
El paso 4 es el único paso inválido en una teoría de conjuntos consistente. En la teoría de conjuntos de Zermelo-Fraenkel , se requeriría una hipótesis adicional que establezca que X es un conjunto, lo cual no es demostrable en ZF o en su extensión ZFC (con el axioma de elección ).
Por lo tanto, en una teoría de conjuntos consistente, el conjunto no existe para Y falsa . Esto puede verse como una variante de la paradoja de Russell , pero no es idéntico. Algunas propuestas de teoría de conjuntos han intentado abordar la paradoja de Russell no restringiendo la regla de comprensión, sino restringiendo las reglas de la lógica para que tolera la naturaleza contradictoria del conjunto de todos los conjuntos que no son miembros de sí mismos. La existencia de pruebas como la anterior muestra que tal tarea no es tan simple, porque al menos una de las reglas de deducción utilizadas en la prueba anterior debe omitirse o restringirse.
Cálculo lambda
La paradoja de Curry puede expresarse en un cálculo lambda no tipificado , enriquecido por una lógica mínima restringida . Para hacer frente a las restricciones sintácticas del cálculo lambda, Denotará la función de implicación tomando dos parámetros, es decir, el término lambda será equivalente a la notación infija habitual .
Una fórmula arbitraria se puede demostrar definiendo una función lambda , y , dónde denota el combinador de punto fijo de Curry . Luego por definición de y , por lo tanto, la prueba lógica enunciativa anterior se puede duplicar en el cálculo: [3] [4] [5]
En el cálculo lambda simplemente tipado , los combinadores de punto fijo no se pueden tipear y, por lo tanto, no se admiten.
Lógica combinatoria
La paradoja de Curry también se puede expresar en lógica combinatoria , que tiene un poder expresivo equivalente al cálculo lambda . Cualquier expresión lambda puede traducirse a lógica combinatoria, por lo que una traducción de la implementación de la paradoja de Curry en el cálculo lambda sería suficiente.
El término anterior se traduce en en lógica combinatoria, donde
por eso
Discusión
La paradoja de Curry se puede formular en cualquier lenguaje que admita operaciones lógicas básicas que también permitan construir una función auto-recursiva como expresión. Dos mecanismos que apoyan la construcción de la paradoja son la autorreferencia (la capacidad de referirse a "esta oración" desde dentro de una oración) y la comprensión sin restricciones en la teoría de conjuntos ingenua. Los lenguajes naturales casi siempre contienen muchas características que podrían usarse para construir la paradoja, al igual que muchos otros lenguajes. Por lo general, la adición de capacidades de metaprogramación a un lenguaje agregará las características necesarias. La lógica matemática generalmente no permite una referencia explícita a sus propias oraciones. Sin embargo, el corazón de los teoremas de incompletitud de Gödel es la observación de que se puede agregar una forma diferente de autorreferencia; ver el número de Gödel .
El axioma de comprensión irrestricta agrega la capacidad de construir una definición recursiva en la teoría de conjuntos. Este axioma no está respaldado por la teoría de conjuntos moderna .
Las reglas lógicas utilizadas en la construcción de la prueba son la regla de suposición para la prueba condicional, la regla de contracción y el modus ponens . Estos se incluyen en los sistemas lógicos más comunes, como la lógica de primer orden.
Consecuencias de alguna lógica formal
En la década de 1930, la paradoja de Curry y la paradoja de Kleene-Rosser relacionada jugaron un papel importante al mostrar que los sistemas lógicos formales basados en expresiones auto-recursivas son inconsistentes . Estos incluyen algunas versiones de cálculo lambda y lógica combinatoria .
Curry comenzó con la paradoja de Kleene-Rosser [7] y dedujo que el problema central podría expresarse en esta paradoja de Curry más simple. [8] [9] Su conclusión puede afirmarse diciendo que la lógica combinatoria y el cálculo lambda no pueden ser consistentes como lenguajes deductivos, mientras que aún permiten la recursividad.
En el estudio de la lógica combinatoria ilativa (deductiva) , Curry en 1941 [10] reconoció que la implicación de la paradoja implica que, sin restricciones, las siguientes propiedades de una lógica combinatoria son incompatibles:
- Completitud combinatoria . Esto significa que un operador de abstracción es definible (o primitivo) en el sistema, lo cual es un requisito del poder expresivo del sistema.
- Completitud deductiva . Este es un requisito de la derivabilidad, a saber, el principio de que en un sistema formal con implicación material y modus ponens, si Y es demostrable a partir de la hipótesis X, entonces también hay una prueba de X → Y. [11]
Resolución
Tenga en cuenta que, a diferencia de la paradoja del mentiroso o la paradoja de Russell, la paradoja de Curry no depende del modelo de negación que se utilice, ya que está completamente libre de negación. Por tanto, las lógicas paraconsistentes pueden seguir siendo vulnerables a esta paradoja, incluso si son inmunes a la paradoja del mentiroso.
Sin resolución en cálculo lambda
El origen de Alonzo Church 's cálculo lambda puede haber sido, '¿Cómo se puede resolver una ecuación, para proporcionar una definición de una función?'. Esto se expresa en esta equivalencia,
Esta definición es válida si hay una y solo una función que satisface la ecuación , pero no válido en caso contrario. Este es el núcleo del problema que Stephen Cole Kleene y luego Haskell Curry descubrieron con la lógica combinatoria y el cálculo Lambda.
La situación puede compararse con definir
Esta definición está bien siempre que solo se permitan valores positivos para la raíz cuadrada. En matemáticas, una variable cuantificada existencialmente puede representar múltiples valores, pero solo uno a la vez. La cuantificación existencial es la disyunción de muchas instancias de una ecuación. En cada ecuación hay un valor para la variable.
Sin embargo, en matemáticas, una expresión sin variables libres debe tener un solo valor. Entonces solo puede representar . Sin embargo, no existe una forma conveniente de restringir la abstracción lambda a un valor o de asegurar que existe un valor.
El cálculo de Lambda permite la recursividad pasando la misma función que se llama como parámetro. Esto permite situaciones donde tiene múltiples o ninguna solución para .
El cálculo lambda puede considerarse parte de las matemáticas si solo se permiten abstracciones lambda que representan una única solución a una ecuación. Otras abstracciones lambda son incorrectas en matemáticas.
La paradoja de Curry y otras paradojas surgen en el cálculo Lambda debido a la inconsistencia del cálculo Lambda considerado como un sistema deductivo . Véase también cálculo lambda deductivo .
Dominio de términos de cálculo lambda
El cálculo lambda es una teoría consistente en su propio dominio . Sin embargo, no es consistente agregar la definición de abstracción lambda a las matemáticas generales . Los términos lambda describen valores del dominio de cálculo lambda. Cada término lambda tiene un valor en ese dominio.
Al traducir expresiones de las matemáticas al cálculo lambda, el dominio de los términos del cálculo lambda no siempre es isomórfico al dominio de las expresiones matemáticas. Esta falta de isomorfismo es el origen de las aparentes contradicciones.
Resolución en idiomas no restringidos
Hay muchas construcciones del lenguaje que invocan implícitamente una ecuación que puede tener ninguna o muchas soluciones. La solución de sonido a este problema es vincular sintácticamente estas expresiones a una variable cuantificada existencialmente. La variable representa los valores múltiples de una manera significativa en el razonamiento humano común, pero también es válida en matemáticas.
Por ejemplo, un lenguaje natural que permite la función Eval no es matemáticamente consistente. Pero cada llamada a Eval en ese lenguaje natural puede traducirse a las matemáticas de una manera coherente. La traducción de Eval (s) a matemáticas es
Entonces, donde s = "Eval (s) → y",
Si y es falso, entonces x = x → y es falso, pero esto es una falsedad, no una paradoja.
La existencia de la variable x estaba implícita en el lenguaje natural. La variable x se crea cuando el lenguaje natural se traduce a las matemáticas. Esto nos permite utilizar lenguaje natural, con semántica natural, manteniendo la integridad matemática.
Resolución en lógica formal
El argumento en lógica formal comienza asumiendo la validez de nombrar (X → Y) como X. Sin embargo, este no es un punto de partida válido. Primero debemos deducir la validez de la denominación. El siguiente teorema se demuestra fácilmente y representa tal denominación:
En la declaración anterior, la fórmula A se denomina X. Ahora intente instanciar la fórmula con (X → Y) para A. Sin embargo, esto no es posible, ya que el alcance de está dentro del alcance de . El orden de los cuantificadores se puede invertir usando Skolemization :
Sin embargo, ahora la instanciacin da
que no es el punto de partida de la prueba y no conduce a una contradicción. No hay otras instancias para A que lleven al punto de partida de la paradoja.
Resolución en teoría de conjuntos
En la teoría de conjuntos de Zermelo-Fraenkel (ZFC), el axioma de comprensión irrestricta se reemplaza por un grupo de axiomas que permiten la construcción de conjuntos. Entonces, la paradoja de Curry no se puede establecer en ZFC. ZFC evolucionó en respuesta a la paradoja de Russell.
Ver también
- La paradoja de Russell
- La paradoja de Girard
- Paradoja de Kleene-Rosser
- Paradoja del mentiroso
- Lista de paradojas
- La paradoja de Richard
- Teoría de conjuntos de Zermelo-Fraenkel
- Combinador de punto fijo
- Cálculo lambda deductivo
- Dejemos expresión
Referencias
- ^ Barwise, Jon ; Etchemendy, John (1987). El mentiroso: un ensayo sobre la verdad y la circularidad . Nueva York: Oxford University Press. pag. 23. ISBN 0195059441. Consultado el 24 de enero de 2013 .
- ^ Un ejemplo paralelo se explica en la Enciclopedia de Filosofía de Stanford. Ver Shapiro, Lionel; Beall, Jc (2018). "Paradoja de Curry" . En Zalta, Edward N. (ed.). Enciclopedia de Filosofía de Stanford .
- ^ El nombre aquí sigue la prueba lógica enunciativa, excepto quese usa" Z " en lugar de " Y " para evitar confusión con el combinador de punto fijo de Curry.
- ^ Gérard Huet (mayo de 1986). Estructuras formales de cálculo y deducción . Escuela Internacional de Verano sobre Lógica de Programación y Cálculos de Diseño Discreto. Marktoberdorf. Archivado desde el original el 14 de julio de 2014. Aquí: p.125
- ^ Haskell B. Curry ; Robert Feys (1958). La lógica combinatoria I . Estudios de Lógica y Fundamentos de las Matemáticas. 22 . Ámsterdem: Holanda Septentrional.[ página necesaria ]
- ^
- ^ Kleene, SC y Rosser, JB (1935). "La inconsistencia de ciertas lógicas formales". Annals of Mathematics . 36 (3): 630–636. doi : 10.2307 / 1968646 . JSTOR 1968646 .
- ^ Curry, Haskell B. (junio de 1942). "Los fundamentos combinatorios de la lógica matemática". Revista de lógica simbólica . 7 (2): 49–64. doi : 10.2307 / 2266302 . JSTOR 2266302 .
- ^ Curry, Haskell B. (septiembre de 1942). "La inconsistencia de ciertas lógicas formales". El diario de la lógica simbólica . 7 (3): 115-117. doi : 10.2307 / 2269292 . JSTOR 2269292 .
- ^ Curry, Haskell B. (1941). "La paradoja de Kleene y Rosser" . Transacciones de la American Mathematical Society . 50 (3): 454–516. doi : 10.1090 / S0002-9947-1941-0005275-6 . Señor 0005275 . Consultado el 24 de enero de 2013 .
- ^ Stenlund, Sören (1972). Combinadores, términos λ y teoría de la prueba . Dordrecht: D. Reidel . pag. 71. ISBN 978-9027703057.
enlaces externos
- Beall, JC "La paradoja de Curry" . En Zalta, Edward N. (ed.). Enciclopedia de Filosofía de Stanford .
- Cantini, Andrea. "Paradojas y lógica contemporánea" . En Zalta, Edward N. (ed.). Enciclopedia de Filosofía de Stanford .
- Los pingüinos gobiernan el universo: una prueba de que los pingüinos gobiernan el universo , una breve y entretenida discusión sobre la paradoja de Curry.