Overview histórico del logicismo
y la lógica matemática

Sogol Thamaem

1. Periodo embrionario
   1. Semántica,
      1

      Aka proprietates terminorum (cf. SEP).
      sintáctica y pragmática de la lógica escolástica:
      2

      Para un recorrido histórico, cf. Beuchot La filosofía del lenguaje en la Edad Media 1981.
      influencia de Peirce.
      3

      Cf. Beuchot Estudios sobre Peirce y la Escolástica 2002.
      1. Basada en los Peri hermenias y los predicamentos de Aristóteles y los predicables de Porfirio, que abren la puerta al problema de los universales.
      2. Iniciada con Anselmo de Canterbury De Grammatico c. 1060: distinción entre significare per se (aka significatio) y significare per aliud (aka appellare),
         4

         Desde William de Sherwood Introductiones in Logicam 1240s, la noción de appellare cambia, tomando suppositio su rol.
         que corresponden respectivamente, guardando las distancias, al sentido y referencia de Frege (1892),
         5

         Cf. Beuchot La teoría semántica medieval de la suppositio 1988 y Un antecesor de Frege: Vicente Ferrer (s.XIV) y la estructura proposicional 1986. Dualidad presente también en el logos apofantikós y semantikós de Aristóteles, y el lektón y pragma de los estoicos. No confundir con el significado denotativo y connotativo de Ockham (rescatado por Mill 1843), donde la denotación no es de un nombre propio (i.e., de un ente particular).
         aunque su preocupación recae más sobre la situación en la que un mismo sentido en diferentes afirmaciones cambia de referente (fallacie parvipontane).
         6

         Ejemplo de la SEP. En «Un dodo vivía, ergo un dodo vive», la referencia de «dodo» cambia en cada frase, pues la conjugación verbal pretérita la amplía a toda la historia (o, análogamente, la conjugación presente la restringe a la actualidad).

         Es interesante notar que la suppositio se dividía a su vez en formalis (uso) y materialis (mención), permitiendo distinguir entre lenguaje objeto y metalenguaje, identificando falacias como «'Caballo' tiene tres sílabas. Rocinante es un caballo. Por lo tanto, Rocinante tiene tres sílabas.» (cf. W), pudiendo asemejar la segunda al significante de Saussure (1906).
      3. Petrus Hispanus Tractatus c. 1230: manual de referencia hasta el s. XVII.
      4. Ockham Summa Logicae 1323
         1. El significatio pasa de tratarse intensional a extensionalmente en su terminismo (I.33).
            7

            «The intension [aka comprehension] of 'ship' as a substantive is 'vehicle for conveyance on water,' whereas its extension embraces such things as cargo ships, passenger ships, battleships, and sailing ships.» Britannica. (aunque esta dualidad es distinta a la de sentido y referencia, el paralelismo es claro)

            A este respecto, no es casualidad que la naive set theory de Frege (1879) introduzca ambas formas para la definición de conjuntos, que devendrán en Zermelo (1908) el axioma de extensionalidad y el de separación (aka esquema axiomático de comprensión restringido, cuya restricción introduce Zermelo para evitar la paradoja de Russell del planteamiento original de Frege: $\{x:\phi \left(x\right)\}$ vs $\{x\in z:\phi \left(x\right)\}$ es un conjunto), si bien no será hasta Fraenkel y Skolem (1922) que se explicitará el sentido de «proposición funcional $\phi$ definida» y, dicho sea de paso, se ampliara la axiomática para admitir los universos de Von Neumann mayores a $V_{2\omega }$, el cual es ya un modelo de la axiomática original y de la práctica matemática usual.

            Peirce se mostrara igualmente interesado en ambos tipos de definición (Upon Logical Comprehension and Extension 1867), y a través de él, C. W. Morris.
         2. Leyes De Morgan (II.32–3).
            8

            Esencialmente conocidas desde Aristóteles, cf. Bocheński History of Formal Logic 1956.
         3. Discusión de la implicación material e instancia de lógica trivaluada (III.III.30).
            9

            Cf. Franciscan Institute Publications: Philosophy series, Número 2, C.III (1945). No empieza a entreverse hasta Peirce 1902, y materializarse hasta Lukasiewicz 1920.
      5. Oxford Calculators XIV: designación de proposiciones mediante letras.
         10

         E.g., Paul of Venice Logica Magna 1398. Aunque las contribuciones a la física del colectivo son loables (cf. Truesdell Essays in The History of Mechanics 1968), no sé hasta que punto son realmente relevantes en ésta discusión, y como de distintiva es su práctica de la de Euclides en la designación de puntos, segmentos y ángulos.
      6. Vicente Ferrer Tractatus de suppositionibus terminorum 1372:
         11

         Cf. Beuchot Un gran lógico medieval: San Vicente Ferrer (ss. XIV-XV) 1996.
         1. En la estructura proposicional tradicional sujeto-cópula-predicado, absorbe la segunda en la tercera.
         2. Cuantificación del predicado.
   2. Análisis de paradojas autoreferenciales
      1. Adamus Parvipontanus Ars disserendi 1132: antecedente de conjunto infinito-Dedekind.
         12

         Cf. Minio-Paluello Twelfth Century Logic: Texts and studies. Vol. 1: Adam Balsamiensis Parvipontani Ars Disserendi (Dialectica Alexandri) 1956. Reaparece independientemente con Bolzano Paradoxien des Unendlichen 1830s? (publicación póstuma 1851), obra admirada por Peirce (quién da su propia definición independiente a 1881), Dedekind (1888) y Cantor, deviniendo germen de la teoría de conjuntos.
      2. Bradwardine On Insolubles 1320s: propuesta de solución.
         13

         Cf. Stephen Read Thomas Bradwardine and Epistemic Paradox 2011. Nótese que la autoreferencia seguirá candente en el s. XX a través de la paradoja de Russell o la técnica demostrativa de Gödel de los teoremas de incompletitud.
   3. Sacrobosco De sphaera mundi 1230: antecedente del mecanicismo de Hobbes.
   4. Ramon Llull Ars generalis ultima 1305: antecedente del ars combinatoria de Leibniz.
   5. Gersonides Maaseh Hoshev 1321: uso sistemático y consciente de la inducción matemática.
      14

      Hasta entonces implícita, e.g., en la demostración de Euclides de la existencia de infinitos primos o el método Chakravala de Bhaskara II (c. 1114 – 1185, Bijaganita). Primera formulación explícita en Pascal Traité du triangle arithmétique (1665). Alcanza su máxima expresión con la demostración de Dedekind por teoría de conjuntos (1888).
