¿Es la lógica de primer orden (FOL) la única lógica fundamental?

Estoy lejos de ser un experto en el campo de la lógica matemática, pero he estado leyendo sobre el trabajo académico invertido en los fundamentos de las matemáticas, tanto en un sentido histórico como objetivo; y aprendí que todo parece reducirse a una formulación -axiomática- propia de la teoría de conjuntos.

También parece que todas las teorías de conjuntos (incluso si vienen en sabores ontológicamente diferentes, como las que persiguen el " enfoque iterativo " como ZFC, versus el " enfoque estratificado " -inspirado en la teoría de tipos de Russell y Whitehead formulada por primera vez en sus Principia - como NFU de Quine o ST de Mendelson) se construyen como colecciones de axiomas expresados ​​en un lenguaje común , que invariablemente implica una lógica de predicado de primer orden subyacente aumentada con el símbolo de relación binaria de pertenencia al conjunto. De esto se deduce que FOL constituye la ( necesaria ) "plantilla formal" en matemáticas, al menos desde una perspectiva fundacional.

La justificación de este mismo hecho, es la razón detrás de esta pregunta. Todo lo que he leído sobre las virtudes metalógicas de FOL y las propiedades de sus "extensiones" podría resumirse en las siguientes declaraciones:

  • FOL es completo ( Gödel, 1929 ), compacto y sólido, y todas sus formalizaciones particulares como sistemas deductivos son equivalentes ( Lindström, 1969 ). Eso significa que, dada una colección (consistente) de axiomas encima de un sistema deductivo FOL, el conjunto de todos los teoremas que son demostrables sintácticamente, son satisfechos semánticamente por al menos un modelo de los axiomas. La especificación de los axiomas conlleva absolutamente todas sus consecuencias; y el hecho de que todo sistema deductivo de primer orden sea equivalente sugiere que FOL es una estructura formal independiente del contexto (es decir, objetiva).
  • Por otro lado, el teorema de Löwenheim-Skolem implica que FOL no puede caracterizar categóricamente estructuras infinitas, por lo que toda teoría de primer orden satisfecha por un modelo de una cardinalidad infinita particular también se satisface por múltiples modelos adicionales de cualquier otra cardinalidad infinita. Se explica que esta característica de no categorización se debe a la falta de poder expresivo de FOL.
  • Los resultados de categoricidad que las teorías basadas en FOL no pueden lograr, se pueden obtener en un marco de lógica de segundo orden (SOL). Los ejemplos abundan en las matemáticas ordinarias, como el axioma Least Upper Bound , que permite la definición del sistema de números reales hasta el isomorfismo . Sin embargo, SOL no logra verificar un análogo a los resultados de completitud de FOL, por lo que no existe una coincidencia general entre la demostrabilidad sintáctica y la satisfacibilidad semántica (en otras palabras, no admite un cálculo de prueba completo). Eso significa que, incluso si una colección escogida de axiomas es capaz de caracterizar categóricamente una estructura matemática infinita, existe un conjunto infinito de wff satisfechas por el modelo único de los axiomas que no pueden derivarse por deducción .
  • El cisma sintáctico-semántico en SOL también implica que no existe tal cosa como una formulación equivalente de sistemas deductivos potenciales, como es el caso en FOL y establecido por el teorema de Lindström. Uno de los resultados de este hecho es que se debe especificar el dominio sobre el cual se extienden las variables de segundo orden , de lo contrario quedaría mal definido. Si se permite que el dominio sea el conjunto completo de subconjuntos del dominio de variables de primer orden, la semántica estándar correspondienteinvolucran las propiedades formales mencionadas anteriormente (suficiente poder expresivo para establecer resultados de categoricidad e incompletitud de sistemas deductivos potenciales no equivalentes). Por otro lado, a través de una definición apropiada de dominios de segundo orden para el rango de variables de segundo orden, la lógica resultante exhibe una semántica no estándar (o semántica de Henkin ) que puede demostrarse que es equivalente a FOL de ordenación múltiple ; y como FOL de clasificación simple, verifica las mismas propiedades metalógicas enunciadas al principio (y por supuesto, su falta de poder expresivo).
  • La extensión de la cuantificación sobre variables de sucesivos órdenes superiores puede formalizarse, o incluso eliminarse la distinción entre variables individuales (de primer orden) y predicados; en cada caso, se obtiene -para cada N- una Lógica de Orden N (NOL), y Lógica de Orden Superior (HOL), respectivamente. Sin embargo, se puede demostrar ( Hintikka, 1955 ) que cualquier oración en cualquier lógica sobre FOL con semántica estándar es equivalente (de manera efectiva) a una oración en SOL completo, usando clasificación múltiple.
  • Todo esto apunta al hecho de que la distinción fundamental, en términos lógicos, se encuentra entre FOL (ya sea de clasificación única o múltiple) y SOL (con semántica estándar ). O lo que parece ser el caso, los fundamentos lógicos de cada teoría matemática deben ser no categóricos o carecer de un cálculo de prueba completo, sin nada en medio de esa compensación.

