Lógica matemática

La lógica matemática es el estudio de la lógica formal dentro de las matemáticas. Las principales subáreas incluyen la teoría de modelos, la teoría de pruebas, la teoría de conjuntos y la teoría de la recursión. La investigación en lógica matemática comúnmente aborda las propiedades matemáticas de los sistemas formales de lógica, como su poder expresivo o deductivo. Sin embargo, también puede incluir usos de la lógica para caracterizar el razonamiento matemático correcto o para establecer los fundamentos de las matemáticas.

Desde sus inicios, la lógica matemática ha contribuido y ha sido motivada por el estudio de los fundamentos de las matemáticas. Este estudio comenzó a fines del siglo XIX con el desarrollo de marcos axiomáticos para geometría, aritmética y análisis. A principios del siglo XX, fue moldeado por el programa de David Hilbert para probar la consistencia de las teorías fundamentales. Los resultados de Kurt Gödel, Gerhard Gentzen y otros brindaron una resolución parcial al programa y aclararon los problemas relacionados con la prueba de consistencia. El trabajo en teoría de conjuntos mostró que casi todas las matemáticas ordinarias pueden formalizarse en términos de conjuntos, aunque hay algunos teoremas que no pueden probarse en sistemas de axiomas comunes para la teoría de conjuntos.

Subcampos y alcance

El Handbook of Mathematical Logic de 1977 hace una división aproximada de la lógica matemática contemporánea en cuatro áreas:

1. teoría de conjuntos
2. teoría del modelo
3. teoría de la recursión, y
4. teoría de la demostración y matemáticas constructivas (consideradas como partes de una sola área).

Además, a veces el campo de la teoría de la complejidad computacional también se incluye como parte de la lógica matemática. Cada área tiene un enfoque distinto, aunque muchas técnicas y resultados se comparten entre múltiples áreas. Los límites entre estos campos y las líneas que separan la lógica matemática y otros campos de las matemáticas no siempre son nítidos. El teorema de incompletitud de Gödel marca no solo un hito en la teoría de la recursión y la teoría de la prueba, sino que también ha llevado al teorema de Löb en la lógica modal. El método de forzamiento se emplea en la teoría de conjuntos, la teoría de modelos y la teoría de la recursión, así como en el estudio de las matemáticas intuicionistas.

El campo matemático de la teoría de categorías utiliza muchos métodos axiomáticos formales e incluye el estudio de la lógica categórica, pero la teoría de categorías normalmente no se considera un subcampo de la lógica matemática. Debido a su aplicabilidad en diversos campos de las matemáticas, matemáticos como Saunders Mac Lane han propuesto la teoría de categorías como un sistema fundamental para las matemáticas, independiente de la teoría de conjuntos. Estos fundamentos utilizan topos, que se asemejan a modelos generalizados de teoría de conjuntos que pueden emplear lógica clásica o no clásica.

Historia

La lógica matemática surgió a mediados del siglo XIX como un subcampo de las matemáticas, reflejando la confluencia de dos tradiciones: la lógica filosófica formal y las matemáticas. "La lógica matemática, también llamada 'logística', 'lógica simbólica', 'álgebra de la lógica' y, más recientemente, simplemente 'lógica formal', es el conjunto de teorías lógicas elaboradas en el transcurso del último siglo [XIX]. con la ayuda de una notación artificial y un método rigurosamente deductivo". Antes de este surgimiento, la lógica se estudiaba con la retórica, con los cálculos, a través del silogismo y con la filosofía. La primera mitad del siglo XX vio una explosión de resultados fundamentales, acompañada de un vigoroso debate sobre los fundamentos de las matemáticas.

Historia temprana

Las teorías de la lógica se desarrollaron en muchas culturas a lo largo de la historia, incluidas China, India, Grecia y el mundo islámico. Los métodos griegos, particularmente la lógica aristotélica (o término lógica) tal como se encuentran en el Organon, encontraron una amplia aplicación y aceptación en la ciencia y las matemáticas occidentales durante milenios. Los estoicos, especialmente Crisipo, comenzaron el desarrollo de la lógica de predicados. En la Europa del siglo XVIII, los matemáticos filosóficos, incluidos Leibniz y Lambert, intentaron tratar las operaciones de la lógica formal de una manera simbólica o algebraica, pero sus trabajos permanecieron aislados y poco conocidos.

Siglo 19

A mediados del siglo XIX, George Boole y luego Augustus De Morgan presentaron tratamientos matemáticos sistemáticos de la lógica. Su trabajo, basado en el trabajo de algebristas como George Peacock, amplió la doctrina tradicional aristotélica de la lógica en un marco suficiente para el estudio de los fundamentos de las matemáticas. Charles Sanders Peirce luego se basó en el trabajo de Boole para desarrollar un sistema lógico para relaciones y cuantificadores, que publicó en varios artículos entre 1870 y 1885.

Gottlob Frege presentó un desarrollo independiente de la lógica con cuantificadores en su Begriffsschrift, publicado en 1879, un trabajo generalmente considerado como un punto de inflexión en la historia de la lógica. Sin embargo, el trabajo de Frege permaneció oscuro hasta que Bertrand Russell comenzó a promocionarlo cerca del cambio de siglo. La notación bidimensional que desarrolló Frege nunca fue ampliamente adoptada y no se usa en los textos contemporáneos.