2. El nacimiento del álgebra y la matemática moderna en Italia y Francia, e impacto filosófico en UK y Alemania
   1. Bombelli L'Algebra 1572: enciclopedia en la que se expone la nueva álgebra iniciada por Scipione del Ferro, y en la que se da el primer tratamiento (instrumental) de los números complejos.
      15

      La idea de plano de Argand no llegará hasta 1811.
   2. Viète In artem analyticem isagoge 1591: estandariza el álgebra simbólica, proyecto continuado con Oughtred Clavis Mathematicae 1631.
      16

      Hasta entonces, cada cual (Chuquet, Pacioli, Rudolff, Stifel...) tenía su propia notación para la suma, resta, potencias, raíces, igualdades...
   3. Descartes La Geometrie 1637: primer tratado matemático moderno, salvo por la carencia de ciertas demostraciones por autoevidentes.
      17

      Dicho estándar de rigor lo inaugurara Bolzano con su aritmetización del análisis en Beyträge zu einer begründeteren Darstellung der Mathematik (1810), Der binomische Lehrsatz (1816) y Rein analytischer Beweis (1817), proyecto culminado independientemente con Weierstrass.
   4. Port-Royal Logic 1662: manual de referencia clásico hasta el s. XX.
   5. Hobbes De Corpore I: Computatio Sive Logica 1655: suggested that all logic and reasoning could be reduced to the mathematical operations of addition and subtraction, augurando la algebraización de la lógica.
   6. Spinoza Descartes 1663 y Ética 1677: el razonamiento filosófico toma la forma del razonamiento matemático del momento, el mos geometricus.
   7. Rüdiger De sensu veri et falsi 1722: defensa de la posibilidad de silogismos sintéticos (IV.II.vi.1); la lógica no es estéril, sino una fuente más de conocimiento.
   8. Wolff Latin Logic 1728: «both philosophy and mathematics derive their method from logic», que a su vez está basada (justificada) en la ontología y la psicología empírica (139, 380, 382–99).
      18

      Irónicamente, Rüdiger atacara el mos geometricus spinoziano, abogando por la separación entre lógica y matemática (siendo Boole su más importante reconciliador). Y más irónicamente aun, Kant negara (en Reflexion 1602) que la lógica tenga ningún valor sintético (separándola de la psicología empírica y la ontología), alegando que sólo clarifica, pero que no produce nuevo conocimiento, opinión que Frege compartirá (y de ahí que su logicismo le lleve a declarar a la matemática como analítica, cf. 1884 The Foundations of Arithmetic, I, 16–7).
3. Proyectos de mathesis universalis del XVII, y sus nociones de alphabet of human thought, characteristica universalis y calculus ratiocinator, que pueden pensarse como precursores de la lógica algebraica, el logicismo, los lenguajes ideales, filosóficos y universales, la lingüística computacional, la demostración automática de teoremas... Asociado con el pansophism y el Invisible College, precedente de la Royal Society.
   1. (UK) Wilkins An Essay Towards a Real Character, and a Philosophical Language 1668. Inspirado por F. Bacon Of proficience and advancement of learning 1605, Herman Hugo De Origine Scribendi 1617, etc. y primeramente divisado en Mercury or the Secret Messenger 1640.
   2. (DE) Leibniz: de Dissertatio de arte combinatoria 1666 a Mathesis Universalis 1695 (inédito hasta Leibnizens mathematische Schriften IV 1859) pasando por Generales Inquisitiones 1686.
      19

      Relevante: New Essays on Leibniz Reception: In Science and Philosophy of Science 1800-2000.
      Inspirado por Sacrobosco, Llull, Bombelli, Hobbes y Descartes (Rules for the Direction of the Mind 1628), citados explícitamente.
