La paradoja de Curry

Paradoja matemática que lleva el nombre de Haskell Curry

La paradoja de Curry es una paradoja en la que una afirmación arbitraria F se prueba a partir de la mera existencia de una oración C que dice de sí misma "Si C , entonces F ". La paradoja requiere sólo unas pocas reglas de deducción lógica aparentemente inocuas. Dado que F es arbitraria, cualquier lógica que tenga estas reglas permite probar todo. La paradoja puede expresarse en lenguaje natural y en varias lógicas , incluidas ciertas formas de teoría de conjuntos , cálculo lambda y lógica combinatoria .

La paradoja recibe su nombre en honor al lógico Haskell Curry , quien escribió sobre ella en 1942. ^[1] También se la ha llamado paradoja de Löb en honor a Martin Hugo Löb , ^[2] 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 afirmaciones condicionales . La paradoja de Curry utiliza un tipo particular de oración condicional autorreferencial, como se demuestra en este ejemplo:

Si esta frase es cierta, entonces Alemania limita con China.

Aunque Alemania no tiene frontera con China , la oración de ejemplo es ciertamente una oración en lenguaje natural, por lo que se puede analizar su veracidad. La paradoja se desprende de este análisis. El análisis consta de dos pasos. En primer lugar, se pueden utilizar técnicas de prueba comunes en lenguaje natural para demostrar que la oración de ejemplo es verdadera [pasos 1 a 4 a continuación] . En segundo lugar, se puede utilizar la verdad de la oración para demostrar que Alemania tiene frontera con China [pasos 5 a 6] :

1. La oración dice: "Si esta oración es verdadera, entonces Alemania limita con China"   [repita la definición para que la numeración de los pasos sea compatible con la prueba formal]
2. Si la oración es verdadera, entonces es verdadera.   [obvio, es decir, una tautología ]
3. Si la oración es verdadera, entonces: si la oración es verdadera, entonces Alemania limita con China.   [reemplazar "es verdad" por la definición de la oración]
4. Si la oración es verdadera, entonces Alemania limita con China.   [Condición repetida del contrato]
5. Pero 4. es lo que dice la frase, por lo que efectivamente es verdad.
6. La oración es verdadera [por 5.] y [por 4.] : si es verdadera, entonces Alemania limita con China.
   Por lo tanto, Alemania limita con China.   [ modus ponens ]

Como Alemania no tiene frontera con China, esto sugiere que ha habido un error en uno de los pasos de la prueba. La afirmación "Alemania tiene frontera con China" podría ser reemplazada por cualquier otra afirmación, y la oración seguiría siendo demostrable. Por lo tanto, todas las oraciones parecen ser demostrables. Como la prueba utiliza solo métodos de deducción bien aceptados, y como ninguno de estos métodos parece ser incorrecto, esta situación es paradójica. ^[3]

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 que A es verdadera y luego, con esa suposición, se demuestra que B 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". Por lo tanto, suponer A es lo mismo que suponer "Si A , entonces B ". Por lo tanto, al suponer A , hemos supuesto tanto A como "Si A , entonces B ". Por lo tanto, B es verdadera, por modus ponens , y hemos demostrado "Si esta oración es verdadera, entonces 'Alemania limita con China' es verdadera" de la manera habitual, asumiendo la hipótesis y derivando la conclusión.

Ahora bien, como hemos demostrado que “si esta oración es verdadera, entonces ‘Alemania limita con China’ es verdadera”, podemos aplicar nuevamente el modus ponens, porque sabemos que la afirmación “esta oración es verdadera” es correcta. De esta manera, podemos deducir que Alemania limita con China.

En lógicas formales

Lógica oracional

El ejemplo de la sección anterior utilizó un razonamiento no formalizado, en lenguaje natural. La paradoja de Curry también ocurre en algunas variedades de lógica formal . En este contexto, muestra que si suponemos 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 dicha prueba formal es el siguiente. Para una explicación de la notación lógica utilizada en esta sección, consulte la lista de símbolos lógicos .

1. X  := ( X → Y )
   
   Suposición , el punto de partida, equivalente a "Si esta oración es verdadera, entonces Y "
2. X → X
   
   ley de identidad
3. X → ( X → Y )
   
   Sustituir el lado derecho de 2 , ya que X es equivalente a X → Y por 1
