La teoría de tipos se creó inicialmente para evitar paradojas en una variedad de lógicas formales y sistemas de reescritura . Más tarde, la teoría de tipos se refirió a una clase de sistemas formales , algunos de los cuales pueden servir como alternativas a la teoría de conjuntos ingenua como base para todas las matemáticas.
Ha estado vinculado a las matemáticas formales desde Principia Mathematica hasta los asistentes de prueba de hoy .
1900-1927
Origen de la teoría de tipos de Russell
En una carta a Gottlob Frege (1902), Bertrand Russell anunció su descubrimiento de la paradoja en la Begriffsschrift de Frege . [1] Frege respondió rápidamente, reconociendo el problema y proponiendo una solución en una discusión técnica de "niveles". Para citar 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 tener a sí misma como argumento (sujeto). Por tanto, preferiría decir que "un concepto se basa en su propia extensión". [2]
Sigue mostrando cómo podría funcionar esto, pero parece retroceder. Como consecuencia de lo que se conoce como la paradoja de Russell, tanto Frege como Russell tuvieron que modificar rápidamente las obras que tenían en las imprentas. En un Apéndice B que Russell añadió a sus Principios de las matemáticas (1903) se encuentra su teoría de tipos "provisional". 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 tipos y la teoría "ramificada" de tipos: tras considerar abandonar la teoría de tipos (1905), Russell propuso a su vez tres teorías:
- la teoría del zigzag
- teoría de la limitación de tamaño,
- la teoría sin clases (1905-1906) y luego,
- retomando la teoría de tipos (1908ff)
Quine observa que la introducción de Russell de la noción de "variable aparente" tuvo el siguiente resultado:
la distinción entre 'todos' y 'cualquiera': 'todos' 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 un cierto aspecto de la teoría de tipos ". [5]
La teoría de tipos "ramificada" de 1908
Quine explica la teoría ramificada de la siguiente manera: "Se 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 excedan los tipos de argumentos ". [5] Stephen Kleene en su Introducción a las metamatemáticas de 1952 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 caigan en uno de estos tipos lógicos (por ejemplo, esto pone las propiedades 'predicables' e 'impredicables' ... fuera del ámbito de la lógica). Una explicación más detallada describiría los tipos admitidos para otros objetos como relaciones y clases. Luego, para excluir definiciones impredicativas dentro de un tipo, los tipos anteriores al tipo 0 se separan 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 propiedades de un orden dado pertenecen al siguiente orden superior. ... Pero esta separación en órdenes hace que sea imposible construir el análisis familiar, que vimos arriba contiene definiciones impredicativas. Para escapar de este resultado, Russell postuló su axioma de reducibilidad , que afirma que para cualquier propiedad que pertenezca a un orden por encima del más bajo, hay una propiedad coextensiva (es decir, una poseída por exactamente los mismos objetos) de orden 0. Si solo las propiedades definibles son Si se considera que existe, entonces el axioma significa que para cada definición impredicativa dentro de un tipo dado hay una predicativa equivalente (Kleene 1952: 44-45).
El axioma de reducibilidad y la noción de "matriz"
Pero debido a que las estipulaciones de la teoría ramificada resultarían (para citar a Quine) "onerosas", Russell en su lógica matemática de 1908 basada en la teoría de tipos [6] también propondría su axioma de reducibilidad . En 1910, Whitehead y Russell en sus Principia Mathematica aumentarían aún más este axioma con la noción de matriz , una especificación completamente extensiva de una función. A partir de su matriz, una función podría derivarse 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 (mediante el uso de variables aparentes) y (ii) el proceso inverso de reducción de tipo por cursos de valores sustitución de argumentos por la variable aparente. Mediante este método se podría evitar la impredicatividad. [7]
Tablas de verdad
En 1921, Emil Post desarrollaría una teoría de las "funciones de verdad" y sus tablas de verdad, que reemplazan la noción de variables aparentes versus variables reales. De 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 a individuos como a funciones proposicionales de diferentes tipos, y como resultado necesita la engorrosa teoría de tipos, esta subteoría utiliza sólo variables reales, y estas variables reales representan sólo un tipo de entidad, que los autores han elegido llamar proposiciones elementales ". [8]
Aproximadamente al mismo tiempo, Ludwig Wittgenstein desarrolló ideas similares en su obra de 1922 Tractatus Logico-Philosophicus :
3.331 De esta observación obtenemos una visión más amplia: la Teoría de tipos de Russell. El error de Russell se demuestra por el hecho de que al redactar 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 (es decir, toda la "teoría de 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 su 4.3 a 5.101, Wittgenstein adopta un trazo de Sheffer ilimitado 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 los años 1940-1950 en el trabajo de Tarski, por ejemplo, sus índices de 1946 "Matriz, ver: Tabla de la verdad" [9]
Las dudas de Russell
Russell en su Introducción a la Filosofía Matemática de 1920 dedica un capítulo completo a "El axioma del infinito y los tipos lógicos" en el que expresa sus preocupaciones: "Ahora bien, la teoría de los tipos no pertenece enfáticamente a la parte terminada y determinada de nuestro tema: gran parte de Esta teoría es todavía incipiente, confusa y oscura. Pero la necesidad de alguna doctrina de tipos es menos dudosa que la forma precisa que debería tomar la doctrina; y en conexión con el axioma del infinito es particularmente fácil ver la necesidad de tal teoría. doctrina". [10]
Russell abandona el axioma de reducibilidad : en la segunda edición de Principia Mathematica (1927) reconoce el argumento de Wittgenstein. [11] Al comienzo de su Introducción, declara que "no puede haber ninguna duda ... de que no es necesaria la distinción entre variables reales y aparentes ...". [12] Ahora abraza completamente la noción de matriz y declara "Una función sólo puede aparecer en una matriz a través de sus valores " (pero objeta en una nota al pie de página: "Toma el lugar (no del todo adecuadamente) del axioma de reducibilidad" [13] ] ). Además, introduce una nueva noción (abreviada, generalizada) de "matriz", la de una "matriz lógica ... una que no contiene constantes. Por tanto, p | q es una matriz lógica". [14] Así Russell prácticamente ha abandonado el axioma de reducibilidad, [15] pero en sus últimos párrafos afirma que de "nuestras actuales proposiciones primitivas" no puede derivar "relaciones dedekindianas y relaciones bien ordenadas" y observa que si hay un nuevo axioma para reemplazar el axioma de reducibilidad "queda por descubrir". [dieciséis]
Teoría de tipos simples
En la década de 1920, Leon Chwistek [17] y Frank P. Ramsey [18] notaron que, si uno está dispuesto a abandonar el principio del círculo vicioso , la jerarquía de niveles de tipos en la "teoría ramificada de tipos" puede colapsar.
La lógica restringida resultante se denomina teoría de tipos simples [19] o, quizás más comúnmente, teoría de tipos simples. [20] R. Carnap, F. Ramsey, WVO Quine y A. Tarski publicaron formulaciones detalladas de la teoría de tipos simples a fines de la década de 1920 y principios de la de 1930. En 1940, Alonzo Church (re) lo formuló simplemente como cálculo lambda mecanografiado . [21] y examinado por Gödel en 1944. Un estudio de estos desarrollos se encuentra en Collins (2012). [22]
Década de 1940 hasta el presente
Gödel 1944
Kurt Gödel en su lógica matemática de Russell de 1944 dio la siguiente definición de la "teoría de tipos simples" en una nota al pie:
- Por teoría de tipos simples me refiero a la doctrina que dice que los objetos del pensamiento (o, en otra interpretación, las expresiones simbólicas) se dividen en tipos, a saber: individuos, propiedades de individuos, relaciones entre individuos, propiedades de tales relaciones, etc. (con una jerarquía similar para las extensiones), y que las oraciones de la forma: " a tiene la propiedad φ ", " b tiene la relación R con c ", etc. no tienen sentido, si a, b, c, R, φ no son de tipos que encajen. Se excluyen los tipos mixtos (como las clases que contienen individuos y clases como elementos) y, por tanto, también los tipos transfinitos (como la clase de todas las clases de tipos finitos). Que la teoría de los tipos simples es suficiente para evitar también las paradojas epistemológicas lo demuestra un análisis más detallado de estas. (Cf. Ramsey 1926 y Tarski 1935 , p. 399) ". [23]
Concluyó que (1) la teoría de tipos simples y (2) la teoría axiomática de conjuntos, "permite la derivación de las matemáticas modernas y al mismo tiempo evita todas las paradojas conocidas" (Gödel 1944: 126); además, la teoría de tipos simples "es el sistema de los primeros Principia [ Principia Mathematica ] en una interpretación apropiada ... [M] cualquier síntoma muestra con demasiada claridad, sin embargo, que los conceptos primitivos necesitan más aclaración" (Gödel 1944 : 126).
Correspondencia Curry-Howard, 1934-1969
La correspondencia Curry-Howard es la interpretación de pruebas como programas y fórmulas como tipos. La idea comenzó en 1934 con Haskell Curry y finalizó en 1969 con William Alvin Howard . Conectó el "componente computacional" de muchas teorías de tipos con las derivaciones en la lógica.
Howard demostró que el cálculo lambda tipificado correspondía a la deducción natural intuicionista (es decir, la deducción natural sin la Ley del medio excluido ). La conexión entre los tipos y la lógica llevó a una gran cantidad de investigaciones posteriores para encontrar nuevas teorías de tipos para las lógicas existentes y nuevas lógicas para las teorías de tipos existentes.
AUTOMATH de Bruijn, 1967-2003
Nicolaas Govert de Bruijn creó la teoría de tipos Automath como base matemática para el sistema Automath, que podía verificar la exactitud de las pruebas. El sistema se desarrolló y agregó características a lo largo del tiempo a medida que se desarrollaba la teoría de tipos.
Teoría de tipos intuicionistas de Martin-Löf, 1971-1984
Per Martin-Löf encontró una teoría de tipos que se correspondía con la lógica de predicados mediante la introducción de tipos dependientes , que se conocieron como teoría de tipos intuicionista o teoría de tipos de Martin-Löf.
La teoría de Martin-Löf utiliza tipos inductivos para representar estructuras de datos ilimitadas, como números naturales.
Cubo lambda de Barendregt, 1991
El cubo lambda no era una nueva teoría de tipos, sino una categorización de las teorías de tipos existentes. Las ocho esquinas del cubo incluían algunas teorías existentes con cálculo lambda simplemente mecanografiado en la esquina más baja y el cálculo de construcciones en la más alta.
Referencias
- ↑ La carta de Russell (1902) a Frege aparece, con comentarios, en van Heijenoort 1967: 124-125.
- ↑ Frege (1902) Letter to Russell aparece, con comentarios, en van Heijenoort 1967: 126-128.
- ^ cf. Comentario de Quine antes de Russell (1908) La lógica matemática basada en la teoría de tipos en van Heijenoort 1967: 150
- ^ cf. Comentario de WVO Quine antes de Russell (1908) La lógica matemática basada en la teoría de tipos en van Hiejenoort 1967: 150-153
- ↑ a b Comentario de Quine antes de Russell (1908) Lógica matemática basada en la teoría de tipos en van Heijenoort 1967: 151
- ^ Russell (1908) Lógica matemática basada en la teoría de tipos en van Heijenoort 1967: 153-182
- ^ cf. en particular p. 51 en el Capítulo II La teoría de tipos lógicos y * 12 La jerarquía de tipos y el axioma de reducibilidad pp. 162-167. Whitehead y Russell (1910-1913, segunda edición de 1927) Principia Mathematica
- ^ Post (1921) Introducción a una teoría general de proposiciones elementales en van Heijenoort 1967: 264-283
- ^ Tarski 1946, Introducción a la lógica y a la metodología de las ciencias deductivas , republicación de Dover 1995
- ↑ Russell 1920: 135
- ^ cf. "Introducción" a la 2ª edición, Russell 1927: xiv y Apéndice C
- ^ cf. "Introducción" a la segunda edición, Russell 1927: i
- ^ cf. "Introducción" a la segunda edición, Russell 1927: xxix
- ^ La barra vertical "|" es el trazo de Sheffer; cf. "Introducción" a la segunda edición, Russell 1927: xxxi
- ^ "La teoría de clases se simplifica a la vez en una dirección y se complica en otra por el supuesto de que las funciones sólo ocurren a través de sus valores y por el abandono del axioma de reducibilidad"; cf. "Introducción" a la segunda edición, Russell 1927: xxxix
- ^ Estas citas de "Introducción" a la 2ª edición, Russell 1927: xliv – xlv.
- ↑ L. Chwistek, Antynomje logikiformalnej, Przeglad Filozoficzny 24 (1921) 164-171
- ^ FP Ramsey, Los fundamentos de las matemáticas, Actas de la Sociedad Matemática de Londres , Serie 2 25 (1926) 338–384.
- ^ Gödel 1944, páginas 126 y 136-138, nota al pie 17: "La lógica matemática de Russell" que aparece en Kurt Gödel: Obras completas: Publicaciones del volumen II 1938-1974 , Oxford University Press, Nueva York NY, ISBN 978-0-19-514721 -6 (v.2.pbk).
- ^ Esto no significa que la teoría sea "simple", significa que la teoría está restringida : los tipos de diferentes órdenes no deben mezclarse: "Tipos mixtos (como clases que contienen individuos y clases como elementos) y, por lo tanto, también tipos transfinitos ( como la clase de todas las clases de tipos finitos) están excluidas ". Gödel 1944, páginas 127, nota al pie 17: "La lógica matemática de Russell" que aparece en Kurt Gödel: Collected Works: Volume II Publications 1938-1974 , Oxford University Press, Nueva York NY, ISBN 978-0-19-514721-6 (v.2.pbk).
- ↑ A. Church, Una formulación de la teoría simple de tipos, Journal of Symbolic Logic 5 (1940) 56–68.
- ^ J. Collins, Una historia de la teoría de tipos: desarrollos después de la segunda edición de 'Principia Mathematica'. LAP Lambert Academic Publishing (2012). ISBN 978-3-8473-2963-3 , esp. cap. 4-6.
- ^ Gödel 1944: 126 nota al pie 17: "La lógica matemática de Russell" que aparece en Kurt Gödel: Obras completas: Publicaciones del volumen II 1938-1974 , Oxford University Press, Nueva York NY, ISBN 978-0-19-514721-6 (v.2.pbk).
Fuentes
- Bertrand Russell (1903), Los principios de las matemáticas: vol. 1 , Cambridge en University Press, Cambridge, Reino Unido.
- Bertrand Russell (1920), Introducción a la filosofía matemática (segunda edición), Dover Publishing Inc., Nueva York NY, ISBN 0-486-27724-0 (en particular los capítulos XIII y XVII).
- Alfred Tarski (1946), Introducción a la lógica y a la metodología de las ciencias deductivas , reeditado en 1995 por Dover Publications, Inc., Nueva York, NY ISBN 0-486-28462-X
- Jean van Heijenoort (1967, tercera edición de 1976), From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931 , Harvard University Press, Cambridge, MA, ISBN 0-674-32449-8 (pbk)
- Bertrand Russell (1902), Carta a Frege con comentario de van Heijenoort, páginas 124-125. Donde Russell anuncia su descubrimiento de una "paradoja" en el trabajo de Frege.
- Gottlob Frege (1902), Carta a Russell con comentario de van Heijenoort, páginas 126-128.
- Bertrand Russell (1908), La lógica matemática basada en la teoría de tipos , con comentario de Willard Quine , páginas 150-182.
- Emil Post (1921), Introducción a una teoría general de proposiciones elementales , con comentario de van Heijenoort, páginas 264-283.
- Alfred North Whitehead y Bertrand Russell (1910-1913, 1927 2ª edición reimpresa en 1962), Principia Mathematica hasta * 56 , Cambridge en University Press, Londres, Reino Unido, sin ISBN ni número de catálogo de tarjetas de EE. UU.
- Ludwig Wittgenstein (reeditado en 2009), Obras principales: Escritos filosóficos seleccionados , HarperCollins, Nueva York. ISBN 978-0-06-155024-9 . Wittgenstein (1921 en inglés), Tractatus Logico-Philosophicus , páginas 1–82.
Otras lecturas
- W. Farmer, "Las siete virtudes de la teoría de tipos simples", Journal of Applied Logic , vol. 6, núm. 3. (septiembre de 2008), págs. 267–286.