4. Algebraización alemana: a menudo siguiendo muy de cerca, directa o independientemente, a Leibniz.
   1. Segner Specimen logicae universaliter demonstratae 1740: tratamiento algebraico de los silogismos mediante 16 definiciones y 2 axiomas, entre las que se incluye la igualdad como dos inclusiones.
      20

      Algo de lo que se vanagloriara Frege (1879), si bien él está hablando a Boole y no, irónicamente, a sus compatriotas. Cf. Haaparanta The Development of Modern Logic, 3.10 (2009).
   2. Gottfried Ploucquet Methodus Calculandi In Logicis 1763: cuantificación no sólo del sujeto, sino también del predicado;
      21

      También presente en sus coetaneos Euler y Lambert.
      supera el intensionalismo por el extensionalismo: «when we think of the shining sun there is no distinction between subject and predicate but, when we want to communicate our thought to others, our language requires more signs, and we say 'the sun is shining'»
      22

      Sammlung der Schriften, welche den logischen Calcul Herrn Ploucquets betreffen (1766), XV, p. 245 (link)
   3. J. H. Lambert Neues Organon 1764: otro intento de mathesis universalis, incluyendo una rama de semiotica, en la que explora la relación entre significado y signo (de su mathesis),
      23

      En particular, no considera los signos del lenguaje natural, y por ende no puede caer en el problema de Venus, Héspero y Fósforo. (que los mathesis universalis solucionan el problema es obvio, lo que no tengo claro es: ¿hasta que punto esto es una de sus motivaciones?)
      en su búsqueda de un isomorfismo entre ellos.
   4. Gergonne Essai de dialectique rationelle 1816: noción de inclusión, y extensionalismo en su máxima expresión: «reasoning does not have to be about objects about which one has perfectly clear ideas, because algebraic operations can be carried out without having any idea of the meaning of the symbols involved». Antecedente Peacock.
   5. Bolzano Wissenschaftslehre 1837: «Hence I say that propositions M,N,O,… are deducible from propositions A,B,C,D,… with respect to variable parts i,j,…, if every class of ideas whose substitution for i,j,… makes all of A,B,C,D,… true, also makes all of M,N,O,… true. Occasionally, since it is customary, I shall say that propositions M,N,O,… follow, or can be inferred or derived, from A,B,C,D,…. Propositions A,B,C,D,… I shall call the premises, M,N,O,… the conclusions.»
      24

      Antecedente para la consecuencia lógica de Tarski. Equiparable al abandono de Frege de los tradicionales sujeto y predicado por argumento y función. Estilo reminiscente del Tractatus de Wittgenstein y el círculo de Viena (cf., e.g., §§31–32), pudiéndose considerar padre de la escuela analítica (cf. SEP Bolzano logic). Rescatado por Twardowski (1894), que funda la escuela polaca Lvov-Warsaw a la que Tarski pertenece. Inspiración para la fenomenología de Husserl, quien también lo reivindica.
5. Algebraización inglesa
   1. Babagge, Peacock y Herschel fundan la Analytical Society en 1812, fuente del renovado interés inglés por la lógica.
   2. George Bentham Outline of a new system of logic 1827: cuantificación de predicados.
   3. Hamilton Logic 1833: reseña la obra de Bentham, popularizando sus ideas y saltando a la fama, obteniendo su cátedra a 1836.
      25

      Publicación póstuma de sus clases en: Lectures on Metaphysics and Logic 1860.
      «induction and deduction are correlative processes of formal logic, each resting on the necessities of thought and deriving thence its several laws».
      26

      Contexto histórico: Herschel 1831, Whewell 1837, J. S. Mill 1843 y H. Spencer 1864 pontifican el razonamiento inductivo como el primordial de la ciencia.
   4. John Stuart Mill System of Logic 1843: «algebra is a highly developed logic, and number but logical discrimination.». Antecedente de logicismo.
   5. Peacock Treatise on Algebra 1830, cuya distinción entre álgebra aritmética y simbólica
      27

      Equiparable a la de Gergonne, y quizá motivada por la libre manipulación simbólica de Euler y la preocupación de Lagrange (comunicada a través de la Academia de Ciencias de Berlin, 1784) por la falta de fundamentación del cálculo.
      abre las puertas a aplicaciones no aritméticas.
      1. Gregory On the real nature of symbolical algebra 1840 y On a difficulty in the theory of algebra 1842, que influenciaran fuertemente a Boole y De Morgan.
      2. Boole Mathematical Analysis of Logic 1847 y The Laws of Thought 1854: germen para las estructuras algebraicas
         28

         Implícitas en las permutaciones de Lagrange (1770) y la aritmética modular de Gauss (1798), y explícitas en Galois (1832), que Dedekind enseña a partir de c. 1854 (Vorlesungen über Zahlentheorie 1863). Paralelamente, Grassman desarrolla su álgebra lineal (1844, 1862), que influenciaría a Schröder y Peano.
         y el álgebra de conjuntos, definiendo conjunto universal, subconjuntos suyos, elementos (electives) suyos, y operadores entre ellos.
      3. De Morgan Induction (mathematics) 1838 (formaliza el concepto), Formal Logic 1847 (cuantificación numérica de predicados: cardinalidad), Syllabus of a Proposed System of Logic 1860 (lógica de relaciones).
   6. W. S. Jevons Pure Logic 1864: extiende, estandariza y populariza a Boole.
      29

      Ejemplo: uso del or frente al xor, haciendolo dual respecto al and.
      Reframing (con el consecuente cambio notacional): la matemática debe subordinarse a la lógica y no viceversa (logicismo también presente en Lotze y Schröder).
      30

      De hecho, Frege lo cita como inspiración en sus Grundlagen (1884) junto a Mill y Leibniz, sec. 15–7.
   7. John Venn Symbolic Logic 1881:
      31

      Aunque popularmente se lo conoce por sus diagramas, «representations of concepts, propositions, and syllogisms by means of circles, lines, and other figures had already been devised by Johann Christoph Sturm (1661), who also introduced circular diagrams representing new syllogisms having negative terms»; by Leibniz; by Johann Christian Lange (1712, 1714); by Ploucquet (1759); by Lambert (1764); by Euler (1768–72)... cf. Gardner 1983, Bernhard 2001.
      continuista.
   8. Lewis Carroll The Game of Logic 1887 y Symbolic Logic 1896: popularización entre profanos.
