Q0 (lógica matemática)

Q0 es la formulación de Peter Andrews del cálculo lambda de tipos simples y proporciona una base matemática 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 las lógicas de la familia de demostradores de teoremas HOL .

Los sistemas de demostración de teoremas TPS y ETPS, archivados el 11 de abril de 2011 en Wayback Machine, se basan en Q ₀ . En agosto de 2009, TPS ganó la primera competición entre sistemas de demostración de teoremas de orden superior. ^{[ 1 ]}

El sistema tiene solo cinco axiomas, que se pueden enunciar de la siguiente manera:

${\displaystyle (1)}$  ${\displaystyle g_{oo}T\land g_{oo}F=\forall x_{o}[g_{oo}x_{o}]}$

${\displaystyle (2^{\alpha })}$  ${\displaystyle [x_{\alpha }=y_{\alpha }]\supset [h_{o\alpha }x_{\alpha }=h_{o\alpha }y_{\alpha }]}$

${\displaystyle (3^{\alpha \beta })}$  ${\displaystyle f_{\alpha \beta }=g_{\alpha \beta }=\forall x_{\beta }[f_{\alpha \beta }x_{\beta }=g_{\alpha \beta }x_{\beta }]}$

${\displaystyle (4)}$  ${\displaystyle [\lambda \mathbf {x_{\alpha }} \mathbf {B} _{\beta }]\mathbf {A} _{\alpha }=\mathbf {S} _{A_{\alpha }}^{\mathbf {x} _{\alpha }}\mathbf {B} _{\beta }}$

${\displaystyle (5)}$  ℩${\displaystyle _{i(oi)}[{\text{Q}}_{oii}y_{i}]=y_{i}\,}$

(Los axiomas 2, 3 y 4 son esquemas axiomáticos: familias de axiomas similares. Las instancias del axioma 2 y del axioma 3 solo varían en los tipos de variables y constantes, pero las instancias del axioma 4 pueden tener cualquier expresión que reemplace a A y B ).

El subíndice " o " indica el tipo de valores booleanos, y el subíndice " i " indica el tipo de 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 en subíndice, 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 funciones bien formadas (WFF), y las letras minúsculas en negrita , como x e y, son variables sintácticas para las variables. La "S" indica sustitución sintáctica en todas las ocurrencias libres.

Las únicas constantes primitivas son Q _{((o α ) α )} , que denota la igualdad de los 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 lenguaje. 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 hace que ninguna ocurrencia de variables libres de A se vuelva ligada en el resultado de la sustitución.

Andrews extiende esta lógica con definiciones de operadores de selección para colecciones de todos los tipos, de modo que

${\displaystyle (5a)}$  ℩${\displaystyle _{\alpha (o\alpha )}[{\text{Q}}_{o\alpha \alpha }y_{i}]=y_{i}\,}$

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 adicional, el axioma 6 , que establece que existen infinitos individuos, junto con axiomas alternativos equivalentes de infinito.

A diferencia de muchas otras formulaciones de la teoría de tipos y asistentes de prueba basados ​​en la teoría de tipos, Q ₀ 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 los postulados habituales de Peano en lugar de un tipo en el sentido de la teoría de tipos simple.

Q ₀ 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 precedida por λ .

La regla de inferencia derivada R ′ permite razonar a partir de un conjunto de hipótesis H .

Regla R ′ . 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 aparición de A _α en C no es una aparición de una variable inmediatamente precedida por λ y
• ninguna variable libre en A _α = B _α y un miembro de H está ligado en C en la ocurrencia reemplazada de A _α .

Nota: La restricción en el reemplazo de A _α por B _α en C garantiza que cualquier variable libre tanto en una hipótesis como en A _α = B _α continúe estando restringida a tener el mismo valor en ambas después de que se haya realizado el reemplazo.

El teorema de deducción para Q ₀ muestra que las demostraciones a partir de hipótesis que utilizan la regla R ′ pueden convertirse en demostraciones sin hipótesis y utilizando la regla R.

A diferencia de algunos sistemas similares, la inferencia en Q ₀ reemplaza una subexpresión en cualquier nivel dentro de una fórmula bien formada con una expresión equivalente. Por ejemplo, dados los 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) instanciando para A y B 4. ∃x (Px ∧ Qx) regla R sustituyendo en la línea 1 usando la línea 3.      

• Andrews, Peter B. (2002). Introducción a la lógica matemática y la teoría de tipos: Hacia la verdad a través de la demostración (2.ª  ed.). Dordrecht, Países Bajos: Kluwer Academic Publishers . ISBN 1-4020-0763-9. Véase también
• Church, Alonzo (1940). «Una formulación de la teoría simple de tipos» (PDF) . Journal of Symbolic Logic . 5 (2): 56– 58. doi : 10.2307/2266170 . JSTOR 2266170. S2CID 15889861. Archivado del original (PDF) el 12 de enero de 2019.  

• Una descripción más detallada de Q ₀ ; parte de un artículo sobre la Teoría de Tipos de Church en la Enciclopedia de Filosofía de Stanford .
• Una visión general de las lógicas matemáticas (incluidos varios sucesores de Q ₀ ): Fundamentos de las matemáticas. Genealogía y visión general doi:10.4444/100.111 .