Lógica Intuicionista

El matemático holandés Luitzen Egbertus Jan Brouwer (1881-1966) a comienzos del siglo XX tuvo la idea fundamental de que los argumentos no constructivos se evitarían si uno abandona un principio de la lógica clásica que está detrás de las leyes de De Morgan. Este es el principio del tercero excluido, que afirma que, para cada proposición p, p o no p; y equivalentemente que, para cada p, no no p implica p. Este principio es básico para la lógica clásica y ya había sido enunciado por Aristóteles, aunque con algunas reservas, ya que señaló que la afirmación de que “habrá una batalla naval mañana” no es ni verdadera ni falsa.

Luitzen Egbertus Jan Brouwer

Brouwer no afirmó que el principio del tercero excluido siempre falla, sólo que puede fallar en la presencia de conjuntos infinitos. De dos números naturales e  uno siempre puede decidir si o , pero de dos números reales esto podría no ser posible, ya que uno podría tener que saber un número infinito de dígitos de sus desarrollos decimales. Objeciones similares se aplican a las leyes de De Morgan, una consecuencia del principio del tercero excluido. Para un conjunto finito , si se ha demostrado que la aserción  conduce a una contradicción,  puede ser verificada mirando cada elemento de por vez; es decir, la afirmación de que ningún miembro de un conjunto dado tiene una determinada propiedad puede ser refutada examinando sucesivamente cada elemento del conjunto. Para un conjunto infinito , no hay forma de realizar tal inspección.

La filosofía de la matemática de Brouwer se llama intuicionismo. Aunque el propio Brouwer sentía que la matemática era independiente del lenguaje, su discípulo Arend Heyting (1898-1980) estableció un lenguaje formal para la aritmética intuicionista de primer orden. Algunos de los seguidores posteriores de Brouwer incluso estudiaron la teoría del tipo intuicionista, que difiere de la teoría de tipos clásicos sólo por la ausencia de un solo axioma (doble negación):

donde  es el tipo de valores de verdad.

Arend Heyting

Aunque no se puede decir que muchos matemáticos practicantes han seguido a Brouwer al rechazar este principio por razones filosóficas, fue una gran sorpresa para las personas que trabajan en la teoría de categorías que a ciertas categorías importantes llamadas topoi (singular: topos) les han asociado un lenguaje que es intuicionista en general.

La forma moderada del intuicionismo considerada aquí abarca el constructivismo de Kronecker, pero no la posición más extrema del finitismo. De acuerdo con esta visión, que se remonta a Aristóteles, no existen conjuntos infinitos, excepto potencialmente. De hecho, es precisamente en la presencia de conjuntos infinitos que los intuicionistas abandonan el principio clásico del tercero excluido.

Una posición aún más extrema, llamada ultrafinitismo, sostiene que incluso no existen números muy grandes, digamos números mayores de . Por supuesto, la gran mayoría de los matemáticos rechaza este punto de vista al referirse a , pero los verdaderos creyentes tienen maneras sutiles de superar esta objeción, la cual, sin embargo, está fuera del alcance de esta discusión.

Argumentos no constructivos

Otra crítica al programa Cantor-Frege fue planteada por Kronecker, quien se opuso a argumentos no constructivos, como la siguiente prueba de que existen números irracionales y tales que es racional. Si es racional, entonces la prueba está completa; de lo contrario tomar y , de modo que . El argumento es no constructivo, porque no nos dice qué alternativa se cumple. En el presente caso, el resultado se puede probar constructivamente tomando y . Pero hay otros teoremas clásicos para los cuales no existe ninguna prueba constructiva.

Leopold Kronecker

Consideremos, por ejemplo,

que simboliza la afirmación de que existe una persona famosa si hay personas famosas. Esto se puede demostrar con la ayuda de las leyes de De Morgan, nombradas después del matemático y lógico inglés Augustus De Morgan (1806-1871). Afirma la equivalencia de  con , usando la lógica clásica, pero no hay manera de construir un , por ejemplo, cuando  afirme la existencia de un buen orden de los reales, como lo demostró Solomon Feferman. Se dice que un conjunto ordenado está bien ordenado si cada subconjunto no vacío tiene un elemento mínimo.

Augustus De Morgan

El matemático alemán Ernst Zermelo (1871-1951) demostró que todo conjunto puede ser bien ordenado, siempre y cuando se adopte otro axioma, el axioma de elección, que dice que, para toda familia no vacía de conjuntos no vacíos, hay un conjunto que se puede obtener seleccionando exactamente un elemento de cada uno de estos conjuntos. Este axioma es una fértil fuente de argumentos no constructivos.

Ernst Zermelo

Construcciones lógicas impredicativas

Una serie de matemáticos del siglo XIX encontró fallas en el programa de reducción de la matemática a la aritmética y la teoría de conjuntos, como sugiere la obra de Cantor y Frege. En particular, el matemático francés Henri Poincaré (1854-1912) se opuso a las construcciones impredicativas, que construyen una entidad de cierto tipo en términos de entidades del mismo tipo o de tipo superior, es decir, construcciones y definiciones auto-referenciadas.

Henri Poincaré

Parecía que para hacer un análisis ordinario se requerían construcciones impredicativas. Russell y Whitehead intentaron infructuosamente basar la matemática en una teoría de tipo predicativo.

B. Russell y A. N. Whitehead

Pero, aunque renuentes, tuvieron que introducir un axioma adicional, el axioma de la reducibilidad, que lograba alcanzar el objetivo después de todo. Más recientemente, el lógico sueco Per Martin-Löf presentó una nueva teoría de tipo predicativo, pero nadie afirma que sea adecuada para todo el análisis clásico. Sin embargo, el matemático alemán-americano Hermann Weyl (1885-1955) y el matemático estadounidense Solomon Feferman demostraron que argumentos impredicativos como los anteriores pueden ser evitados y no son necesarios para la mayoría, o incluso para todo el análisis. Por otro lado, como lo señaló el científico italiano Giuseppe Longo (1941-), las construcciones impredicativas son extremadamente útiles en informática, es decir, para producir puntos fijos (entidades que permanecen sin cambios en un proceso dado).

Per Martin-Löf

Hermann Weyl

Solomon Feferman