6. Lógica matemática
   1. (UK) Hugh MacColl The Calculus of Equivalent Statements and Integration Limits I-III (1877-9): lógica proposicional. Influencia a Pierce.
   2. (DE) Frege Begriffsschrift 1879: lógica de predicados, solucionando, en particular, el problem of multiple generality.
   3. (USA) Peirce.
      32

      Cf. Irving H. Anellis How Peircean was the “‘Fregean’ Revolution” in Logic? 2012.
      1. On a New List of Categories 1867: modelo semántico triádico a la Frege, donde su ground (fundamentación) e interpretante son equiparables respectivamente al mode of presentation y sentido de Frege.
         33

         Cf. María Uxía Rivas Monroy Frege y Peirce: en torno al signo y su fundamento 1996.
      2. Logic of Relatives 1870 (ampliado en 1883 y 1897): recupera y mejora a De Morgan; Tarski construye sobre él.
      3. On the Logic of Number 1881: axiomatiza la aritmética;
         34

         Fundamentaciones constructivas independientes de Frege y Dedekind a 1884 y 1888 como parte de sus respectivos logicismos, bebiendo las axiomáticas de Peano (1891) y Zermelo (1908) de ésta última, en la que esencialmente se funda la teoría de conjuntos (que se empieza a entrever desde Dedekind 1863 y, en su vertiente transfinita, Cantor 1867, con la que Peirce también coquetea en 1860 Orders of Infinity). Cf. W. W. Tait Frege versus Cantor and Dedekind: On the Concept of Number 1992 y E. H. Reck Frege or Dedekind? Towards a Reevaluation of Their Legacies 2013.
         «father of» y «lover of» relations.
         35

         Relations of ancestral y proper ancestral en Frege 1879 (aunque no los explota en la construcción de los naturales hasta 1884), y cadenas en Dedekind 1887 (borrador 1872-8), bebiendo Zermelo (1908) y Noether de este último.
      4. On the Algebra of Logic 1885: lógica de predicados,
         36

         Conjuntamente con Oscar Howard Mitchell (1883).
         distinguiendo (a diferencia de Frege) entre 1r y 2n orden, algo que no sería practica común hasta la paradoja de Russell (1903). Primera axiomática primitiva de conjuntos.
   4. (UK) W. E. Johnson The Logical Calculus (1892) y Logic I–III (1921–1924): influenciado por Peirce.
   5. (DE) Schröder Der Operationskreis des Logikkalküls 1877 (fuertemente influenciado por Grassman,
      37

      De hecho, Schröder considera su campo de estudio el álgebra universal y no la lógica.
      y citado con aprecio por Venn y Pierce) y Vorlesungen I-III, II.2 (1890, 1891, 1895, 1905): populariza las relaciones (1895)
      38

      A través de las cuales demuestra el teorema de Cantor–Schröder–Bernstein a 1897 (propuesto por Cantor en 1887, y demostrado sin publicación ese mismo año por Dedekind). Concepto clave de los Principia y mucha de la matemática posterior.
      y la cuantificación de Peirce frente a la de Frege (1891),
      39

      Cf. Hilary Putnam Peirce the Logician 1982, quién toma como ejemplo Löwenheim y Zermelo. Salvo las dos instancias citadas, la obra de Peirce pasa bastante desapercibida: Whitehead lo descubre a 1924 y Tarski a 1940, se publica la primera antología de inéditos a 1923, la más importante a 1931–1935 (ampliada en 1958) y la definitiva (en progreso) desde 1982.
      culminando la lógica del momento.
      40

      A pesar de su modernidad, en su introducción aun se discute la fundación de la lógica en la psicología, y se mantiene la división clasica de concepto, juicio e inferencia.