¿Por qué, entonces, FOL se elige invariablemente como la lógica subyacente sobre la cual se establecen los axiomas teóricos de conjuntos, en cualquier formalización potencialmente fundacional de las matemáticas?

Como he dicho, no soy un experto en este tema, y ​​simplemente estoy interesado en estos temas. Lo que escribí aquí es un resumen de lo que asumo que entendí de lo que leí (aunque personalmente me inclino en contra de las personas que hablan de lo que no entienden completamente). En este sentido, estaría muy complacido si alguna respuesta a esta pregunta implica una rectificación de cualquier afirmación que resultó ser incorrecta.

A partir de sus elaboraciones, bien podría ser que conozca los siguientes hilos o su contenido, pero señalaré este hilo en el tablero de matemáticas y especialmente los enlaces publicados allí. Además, una pregunta que hice aquí terminó siendo más o menos sobre este tema también.
Lo he estado pensando, y la falta de respuesta de la comunidad de filósofos podría deberse a que esta es una pregunta demasiado matemática, por lo que debería intentar volver a publicarla en Math.SE. He estado visitando periódicamente la red SE desde hace algún tiempo debido a la calidad de las respuestas dadas, pero hace solo unos días decidí unirme, por lo que desconozco bastante todas las reglas y capacidades del sitio. . Entonces, puedo preguntarle: 1) ¿Hay alguna manera de "migrar" una pregunta de un sitio de preguntas y respuestas a otro en la red sin volver a publicar "manualmente" (es decir, copiar y pegar)?
2) Mi experiencia reciente en el sitio de física aparentemente sugiere que las preguntas demasiado largas y elaboradas que no exhiben una respuesta de libro de texto simple, concisa y fácilmente reconocible no son bien recibidas (al menos allí). ¿Es esta una característica general, o es probable que preguntas como esta no se cierren si se publican en Math.SE? El tiempo que he estado dando vueltas no fue suficiente para estar seguro de esto.
(i) Desde la estructura de stackExchange, considero que ninguno de estos sitios (física o filosofía, y hasta cierto punto matemáticas también) es un buen lugar para las preguntas que son realmente interesantes, porque de este tipo de preguntas, generalmente aprendes a través de la discusión. . Las preguntas en el tablero de matemáticas generalmente tienen una respuesta, en mi humilde opinión, si son de naturaleza "filosófica" que no son preguntas matemáticas reales, o si se trata de ciertos conceptos, para los cuales uno no está seguro de la definición. En cuanto a esta pregunta, no veo por qué FOL necesita más argumentos que el montón de puntos que ya conoce.
(ii) Creo que puedes hacer una base teórica de conjunto SOL. Pero en los enlaces, la gente comenta que prefieren no haberlo visto nunca, así que concluyo que no hay suficientes recursos; después de todo, puedes simular SOL y FOL, como dicen. Volviendo, básicamente los sitios son buenos para hacer preguntas, que podrías responder tú mismo, si te tomas el tiempo de leer los libros correctos. Estas también son preguntas importantes, por supuesto, porque la gente tiene un tiempo finito. Estoy dispuesto a discutir un poco, pero, de nuevo, dices que no quieres que los no expertos abran la boca y, básicamente, tengo menos idea que tú;)
(iii) Ah, y sí, alguien (¿moderadores?) puede mover preguntas de un foro a otro.
Gracias por tomarte el tiempo de responderme, Nick. Tengo que estar de acuerdo en que la imagen que das es correcta: uno no puede quejarse de los sitios de preguntas y respuestas al tratar de enfocarse en sus objetivos originales. Pero, de nuevo, lo incómodo es que aquí tenemos mucha gente inteligente que difícilmente podría encontrar en ningún otro lugar y, sin embargo, en nombre de la limpieza de la plataforma, se espera que no participemos en discusiones más profundas entre nosotros. Tal vez debería explorar la aplicación de chat, aún no la he revisado, pero parece ser principalmente una forma de discutir temas en privado. Sin embargo, indudablemente prefiero la discusión pública.
Y para la cita de "no quiero que los no expertos abran la boca": acabo de dejar en claro mi condición de no experto (y podría agregar, alguien que no tiene ningún plan para vivir de esto ) para poner la pregunta en contexto. Quizás alguien que comprenda completamente todas las consecuencias del resumen que mencioné anteriormente encontraría la pregunta descaradamente obvia. Simplemente no puedo saberlo. En cierto sentido, traté de hacer explícito lo que todos los demás deberían interpretar sobre mi comprensión del campo para poder dar una respuesta. ¡Pero su voluntad de discutir es más que bienvenida, por supuesto!
Parece que en el enlace que publicó en el comentario de la respuesta, se está refiriendo a mi ida y vuelta con un dador de respuestas con respecto a la necesidad de contexto para distinguir entre las declaraciones FOL y SOL. Si es así, estoy feliz de proporcionarle información indirectamente y estoy feliz de que haya personas que tengan las mismas preguntas ^^
complemento: en las discusiones de uno de sus hilos, parece estar satisfecho con FOL porque existe el teorema de integridad. Mientras luchas con la semántica de la lógica de segundo orden, todavía tengo suficientes problemas con la semántica de la lógica de primer orden, jeje. Vea, por ejemplo, mi hilo aquí (la discusión que tengo allí) seguido de mí tratando de darle sentido aquí .
Supongo que estás citando la última referencia que dejé en esta pregunta mía , y sí, ese ida y vuelta en el que participaste fue de gran ayuda. Como te diste cuenta correctamente, parece que estamos preocupados por las mismas cosas. En su complemento, hay una razón perfectamente explicable por la que no me preocupo demasiado con la semántica de FOL, pero me gustaría ponerlo todo en una respuesta si lo escribió como pregunta.
La cosa es así: en FOL, evitas los problemas semánticos porque nunca llegas a saber realmente de qué estás hablando cuando escribes los axiomas y las reglas de inferencia de tu teoría formalizada. Eso significa literalmente que (por ejemplo) se le puede agregar la negación de una oración de Gödel "G" de una teoría "T" de FO para obtener una teoría más fuerte perfectamente consistente "T + ¬G" (asumiendo la consistencia de T), y entonces ves que tu teoría original tenía modelos muy esotéricos -porque los modelos restantes en los que ¬G es verdadera no son estándar, es decir, en ellos, no significa lo que "lees"-.
Entonces, si T = PA y G = Con(PA), en un modelo de "T + ¬G", ¬G no significa lo que lees, es decir, que PA es de hecho inconsistente. Es solo una propiedad formal que necesita otra interpretación para ser sólida (la construcción de un modelo apropiado es, en realidad, la forma de encontrar la interpretación necesaria). Por supuesto, en la "interpretación estándar" G es verdadera y ¬G es falsa; pero eso significa que ya sabes de qué estabas hablando, por ejemplo, qué es un número natural, por lo que la interpretación la arreglaste tú de antemano. Eso, formalmente hablando, no tiene sentido.
Si quieres que vea cosas, debes hacer referencia a mi nombre. Además, no creo ni veo que lo que dices resuelva mis problemas. El hilo G vs no G es un vehículo para responder a los problemas de la sección de comentarios del otro hilo que publiqué. Es decir, en qué sentido la gente piensa que algo es cierto sin necesidad de una prueba. Mi problema es casi anterior a la teoría de conjuntos y los modelos: las personas sienten que hay una verdad que guía qué modelar. Eso es realmente solo platonismo versus (tal vez mi variante personal de) formalismo. Y quiero poder entender a los platónicos, porque la historia matemática está llena de ellos.
No entiendo de qué te quejas en tu primera oración. No intenté persuadirte de que "vieras nada", y no entiendo de dónde viene la "referencia personal". Por otro lado, no hay nada impenetrable en el platonismo: si sostiene que las cadenas de símbolos son meros rasguños en el papel a menos que pueda identificarlos con alguna propiedad matemática que reconozca (por ejemplo, podría ver "%<$!$<%" y reconoce la propiedad conmutativa de un grupo abeliano, donde "%" y "$" son metavariables, "<" es la operación de grupo y "!" es el símbolo de igualdad), entonces eres uno.
El sentido en el que "la gente piensa que algo es cierto sin necesidad de una prueba" está en el centro de las discusiones sobre las axiomatizaciones de cualquier campo matemático suficientemente complejo, es decir, donde se mantiene la incompletud. Los axiomas (si eres un platónico, como lo son la mayoría de los matemáticos) pueden no ser solo una serie de símbolos, pero deberíamos poder interpretarlos como propiedades significativas de objetos abstractos; el problema es que la incompletud genera una multiplicidad de sistemas axiomáticos consistentes, y algunos de ellos tienen propiedades extrañas satisfechas por su semántica.
En esencia, el platónico "favorece" un tipo de semántica (en un FOT como ZFC significa "el" universo de conjuntos V , y en PA significa "los" números naturales N ) para los formalismos que escribe, pero hay siempre extrañas semánticas alternativas a aquellas (las "estándar") que sin embargo satisfacen los axiomas -y los hacen "verdaderos" bajo esas semánticas de hecho-. ¿Cómo encuentra el platónico la semántica "correcta"? La posición godeliana es que la intuición (matemática) hace el trabajo. Mi opinión personal sobre esto es que la intuición funciona solo en el ámbito finito pero falla en el transfinito.
No recibí el comentario la última vez, de eso se trataba la primera oración y por referencia me refiero a usar el @.
@NickKidman: Me disculpo si no te entendí bien. No soy un lógico, pero esto es lo que he concluido al leer sobre el tema. FOL parece tener un nivel de "libertad" en su semántica, que hace que el tema platónico sea una cuestión de "familiaridad" o "reconocimiento intuitivo de patrones" cuando el matemático interactúa con el sistema formal. Dicho esto, creo que la multiplicidad de semánticas independientes (modelos mutuamente inconsistentes) que pueden satisfacer el mismo conjunto de axiomas de FO, en cierto sentido implica la contingencia de cada interpretación, incluso la estándar (platónica).
Realmente no te entiendo ni sé cómo interpretas mis problemas, pero gracias por el aporte de todos modos.
@NickKidman: como esto se está haciendo demasiado largo, ¿puedo sugerirle nuevamente que publique esto como una pregunta directa? A menos, por supuesto, que ya lo hayas hecho.
No veo una forma de hacer la pregunta que produzca una respuesta neutral o incluso definitiva.
@NickKidman: bueno, esa es otra historia. Lo que obtuve de sus respuestas aquí es que está desconcertado por el hecho de que alguien pueda creer en la verdad de un enunciado matemático porque "siente" que es el caso: la intuición detrás de las ideas sobre las cuales se construyen los sistemas axiomáticos. Mi posición es que (en FOL) eso probablemente no sea un problema, porque la intuición nos engaña cuando tratamos con estructuras infinitas, por lo que no hay una justificación fundamental para la noción de "semántica estándar", es decir, que V o N son objetos perfectamente definidos. . no lo son
Me acabo de enterar de tu comentario sobre V. Respecto al problema de encontrar el modelo adecuado, te puede interesar este post . De todos modos, realmente no entiendo tu pregunta aquí. La realidad parece obedecer por completo al FOL clásico. ¿No es eso suficiente para querer trabajar dentro de FOL? En cualquier caso, ¿a qué te refieres con "fundamental"? Todas las versiones comúnmente promocionadas de "platonismo matemático" están mal definidas, entonces, ¿qué significa "fundamental" aquí?

