Q 0 es la formulación de Peter Andrews del cálculo lambda de tipo simple y proporciona una base para las matemáticas comparable a la lógica de primer orden más la teoría de conjuntos. Es una forma de lógica de orden superior y está estrechamente relacionada con la lógica de la familia de probadores de teoremas HOL .
Los sistemas de prueba de teoremas TPS y ETPS se basan en Q 0 . En agosto de 2009, TPS ganó la primera competencia entre los sistemas de prueba de teoremas de orden superior. [1]
Axiomas de Q 0
El sistema tiene solo cinco axiomas, que se pueden enunciar como:
℩
(Los axiomas 2, 3 y 4 son esquemas de axiomas: familias de axiomas similares. Las instancias del axioma 2 y el axioma 3 varían solo según los tipos de variables y constantes, pero las instancias del axioma 4 pueden tener cualquier expresión que reemplace A y B ).
La " o " subindicada es el símbolo de tipo para valores booleanos, y la " i " subindicada es el símbolo de tipo para valores individuales (no booleanos). Las secuencias de estos representan tipos de funciones y pueden incluir paréntesis para distinguir diferentes tipos de funciones. Las letras griegas subindicadas como α y β son variables sintácticas para los símbolos de tipo. Las letras mayúsculas en negrita, como A , B y C, son variables sintácticas para las WFF, y las letras minúsculas en negrita, como x , y , son variables sintácticas para las variables. S indica sustitución sintáctica en todas las apariciones libres.
Las únicas constantes primitivas son Q ((oα) α) , que denota la igualdad de miembros de cada tipo α, y ℩ (i (oi)) , que denota un operador de descripción para individuos, el elemento único de un conjunto que contiene exactamente un individuo. Los símbolos λ y corchetes ("[" y "]") son la sintaxis del idioma. Todos los demás símbolos son abreviaturas de los términos que los contienen, incluidos los cuantificadores ∀ y ∃.
En el axioma 4, x debe ser libre para A en B , lo que significa que la sustitución no hace que ninguna ocurrencia de variables libres de A quede ligada en el resultado de la sustitución.
Sobre los axiomas
- El axioma 1 expresa la idea de que T y F son los únicos valores booleanos.
- Los esquemas de axioma 2 α y 3 αβ expresan propiedades fundamentales de funciones.
- El esquema de axioma 4 define la naturaleza de la notación λ.
- El axioma 5 dice que el operador de selección es el inverso de la función de igualdad en los individuos. (Dado un argumento, Q asigna a ese individuo al conjunto / predicado que contiene al individuo. En Q 0 , x = y es una abreviatura de Qxy , que es una abreviatura de (Qx) y ).
En Andrews 2002 , Axiom 4 se desarrolla en cinco subpartes que desglosan el proceso de sustitución. El axioma que se presenta aquí se discute como una alternativa y se demuestra a partir de las subpartes.
Inferencia en Q 0
Q 0 tiene una sola regla de inferencia.
Regla R. De C y A α = B α para inferir el resultado de reemplazar una ocurrencia de A α en C por una ocurrencia de B α , siempre que la ocurrencia de A α en C no sea (una ocurrencia de una variable) inmediatamente precedido por λ .
Regla derivada de la inferencia R ' permite razonamiento a partir de un conjunto de hipótesis H .
Regla'. Si H ⊦ A α = B α , y H ⊦ C , y D se obtiene de C reemplazando una ocurrencia de A α por una ocurrencia de B α , entonces H ⊦ D , siempre que:
- La ocurrencia de A α en C no es una ocurrencia de una variable inmediatamente precedida por λ , y
- ninguna variable está libre en A α = B α y un miembro de H está unido en C en la ocurrencia reemplazada de A α .
Nota: La restricción sobre el reemplazo de A α por B α en C asegura que cualquier variable libre tanto en una hipótesis como en A α = B α continúe restringida para tener el mismo valor en ambos después de que se realice el reemplazo.
El teorema de deducción para Q 0 muestra que las pruebas de hipótesis que usan la regla R ′ se pueden convertir en pruebas sin hipótesis y usando la regla R.
A diferencia de algunos sistemas similares, la inferencia en Q 0 reemplaza una subexpresión en cualquier profundidad dentro de un WFF con una expresión igual. Entonces, por ejemplo, axiomas dados:
1. ∃x Px
2. Px ⊃ Qx
y el hecho de que A ⊃ B ≡ (A ≡ A ∧ B) , podemos proceder sin quitar el cuantificador:
3. Px ≡ (Px ∧ Qx) instanciando para A y B
4. ∃x (Px ∧ Qx) regla R sustituyendo en la línea 1 usando la línea 3.
Notas
Referencias
- Andrews, Peter B. (2002). Una introducción a la lógica matemática y la teoría de tipos: a la verdad a través de la prueba (2ª ed.). Dordrecht, Países Bajos: Kluwer Academic Publishers . ISBN 1-4020-0763-9.Ver también [1]
- Iglesia, Alonzo (1940). "Una formulación de la teoría simple de tipos" (PDF) . Revista de lógica simbólica . 5 : 56–58. doi : 10.2307 / 2266170 . Archivado desde el original (PDF) el 12 de enero de 2019.
Otras lecturas
- Una descripción de Q 0 en mayor profundidad; parte de un artículo sobre la teoría de tipos de Church en la Enciclopedia de Filosofía de Stanford .
- Una descripción general de la lógica matemática (incluidos varios sucesores de Q 0 ): Fundamentos de las matemáticas. Genealogía y descripción general doi: 10.4444 / 100.111 .