7. Antinomias
   1. Cantor
      1. Fundamentos para una teoría general de conjuntos 1883.
         41

         Cf. Tait Cantor’s Grundlagen and the Paradoxes of Set Theory 2000. De la misma opinión es Purkert, aunque Ferreirós contraargumenta con un comentario de 1892 que pone de manifiesto la carencia de su comprensión del problema, cf. Cantor, descubridor de las antinomias de la teoría de conjuntos.
      2. Desde 1896, tras identificar claramente la paradoja de Cantor y de Burali-Forti, distingue entre sistemas consistentes e inconsistentes (diferenciación presente ya en Schröder 1890), y llama conjunto sólo a los primeros (análogo a la diferenciación entre conjunto y clase en NBG).
      3. Comunica el hallazgo a Hilbert, Dedekind y Berstein en 1899.
   2. Zermelo descubre independientemente la paradoja de Russell y la comunica a Hilbert, Husserl y otros miembros de Göttingen en 1899.
   3. Hilbert Über den Zahlbegriff 1900: primera publicación escrita de la paradoja de Russell, aunque de manera tangencial.
   4. Russell
      1. Empieza a interesarse por la lógica a 1897.
      2. Se familiariza con la obra de Peano en el I Congreso Internacional de Filosofía (1900), quien a su vez se había familiarizado con Dedekind y Frege a 1891.
      3. Descubre la paradoja de Russell en 1901 a propósito de los intentos de demostración de la hipótesis del continuo de Cantor.
      4. La identifica también en Begriffsschrift a 1902, carteándose con Frege.
      5. La publica en The Principles of Mathematics 1903, que en muchos sentidos es el pistoletazo de salida oficial (en tanto que mediático) del logicismo y la filosofía analítica. Preámbulo para los Principia.