De 1890 a 1905, Ernst Schröder publicó Vorlesungen über die Algebra der Logik en tres volúmenes. Este trabajo resumió y amplió el trabajo de Boole, De Morgan y Peirce, y fue una referencia completa a la lógica simbólica tal como se entendía a fines del siglo XIX.

Teorías fundamentales

Las preocupaciones de que las matemáticas no se habían construido sobre una base adecuada llevaron al desarrollo de sistemas axiomáticos para áreas fundamentales de las matemáticas como la aritmética, el análisis y la geometría.

En lógica, el término aritmética se refiere a la teoría de los números naturales. Giuseppe Peano publicó un conjunto de axiomas para la aritmética que llegó a llevar su nombre (axiomas de Peano), utilizando una variación del sistema lógico de Boole y Schröder pero añadiendo cuantificadores. Peano desconocía el trabajo de Frege en ese momento. Casi al mismo tiempo, Richard Dedekind demostró que los números naturales se caracterizan únicamente por sus propiedades de inducción. Dedekind propuso una caracterización diferente, que carecía del carácter lógico formal de los axiomas de Peano.El trabajo de Dedekind, sin embargo, demostró teoremas inaccesibles en el sistema de Peano, incluida la unicidad del conjunto de números naturales (hasta el isomorfismo) y las definiciones recursivas de suma y multiplicación a partir de la función sucesora y la inducción matemática.

A mediados del siglo XIX, se conocieron las fallas en los axiomas geométricos de Euclides. Además de la independencia del postulado de las paralelas, establecido por Nikolai Lobachevsky en 1826, los matemáticos descubrieron que ciertos teoremas que Euclides daba por sentado no eran de hecho demostrables a partir de sus axiomas. Entre estos está el teorema de que una línea contiene al menos dos puntos, o que los círculos del mismo radio cuyos centros están separados por ese radio deben intersecarse. Hilbert desarrolló un conjunto completo de axiomas para la geometría, basándose en el trabajo previo de Pasch. El éxito en la axiomatización de la geometría motivó a Hilbert a buscar axiomatizaciones completas de otras áreas de las matemáticas, como los números naturales y la línea real. Esto demostraría ser un área importante de investigación en la primera mitad del siglo XX.

