La paradoja de Curry

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

La paradoja recibe su nombre del 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 proposiciones de la forma "si A , entonces B " se denominan proposiciones condicionales . La paradoja de Curry utiliza un tipo particular de oración condicional autorreferencial, como se demuestra en este ejemplo:

Si esta afirmación es cierta, entonces Alemania limita con China.

Aunque Alemania no limita con China , la oración de ejemplo es sin duda una oración en lenguaje natural, por lo que se puede analizar su veracidad. La paradoja surge de este análisis. El análisis consta de dos pasos. Primero, se pueden utilizar técnicas comunes de demostración en lenguaje natural para probar que la oración de ejemplo es verdadera [pasos 1-4 a continuación] . Segundo, se puede utilizar la veracidad de la oración para probar que Alemania limita con China [pasos 5-6] .

La oración dice: "Si esta oración es verdadera, entonces Alemania limita con China" [repetir la definición para obtener una numeración de pasos compatible con la prueba formal ].
Si la oración es verdadera, entonces es verdadera. [obvio, es decir, una tautología ]
Si la oración es verdadera, entonces: si la oración es verdadera, entonces Alemania limita con China. [reemplazar "es verdadera" por la definición de la oración]
Si la frase es verdadera, entonces Alemania limita con China. [Contrato de condición repetida]
Pero 4. es lo que dice la oración, así que efectivamente es cierto.
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 ]

Dado que Alemania no limita con China, esto sugiere que ha habido un error en uno de los pasos de la demostración. La afirmación «Alemania limita con China» podría sustituirse por cualquier otra afirmación, y la oración seguiría siendo demostrable. Por lo tanto, todas las oraciones parecen ser demostrables. Dado que la demostración utiliza únicamente métodos de deducción bien aceptados, y dado que ninguno de estos métodos parece ser incorrecto, esta situación resulta paradójica. ^{[ 3 ]}

Prueba informal

El método estándar para demostrar oraciones condicionales (oraciones de la forma "si A , entonces B ") se denomina " prueba condicional ". En este método, para probar "si A , entonces B ", primero se asume A y luego, con esa suposición, se demuestra que B es verdadero.

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 completa, mientras que B es "Alemania limita con China". Por lo tanto, asumir A es lo mismo que asumir "Si A , entonces B ". En consecuencia, al asumir A , hemos asumido 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, ya que 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 proposicional

El ejemplo de la sección anterior utilizó razonamiento no formalizado en lenguaje natural. La paradoja de Curry también aparece en algunas variantes de la lógica formal . En este contexto, demuestra que si asumimos que existe una proposición formal ( X → Y ), donde X es equivalente a ( X → Y ), entonces podemos probar Y con una demostración formal. Un ejemplo de dicha demostración 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 .

X := ( X → Y )
suposición , el punto de partida, equivalente a "Si esta oración es verdadera, entonces Y "
X → X
ley de identidad
X → ( X → Y )
Sustituimos el lado derecho de 2 , ya que X es equivalente a X → Y por 1.
X → Y
de 3 por contracción
incógnita
Sustituir 4 por 1
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, por consiguiente, Y (como en la prueba anterior).

La derivación anterior muestra que, si Y es una proposición indemostrable en un sistema formal, entonces no existe ninguna proposició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 el lenguaje natural (no formalizado), para cada proposición Y en lenguaje natural existe una proposició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 ingenua de conjuntos

Aunque la lógica matemática subyacente no admita ninguna oración autorreferencial, 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 irrestricta , podemos demostrar cualquier enunciado lógico Y examinando el conjunto. $X\ {\stackrel {\mathrm {def} }{=}}\ \left\{x\mid (x\in x)\to Y\right\}.$ Entonces se demuestra fácilmente que la afirmación $X\in X$ es equivalente a $(X\in X)\to Y$ . A partir de esto, $Y$ puede deducirse, de forma similar a las demostraciones mostradas anteriormente. (" $X\in X$ " significa "esta oración".)

Por lo tanto, en una teoría de conjuntos consistente, el conjunto $\left\{x\mid (x\in x)\to Y\right\}$ No existe para Y falsa . Esto puede considerarse una variante de la paradoja de Russell , pero no es idéntica. 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 tolere la naturaleza contradictoria del conjunto de todos los conjuntos que no son miembros de sí mismos. La existencia de demostraciones como la anterior muestra que tal tarea no es tan sencilla, ya que al menos una de las reglas de deducción utilizadas en la demostración anterior debe omitirse o restringirse.

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

La paradoja de Curry puede expresarse en el cálculo lambda no tipado , enriquecido por el cálculo proposicional implicacional . Para lidiar con las restricciones sintácticas del cálculo lambda, $m$ denotará la función de implicación que toma dos parámetros, es decir, el término lambda. $((mA)B)$ será equivalente a la notación infija usual $A\to B$ .

Una fórmula arbitraria $Z$ Esto se puede demostrar definiendo una función lambda. $N:=\lambda p.((mp)Z)$ , y $X:=({\textsf {Y}}N)$ , dónde ${\textsf {Y}}$ denota el combinador de punto fijo de Curry . Entonces $X=(NX)=((mX)Z)$ por definición de ${\textsf {Y}}$ y $N$ , por lo tanto, la demostración lógica sentencial anterior puede duplicarse en el cálculo: ^{[ 4 ]}^{[ 5 ]}

