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:
¿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.
¿Es la lógica de primer orden (FOL) la única lógica fundamental?
no _ Es simplemente la lógica más popular entre matemáticos y filósofos principalmente por razones históricas y culturales.
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) :
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 LCF
como 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.
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.
Fundaciones tiene objetivos:
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.
Nikolaj-K
Mononucleosis infecciosa
Mononucleosis infecciosa
Nikolaj-K
Nikolaj-K
Nikolaj-K
Mononucleosis infecciosa
Mononucleosis infecciosa
Nikolaj-K
Nikolaj-K
Mononucleosis infecciosa
Mononucleosis infecciosa
Mononucleosis infecciosa
Nikolaj-K
Mononucleosis infecciosa
Mononucleosis infecciosa
Mononucleosis infecciosa
Nikolaj-K
Mononucleosis infecciosa
Nikolaj-K
Mononucleosis infecciosa
Nikolaj-K
Mononucleosis infecciosa
usuario21820