4. X → Y
   
   de 3 por contracción
5. incógnita
   
   sustituir 4 por 1
6. Y
   
   de 5 y 4 por modus ponens

Una prueba alternativa es mediante la ley de Peirce . Si X = X → Y , entonces ( X → Y ) → X . Esto, junto con la ley de Peirce (( X → Y ) → X ) → X y el modus ponens implica X y, posteriormente, Y (como en la prueba anterior).

La derivación anterior muestra que, si Y es una afirmación indemostrable en un sistema formal, entonces no existe ninguna afirmación X en ese sistema tal que X sea equivalente a la implicación ( X → Y ). En otras palabras, el paso 1 de la demostración anterior falla. Por el contrario, la sección anterior muestra que en lenguaje natural (no formalizado), para cada afirmación Y en lenguaje natural hay una afirmación Z en lenguaje natural tal que Z es equivalente a ( Z → Y ) en lenguaje natural. Es decir, Z es "Si esta oración es verdadera entonces Y ".

Teoría de conjuntos ingenua

Incluso si la lógica matemática subyacente no admite ninguna oración autorreferencial, ciertas formas de teoría de conjuntos ingenua aún son vulnerables a la paradoja de Curry. En las teorías de conjuntos que permiten la comprensión sin restricciones , podemos probar cualquier enunciado lógico Y examinando el conjunto . Entonces, se demuestra fácilmente que el enunciado es equivalente a . De esto, se puede deducir, de manera similar a las pruebas mostradas anteriormente. (" " significa "esta oración".) $${\displaystyle X\ {\stackrel {\mathrm {def} }{=}}\ \left\{x\mid (x\in x)\to Y\right\}.}$$ ${\displaystyle X\in X}$ ${\displaystyle (X\in X)\to Y}$ ${\displaystyle Y}$ ${\displaystyle X\in X}$

Por lo tanto, en una teoría de conjuntos consistente, el conjunto no existe para Y falso . Esto puede verse como una variante de la paradoja de Russell , pero no es idéntica. Algunas propuestas para la teoría de conjuntos han intentado lidiar con la paradoja de Russell no restringiendo la regla de comprensión, sino restringiendo las reglas de la lógica de modo que tolere 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. ${\displaystyle \left\{x\mid (x\in x)\to Y\right\}}$

Cálculo lambda con lógica mínima restringida

La paradoja de Curry puede expresarse mediante un cálculo lambda no tipificado , enriquecido con un cálculo proposicional implicacional . Para hacer frente a las restricciones sintácticas del cálculo lambda, deberá denotar la función de implicación que toma dos parámetros, es decir, el término lambda deberá ser equivalente a la notación infija habitual . ${\displaystyle m}$ ${\displaystyle ((mA)B)}$ ${\displaystyle A\to B}$

Se puede demostrar una fórmula arbitraria definiendo una función lambda , y , donde denota el combinador de punto fijo de Curry . Luego, por definición de y , la prueba lógica propositiva anterior se puede duplicar en el cálculo: ^{[4] [5] [6]} ${\displaystyle Z}$ ${\displaystyle N:=\lambda p.((mp)Z)}$ ${\displaystyle X:=({\textsf {Y}}N)}$ ${\displaystyle {\textsf {Y}}}$ ${\displaystyle X=(NX)=((mX)Z)}$ ${\displaystyle {\textsf {Y}}}$ ${\displaystyle N}$

$${\displaystyle {\begin{array}{cll}\vdash &((mX)X)&{\mbox{ by the minimal logic axiom }}A\to A\\\vdash &((mX)((mX)Z))&{\mbox{ since }}X=((mX)Z)\\\vdash &((mX)Z)&{\mbox{ by the theorem }}(A\to (A\to B))\vdash (A\to B){\mbox{ of minimal logic }}\\\vdash &X&{\mbox{ since }}X=((mX)Z)\\\vdash &Z&{\mbox{ by modus ponens }}A,(A\to B)\vdash B{\mbox{ from }}X{\mbox{ and }}((mX)Z)\\\end{array}}}$$

En el cálculo lambda de tipos simples , los combinadores de punto fijo no se pueden tipificar y, por lo tanto, no se admiten.

Lógica combinatoria

