Lógica y computación: un punto de vista filosófico sobre el isomorfismo de Curry-Howard

El vínculo entre la lógica y la computación es más fuerte que nunca, especialmente desde el establecimiento del isomorfismo de Curry-Howard que especifica que proofspuede verse como programsy formulascomo del programa types.

Me preguntaba si podríamos encontrar algún texto que proporcione un punto de vista filosófico de la relación entre la lógica y la computación. No pude encontrar ningún documento al respecto.

Además, tengo algunas preguntas relacionadas:

1) Dado que la mayoría de los sistemas lógicos (p. ej., deducción natural intuicionista, cálculo secuente clásico) corresponden a sistemas computacionales (p. ej., cálculo λ simplemente tipificado, sistema F, lógica combinatoria...), ¿podemos decir que la lógica y la computación tienen la misma naturaleza y origen ? Muchas dificultades surgieron de la pregunta sobre la naturaleza de la Lógica, ¿la computación da una respuesta?

2) ¿Podemos decir que cualquier sistema que no comparte propiedades computacionales con un sistema computacional no es "una lógica"? (p. ej., sin teorema de eliminación de cortes, sin propiedad de confluencia/church-rosser)

EDITAR: Después de algunas investigaciones

Lo único que pude encontrar fue el trabajo del grupo francés LIGC , pero la mayoría de los artículos que escriben están solo en francés.

Parece que la mayoría de los trabajos que vinculan la filosofía y la computación se refieren a la Lógica Lineal (que surge del isomorfismo de Curry-Howard) y al Lambda-Calculus (que dan cuenta formal de los programas de computadora [funcionales]).

Si no me equivoco, Linear Logic toma la computación (eliminación de reglas de corte vista como evaluación de programas) como base para la lógica. Algunas propiedades de los programas como el teorema de eliminación de cortes, la confluencia o la propiedad de church-rosser, desde el punto de vista de la lógica, aseguran que nuestra lógica se comporte de forma coherente. Nos basamos en el comportamiento operativo de la lógica más que en el lenguaje o en fundamentos puramente filosóficos.

Parece que estos trabajos aún no han llegado a la comunidad inglesa, pero tal vez uno pueda encontrar algunos artículos en inglés escritos por los miembros del grupo.

Algunos documentos no demasiado técnicos (desafortunadamente en francés):