${\begin{array}{cll}\vdash &((mX)X)&{\mbox{ por el axioma de lógica mínima }}A\to A\\\vdash &((mX)((mX)Z))&{\mbox{ ya que }}X=((mX)Z)\\\vdash &((mX)Z)&{\mbox{ por el teorema }}(A\to (A\to B))\vdash (A\to B){\mbox{ de lógica mínima }}\\\vdash &X&{\mbox{ ya que }}X=((mX)Z)\\\vdash &Z&{\mbox{ por modus ponens }}A,(A\to B)\vdash B{\mbox{ de }}X{\mbox{ y }}((mX)Z)\\\end{array}}$

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

Lógica combinatoria

La paradoja de Curry también puede expresarse en lógica combinatoria , que posee una capacidad expresiva equivalente a la 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 al cálculo lambda.

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

Discusión

La paradoja de Curry puede formularse en cualquier lenguaje que admita operaciones lógicas básicas y que también permita construir una función autorrecursiva como una 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 irrestricta 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 utilizadas en la construcción de la demostración son la regla de suposición para la demostración 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 cierta lógica formal

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

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

Véase también

Referencias

1 2 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 .
↑ Barwise, Jon ; Etchemendy, John (1987). El mentiroso: un ensayo sobre la verdad y la circularidad . Nueva York: Oxford University Press. pág. 23. ISBN 0195059441Consultado el 24 de enero de 2013 .
↑ Un ejemplo similar se explica en la Enciclopedia de Filosofía de Stanford. Véase Shapiro, Lionel; Beall, Jc (2018). "La paradoja de Curry" . En Zalta, Edward N. (ed.). Enciclopedia de Filosofía de Stanford . ISSN 1095-5054 . OCLC 429049174 .
↑ La nomenclatura aquí sigue la demostración de lógica sentencial, excepto quese usa " Z " en lugar de " Y " para evitar confusiones con el combinador de punto fijo de Curry. ${\textsf {Y}}$ .
↑ Gérard Huet (mayo de 1986). Estructuras formales para la computación y la deducción . Escuela Internacional de Verano sobre Lógica de Programación y Cálculos de Diseño Discreto. Marktoberdorf. Archivado del original el 14 de julio de 2014.{{cite book}}: CS1 mantenimiento: falta el editor de la ubicación ( enlace ) Aquí: pág. 125
↑ $(rr)$ $=$ $({\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)))$ $\to$ $({\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))))$ $\to$ $({\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)$ $\to$ $({\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)$ $\to$ $(m({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $\to$ $(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)$ $\to$ $(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)$ $\to$ $(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)$ $=$ $((m(rr))\ Z)$
↑ Curry, Haskell B. (junio de 1942). "Los fundamentos combinatorios de la lógica matemática". Journal of Symbolic Logic . 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.). Enciclopedia de filosofía de Stanford . ISSN 1095-5054 . OCLC 429049174 .
Cantini, Andrea. "Paradojas y lógica contemporánea" . En Zalta, Edward N. (ed.). Enciclopedia de filosofía de Stanford . ISSN 1095-5054 . OCLC 429049174 .
Los pingüinos dominan el universo: una prueba de que los pingüinos dominan el universo , un análisis breve y entretenido de la paradoja de Curry.

[:0-1] 1 2 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ág. 23. ISBN 0195059441Consultado el 24 de enero de 2013 .

[3] Un ejemplo similar se explica en la Enciclopedia de Filosofía de Stanford. Véase Shapiro, Lionel; Beall, Jc (2018). "La paradoja de Curry" . En Zalta, Edward N. (ed.). Enciclopedia de Filosofía de Stanford . ISSN 1095-5054 . OCLC 429049174 .

[4] La nomenclatura aquí sigue la demostración de lógica sentencial, excepto quese usa " Z " en lugar de " Y " para evitar confusiones con el combinador de punto fijo de Curry. ${\textsf {Y}}$ .

[5] Gérard Huet (mayo de 1986). Estructuras formales para la computación y la deducción . Escuela Internacional de Verano sobre Lógica de Programación y Cálculos de Diseño Discreto. Marktoberdorf. Archivado del original el 14 de julio de 2014.{{cite book}}: CS1 mantenimiento: falta el editor de la ubicación ( enlace ) Aquí: pág. 125

[6] $(rr)$ $=$ $({\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)))$ $\to$ $({\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))))$ $\to$ $({\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)$ $\to$ $({\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)$ $\to$ $(m({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $\to$ $(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)$ $\to$ $(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)$ $\to$ $(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)$ $=$ $((m(rr))\ Z)$

[7] Curry, Haskell B. (junio de 1942). "Los fundamentos combinatorios de la lógica matemática". Journal of Symbolic Logic . 7 (2): 49– 64. doi : 10.2307/2266302 . JSTOR 2266302. S2CID 36344702 .

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]