Respuestas (3)

¿Es la lógica de primer orden (FOL) la única lógica fundamental?

Respuesta corta

no _ Es simplemente la lógica más popular entre matemáticos y filósofos principalmente por razones históricas y culturales.

Respuesta larga

Ya que escribiste una pregunta larga, aquí hay una respuesta larga :-)

Originalmente, Frege propuso una forma de lógica de segundo orden como base para las matemáticas en su Grundlagen der Arithmetik (1884). Esta base pasó de moda después de que Russell encontrara una contradicción en este sistema (puede leer todo sobre esto en SEP ).

Desde entonces, muy pocos filósofos y matemáticos han defendido el renacimiento de la lógica de segundo orden como fundamento de las matemáticas. El único conocido de tres: Jouko Väänänen, Stewart Shapiro y George Boolos. Stewart Shapiro tiene un libro al respecto: Foundations without Foundationalism: A Case for Second-order Logic (2000) .

SOL es feo, sin embargo. No tiene un sistema de axiomas completo para su semántica estándar; los únicos cálculos completos son para modelos no estándar (ver Henkin (1950) ). Además, los teoremas de compacidad fallan para la semántica habitual de SOL; la teoría del modelo para FOL generalmente se puede considerar como más bien comportada. Väänänen (2001) tiene un buen resumen de las propiedades de la lógica de segundo orden. Además, mientras que el teorema de Löwenheim-Skolem falla para la semántica estándar de SOL, se cumple para la semántica no estándar de Henkin. Väänänen argumenta: "Si la lógica de segundo orden se interpreta como nuestra lógica primitiva, no se puede decir si tiene semántica completa o semántica de Henkin, ni podemos decir de manera significativa si axiomatiza categóricamente ℕ y ℝ".