8. Soluciones
   1. Logicismo. Russell y Whitehead Principia (1910–3): reducción de la matemática a la lógica mediante teoría de tipos.
      1. Church An unsolvable problem of elementary number theory 1936: untyped $\lambda$-calculus, y teoría de la computabilidad.
   2. Constructivismo-intuicionismo: limitación de los objetos matemáticos a aquellos sobre los cuales tengamos una clara intuición y podamos construir explícitamente.
      1. Brouwer 1907–1927
         42

         Precedentes: Kronecker, Poincaré, teoría descriptiva de conjuntos (Borel, Heine, Lebesgue).
         1. Interpretación «local», «verificacional» o «constructiva» (por obtención de «testigos») del cuantificador existencial, haciendose eco del «Esto es teología, ¡no matemática!» de Gordon al teorema de finitu de Hilbert (1888). Antecedente de la semántica de Kripke–Joyal (c. 1965) en teoría de topos.
            43

            Año en el que Kripke demuestra el teorema de completitud y solidez de la lógica intuicionista (Semantical analysis of intuitionistic logic).
         2. Crítica del tercero excluido y, en particular, la reducción al absurdo: demostrar que la negación es falsa no me dice nada sobre la afirmación, no me la construye; bien podría ser indemostrable. Creemos lo contrario porque ello tiene sentido en el caso finito, donde podemos verificar todas las posibilidades. Antecedente de Gödel 1931, a quien de hecho influye con sus conferencias de Viena de 1928-3-10 y 14.
            44

            Atendidas también por Wittgenstein, y posible causa para su retorno a Cambridge en 1929.
      2. Heyting
         1. Die formalen Regeln der intuitionistischen Logik I-III 1930: formalización de la lógica intuicionista; Aritmética de Heyting (HA).
         2. Die intuitionistische Grundlegung der Mathematik 1931. Interpretación BHK de las conectivas lógicas como instrucciones o algoritmos $f$ de construcción de una prueba de lo enunciado.
            45

            Ejemplo: una prueba de $p\to q$ es una función $f$ que convierte una prueba de $p$ en una prueba de $q$, en lugar de una prueba de que si $p$ es cierto $q$ también.
            Materializaciones:
            • $f$ como función computable
              46

              O equivalentemente, según la conjetura de Church-Turing, como maquina de Turing.
              (realizability theory): Kleene On the Interpretation of Intuitionistic Number Theory 1945. Continúan su senda Markov Jr y Shanin.
            • $f$ como programa, explotando la correspondencia de Curry–Howard–Bruijn (1958, 1969 [1980], 1970),
              47

              Ampliada por Lambeck a principios de los 1970s a la teoría de categorías.
              que inspira
              • Bruijn Automath: a language for mathematics 1968: precursor de Mizar (1973) y, a través de él, el QED manifesto (1994).
              • Martin-Löf An intuitionistic theory of types 1972: primero de una serie de artículos, que llegan hasta 1986,
                48

                Unifying Scott’s theory of domains for denotational semantics and intuitionistic type theory (abstract), Scott (1970) que influye también a LCF (1972), y que había sido a su vez influido por la lógica categorial de Lawrence.
                en los que va refinando su teoría, que es normalizante y, por ende, decidible. Modelo estándar de la CZF (1977 Aczel), una teoría de conjuntos constructiva.
              • Girard Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur 1972 (tesis): cálculo lambda polimorfico $F_{\omega }$.
              • Coquand y Huet A Theory of Constructions 1984 (adelanto tesis): CoC, siguiendo la estela de los anteriores; extendido a CIC en 1989, base para el asistente de prueba Coq.
                49

                Otros precedentes: McCarthy Computer programs for checking mathematical proofs 1962, que inspiraría Nqthm (1971); Kaluznin O jezyku informacyjnym matematyki 1962; J. A. Robinson A Machine-Oriented Logic Based on the Resolution Principle 1965, que inspiraría PROLOG (1972); el algoritmo DPLL (1960, 1962).
                Fuertemente normalizante y, en particular, consistente y decidible.
                50

                Demostración por modelos (pCuIC, HoTT).
      3. Errett Bishop Foundations of Constructive Analysis 1967: germen de una nueva ola, continuada por Paul Lorenzen. Myhill (1971) construye para ella la primera teoría de conjuntos de esta clase.
   3. El programa finitista de Hilbert, en dos fases:
      1. Formalismo axiomático: eliminar toda dependencia de la libre intuición que nos ha llevado a dichas antinomias fijando unas reglas, reduciendo la legitimidad de la matemática a la de dichos axiomas (a la Principia con la lógica). Popularizado por Pasch, Padoa y Hilbert. Ejemplos:
         1. Aritmética: Peirce (1881), Peano (1889).
         2. Grupos: Walther von Dyck (1882).
         3. Geometría: Pasch (1882), Mario Pieri (1898, 1900, 1908), Hilbert (1899), Veblen (1903), Heyting (1959, 1963).
         4. Conjuntos: Zermelo (1908), Fraenkel y Skolem (1922).
         5. Probabilidades: Kolmogórov (1930).
         6. Física: Hamel (1903), Carathéodory (1909, 1924), Robb (1914), von Neumann (1927).
            51

            Motivadas por el 6º problema de Hilbert.
         7. Huntington: grupos, geometría, números reales (1902) y complejos, álgebra de Boole (1904, 1933).
      2. Demostrar la consistencia de dichas formalizaciones mediante métodos finitistas basados en la pura intuición de signos concretos y su mera mera manipulación sintáctica,
         52

         Calificado por H. Weyl (1925 Die heutige Erkenntnislage in der Mathematik) de juego de formulas sin significado. En cierta manera, reconciliación con las críticas de Brouwer, en el sentido de que el garante último es una intuición de un objeto concreto, y las construcciones explicitas que de él se derivan; otro tema es que las reglas de dicha sintaxis difieran entre Hilbert y Brouwer, entre la lógica de predicados clásica y la intuicionista.
         reduciendo la legitimidad del primero a la del segundo.
         53

         Aka conservación: cualquier demostración vía objetos ideales (como los conjuntos incontables) puede demostrarse sin ellos.
         1. Hilbert Mathematische Probleme, Nachrichten von der königlichen Gesellschaft der Wissenschaften zu Göttingen 1900 (2º): populariza el problema.
         2. Hilbert Prinzipien der Mathematik 1918, Neubegründung der Mathematik: Erste Mitteilung 1922, etc.: de 1917 a 1923, y con la asistencia de sus alumnos Behmann (que empieza a estudiar los Principia a 1914) y más particularmente Bernays, retoma su interés por la lógica, marcado por:
            • Su desconfianza del logicismo: la matemática no puede reducirse a la lógica, como pone de manifiesto el polémico axioma de reducibilidad de los Principia, más matemático que lógico.
            • Su rechazo al intuicionismo de Brouwer, que considera demasiado limitante.
              54

              «Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists» Die logischen Grundlagen der Mathematik 1923
            • Las carencias de la lógica de Schröder, basada en la tradición algebraica,
              55

              En este sentido, probablemente habría que decir que los genuinos padres de la lógica matemática (en el sentido metamatematico) son Hilbert, Russell, Gödel, Gentzen y Tarski, con quienes se alcanza una clara separación entre sintaxis y semántica. Cf., e.g., Logic Without Borders, preface 2015.
              y que hacen necesario introducir:
              • un nuevo formalismo o lenguaje lógico para los nuevos planteamientos axiomáticos, el $\epsilon$-calculus.
                56

                Dicha epsilon es el germen del actual símbolo de pertenencia, a través de la obra de Bourbaki, así como del operador epsilon de ATPs tipo HOL o Isabelle. En este sentido
              • un procedimiento asociado de demostración de consistencia, el $\epsilon$-substitution method.
            • El problema de la decibilidad
              57

              Aunque presente en 1900, se explicita en su forma de Entscheidungsproblem en 1928, probado negativamente por Church y Turing a 1936.
              y la completitud: probar que todas las afirmaciones verdaderas son demostrables, y dar un algoritmo que determine su veracidad o, aun mejor, las enumere.
         3. Ackermann Die Widerspruchsfreiheit des Auswahlaxioms 1924:
            58

            Tesis dirigida por Hilbert.
            presentación final de la nueva lógica, generalizando la $\epsilon$-substitution a la aritmética de segundo orden (aka análisis).
            59

            Su prueba de consistencia se demuestra errónea con Neuman a 1927 (Zur Hilbertschen Beweistheorie), y parcialmente fútil con Gödel y Gentzen, corrigiéndola a 1940.
            Teorema de consistencia de Hilbert–Ackerman, extendido por Herbrand en 1930.
         4. Hilbert y Bernays Grundlagen der Mathematik I-II (1934,9): culminación de la lógica del momento, incluyendo una detallada demostración del teorema de incompletitud de Gödel (1939).
