teoría del tipo ST

El siguiente sistema es la teoría de tipos ST de Mendelson (1997, 289–293) . ST es equivalente a la teoría ramificada de Russell más el axioma de reducibilidad . El dominio de cuantificación se divide en una jerarquía ascendente de tipos, donde a todos los individuos se les asigna un tipo. Las variables cuantificadas abarcan solo un tipo; por lo tanto, la lógica subyacente es lógica de primer orden . ST es "simple" (en relación con la teoría de tipos de Principia Mathematica ) principalmente porque todos los miembros del dominio y codominio de cualquier relación deben ser del mismo tipo. Existe un tipo más bajo, cuyos individuos no tienen miembros y pertenecen al segundo tipo más bajo. Los individuos del tipo más bajo corresponden a los urelementos de ciertas teorías de conjuntos. Cada tipo tiene un tipo inmediatamente superior, análogo a la noción de sucesor en la aritmética de Peano . Si bien ST no especifica si existe un tipo máximo, un número transfinito de tipos no plantea ninguna dificultad. Estos hechos, que recuerdan a los axiomas de Peano, hacen que sea conveniente y convencional asignar un número natural a cada tipo, comenzando con 0 para el tipo más básico. Pero la teoría de tipos no requiere una definición previa de los números naturales.

Los símbolos peculiares de ST son las variables primadas y el operador infijo.${\displaystyle \in }$. En cualquier fórmula dada, todas las variables sin prima tienen el mismo tipo, mientras que las variables con prima (${\displaystyle x'}$) abarcan el siguiente tipo superior. Las fórmulas atómicas de ST son de dos formas,${\displaystyle x=y}$( identidad ) y${\displaystyle y\in x'}$El símbolo del operador infijo${\displaystyle \in }$sugiere la interpretación prevista , pertenencia al conjunto.

Todas las variables que aparecen en la definición de identidad y en los axiomas Extensionalidad y Comprensión abarcan individuos de uno de dos tipos consecutivos. Solo las variables no primadas (que abarcan el tipo "inferior") pueden aparecer a la izquierda de '${\displaystyle \in }$Mientras que a su derecha, solo pueden aparecer variables primadas (que abarcan el tipo "superior"). La formulación de primer orden de ST descarta la cuantificación sobre tipos. Por lo tanto, cada par de tipos consecutivos requiere su propio axioma de Extensionalidad y de Comprensión, lo cual es posible si Extensionalidad y Comprensión, que se presentan a continuación, se consideran esquemas axiomáticos que abarcan tipos.

• Identidad , definida por${\displaystyle x=y\leftrightarrow \forall z'[x\in z'\leftrightarrow y\in z']}$.
• Extensionalidad . Un esquema axiomático .${\displaystyle \forall x[x\in y'\leftrightarrow x\in z']\rightarrow [y'=z']}$.

Dejar${\displaystyle \Phi (x)}$denota cualquier fórmula de primer orden que contenga la variable libre.${\displaystyle x}$.

• Comprensión . Un esquema axiomático .${\displaystyle \exists z'\forall x[x\in z'\leftrightarrow \Phi (x)]}$.

Observación . Cualquier conjunto de elementos del mismo tipo puede formar un objeto del siguiente tipo superior. La comprensión es esquemática con respecto a${\displaystyle \Phi (x)}$así como a los tipos.

• Infinito . Existe una relación binaria no vacía.${\displaystyle R}$sobre los individuos del tipo más bajo, es decir, irreflexivos , transitivos y fuertemente conectados:${\displaystyle \forall x,y[x\neq y\rightarrow [xRy\vee yRx]]}$y con codominio contenido en el dominio.

Observación . El infinito es el único axioma verdadero de ST y es de naturaleza completamente matemática. Afirma que${\displaystyle R}$es un orden total estricto , con un codominio contenido en su dominio . Si se asigna 0 al tipo más bajo, el tipo de${\displaystyle R}$es 3. El infinito solo puede satisfacerse si el (co)dominio de${\displaystyle R}$es infinito , lo que obliga a la existencia de un conjunto infinito. Si las relaciones se definen en términos de pares ordenados , este axioma requiere una definición previa de par ordenado; la definición de Kuratowski, adaptada a ST , servirá. La literatura no explica por qué el axioma usual de infinito (existe un conjunto inductivo ) de ZFC de otras teorías de conjuntos no podría combinarse con ST .

La teoría de conjuntos revela cómo la teoría de tipos puede asemejarse mucho a la teoría axiomática de conjuntos . Además, la ontología más elaborada de la teoría de conjuntos , basada en lo que ahora se denomina la "concepción iterativa de conjunto", genera axiomas (esquemas) mucho más simples que los de las teorías de conjuntos convencionales, como ZFC , con ontologías más sencillas. Entre las teorías de conjuntos cuyo punto de partida es la teoría de tipos, pero cuyos axiomas, ontología y terminología difieren de las anteriores, se incluyen New Foundations y la teoría de conjuntos de Scott-Potter .

La teoría de tipos de Church ha sido estudiada exhaustivamente por dos de sus alumnos, Leon Henkin y Peter B. Andrews . Dado que ST es una lógica de orden superior , y en lógicas de orden superior se pueden definir conectores proposicionales en términos de equivalencia lógica y cuantificadores, en 1963 Henkin desarrolló una formulación de ST basada en la igualdad, pero en la que restringió la atención a los tipos proposicionales. Esta formulación fue simplificada posteriormente ese mismo año por Andrews en su teoría Q ₀ . ^{[ 1 ]} En este sentido, ST puede considerarse un tipo particular de lógica de orden superior, clasificada por P. T. Johnstone en Sketches of an Elephant como poseedora de una signatura lambda , es decir, una signatura de orden superior que no contiene relaciones y utiliza únicamente productos y flechas (tipos de función) como constructores de tipos . Además, como lo expresó Johnstone, ST es "libre de lógica" en el sentido de que no contiene conectores lógicos ni cuantificadores en sus fórmulas. ^{[ 2 ]}

• teoría de tipos