Abraham Robinson probablemente estuvo de acuerdo con Väänänen en este punto. En su obra Análisis no estándar (1960), Capítulo 2, presenta la semántica de Henkin para la lógica de orden superior. Continúa demostrando la compacidad, Löwenheim-Skolem y el teorema de Łoś. Robinson apenas presta atención a la clase de modelos estándar de orden superior (a los que se refiere como "modelos completos"). Que Robinson aceptaría la semántica no estándar de Henkin tiene sentido, por supuesto. Todo el mordisco del análisis no estándar proviene del hecho de que ℝ no es categórico y el Teorema de Łoś funciona .

Aparte de Robinson (y tal vez Väänänen), nadie realmente considera la semántica de Henkin como una base. Tampoco a nadie que trabaje sobre cimientos le interesen tanto los sistemas que no son axiomatizables. El punto central del programa de investigación de matemáticas inversas de Harvey Friedman es que tenemos varios sistemas axiomáticos y podemos razonar sobre su poder de demostrabilidad.

Por supuesto, la idea de que es FOL vs SOL para los fundamentos de las matemáticas es una dicotomía falsa de todos modos.

¿Por qué, entonces, FOL se elige invariablemente como la lógica subyacente sobre la cual se establecen los axiomas teóricos de conjuntos, en cualquier formalización potencialmente fundacional de las matemáticas?

