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 demostradores de teoremas HOL .
Los sistemas de demostración de teoremas TPS y ETPS se basan en Q 0 . En agosto de 2009, TPS ganó la primera competencia entre sistemas de demostración de teoremas de orden superior. [1]
El sistema tiene sólo cinco axiomas, que se pueden expresar como:
℩
(Los axiomas 2, 3 y 4 son esquemas de axiomas: familias de axiomas similares. Los ejemplos del axioma 2 y el 3 varían sólo según los tipos de variables y constantes, pero los ejemplos del axioma 4 pueden tener cualquier expresión que reemplace a A y B ).
El subíndice " o " es el símbolo de tipo para valores booleanos y el subíndice " i " 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 con subíndices como α y β son variables sintácticas para símbolos de tipo. Las letras mayúsculas en negrita, como A , B y C, son variables sintácticas para WFF, y las letras minúsculas en negrita, como x , y, son variables sintácticas para variables. S indica sustitución sintáctica en todas las apariciones libres.
Las únicas constantes primitivas son Q ((oα)α) , que denota 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 los corchetes ("[" y "]") son la sintaxis del idioma. Todos los demás símbolos son abreviaturas de 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 causa que ninguna ocurrencia de variables libres de A quede ligada en el resultado de la sustitución.
En Andrews 2002, el Axioma 4 se desarrolla en cinco subpartes que desglosan el proceso de sustitución. El axioma tal como se presenta aquí se analiza como alternativa y se demuestra a partir de las subpartes.
Andrews amplía esta lógica con definiciones de operadores de selección para colecciones de todo tipo, de modo que
℩
es un teorema (número 5309). En otras palabras, todos los tipos tienen un operador de descripción definido. Esta es una extensión conservadora , por lo que el sistema extendido es consistente si el núcleo es consistente.
También presenta un axioma 6 adicional , que establece que hay infinitos individuos, junto con axiomas alternativos equivalentes de infinito.
A diferencia de muchas otras formulaciones de teoría de tipos y asistentes de prueba basados en la teoría de tipos, Q 0 no proporciona tipos base distintos de o e i , por lo que los números cardinales finitos, por ejemplo, se construyen como colecciones de individuos que obedecen a los postulados habituales de Peano en lugar de un tipo en el sentido de la teoría de tipos simple.
Q 0 tiene una única 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 λ .
La regla de inferencia derivada R′ permite razonar a partir de un conjunto de hipótesis H.
Gobernante'. Si H ⊦ A α = B α , y H ⊦ C , y D se obtiene de C reemplazando una aparición de A α por una aparición de B α , entonces H ⊦ D , siempre que:
Nota: La restricción de reemplazo de A α por B α en C asegura que cualquier variable libre tanto en una hipótesis como en A α = B α continúe restringida a tener el mismo valor en ambas una vez realizado el reemplazo.
El teorema de deducción para Q 0 muestra que las pruebas de hipótesis que utilizan la regla R′ se pueden convertir en pruebas sin hipótesis y que utilizan 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. Así, por ejemplo, dados axiomas:
1. ∃x Px
2. Px ⊃ Qx
y el hecho de que A ⊃ B ≡ (A ≡ A ∧ B) , podemos proceder sin eliminar el cuantificador:
3. Px ≡ (Px ∧ Qx) instanciación para A y B
4. Regla ∃x (Px ∧ Qx) R sustituyendo en la línea 1 usando la línea 3.
![{\displaystyle g_{oo}T\land g_{oo}F=\forall x_{o}[g_{oo}x_{o}]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/104d9c0625b68d01d933e825815780b20f3579bf)
![{\displaystyle [x_{\alpha }=y_{\alpha }]\supset [h_{o\alpha }x_{\alpha }=h_{o\alpha }y_{\alpha }]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dc54dbf3082878608f8669d84c97990c239f682e)
![{\displaystyle f_{\alpha \beta }=g_{\alpha \beta }=\forall x_{\beta }[f_{\alpha \beta }x_{\beta }=g_{\alpha \beta }x_{\ beta }]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6f18cfb7d5cf8e8591630ffe83e1962ff9c161ee)
![{\displaystyle [\lambda \mathbf {x_{\alpha }} \mathbf {B} _{\beta }]\mathbf {A} _{\alpha }=\mathbf {S} _{A_{\alpha }} ^{\mathbf {x} _{\alpha }}\mathbf {B} _{\beta }}](https://wikimedia.org/api/rest_v1/media/math/render/svg/83630aad2582d53d89d9dc8273a7d4921cfca78e)
![{\displaystyle _{i(oi)}[{\text{Q}}_{oii}y_{i}]=y_{i}\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cb23b012d3df75af219fcf9cd6e423b0c494669f)
![{\displaystyle _{\alpha (o\alpha )}[{\text{Q}}_{o\alpha \alpha }y_{i}]=y_{i}\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b2cdbe3afbec4154893fa7210650bd32a4bfbb38)