Definición
La teoría de tipos es la solución técnica que Bertrand Russell elaboró para resolver la paradoja lógica que él mismo había descubierto en 1901 al reflexionar sobre el sistema formal de Gottlob Frege, paradoja hoy conocida como paradoja de Russell y que amenazaba con la inconsistencia del programa logicista de reducción de las matemáticas a la lógica. La paradoja surge al considerar el conjunto R de todos los conjuntos que no son miembros de sí mismos; si R es miembro de sí mismo, entonces por definición no debería serlo, y si no lo es, entonces por definición debería serlo, produciendo así una contradicción irresoluble en los términos del sistema. Russell comunicó el hallazgo a Frege en una célebre carta de 1902 que llegó cuando el segundo volumen de las Grundgesetze der Arithmetik estaba en imprenta, y Frege reconoció en un apéndice que su sistema quedaba socavado. La solución russelliana se despliega en la Introducción de los Principia Mathematica (1910-1913), obra monumental coescrita con Alfred North Whitehead. La teoría de tipos estipula que los objetos lógicos deben estratificarse en una jerarquía de tipos (tipo 0 para individuos, tipo 1 para propiedades de individuos o conjuntos de individuos, tipo 2 para propiedades de propiedades, y así sucesivamente), y establece que una propiedad de tipo n sólo puede aplicarse a entidades de tipo n-1. Esta restricción, denominada axioma del círculo vicioso siguiendo a Poincaré, prohíbe las autorreferencias problemáticas al no permitir que un conjunto pueda ser miembro de sí mismo, disolviendo así la paradoja al declarar mal formada la expresión que la genera. Russell distingue posteriormente entre teoría ramificada de tipos, que estratifica también las proposiciones según niveles de generalidad, y teoría simple de tipos, formulación posterior más económica de Frank Ramsey y otros. Aunque la teoría cumplió su función técnica, dejó insatisfechos a muchos por su complejidad y por la necesidad de introducir axiomas ad hoc como el axioma de reducibilidad. La teoría de conjuntos de Zermelo-Fraenkel (ZF) proveyó posteriormente una solución alternativa más económica. La teoría de tipos ha renacido en las últimas décadas en la teoría de tipos de Martin-Löf y en los fundamentos homotópicos de la matemática y de la computación.