No se elige invariablemente . Su primacía en matemáticas y filosofía se debe a su temprano éxito y rápido desarrollo en comparación con su competencia.

La investigación de matemáticos y filósofos sobre los fundamentos de las matemáticas se dividió en varias direcciones después del rechazo de los Grundlagen de Frege . Puede leer sobre ellos en la antología de Heijenoort From Frege to Gödel: A Source Book in Mathematical Logic (1999) :

  • Los lógicos de primer orden : la gran mayoría temprana. Estos incluyen a Guisseppe Peano, CS Pierce, David Hilbert, George Cantor, Richard Dedekind, Skolem, Löwenheim, Zermelo, Fraenkel, Herbrand, los chicos de Bourbaki, Quine, Tarski, (primeros) Wittgenstein, etc.
  • Los muchos lógicos ordenados : Russell, Whitehead y (a veces) Gödel.
  • Los padres de la computación : Moses Schoenfinkle, Alonzo Church y sus alumnos.
  • Los constructivistas : Kronecker, Kolmogorov y Brouwer y sus alumnos.

Debe señalarse que Peano, Pierce e Hilbert desarrollaron Lógica de primer orden de manera aproximadamente independiente; esto da crédito a la idea de que FOL es una base natural para las matemáticas.

Si bien los otros enfoques no han desaparecido, todos enfrentaron dificultades tempranas.