Con respecto a (1) la teoría de la computabilidad y la teoría de la prueba son ramas de la lógica (matemática) que parece ser la lógica que le interesa, por lo que no veo cómo alguien podría decir que no están relacionados. Pero recuerda que la noción de computabilidad es informal, la tesis de Church-Turing se basa en la idea informal de computabilidad. Con respecto a (2), eso depende de lo que quiera decir con "una lógica", si solo se refiere a cualquier sistema formal, entonces no. Se trata de un sistema formal deductivo axiomático muy básico como el sistema MU de Hofstadter. ¿Está utilizando "una lógica" como sinónimo de "un sistema formal"?
Pero también deberías pensar en qué es un 'sistema computacional'. Hay un argumento fácil para hacer que incluso un sistema básico como MU se puede usar para representar algún tipo de cálculo. Creo que Scott Aaronson en una conferencia sobre los límites de la computación hizo la broma de que es posible considerar cualquier sistema como un sistema computacional, incluso una tostadora haciendo tostadas, pero eso no significa que sea útil hacerlo. Asocia una de las reglas deductivas con la función sucesora y si puedes mostrar una prueba de que hay alguna derivación de alguna cadena en ese idioma, entonces puedes probar algo de aritmética.
@Not_Here (1) Leí que la "naturaleza" de la lógica no estaba clara. Tal vez estoy un poco desactualizado, pero algunos parecen pensar que la lógica depende de las ideas humanas (psicologismo), proviene de la razón, etc., mientras que la computación "parece" provenir de "la naturaleza". Pensé que de alguna manera podría proporcionar respuestas sobre la justificación de las reglas/leyes lógicas o los fundamentos de la Lógica, por ejemplo.
@Not_Here (2) Admito que no está claro. Yo mismo no estoy seguro, pero creo que me refiero a "lógica" de una manera informal, en la que pensamos cuando hablamos del razonamiento humano. Tal vez sigo teniendo una concepción ingenua de la Lógica pero me preguntaba si los sistemas lógicos sin ninguna correspondencia con un sistema como el cálculo lambda deberían gozar del mismo estatus que, digamos, la deducción natural. JY Girard dijo una vez que ve las lógicas sin corte-eliminación como autos sin motor.
¿La sintaxis trascendental de Girard, sobre la que preguntó antes, no se enfoca exactamente en este tipo de problemas: isomorfismo de Curry-Howard, justificación computacional para reglas lógicas, etc.? La segunda pregunta lo lleva demasiado lejos, creo. La lógica clásica, en la interpretación estándar, ciertamente no presta atención a la computabilidad, que parece ser un rasgo constructivista/teórico de la prueba. La lógica modal, la versión de Kripke de todos modos, tiene una semántica platónica aún más hinchada. Diría que uno puede destacar las lógicas fáciles de computar, pero no es necesario que lo sean.
@Conifold Tienes razón sobre la sintaxis trascendental, pero quiero opiniones alternativas sobre el tema. No quiero estar demasiado sesgado por los puntos de vista de Girard. En cuanto a la lógica clásica, hasta donde yo sé, sus propiedades computacionales están actualmente bajo investigación. Parece que todavía tiene algo de contenido computacional (realización clásica, cálculo lambda-µ de Parigot, cálculo lambda-µ-µ~ de Curien y Herbelin, etc.). Pero supongo que no es lo que quisiste decir con "interpretación estándar".
Parece que los usos clásicos de la lógica clásica prestaron poca atención a sus propiedades computacionales, cualesquiera que fueran, y el razonamiento no constructivo ya aparece en Euclides. Si es así, entonces nuestro ejemplo paradigmático ya muestra que la idea de lógica es distinta de la idea de algoritmo. Intuitivamente, incluso en contextos computacionales, la lógica no se trata tanto de la computación per se, sino de verificar la validez de un cómputo documentado, es normativa en una forma en que la computación no lo es.
la noción central de computabilidad es la noción intuitiva de procedimiento efectivo ; la preocupación central de la lógica es la noción intuitiva de consecuencia (lógica) . Turing nos dio un modelo formal del primero; aún nos falta un modelo formal del primero. consulte home.uchicago.edu/~wwtx yphilosofy.su.se/english/research/our-researchers/emeriti/… , y siga las bibliografías .

Respuestas (1)

Creo que tiene razón al estar impresionado con la correspondencia Curry-Howard. Es un isomorfismo detallado y extenso regla por regla y característica por característica. Esto sugiere fuertemente que la prueba y la computabilidad están estrechamente relacionadas. También estoy de acuerdo en que se subestima dentro de la filosofía de la lógica y que podemos y debemos permitir que informe nuestra comprensión de la lógica.

A los lógicos les gusta discutir sobre lógica. Estarán en desacuerdo incluso sobre cosas básicas como qué cuenta dar del concepto de validez . Pregúntele a Frege, Quine, Tarski, Davidson, Lewis, Prawitz, Etchemendy, McGee, Brandom y MacFarlane y obtendrá diez respuestas diferentes. También discutirán sobre si existe una única "lógica para gobernarlos a todos" y, de ser así, cuál es, o si el pluralismo lógico es defendible. Según Dummett, el intuicionismo es el único camino a seguir; para Read es lógica de relevancia, para Priest lógica paraconsistente, para Quine lógica clásica.

En el lado de la computabilidad de la valla, hay relativamente poca discusión sobre qué cuenta dar de la computabilidad. Existen algunas cuestiones sobre la forma precisa de enunciar la tesis de Church-Turing, si se aplica y cómo se aplica a las computadoras interactivas, y si se debe permitir que consideraciones tales como las leyes de la naturaleza determinen lo que podemos llamar un cálculo.