9. Gödel, intentando contribuir al programa de Hilbert, lo entierra
   1. Über die Vollständigkeit des Logikkalküls 1929: si una formula de la lógica de primer orden es cierta para todo modelo suyo, entonces es demostrable.
   2. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I 1931
      1. Cualquier sistema formal $F$ consistente con suficiente aritmética
         60

         I.e., en la que se pueda probar que la multiplicación es una función total, cf. Willard Self Verifying Axiom Systems, the Incompleteness Theorem and the Tangibility Reflection Principle 2001.
         (e.g., ZF, Peano, Robinson) es incompleto, i.e., contiene proposiciones indemostrables en $F$ (i.e., por 1929, ciertas o falsas según el modelo).
         61

         Formulación generalizada en Kleene 1936. Utilizado como defensa de la existencia de verdades sintéticas en matemáticas por Gödel (1944 Russell’s Mathematical Logic) y Putnam (1975 What is Mathematical Truth?).
      2. Su consistencia es una proposición indemostrable.
   3. Ejemplos de resultados indemostrables:
      1. Teorema de Paris–Harrington (1977): versión fortificada del teorema de Ramsey finito (1930), enunciable pero indemostrable en (aka independiente de) la Aritmética de Peano (PA). Prueba vía demostración de la consistencia de PA en PA+teorema.
      2. Teorema de Goodstein (1944): independencia de PA por Kirby y Paris (1982).
      3. Teorema de Kruskal (1960): independiente de la matemática predicativista, a medio camino entre PA y CZF (Simpson 1985).
      4. Teorema de determinación de Borel (1975): Friedman demuestra en 1971 (construyendo un modelo para el que falla) que es independiente de ZC (i.e., que requiere del axioma de remplazo).
      5. Axioma de determinación proyectiva: problema abierto durante décadas, se demuestra su independencia de ZFC a 1970 construyendo el modelo de Solovay. Demostración usando cardinales de Woodin a 1989 (Martin y Steel).
   4. Ejemplos de sistemas sin suficiente aritmética que son consistentes y completos:
      62

      Si $F$ es completa, entonces $F$ es decidible, pero el reciproco no es cierto en general. Otros resultados relevantes: teorema de indecibilidad de Church (1936) y test de Łoś–Vaught (1954).
      1. Presburger Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt 1929: aritmética sin multiplicación; incluye un algoritmo de decibilidad.
      2. Tarski What is elementary geometry? 1959: axiomática de la geometría euclideana.
      3. The theory of algebraically closed fields of a given characteristic.
         63

         Relevante: Tarski A decision method for elementary algebra and geometry (1948), explotando el axioma de Cantor–Dedekind.
