Historia de la teoría de tipos

En una carta a Gottlob Frege (1902), Bertrand Russell anunció su descubrimiento de la paradoja en el Begriffsschrift de Frege . ^{[ 1 ]} Frege respondió de inmediato, reconociendo el problema y proponiendo una solución en una discusión técnica sobre " niveles ". Citando a Frege:

Por cierto, me parece que la expresión «un predicado se predica de sí mismo» no es exacta. Un predicado es, por regla general, una función de primer nivel, y esta función requiere un objeto como argumento y no puede tenerse a sí misma como argumento (sujeto). Por lo tanto, preferiría decir «un concepto se predica de su propia extensión». ^{[ 2 ]}

Intenta mostrar cómo podría funcionar, pero parece retractarse. Como consecuencia de lo que se conoce como la paradoja de Russell, tanto Frege como Russell tuvieron que enmendar rápidamente las obras que tenían en imprenta. En un apéndice B que Russell añadió a sus Principios de las Matemáticas (1903) se encuentra su teoría "tentativa" de los tipos. El asunto atormentó a Russell durante unos cinco años. ^{[ 3 ]}

Willard Quine ^{[ 4 ]} presenta una sinopsis histórica del origen de la teoría de los tipos y la teoría "ramificada" de los tipos: después de considerar abandonar la teoría de los tipos (1905), Russell propuso a su vez tres teorías:

Quine observa que la introducción por parte de Russell de la noción de "variable aparente" tuvo el siguiente resultado:

La distinción entre "todo" y "cualquiera": "todo" se expresa mediante la variable ligada ("aparente") de cuantificación universal, que abarca un tipo, y "cualquiera" se expresa mediante la variable libre ("real") que se refiere esquemáticamente a cualquier cosa no especificada, independientemente del tipo.

Quine descarta esta noción de "variable ligada" como " inútil aparte de cierto aspecto de la teoría de tipos ". ^{[ 5 ]}

Quine explica la teoría ramificada de la siguiente manera: «Se la ha llamado así porque el tipo de una función depende tanto de los tipos de sus argumentos como de los tipos de las variables aparentes contenidas en ella (o en su expresión), en caso de que estas excedan los tipos de los argumentos». ^{[ 5 ]} Stephen Kleene, en su Introducción a la metamatemática de 1952 ^{[ 6 ],} describe la teoría ramificada de tipos de esta manera:

Los objetos o individuos primarios (es decir, las cosas dadas que no están sujetas a análisis lógico) se asignan a un tipo (digamos tipo 0 ), las propiedades de los individuos al tipo 1 , las propiedades de las propiedades de los individuos al tipo 2 , etc.; y no se admiten propiedades que no se incluyan en uno de estos tipos lógicos (por ejemplo, esto coloca las propiedades "predecible" e "impredicable"... fuera del ámbito de la lógica). Una descripción más detallada describiría los tipos admitidos para otros objetos como relaciones y clases. Luego, para excluir las definiciones impredicativas dentro de un tipo, los tipos por encima del tipo 0 se separan aún más en órdenes. Así, para el tipo 1, las propiedades definidas sin mencionar ninguna totalidad pertenecen al orden 0 , y las propiedades definidas utilizando la totalidad de las propiedades de un orden dado pertenecen al siguiente orden superior. ... Pero esta separación en órdenes hace imposible construir el análisis familiar, que vimos anteriormente que contiene definiciones impredicativas. Para evitar este resultado, Russell postuló su axioma de reducibilidad , que afirma que a cualquier propiedad perteneciente a un orden superior al más bajo, le corresponde una propiedad coextensiva (es decir, una que poseen exactamente los mismos objetos) de orden 0. Si solo se consideran propiedades definibles, entonces el axioma significa que a cada definición impredicativa dentro de un tipo dado le corresponde una definición predicativa equivalente (Kleene 1952:44–45).

Pero como las estipulaciones de la teoría ramificada resultarían (citando a Quine) "onerosas", Russell, en su obra de 1908, Lógica matemática basada en la teoría de tipos ^{[ 7 ],} también propuso su axioma de reducibilidad . En 1910, Whitehead y Russell, en sus Principia Mathematica, ampliaron aún más este axioma con la noción de matriz : una especificación completamente extensional de una función. A partir de su matriz, se podía derivar una función mediante el proceso de "generalización" y viceversa; es decir, los dos procesos son reversibles: (i) generalización de una matriz a una función (utilizando variables aparentes) y (ii) el proceso inverso de reducción de tipo mediante la sustitución de argumentos por la variable aparente en cursos de valores. Con este método se podía evitar la impredicatividad. ^{[ 8 ]}