El siglo XIX vio grandes avances en la teoría del análisis real, incluidas las teorías de convergencia de funciones y series de Fourier. Matemáticos como Karl Weierstrass comenzaron a construir funciones que ampliaban la intuición, como funciones continuas diferenciables en ninguna parte. Las concepciones anteriores de una función como regla para el cálculo, o un gráfico uniforme, ya no eran adecuadas. Weierstrass comenzó a defender la aritmetización del análisis, que buscaba axiomatizar el análisis utilizando las propiedades de los números naturales. La definición moderna (ε, δ) de funciones límite y continuas ya fue desarrollada por Bolzano en 1817,pero permaneció relativamente desconocido. Cauchy en 1821 definió la continuidad en términos de infinitesimales (ver Cours d'Analyse, página 34). En 1858, Dedekind propuso una definición de los números reales en términos de cortes de Dedekind de números racionales, una definición que todavía se emplea en textos contemporáneos.

Georg Cantor desarrolló los conceptos fundamentales de la teoría de conjuntos infinitos. Sus primeros resultados desarrollaron la teoría de la cardinalidad y probaron que los números reales y naturales tienen diferentes cardinalidades. Durante los próximos veinte años, Cantor desarrolló una teoría de los números transfinitos en una serie de publicaciones. En 1891, publicó una nueva demostración de la incontabilidad de los números reales que introdujo el argumento de la diagonal y utilizó este método para demostrar el teorema de Cantor de que ningún conjunto puede tener la misma cardinalidad que su conjunto potencia. Cantor creía que todos los conjuntos podían estar bien ordenados, pero no pudo producir una prueba de este resultado, dejándolo como un problema abierto en 1895.

Siglo 20

En las primeras décadas del siglo XX, las principales áreas de estudio fueron la teoría de conjuntos y la lógica formal. El descubrimiento de paradojas en la teoría informal de conjuntos hizo que algunos se preguntaran si las matemáticas en sí son inconsistentes y buscaron pruebas de consistencia.

En 1900, Hilbert planteó una famosa lista de 23 problemas para el próximo siglo. Los dos primeros fueron para resolver la hipótesis del continuo y probar la consistencia de la aritmética elemental, respectivamente; el décimo fue producir un método que pudiera decidir si una ecuación polinomial multivariante sobre los números enteros tiene una solución. El trabajo posterior para resolver estos problemas dio forma a la dirección de la lógica matemática, al igual que el esfuerzo por resolver el Entscheidungsproblem de Hilbert, planteado en 1928. Este problema requería un procedimiento que decidiera, dado un enunciado matemático formalizado, si el enunciado es verdadero o falso.

Teoría de conjuntos y paradojas

Ernst Zermelo dio una prueba de que cada juego podía estar bien ordenado, un resultado que Georg Cantor no había podido obtener. Para lograr la prueba, Zermelo introdujo el axioma de elección, que suscitó un acalorado debate e investigación entre los matemáticos y los pioneros de la teoría de conjuntos. La crítica inmediata al método llevó a Zermelo a publicar una segunda exposición de su resultado, abordando directamente las críticas a su demostración. Este artículo condujo a la aceptación general del axioma de elección en la comunidad matemática.

El escepticismo sobre el axioma de elección se vio reforzado por paradojas descubiertas recientemente en la teoría ingenua de conjuntos. Cesare Burali-Forti fue el primero en afirmar una paradoja: la paradoja de Burali-Forti muestra que la colección de todos los números ordinales no puede formar un conjunto. Muy poco después, Bertrand Russell descubrió la paradoja de Russell en 1901 y Jules Richard descubrió la paradoja de Richard.

Zermelo proporcionó el primer conjunto de axiomas para la teoría de conjuntos. Estos axiomas, junto con el axioma adicional de reemplazo propuesto por Abraham Fraenkel, ahora se denominan teoría de conjuntos de Zermelo-Fraenkel (ZF). Los axiomas de Zermelo incorporaron el principio de limitación de tamaño para evitar la paradoja de Russell.

En 1910, se publicó el primer volumen de Principia Mathematica de Russell y Alfred North Whitehead. Este trabajo seminal desarrolló la teoría de funciones y cardinalidad en un marco completamente formal de teoría de tipos, que Russell y Whitehead desarrollaron en un esfuerzo por evitar las paradojas. Principia Mathematica se considera una de las obras más influyentes del siglo XX, aunque el marco de la teoría de tipos no resultó popular como teoría fundamental de las matemáticas.

Fraenkel demostró que el axioma de elección no se puede probar a partir de los axiomas de la teoría de conjuntos de Zermelo con urelementos. El trabajo posterior de Paul Cohen demostró que la adición de urelements no es necesaria, y el axioma de elección no es demostrable en ZF. La prueba de Cohen desarrolló el método de forzar, que ahora es una herramienta importante para establecer resultados de independencia en la teoría de conjuntos.

Lógica simbólica

Leopold Löwenheim y Thoralf Skolem obtuvieron el teorema de Löwenheim-Skolem, que dice que la lógica de primer orden no puede controlar las cardinalidades de estructuras infinitas. Skolem se dio cuenta de que este teorema se aplicaría a las formalizaciones de primer orden de la teoría de conjuntos y que implica que cualquier formalización de este tipo tiene un modelo contable. Este hecho contrario a la intuición se conoció como la paradoja de Skolem.

En su tesis doctoral, Kurt Gödel demostró el teorema de completitud, que establece una correspondencia entre sintaxis y semántica en lógica de primer orden. Gödel usó el teorema de completitud para probar el teorema de compacidad, demostrando la naturaleza finita de la consecuencia lógica de primer orden. Estos resultados ayudaron a establecer la lógica de primer orden como la lógica dominante utilizada por los matemáticos.

En 1931, Gödel publicó On Formally Undecidible Propositions of Principia Mathematica and Related Systems, que demostró la incompletitud (en un significado diferente de la palabra) de todas las teorías de primer orden suficientemente fuertes y efectivas. Este resultado, conocido como teorema de incompletud de Gödel, establece severas limitaciones en los fundamentos axiomáticos de las matemáticas, asestando un duro golpe al programa de Hilbert. Mostró la imposibilidad de proporcionar una prueba de consistencia de la aritmética dentro de cualquier teoría formal de la aritmética. Hilbert, sin embargo, no reconoció la importancia del teorema de incompletitud durante algún tiempo.

El teorema de Gödel muestra que una prueba de consistencia de cualquier sistema de axiomas eficaz y suficientemente fuerte no se puede obtener en el sistema mismo, si el sistema es consistente, ni en ningún sistema más débil. Esto deja abierta la posibilidad de pruebas de consistencia que no pueden formalizarse dentro del sistema que consideran. Gentzen demostró la consistencia de la aritmética utilizando un sistema finitista junto con un principio de inducción transfinita. El resultado de Gentzen introdujo las ideas de eliminación de cortes y ordinales de la teoría de la prueba, que se convirtieron en herramientas clave en la teoría de la prueba. Gödel dio una prueba de consistencia diferente, que reduce la consistencia de la aritmética clásica a la de la aritmética intuicionista en tipos superiores.

El primer libro de texto sobre lógica simbólica para el profano fue escrito por Lewis Carroll, autor de Alicia en el país de las maravillas, en 1896.

Comienzos de las otras ramas

Alfred Tarski desarrolló los fundamentos de la teoría de modelos.

A partir de 1935, un grupo de destacados matemáticos colaboró ​​bajo el seudónimo de Nicolas Bourbaki para publicar Éléments de mathématique, una serie de textos matemáticos enciclopédicos. Estos textos, escritos en un estilo austero y axiomático, enfatizaban la presentación rigurosa y los fundamentos de la teoría de conjuntos. La terminología acuñada por estos textos, como las palabras biyección, inyección y sobreyección, y los fundamentos teóricos de conjuntos empleados en los textos, fueron ampliamente adoptados en las matemáticas.

El estudio de la computabilidad llegó a conocerse como teoría de la recursión o teoría de la computabilidad, porque las primeras formalizaciones de Gödel y Kleene se basaban en definiciones recursivas de funciones. Cuando se mostró que estas definiciones eran equivalentes a la formalización de Turing que involucraba máquinas de Turing, quedó claro que se había descubierto un nuevo concepto, la función computable, y que esta definición era lo suficientemente sólida como para admitir numerosas caracterizaciones independientes. En su trabajo sobre los teoremas de incompletud de 1931, Gödel carecía de un concepto riguroso de un sistema formal efectivo; Inmediatamente se dio cuenta de que las nuevas definiciones de computabilidad podrían usarse para este propósito, lo que le permitió establecer los teoremas de incompletitud en general que solo podían estar implícitos en el artículo original.

Stephen Cole Kleene y Emil Leon Post obtuvieron numerosos resultados en la teoría de la recursión en la década de 1940. Kleene introdujo los conceptos de computabilidad relativa, presagiados por Turing, y la jerarquía aritmética. Más tarde, Kleene generalizó la teoría de la recursión a funcionales de orden superior. Kleene y Georg Kreisel estudiaron versiones formales de las matemáticas intuicionistas, particularmente en el contexto de la teoría de la prueba.

Sistemas lógicos formales

En esencia, la lógica matemática se ocupa de los conceptos matemáticos expresados ​​mediante sistemas lógicos formales. Estos sistemas, aunque difieren en muchos detalles, comparten la propiedad común de considerar solo expresiones en un lenguaje formal fijo. Los sistemas de lógica proposicional y lógica de primer orden son los más estudiados en la actualidad, debido a su aplicabilidad a los fundamentos de las matemáticas y debido a sus deseables propiedades de demostración teórica. También se estudian lógicas clásicas más fuertes, como la lógica de segundo orden o la lógica infinita, junto con lógicas no clásicas, como la lógica intuicionista.

Lógica de primer orden

La lógica de primer orden es un sistema formal particular de lógica. Su sintaxis involucra solo expresiones finitas como fórmulas bien formadas, mientras que su semántica se caracteriza por la limitación de todos los cuantificadores a un dominio fijo del discurso.

Los primeros resultados de la lógica formal establecieron las limitaciones de la lógica de primer orden. El teorema de Löwenheim-Skolem (1919) mostró que si un conjunto de oraciones en un lenguaje contable de primer orden tiene un modelo infinito, entonces tiene al menos un modelo de cada cardinalidad infinita. Esto demuestra que es imposible que un conjunto de axiomas de primer orden caracterice los números naturales, los números reales o cualquier otra estructura infinita hasta el isomorfismo. Dado que el objetivo de los primeros estudios fundamentales era producir teorías axiomáticas para todas las partes de las matemáticas, esta limitación era particularmente marcada.

El teorema de completitud de Gödel estableció la equivalencia entre las definiciones semántica y sintáctica de consecuencia lógica en la lógica de primer orden.Muestra que si una oración en particular es verdadera en cada modelo que satisface un conjunto particular de axiomas, entonces debe haber una deducción finita de la oración a partir de los axiomas. El teorema de la compacidad apareció por primera vez como un lema en la prueba del teorema de la completitud de Gödel, y pasaron muchos años antes de que los lógicos comprendieran su significado y comenzaran a aplicarlo de manera rutinaria. Dice que un conjunto de oraciones tiene un modelo si y solo si todo subconjunto finito tiene un modelo, o en otras palabras, que un conjunto inconsistente de fórmulas debe tener un subconjunto inconsistente finito. Los teoremas de completitud y compacidad permiten un análisis sofisticado de la consecuencia lógica en la lógica de primer orden y el desarrollo de la teoría de modelos, y son una razón clave de la importancia de la lógica de primer orden en las matemáticas.

Los teoremas de incompletitud de Gödel establecen límites adicionales a las axiomatizaciones de primer orden. El primer teorema de incompletitud establece que para cualquier sistema lógico consistente, efectivamente dado (definido a continuación) que sea capaz de interpretar la aritmética, existe una afirmación que es verdadera (en el sentido de que es válida para los números naturales) pero no demostrable dentro de esa lógica. (y que de hecho puede fallar en algunos modelos aritméticos no estándar que pueden ser consistentes con el sistema lógico). Por ejemplo, en todo sistema lógico capaz de expresar los axiomas de Peano, la oración de Gödel se cumple para los números naturales pero no se puede demostrar.

Aquí se dice que un sistema lógico está efectivamente dado si es posible decidir, dada cualquier fórmula en el lenguaje del sistema, si la fórmula es un axioma, y ​​uno que puede expresar los axiomas de Peano se llama "suficientemente fuerte". Cuando se aplica a la lógica de primer orden, el primer teorema de incompletitud implica que cualquier teoría de primer orden suficientemente fuerte, consistente y efectiva tiene modelos que no son elementalmente equivalentes, una limitación más fuerte que la establecida por el teorema de Löwenheim-Skolem. El segundo teorema de incompletitud establece que ningún sistema de axiomas suficientemente fuerte, consistente y efectivo para la aritmética puede demostrar su propia consistencia, lo que se ha interpretado para mostrar que no se puede alcanzar el programa de Hilbert.

Otras lógicas clásicas

Se estudian muchas lógicas además de la lógica de primer orden. Estos incluyen lógicas infinitas, que permiten que las fórmulas proporcionen una cantidad infinita de información, y lógicas de orden superior, que incluyen una parte de la teoría de conjuntos directamente en su semántica.

La lógica infinitaria mejor estudiada es . En esta lógica, los cuantificadores solo se pueden anidar hasta profundidades finitas, como en la lógica de primer orden, pero las fórmulas pueden tener conjunciones y disyunciones finitas o contablemente infinitas dentro de ellas. Así, por ejemplo, es posible decir que un objeto es un número entero usando una fórmula de como

Las lógicas de orden superior permiten la cuantificación no solo de elementos del dominio del discurso, sino también de subconjuntos del dominio del discurso, conjuntos de dichos subconjuntos y otros objetos de tipo superior. La semántica se define de modo que, en lugar de tener un dominio separado para cada cuantificador de tipo superior, los cuantificadores abarcan todos los objetos del tipo apropiado. Las lógicas estudiadas antes del desarrollo de la lógica de primer orden, por ejemplo, la lógica de Frege, tenían aspectos similares de teoría de conjuntos. Aunque las lógicas de orden superior son más expresivas y permiten axiomatizaciones completas de estructuras como los números naturales, no satisfacen los análogos de los teoremas de completitud y compacidad de la lógica de primer orden y, por lo tanto, son menos susceptibles de análisis teórico de prueba.

Otro tipo de lógica sonlógica de punto fijo que permite definiciones inductivas, como se escribe para funciones recursivas primitivas.

Se puede definir formalmente una extensión de la lógica de primer orden, una noción que abarca todas las lógicas de esta sección porque se comportan como lógica de primer orden en ciertas formas fundamentales, pero no abarca todas las lógicas en general, por ejemplo, no abarca la lógica intuicionista, lógica modal o difusa.

El teorema de Lindström implica que la única extensión de la lógica de primer orden que satisface tanto el teorema de compacidad como el teorema descendente de Löwenheim-Skolem es la lógica de primer orden.

Lógica no clásica y modal

Las lógicas modales incluyen operadores modales adicionales, como un operador que establece que una fórmula en particular no solo es verdadera, sino necesariamente verdadera. Aunque la lógica modal no se usa a menudo para axiomatizar las matemáticas, se ha usado para estudiar las propiedades de la demostrabilidad de primer orden y el forzamiento de la teoría de conjuntos.

Heyting desarrolló la lógica intuicionista para estudiar el programa de intuicionismo de Brouwer, en el que el propio Brouwer evitaba la formalización. La lógica intuicionista específicamente no incluye la ley del tercero excluido, que establece que cada oración es verdadera o su negación es verdadera. El trabajo de Kleene con la teoría de la prueba de la lógica intuicionista mostró que la información constructiva se puede recuperar de las pruebas intuicionistas. Por ejemplo, cualquier función demostrablemente total en la aritmética intuicionista es computable; esto no es cierto en las teorías clásicas de la aritmética como la aritmética de Peano.

Lógica algebraica

La lógica algebraica utiliza los métodos del álgebra abstracta para estudiar la semántica de la lógica formal. Un ejemplo fundamental es el uso de álgebras booleanas para representar valores de verdad en la lógica proposicional clásica y el uso de álgebras de Heyting para representar valores de verdad en la lógica proposicional intuicionista. Las lógicas más fuertes, como la lógica de primer orden y la lógica de orden superior, se estudian utilizando estructuras algebraicas más complicadas, como las álgebras cilíndricas.

Teoría de conjuntos

La teoría de conjuntos es el estudio de conjuntos, que son colecciones abstractas de objetos. Muchas de las nociones básicas, como los números ordinales y cardinales, fueron desarrolladas informalmente por Cantor antes de que se desarrollaran las axiomatizaciones formales de la teoría de conjuntos. La primera axiomatización de este tipo, debida a Zermelo, se amplió ligeramente para convertirse en la teoría de conjuntos de Zermelo-Fraenkel (ZF), que ahora es la teoría fundamental más utilizada para las matemáticas.

Se han propuesto otras formalizaciones de la teoría de conjuntos, incluida la teoría de conjuntos de von Neumann-Bernays-Gödel (NBG), la teoría de conjuntos de Morse-Kelley (MK) y New Foundations (NF). De estos, ZF, NBG y MK son similares en la descripción de una jerarquía acumulativa de conjuntos. New Foundations adopta un enfoque diferente; permite objetos como el conjunto de todos los conjuntos a costa de restricciones sobre sus axiomas de existencia de conjuntos. El sistema de teoría de conjuntos de Kripke-Platek está estrechamente relacionado con la teoría de recursión generalizada.

Dos afirmaciones famosas en la teoría de conjuntos son el axioma de elección y la hipótesis del continuo. El axioma de elección, establecido por primera vez por Zermelo, fue demostrado independientemente de ZF por Fraenkel, pero ha llegado a ser ampliamente aceptado por los matemáticos. Establece que dada una colección de conjuntos no vacíos, hay un único conjunto C que contiene exactamente un elemento de cada conjunto de la colección. el conjunto cse dice que "elige" un elemento de cada conjunto de la colección. Si bien algunos consideran obvia la capacidad de hacer tal elección, ya que cada conjunto en la colección no está vacío, la falta de una regla general y concreta por la cual se puede hacer la elección hace que el axioma no sea constructivo. Stefan Banach y Alfred Tarski demostraron que el axioma de elección se puede usar para descomponer una bola sólida en un número finito de piezas que luego se pueden reorganizar, sin escala, para formar dos bolas sólidas del tamaño original. Este teorema, conocido como la paradoja de Banach-Tarski, es uno de los muchos resultados contrarios a la intuición del axioma de elección.

La hipótesis del continuo, propuesta por primera vez como una conjetura por Cantor, fue enumerada por David Hilbert como uno de sus 23 problemas en 1900. Gödel demostró que la hipótesis del continuo no se puede refutar a partir de los axiomas de la teoría de conjuntos de Zermelo-Fraenkel (con o sin el axioma de elección), desarrollando el universo construible de la teoría de conjuntos en el que debe mantenerse la hipótesis del continuo. En 1963, Paul Cohen demostró que la hipótesis del continuo no puede probarse a partir de los axiomas de la teoría de conjuntos de Zermelo-Fraenkel. Sin embargo, este resultado de independencia no resolvió completamente la pregunta de Hilbert, ya que es posible que nuevos axiomas para la teoría de conjuntos puedan resolver la hipótesis. W. Hugh Woodin ha realizado un trabajo reciente en este sentido, aunque su importancia aún no está clara.

La investigación contemporánea en la teoría de conjuntos incluye el estudio de los grandes cardinales y la determinación. Los cardinales grandes son números cardinales con propiedades particulares tan fuertes que la existencia de dichos cardinales no se puede probar en ZFC. La existencia del cardenal grande más pequeño típicamente estudiado, un cardenal inaccesible, ya implica la consistencia de ZFC. A pesar de que los cardenales grandes tienen una cardinalidad extremadamente alta, su existencia tiene muchas ramificaciones para la estructura de la línea real. La determinación se refiere a la posible existencia de estrategias ganadoras para ciertos juegos de dos jugadores (se dice que los juegos están determinados). La existencia de estas estrategias implica propiedades estructurales de la línea real y otros espacios polacos.

Teoría del modelo

La teoría de modelos estudia los modelos de varias teorías formales. Aquí una teoría es un conjunto de fórmulas en una lógica formal particular y firma, mientras que un modelo es una estructura que da una interpretación concreta de la teoría. La teoría de modelos está estrechamente relacionada con el álgebra universal y la geometría algebraica, aunque los métodos de la teoría de modelos se centran más en consideraciones lógicas que en esos campos.

El conjunto de todos los modelos de una teoría particular se denomina clase elemental; La teoría clásica de modelos busca determinar las propiedades de los modelos en una clase elemental particular, o determinar si ciertas clases de estructuras forman clases elementales.

El método de eliminación de cuantificadores se puede usar para mostrar que los conjuntos definibles en teorías particulares no pueden ser demasiado complicados. Tarski estableció la eliminación de cuantificadores para campos cerrados reales, un resultado que también muestra que la teoría del campo de los números reales es decidible. También señaló que sus métodos eran igualmente aplicables a campos algebraicamente cerrados de características arbitrarias. Un subcampo moderno que se desarrolla a partir de esto se ocupa de las estructuras o-minimal.

El teorema de categoricidad de Morley, demostrado por Michael D. Morley, establece que si una teoría de primer orden en un lenguaje contable es categórica en alguna cardinalidad incontable, es decir, todos los modelos de esta cardinalidad son isomorfos, entonces es categórica en todas las cardinalidades incontables.

Una consecuencia trivial de la hipótesis del continuo es que una teoría completa con menos de un continuo muchos modelos contables no isomorfos puede tener solo muchos numerables. La conjetura de Vaught, llamada así por Robert Lawson Vaught, dice que esto es cierto incluso independientemente de la hipótesis del continuo. Se han establecido muchos casos especiales de esta conjetura.

Teoría de la recursividad

La teoría de la recursión, también llamada teoría de la computabilidad, estudia las propiedades de las funciones computables y los grados de Turing, que dividen las funciones no computables en conjuntos que tienen el mismo nivel de incomputabilidad. La teoría de la recursión también incluye el estudio de la computabilidad generalizada y la definibilidad. La teoría de la recursión surgió del trabajo de Rózsa Péter, Alonzo Church y Alan Turing en la década de 1930, que Kleene y Post ampliaron en gran medida en la década de 1940.

La teoría de la recursión clásica se centra en la computabilidad de las funciones de los números naturales a los números naturales. Los resultados fundamentales establecen una clase robusta y canónica de funciones computables con numerosas caracterizaciones independientes equivalentes utilizando máquinas de Turing, cálculo λ y otros sistemas. Los resultados más avanzados se refieren a la estructura de los grados de Turing y la red de conjuntos recursivamente enumerables.

La teoría de recursión generalizada extiende las ideas de la teoría de recursión a cálculos que ya no son necesariamente finitos. Incluye el estudio de la computabilidad en tipos superiores, así como áreas como la teoría hiperaritmética y la teoría de recursividad α.

La investigación contemporánea en la teoría de la recursión incluye el estudio de aplicaciones como la aleatoriedad algorítmica, la teoría del modelo computable y las matemáticas inversas, así como nuevos resultados en la teoría de la recursión pura.

Problemas algorítmicamente irresolubles

Un subcampo importante de la teoría de la recursión estudia la irresolubilidad algorítmica; un problema de decisión o un problema de función no tiene solución algorítmica si no existe un algoritmo computable posible que devuelva la respuesta correcta para todas las entradas legales del problema. Los primeros resultados sobre la insolubilidad, obtenidos de forma independiente por Church y Turing en 1936, mostraron que el Entscheidungsproblem es algorítmicamente irresoluble. Turing demostró esto al establecer la imposibilidad de resolver el problema de la detención, un resultado con implicaciones de gran alcance tanto en la teoría de la recursión como en la informática.

Hay muchos ejemplos conocidos de problemas indecidibles de las matemáticas ordinarias. Pyotr Novikov en 1955 demostró algorítmicamente irresoluble el problema verbal para grupos y W. Boone de forma independiente en 1959. El problema del castor ocupado, desarrollado por Tibor Radó en 1962, es otro ejemplo bien conocido.

El décimo problema de Hilbert pedía un algoritmo para determinar si una ecuación polinomial multivariante con coeficientes enteros tiene una solución en los números enteros. Julia Robinson, Martin Davis y Hilary Putnam lograron avances parciales. La irresolubilidad algorítmica del problema fue probada por Yuri Matiyasevich en 1970.

Teoría de la prueba y matemática constructiva

La teoría de la prueba es el estudio de las pruebas formales en varios sistemas de deducción lógica. Estas demostraciones se representan como objetos matemáticos formales, facilitando su análisis mediante técnicas matemáticas. Comúnmente se consideran varios sistemas de deducción, incluidos los sistemas de deducción estilo Hilbert, los sistemas de deducción natural y el cálculo secuencial desarrollado por Gentzen.

El estudio de las matemáticas constructivas, en el contexto de la lógica matemática, incluye el estudio de sistemas en lógica no clásica como la lógica intuicionista, así como el estudio de sistemas predicativos. Uno de los primeros defensores del predicativismo fue Hermann Weyl, quien demostró que es posible desarrollar una gran parte del análisis real utilizando solo métodos predicativos.

Debido a que las pruebas son completamente finitarias, mientras que la verdad en una estructura no lo es, es común que el trabajo en matemáticas constructivas enfatice la demostrabilidad. La relación entre demostrabilidad en sistemas clásicos (o no constructivos) y demostrabilidad en sistemas intuicionistas (o constructivos, respectivamente) es de particular interés. Resultados como la traducción negativa de Gödel-Gentzen muestran que es posible incorporar (o traducir) la lógica clásica a la lógica intuicionista, lo que permite que algunas propiedades sobre las pruebas intuicionistas se transfieran a las pruebas clásicas.

Los desarrollos recientes en la teoría de la prueba incluyen el estudio de la minería de prueba por parte de Ulrich Kohlenbach y el estudio de los ordinales teóricos de la prueba por Michael Rathjen.

Aplicaciones

"La lógica matemática se ha aplicado con éxito no solo a las matemáticas y sus fundamentos (G. Frege, B. Russell, D. Hilbert, P. Bernays, H. Scholz, R. Carnap, S. Lesniewski, T. Skolem), sino también a la física (R. Carnap, A. Dittrich, B. Russell, CE Shannon, AN Whitehead, H. Reichenbach, P. Fevrier), a la biología (JH Woodger, A. Tarski), a la psicología (FB Fitch, CG Hempel), al derecho y la moral (K. Menger, U. Klug, P. Oppenheim), a la economía (J. Neumann, O. Morgenstern), a cuestiones prácticas (EC Berkeley, E. Stamm), e incluso a la metafísica (J. [Jan] Salamucha, H. Scholz, JM Bochenski), sus aplicaciones a la historia de la lógica han resultado sumamente fructíferas (J. Lukasiewicz, H. Scholz, B. Mates, A. Becker, E. Moody, J. Salamucha, K. Duerr, Z. Jordan, P. Boehner, JM Bochenski, S. [Stanislaw] T. Schayer, D. Ingalls)"."También se han hecho aplicaciones a la teología (F. Drewnowski, J. Salamucha, I. Thomas)".

Conexiones con la informática

El estudio de la teoría de la computabilidad en informática está estrechamente relacionado con el estudio de la computabilidad en lógica matemática. Sin embargo, hay una diferencia de énfasis. Los científicos informáticos a menudo se centran en lenguajes de programación concretos y computabilidad factible, mientras que los investigadores en lógica matemática a menudo se centran en la computabilidad como concepto teórico y en la no computabilidad.

La teoría de la semántica de los lenguajes de programación está relacionada con la teoría de modelos, al igual que la verificación de programas (en particular, la verificación de modelos). La correspondencia de Curry-Howard entre pruebas y programas se relaciona con la teoría de la prueba, especialmente con la lógica intuicionista. Los cálculos formales como el cálculo lambda y la lógica combinatoria ahora se estudian como lenguajes de programación idealizados.

La informática también contribuye a las matemáticas mediante el desarrollo de técnicas para la verificación automática o incluso la búsqueda de demostraciones, como la demostración automatizada de teoremas y la programación lógica.

La teoría de la complejidad descriptiva relaciona la lógica con la complejidad computacional. El primer resultado significativo en esta área, el teorema de Fagin (1974) estableció que NP es precisamente el conjunto de lenguajes expresables por oraciones de lógica existencial de segundo orden.

Fundamentos de las matematicas

En el siglo XIX, los matemáticos se dieron cuenta de las lagunas e inconsistencias lógicas en su campo. Se demostró que los axiomas de geometría de Euclides, que se habían enseñado durante siglos como un ejemplo del método axiomático, estaban incompletos. El uso de infinitesimales y la definición misma de función se cuestionaron en el análisis, a medida que se descubrieron ejemplos patológicos como la función continua no diferenciable en ninguna parte de Weierstrass.

El estudio de Cantor de conjuntos infinitos arbitrarios también generó críticas. Leopold Kronecker dijo que "Dios hizo los números enteros; todo lo demás es obra del hombre", respaldando un regreso al estudio de objetos finitos y concretos en matemáticas. Aunque el argumento de Kronecker fue llevado adelante por los constructivistas en el siglo XX, la comunidad matemática en su conjunto los rechazó. David Hilbert argumentó a favor del estudio del infinito, diciendo: "Nadie nos expulsará del Paraíso que ha creado Cantor".

Los matemáticos comenzaron a buscar sistemas de axiomas que pudieran usarse para formalizar gran parte de las matemáticas. Además de eliminar la ambigüedad de términos previamente ingenuos como función, se esperaba que esta axiomatización permitiera pruebas de consistencia. En el siglo XIX, el método principal para probar la consistencia de un conjunto de axiomas era proporcionar un modelo para ello. Así, por ejemplo, se puede demostrar que la geometría no euclidiana es consistente definiendo punto para significar un punto en una esfera fija y línea para significar un gran círculo en la esfera. La estructura resultante, un modelo de geometría elíptica, satisface los axiomas de la geometría plana excepto el postulado de las paralelas.

Con el desarrollo de la lógica formal, Hilbert preguntó si sería posible probar que un sistema de axiomas es consistente analizando la estructura de las posibles pruebas en el sistema y mostrando a través de este análisis que es imposible probar una contradicción. Esta idea condujo al estudio de la teoría de la prueba. Además, Hilbert proponía que el análisis fuera totalmente concreto, utilizando el término finitarypara referirse a los métodos que permitiría pero sin definirlos con precisión. Este proyecto, conocido como el programa de Hilbert, se vio seriamente afectado por los teoremas de incompletitud de Gödel, que muestran que la consistencia de las teorías formales de la aritmética no puede establecerse utilizando métodos formalizables en esas teorías. Gentzen demostró que es posible producir una prueba de la consistencia de la aritmética en un sistema finito aumentado con axiomas de inducción transfinita, y las técnicas que desarrolló para hacerlo fueron fundamentales en la teoría de la prueba.

Un segundo hilo en la historia de los fundamentos de las matemáticas involucra la lógica no clásica y las matemáticas constructivas. El estudio de las matemáticas constructivas incluye muchos programas diferentes con varias definiciones de constructivo. En el extremo más complaciente, muchos matemáticos llaman constructivas a las demostraciones en la teoría de conjuntos ZF que no utilizan el axioma de elección. Las versiones más limitadas del constructivismo se limitan a los números naturales, las funciones teóricas de números y los conjuntos de números naturales (que se pueden usar para representar números reales, lo que facilita el estudio del análisis matemático). Una idea común es que se debe conocer un medio concreto para calcular los valores de la función antes de que se pueda decir que la función misma existe.

A principios del siglo XX, Luitzen Egbertus Jan Brouwer fundó el intuicionismo como parte de la filosofía de las matemáticas. Esta filosofía, mal entendida al principio, afirmaba que para que un enunciado matemático sea verdadero para un matemático, esa persona debe ser capaz de intuirla declaración, no sólo para creer en su verdad sino para entender la razón de su verdad. Una consecuencia de esta definición de la verdad fue el rechazo de la ley del tercero excluido, pues hay enunciados que, según Brouwer, no podrían ser considerados verdaderos mientras que sus negaciones tampoco podrían serlo. La filosofía de Brouwer fue influyente y la causa de amargas disputas entre destacados matemáticos. Más tarde, Kleene y Kreisel estudiarían versiones formalizadas de la lógica intuicionista (Brouwer rechazó la formalización y presentó su trabajo en un lenguaje natural no formalizado). Con el advenimiento de la interpretación BHK y los modelos Kripke, el intuicionismo se volvió más fácil de reconciliar con las matemáticas clásicas.