Creo que el Teorema 1 de Bezboruah y Shepherdson 1976 [1] cubre tu pregunta, al menos en espíritu. Su teoría $T_0$ es una teoría finita que extiende $Q$ . Citando su documento:
Teorema 1. Sea $L$ sea cualquier sistema formal con un conjunto recursivo de axiomas, un número finito de reglas de inferencia finitas y recursivas, incluido el modus ponens, y que tenga $A \to A$ como teorema para todas las sentencias $A$ . L $$Con_L =_{df}\quad \lnot(\exists y,z)(Th_L(y) \land Th_L(z) \land neg(z,y))$$ donde $\text{Th}_L$ , $\text{neg}$ figuran en la definición 3. Entonces $\text{Con}_L$ no es demostrable en $T_0$ .
Los autores, sin embargo, expresan la duda común de que las pruebas de consistencia en Q tengan sentido filosófico.
"Debemos estar de acuerdo con Kreisel en que esto carece de todo interés filosófico y que en un sistema tan débil no puede decirse que esta fórmula exprese la consistencia, sino sólo una propiedad algebraica que en un sistema más fuerte (por ejemplo, la aritmética P de Peano) podría razonablemente decirse que expresa la consistencia de Q."
La dificultad (¿bien conocida?) aquí es que Q puede formalizar el predicado de demostrabilidad pero no puede verificar las condiciones de derivabilidad de Hilbert-Bernays para él.
1: A. Bezboruah y J. C. Shepherdson, "Gödel's Second Incompleteness Theorem for Q", Revista de Lógica Simbólica Vol. 41, No. 2 (jun., 1976), pp. 503-512, JStor .