En 1921, Emil Post desarrolló una teoría de las "funciones de verdad" y sus tablas de verdad, que reemplazan la noción de variables aparentes frente a variables reales. En su "Introducción" (1921): "Mientras que la teoría completa [de Whitehead y Russell (1910, 1912, 1913)] requiere para la enunciación de sus proposiciones variables reales y aparentes, que representan tanto individuos como funciones proposicionales de diferentes tipos, y como resultado requiere la engorrosa teoría de tipos, esta subteoría utiliza solo variables reales, y estas variables reales representan solo un tipo de entidad, que los autores han optado por llamar proposiciones elementales". ^{[ 9 ]}

Casi al mismo tiempo, Ludwig Wittgenstein desarrolló ideas similares en su obra de 1922, Tractatus Logico-Philosophicus :

3.331 A partir de esta observación, obtenemos una perspectiva más amplia sobre la Teoría de los Tipos de Russell. El error de Russell se evidencia en el hecho de que, al elaborar sus reglas simbólicas, tiene que hablar de los significados de sus signos.

3.332 Ninguna proposición puede decir nada sobre sí misma, porque el signo proposicional no puede estar contenido en sí mismo (esa es toda la "teoría de los tipos").

3.333 Una función no puede ser su propio argumento, porque el signo funcional ya contiene el prototipo de su propio argumento y no puede contenerse a sí mismo...

Wittgenstein también propuso el método de la tabla de verdad. En sus secciones 4.3 a 5.101, Wittgenstein adopta un trazo de Sheffer no acotado como su entidad lógica fundamental y luego enumera las 16 funciones de dos variables ( 5.101 ).

La noción de matriz como tabla de verdad aparece tan tarde como en los años 1940-1950 en la obra de Tarski, por ejemplo, en sus índices de 1946 "Matriz, ver: Tabla de verdad" ^{[ 10 ].}

Russell, en su Introducción a la filosofía matemática de 1920, dedica un capítulo entero a «El axioma del infinito y los tipos lógicos», donde expone sus inquietudes: «Ahora bien, la teoría de tipos no pertenece enfáticamente a la parte acabada y certera de nuestra materia: gran parte de esta teoría aún es incipiente, confusa y oscura. Pero la necesidad de alguna doctrina de tipos es menos dudosa que la forma precisa que debería adoptar dicha doctrina; y en relación con el axioma del infinito, resulta particularmente fácil ver la necesidad de tal doctrina». ^{[ 11 ]}

Russell abandona el axioma de reducibilidad : En la segunda edición de Principia Mathematica (1927) reconoce el argumento de Wittgenstein. ^{[ 12 ]} Al comienzo de su Introducción declara «no cabe duda... de que no hay necesidad de distinguir entre variables reales y aparentes...». ^{[ 13 ]} Ahora adopta plenamente la noción de matriz y declara «Una función solo puede aparecer en una matriz a través de sus valores » (pero discrepa en una nota a pie de página: «Sustituye (no del todo adecuadamente) al axioma de reducibilidad» ^{[ 14 ]} ). Además, introduce una nueva noción (abreviada y generalizada) de «matriz», la de una « matriz lógica ... una que no contiene constantes. Así, p | q es una matriz lógica». ^{[ 15 ]} Así, Russell prácticamente ha abandonado el axioma de reducibilidad, ^{[ 16 ]} pero en sus últimos párrafos afirma que de "nuestras proposiciones primitivas actuales" no puede derivar "relaciones de Dedekindia y relaciones bien ordenadas" y observa que si existe un nuevo axioma que reemplace al axioma de reducibilidad, "aún está por descubrirse". ^{[ 17 ]}

En la década de 1920, Leon Chwistek ^{[ 18 ]} y Frank P. Ramsey ^{[ 19 ]} observaron que, si uno está dispuesto a renunciar al principio del círculo vicioso , la jerarquía de niveles de tipos en la "teoría ramificada de tipos" puede colapsarse.

La lógica restringida resultante se denomina teoría de tipos simples ^{[ 20 ]} o, quizás más comúnmente, teoría de tipos simples ^{[ 21 ]} . Formulaciones detalladas de la teoría de tipos simples fueron publicadas a finales de la década de 1920 y principios de la de 1930 por R. Carnap, F. Ramsey, WVO Quine y A. Tarski. En 1940, Alonzo Church la reformuló como cálculo lambda de tipos simples ^{[ 22 ] y fue examinada por Gödel en 1944. Un resumen de estos desarrollos se encuentra en Collins (2012) [ 23 ]} .