10. Reacciones
    1. Pruebas de consistencia relativa (i.e., desde otro sistema formal) y pruebas de consistencia para modelos particulares. Ejemplos:
       1. Gentzen: ordinal analysis
          64

          Senda continuada por Schütte.
          1. Untersuchungen über das logische Schließen I-II 1934-5: teorema de corte-eliminación, piedra angular de la proof-theoretic semantics.
             65

             Por el isomorfismo de Curry–Howard, corresponde a algoritmos de normalización fuerte.
          2. Die Widerspruchsfreiheit der reinen Zahlentheorie 1936: consistencia de PA asumiendo el principio de inducción transfinita hasta el ordinal ${\epsilon }_0$ (que por Gödel 1931, es por ende indemostrable en PA).
             66

             En otras palabras, la consistency strength de PA es ${\epsilon }_0=sup{\{}^n\omega {\}}_n$.
       2. Ackermann Die Widerspruchsfreiheit der allgemeinen Mengenlehr 1937: consistencia para un modelo de ZFC sin el axioma de infinitud.
          67

          Cf. Abian y LaMacchia On the consistency and independence of some set-theoretical axioms 1978 para una reexposición más moderna.
       3. Gödel
          1. Zur intuitionistischen Arithmetik und Zahlentheorie 1933: HA y PA son equiconsistentes, vía el Gödel–Gentzen negative translation.
             68

             «this result of Gödel's drew the attention of the Hilbert school to two observations: first, that intuitionistic logic goes beyond finitism, and secondly, that finitist systems may not be the only acceptable ones from the foundational point of view»
          2. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes 1958: consistencia de HA en el sistema T (a simply typed lambda calculus) mediante su semántica dialéctica.
    2. Limitar dentro de lo posible la práctica matemática a sistemas con mayor consistency strength, atendiendo al programa de Reverse mathematics de Friedman (1975) y Simpson.
       1. Feferman: la matemática predicativista
          69

          Abusando mucho de la notación, de ordinal ${\Gamma }_0=min\{\alpha :{\varphi }_{\alpha }\left(0\right)=\alpha \}$, con ${\varphi }_{\alpha }$ la función de Veblen: ${\varphi }_0\left(\gamma \right)={\omega }^{\gamma }$, ${\varphi }_1\left(\gamma \right)={\epsilon }_{\gamma }$ y ${\varphi }_{\alpha }\left(\gamma \right)$ el $\left(\gamma +1\right)$-ésimo (en orden de tamaño) punto fijo común a toda ${\varphi }_{\beta }$ con $\beta <\alpha$ (i.e., ${\varphi }_{\alpha }=\{\delta :{\bigwedge }_{\beta <\alpha }\delta ={\varphi }_{\beta }\left(\delta \right)\}$). Notablemente, ${\Gamma }_0$ es contable, aunque existen ordinales mucho mayores que también siguen siendolo. No se conoce el ordinal correspondiente a ZFC.
          es suficiente para la mayor parte de la matemática ordinaria.
          70

          Cf., e.g., Why a little bit goes a long way: Logical foundations of scientifically applicable mathematics 1993.
       2. Friedman grand conjectures (1999): ídem con EFA, de ordinal ${\omega }^3$.
          71

          Relevante: McLarty The large structures of Grothendieck founded on finite order arithmetic 2011.
    3. QED Manifesto (1994): en pos de una informatización de todo el conocimiento matemático, permitiendo la verificación automática de teoremas sin necesidad de pasar por cada vez más largas revisiones por pares.
       72

       E.g., 6 años para la propuesta de solución de la conjetura abc de Mochizuki, tumbada por Scholze en 2018.
    4. Instrumentalismo: no hay razones para desconfiar de la consistencia de las formalizaciones axiomáticas, ya que no han vuelto a aparecer antinomias. No en balde, no hemos renunciado a la física de Newton, Einstein o Planck simplemente por no ser teorías del todo.
11. Categorical logic y theory of toposes: ¿una nueva master theory?
    1. William Lawvere
       1. Functorial Semantics of Algebraic Theories 1963 (tesis): los cuantificadores existenciales y universales pueden ser caracterizados como casos especiales de functores adjuntos.
       2. Adjointness in Foundations 1969: generaliza los topos de Grothendieck a topos elementales.
    2. Peter Johnstone
       1. Topos Theory 1977: referencia estándar.
       2. Sketches of an Elephant: A Topos Theory Compendium I-II (2002): renombrado como «Principia Toposophica» por S. Awodoy. El índice por sí solo (desglosado en nLab) ya es bastante revelador.

Adenda

Esta investigación de dos semanas nace ante la incomodidad que me producía la afirmación «la lógica matemática nace con Frege en 1879»,

73

Y de ahí que la primera parte del overview histórico sea en constante referencia a Frege, incluyendo antecedentes de su semántica y su propuesta de un lenguaje ideal.

debido a que:

1. En la carrera sólo recuerdo oír el nombre de Frege en relación a Dedekind (1888), obra sobre la que hice un trabajo-reseña en Historia, y para la cual llegué a ojear la obra de Frege: mi primera impresión, que sigo manteniendo, fue que Dedekind era mucho más elegante que Frege, y de ahí parte de mi inquietud.
   1. También es verdad que sus intereses eran muy distintos, y que los míos se alinean más con los de Dedekind, por los que mi sesgo es inescapable: mientras Frege (y su logicismo) devendría el germen de la teoría de pruebas y de la computabilidad con Gödel & co durante los 1930s a través de los Principia, Dedekind (y su estructuralismo) lo sería de la teoría de conjuntos y de modelos, siendo todas ellas las cuatro ramas que componen la lógica matemática.
2. En la carrera me incline hacia las optativas de lógica, por lo que situar su nacimiento tan reciente se sentía como un ataque a toda la matemática, pero lo cierto es que la lógica nunca jugó un papel determinante en su práctica. Sí, Descartes, Bolzano y Bourbaki elevaron sucesivamente los estándares de rigor, pero el matemático promedio actual apenas necesita de los rudimentos de teoría de conjuntos y de lógica de primer orden para subsistir (y a veces ni eso), y la demostración de Euclides de la infinitud de números primos sigue siendo tan vigente como en su origen. En otras palabras, que la lógica matemática nazca en el s. XX no significa que la matemática anterior fuera ilógica.
   1. Y tampoco hay que olvidar que durante buena parte de su historia, sus preocupaciones fueron mucho más concretas (o quizá, incluso, simplemente distintas): la geometría euclideana (que seguía desarrollándose a I dC con autores como Menelao), la resolución de ecuaciones (eliminación gaussiana,
      74

      Los nueve capítulos sobre arte matemático 179 dC
      algoritmo de Horner,
      75

      Zhu Shijie Jade Mirror of the Four Unknowns s. XIII.
      etc.), el desarrollo del cálculo (Eudoxo, Zu Chongzhi, etc.)...