La teoría de tipos estaba poco desarrollada: todo el mundo sabe que los Principia Mathematica de Russell y Whitehead son legendariamente opacos. Russell luchó durante mucho tiempo antes de desarrollar tipos ramificados , que eran desafiantes y difíciles de trabajar. Finalmente, Leon Chwistek y Frank Ramsey demostraron que el sistema podía simplificarse, dando como resultado la teoría de los tipos simples en la década de 1920. Trágicamente, Ramsey murió muy joven, por lo que cualquier contribución que pudiera haber hecho se vio interrumpida. Además de eso, Russell abandonó la lógica después de escribir los Principia , y su alumno Wittgenstein no hizo ningún esfuerzo por desarrollarla.

Los "padres de la computación" también enfrentaron desafíos, aunque también llegaron más tarde que la teoría de conjuntos FOL y ZF. Después de publicar On The Building Blocks of Mathematical Logic en 1924, Moses Schönfinkel se encontró atrapado detrás de la cortina de hierro y nunca volvió a publicar. Su trabajo fue retomado más tarde por Church, quien lo conectó con su cálculo λ. El cálculo λ, aunque más expresivo que FOL, nunca fue realmente adecuado como base para las matemáticas. Church y otros propusieron en los años 30 una serie de sistemas fundamentales basados ​​en el cálculo λ. Se demostró que el más popular de estos sistemas era contradictorio por lo que ahora se conoce como la paradoja de Curry (ver Curry (1941) ).

Finalmente, el constructivismo y el intuicionismo tenían sus propios problemas. El defecto obvio del constructivismo es demasiado restrictivo. Un matemático siempre aceptará una prueba constructiva, pero encontrar una prueba no constructiva es más fácil y generalmente aceptable. Otro problema es la lógica: la lógica intuicionista y la aritmética no fueron axiomatizadas hasta Heyting a fines de la década de 1920. La semántica adecuada para la lógica de predicados intuicionistas (IPC) también siguió siendo un problema abierto durante mucho tiempo. Kreisel proporcionó una prueba de integridad débil en la década de 1950, utilizando la semántica prevista de Brouwer (es decir, secuencias de elección ). Kripke luego dio una fuerte prueba de integridadpara IPC en la década de 1960, utilizando estructuras Kripke. El "día de heno" de la teoría del modelo intuicionista en los años 50 y 60 fue 30 años demasiado tarde para tener algún impacto en los fundamentos de las matemáticas.

Mientras tanto, mientras las fundaciones rivales luchaban, FOL/ZF finalmente ganó los corazones de los principales matemáticos y filósofos. Los matemáticos fundacionales modernos exploran principalmente el ajuste fino de la base existente. Después de que Paul Cohen demostrara la independencia de la hipótesis del continuo ( 1963 ), los matemáticos comenzaron a explorar la independencia de varias proposiciones en ZF y ciertas extensiones. Una importante extensión axiomática es el Axioma del Universo de Grothendieck , que equivale a la existencia de un cardenal fuertemente inaccesible. Este axioma es muy popular en geometría algebraica, y Wiles lo utilizó en su demostración del último teorema de Fermat (aunque aquíHarvey Friedman argumenta que el uso del axioma no es realmente esencial). Hablando de Harvey Friedman, otro importante programa de investigación fundamental es la matemática inversa , que estudia el poder de prueba de los sistemas que amplían la aritmética de Peano pero son más débiles que ZF.

También se ha desarrollado la teoría del modelo de primer orden. Un viejo triunfo de la teoría de modelos es la demostración teórica de modelos de Hrushovski de la conjetura de Lang ( 1998 ). A pesar de la categorización de ℕ y ℝ en SOL, pocos matemáticos han estudiado la teoría de modelos de segundo orden desde los años 50. También hay resultados de categoricidad en FOL: por ejemplo (ℚ,<) es ω-categórico en FOL.

Y en filosofía, ningún filósofo ha evangelizado a FOL más que Quine. Diría que la preeminencia de Quine es probablemente la razón por la cual los filósofos solo conocen FOL y ZF y no conocen nada más.

Mientras que los principales matemáticos y filósofos los ignoraban, los otros programas de investigación fundacionales se consolidaron y finalmente florecieron.