La paradoja de Curry también puede expresarse en lógica combinatoria , que tiene un poder expresivo equivalente al del cálculo lambda . Cualquier expresión lambda puede traducirse a lógica combinatoria, por lo que bastaría con una traducción de la implementación de la paradoja de Curry en el cálculo lambda.

El término anterior se traduce como en lógica combinatoria, por lo que ^[7] ${\displaystyle X}$ ${\displaystyle (r\ r)}$ $${\displaystyle r={\textsf {S}}\ ({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))\ ({\textsf {K}}Z);}$$ $${\displaystyle (r\ r)=((m(rr))\ Z).}$$

Discusión

La paradoja de Curry puede formularse en cualquier lenguaje que admita operaciones lógicas básicas que también permitan construir una función autorrecursiva como expresión. Dos mecanismos que respaldan 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 la referencia explícita a sus propias oraciones; sin embargo, el núcleo de los teoremas de incompletitud de Gödel es la observación de que se puede agregar una forma diferente de autorreferencia (véase el número de Gödel) .

Las reglas que se utilizan 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 . Estas se incluyen en la mayoría de los sistemas lógicos comunes, como la lógica de primer orden.

Consecuencias para alguna lógica formal

En la década de 1930, la paradoja de Curry y la paradoja de Kleene-Rosser relacionada , a partir de la cual se desarrolló la paradoja de Curry, ^{[8] [1]} desempeñaron un papel importante al demostrar que varios sistemas lógicos formales que permiten expresiones autorrecursivas son inconsistentes .

El axioma de comprensión irrestricta no está respaldado por la teoría de conjuntos moderna , y de esta manera se evita la paradoja de Curry.

Véase también

• La paradoja de Girard
• Lista de paradojas
• La paradoja de Richard
• Teoría de conjuntos de Zermelo-Fraenkel
• Combinador de punto fijo

Referencias

1. Curry, Haskell B. (septiembre de 1942). "La inconsistencia de ciertas lógicas formales". The Journal of Symbolic Logic . 7 (3): 115–117. doi :10.2307/2269292. JSTOR  2269292. S2CID  121991184.
2. Barwise, Jon ; Etchemendy, John (1987). El mentiroso: un ensayo sobre la verdad y la circularidad. Nueva York: Oxford University Press. p. 23. ISBN 0195059441. Recuperado el 24 de enero de 2013 .
3. Un ejemplo paralelo se explica en la Stanford Encyclopedia of Philosophy. Véase Shapiro, Lionel; Beall, Jc (2018). "Curry's Paradox". En Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .
4. El nombre aquí sigue la prueba de lógica oracional, excepto que se utiliza " Z " en lugar de " Y " para evitar confusiones con el combinador de punto fijo de Curry . ${\displaystyle {\textsf {Y}}}$
5. Gérard Huet (mayo de 1986). Estructuras formales para computación y deducción. Escuela de verano internacional sobre lógica de programación y cálculos de diseño discreto. Marktoberdorf. Archivado desde el original el 14 de julio de 2014.{{cite book}}: CS1 maint: location missing publisher (link)Aquí: p.125
6. Haskell B. Curry ; Robert Feys (1958). Lógica combinatoria I. Estudios de lógica y fundamentos de las matemáticas. Vol. 22. Ámsterdam: Holanda Septentrional.^{[ página necesaria ]}
7. ${\displaystyle (rr)}$ ${\displaystyle =}$ ${\displaystyle ({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))}$ ${\displaystyle \to }$ ${\displaystyle ({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}})({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {K}}Z({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))}$ ${\displaystyle \to }$ ${\displaystyle ({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}})({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))Z)}$ ${\displaystyle \to }$ ${\displaystyle ({\textsf {K}}m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)}$ ${\displaystyle \to }$ ${\displaystyle (m({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)}$ ${\displaystyle \to }$ ${\displaystyle (m({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))Z)}$ ${\displaystyle \to }$ ${\displaystyle (m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))Z)}$ ${\displaystyle \to }$ ${\displaystyle (m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)}$ ${\displaystyle =}$ ${\displaystyle ((m(rr))\ Z)}$
8. 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. S2CID  36344702.

Enlaces externos

• Beall, JC "La paradoja de Curry". En Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .
• Cantini, Andrea. "Paradojas y lógica contemporánea". En Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .
• Los pingüinos gobiernan el universo: una prueba de que los pingüinos gobiernan el universo, una discusión breve y entretenida de la paradoja de Curry.