Entonces, dado que aparentemente entendemos la computabilidad bastante bien y la lógica un poco menos, parece tener sentido permitir que nuestra comprensión de la primera nos ayude con la segunda.

Es importante notar que la correspondencia Curry-Howard se extiende a la lógica clásica. Curry y Howard mismos no eran conscientes de esto cuando formularon la correspondencia. Partieron de la interpretación del intuicionismo de BHK y utilizaron el hecho de que las pruebas intuicionistas son constructivas para leer estas pruebas como recetas para un cálculo. Pero el trabajo posterior de científicos informáticos, incluidos Griffin, Parigot, Aschieri y otros, mostró que incluso la lógica clásica comparte la correspondencia. Lo que esto significa en la práctica es que existen interpretaciones computacionales de los sistemas clásicos que son normalizables y permiten extraer cálculos de las pruebas clásicas.

Esto no significa que cualquier oración clásica sea computable: claramente hay cualquier número de oraciones indecidibles. El alcance total de lo que es clásicamente computable sigue siendo un área de investigación. Pero sí significa que podemos prescindir de la idea simplista de que la lógica clásica no es constructiva mientras que la lógica intuicionista es constructiva. Las disyunciones clásicas, por ejemplo, pueden ser objeto de pruebas sin cortes, como señaló Girard en su artículo A New Constructive Logic: Classical Logic .

Para abordar sus preguntas específicas:

  1. De hecho, la lógica y la computabilidad están estrechamente relacionadas. Sin embargo, no son idénticos. Como mínimo, los cálculos se realizan a lo largo del tiempo y requieren algún tipo de motor informático. Las pruebas a menudo se consideran estructuras abstractas, aunque cualquier instancia de una prueba requerirá alguna forma física.

  2. La idea de que una lógica debe poseer algún aparato computable para calificar como lógica no es tan extraña como puede parecer. No excluiría la lógica clásica de la calificación. Sin embargo, es un requisito fuerte y podría ser cuestionado por aquellos que ven que la semántica de la lógica tiene primacía sobre la teoría de la prueba.

Como especulación final, sospecho que el vínculo entre la lógica y la computabilidad respalda la opinión de que debemos entender la lógica como una naturaleza esencialmente formal. Las explicaciones de la lógica que restan importancia a la formalidad tendrían más dificultades para explicar la conexión con la computabilidad. Además, algunas nociones muy amplias de lo que cuenta como validez podrían rechazarse sobre la base de que no pueden traducirse directamente en una forma computable.

Muy clara e interesante respuesta. También sentí que está "infravalorado" como dijiste. Ahora, tengo algunas preguntas y comentarios. (1) ¿Estamos seguros de que Lógica y computabilidad no son idénticas? ¿Entendemos realmente lo que es una demostración? Parece que las Lúdicas de Girard dan una naturaleza computacional/interactiva a las demostraciones, no sé si es relevante en nuestro contexto. (2) ¿Qué quiere decir con "naturaleza formal" (sobre lógica) (3) No tiene referencias que discutan la correspondencia desde un punto de vista filosófico?
Se podría argumentar que lo que es computable está limitado por las leyes de la naturaleza. Hay varios 'hiperordenadores' propuestos, es decir, dispositivos que trascienden lo que es computable por Turing, pero no se pueden construir en nuestro universo. La lógica suele entenderse como más abstracta. Por 'naturaleza formal' solo me refiero a explicaciones de la lógica en las que la formalidad es una característica esencial de lo que entendemos por lógica, más que un producto de la forma en que la estudiamos. Hay varias maneras diferentes en que la lógica puede ser formal. Si busca el Ph.D. de John MacFarlane. tesis en línea tiene una buena cuenta de esto...
En cuanto a las referencias filosóficas sobre la correspondencia Curry-Howard en sí, creo que hay muy pocas: la mayor parte de la discusión se centra en los aspectos técnicos.
Lógica y computación: un punto de vista filosófico sobre el isomorfismo de Curry-Howard
RespuestasAquíPolítica de privacidad1y, 0v