Después del fracaso de usar el cálculo λ como base, Church y muchos de sus estudiantes recurrieron al uso de tipos simples. Lo que surgió combinó el programa de investigación de Russell con el programa de Church.

Un desarrollo posterior fue una interpretación inesperada, no holandesa, de la lógica intuicionista: los tipos construibles en el cálculo λ simplemente tipificado corresponden exactamente a la lógica intuicionista proposicional. Esta es la llamada Correspondencia Curry-Howard .

La Correspondencia Curry-Howard finalmente inspiró a Per Martin-Löf a inventar la Teoría Intuicionista de Tipos a principios de los años 70, como una nueva base alternativa para las matemáticas. La formulación original adolecía de un defecto conocido como paradoja de Girard , aunque el sistema era salvable y Martin-Löf no lo abandonó.

En general, los estudiantes de informática saben bien que el cálculo λ inspiró a John McCarthy y Steve Russell a inventar LISP. Algo similar sucedió con el cálculo λ de tipo simple a principios de los años 70. Dana Scott, una ex alumna de la iglesia de Alonzo, inventó la Lógica para funciones computables para razonar sobre la semántica de denotación de los programas funcionales escritos a finales de los años 60. En 1973, Robin Milner y compañía lo implementaron LCFcomo el primer asistente de prueba por computadora. Esto se hizo después de desarrollar el primer lenguaje de programación funcional de tipo simple ML("MetaLanguage") en el que estaba escrito.

Desde entonces, la investigación fundamental ajena a FOL/ZF ha trabajado en gran medida con la comunidad informática.

Un ejemplo es HOL, o "Lógica de orden superior", modelado aproximadamente a partir del cálculo lambda de tipo simple de Church ( 1940 ). Después de una serie de revisiones, Mike Gordon lanzó HOL88, destinado a la verificación de hardware. Como Gordon admite en su breve historia sobre el tema, su código pirateó partes de LCF cuando fue conveniente y fue más bien ad hoc ( 1996 ). HOL fue posteriormente pulido por John Harrison y Konrad Slind en HOL-Light ; HOL-Light tiene 9 reglas elementales que se parecen vagamente a la Lógica Ecuacional y tres axiomas (el axioma del infinito , el axioma de elección usando el ε de Hilbert y la Ley de Leibniz ).

Otra extensión es Isabelle/HOL , que amplía de forma conservadora el sistema de tipos de HOL con "contexto". Otro sistema más es el HOL-Omega de Homeier , que de forma conservadora amplía aún más el sistema de tipos.

Otro desarrollo es NuPRL de la Universidad de Cornell, que implementa la teoría de tipo intuicionista de Martin-Löf. Agda es similar. Un sistema relacionado fuera de INRIA es Coq , que implementa el cálculo de construcciones de Thierry Coquand que amplía la teoría de tipo intuicionista.

El desarrollo de nuevos sistemas se ha desacelerado en la última década, pero no se ha detenido. Los pocos sistemas FOL/ZF (a saber, Isabelle/ZF y Mizar ) están comparativamente inactivos.

Resumiría mi posición así: decir que FOL se elige invariablemente como la lógica subyacente es como decir que Windows se elige invariablemente como la plataforma subyacente para los juegos de PC .

En ambos casos, es una cuestión cultural.

Uno de los principales problemas que enfrento cuando trato de razonar sobre la relación entre HOL (y cualquier otra lógica de orden superior a FOL) y los sistemas informáticos, es que no entiendo muy bien la forma en que ese tipo de lógica -con su semántica estándar- funciona en un sistema "mecánico" como una computadora.
Por ejemplo, en esta publicación tienes un ejemplo de una oración en el lenguaje de la teoría de conjuntos que no se puede reconocer como FO o SO a menos que se indique explícitamente el contexto . Parece como si la "aplicación semántica de la interpretación" en los sistemas formales basados ​​en lógicas superiores a FOL no pudiera incluirse en el propio formalismo. Mi falta de experiencia en informática hace que esto sea especialmente difícil de entender para mí y, por supuesto, esa es la razón detrás de la mayoría de mis problemas para aceptar la "diversidad" de lógicas posibles.
Por cierto, esta es una respuesta muy agradable y elaborada. Gracias por tomarte tu tiempo.
@Mono: Realmente no tengo espacio para responder adecuadamente a sus preguntas en estos comentarios; tal vez podrías escribir algunas preguntas nuevas que te desconcierten aquí, CSTheory, Mathematics o MathOverflow.
Tienes razón. Aquí he pedido uno nuevo en Math.SE:
¡Esta es una respuesta fantástica! Ojalá tuviera más votos a favor. =)
Es Kronecker.
@NikolajK ¡Arreglado!
"Esto se hizo después de desarrollar el primer lenguaje de programación funcional de tipo simple ML": ¿ML no se basó en el sistema de tipos Hindley-Milner, no en el cálculo lambda de tipo simple? ¿O quiso referirse al sistema de tipos de LCF?

Alguien debería señalar que la semántica que los matemáticos usan en el día a día sigue siendo lógica de segundo orden, o el equivalente, a pesar de toda la preocupación por los fundamentos.

Generalmente permitimos una capa de referencia a conjuntos de conjuntos, e implícitamente asumimos que 'Currying' hace que esto sea totalmente suficiente. Y no debilitamos la lógica para evitar la contradicción, a menos que un lógico o una paradoja nos atrapen en un rincón.

Incluso las personas que rechazan grandes porciones de la lógica estándar de las matemáticas al exigir cierto nivel de "constructividad" no reducen su pensamiento a manipulaciones de primer orden, sino que controlan el acceso a las afirmaciones de negación y universalidad que no están basadas en alguna perspectiva específica.

El enfoque en la lógica de primer orden como la base de todo parece haber desviado la lógica de la práctica matemática real, y básicamente detuvo la búsqueda de una lógica estándar utilizable dentro de la lógica de segundo orden, con la suposición de que todos ellos serán víctimas de la versión elevada del teorema de Gödel. Esta no es una conclusión inevitable.

He visto trabajos ocasionales sobre definiciones de 'bien fundamentadas' (al estilo de la Teoría de categorías como una teoría de conjuntos alternativa) y otras restricciones sobre la autorreferencia como base para una forma de lógica que funciona más sobre la base de la consistencia al resolver o converger. bucles que sobre una base positivista que requiere un fundamento absoluto, pero parece avanzar lentamente y no se enseña.

Esta respuesta es completamente incorrecta y está claramente escrita por alguien que no sabe de lo que está hablando. Absolutamente nadie puede usar SOL con semántica completa. SOL con la semántica de Henkin puede subsumirse trivialmente en FOL. ¡Y el autor de la pregunta ya dijo esto! Y todos los sistemas fundacionales razonables sufren de los teoremas de incompletitud generalizados; está perdido .

Fundaciones tiene objetivos:

  1. Presentar un enfoque de las matemáticas en el que podamos estar seguros de que es coherente
  2. Presentar el lenguaje y la metodología con los que realmente podemos hacer matemáticas.

Estos objetivos son básicamente diametralmente opuestos. El método más simple para lograr el primer objetivo es básicamente tener un conjunto mínimo de herramientas para que sea factible razonar sobre su corrección. Sin embargo, el segundo objetivo nos anima encarecidamente a lanzar montones y montones de herramientas diferentes para construir, manipular y probar cosas.

Una muy buena solución a este problema es simplemente dividir los cimientos en dos capas: la primera capa es muy mínima en cuya corrección confiamos, y con eso construimos la segunda capa que tiene todas las características prácticas que queremos usar. por hacer matemáticas.

Eso es lo que ves hoy; la lógica de primer orden es una opción común para la primera capa, y luego alguna forma de teoría de conjuntos como la segunda capa.

Tenga en cuenta, por cierto, que la lógica de orden superior es en sí misma una forma de teoría de conjuntos.

Tenga en cuenta, por cierto, que una vez que haya establecido los cimientos, aún desea desarrollar una teoría de la lógica formal sobre esos cimientos; es esa formulación de la lógica, no lo que aparece en la base de sus fundamentos, lo que es más relevante para la práctica real de las matemáticas.

¿Es la lógica de primer orden (FOL) la única lógica fundamental?
RespuestasAquíPolítica de privacidad1y, 0v