Prueba $\forall x (A\to B) \to(A \to \forall x B):x\notin \mbox{free}(A)$ en un sistema de Hilbert donde no es un axioma

Question

No tengo ni idea de si esta pregunta es demasiado específica o si ya se ha preguntado algo similar (supongo que todavía tenemos que encontrar una forma de buscar fórmulas).

De todos modos aquí voy: Quiero demostrar que alguna elección de axiomas (lógicos/cuantitativos) para un sistema de derivación de Hilbert (lógica de primer orden, un tipo) puede demostrar todos los axiomas de alguna otra elección.

Tengo lo siguiente a mi disposición:

Axiomas:

• (fot): tautologías de primer orden (es decir, insertar fórmulas para las proposiciones en una tautología proposicional)

• (aax): $\forall x A[x] \to A[t]$ (donde $t$ es cualquier término y suponemos que no hay conflictos con las variables libres que se ligan, $[...]$ denota sustitución)

Reglas de inferencia:

• (mp): modus ponens

• (aru): $\frac{A\to B}{A\to\forall x B}$ donde $x$ no es libre en $A$ .

Quiero demostrar que este sistema demuestra la fórmula:

$\forall x (A\to B) \to(A \to \forall x B)$ para $x$ no libre en $A$ (que asumiré en lo que sigue).

Esto es, por supuesto, muy similar a (aru), pero quiero esta fórmula, que es, por supuesto, una declaración más fuerte. Estoy bastante perdido aquí.

Aquí están mis intentos fallidos: Con (aax) y (aru), obtengo fácilmente la regla demostrable $\frac{\forall x(A\to B)}{A\to\forall x B}$ que es la formulación de mi fórmula de meta como regla (más débil).

Incluso tengo

$$\frac{\bar\forall(A\to B)}{A\to\forall x B}$$ donde $\bar\forall$ denota el cierre universal de la siguiente fórmula.

Usando el Teorema de la Deducción (que demostré para esta teoría) obtengo que mi sistema demuestra $$\bar\forall(A\to B)\to(A\to\forall x B).$$ pero eso no es exactamente lo que estoy buscando.

Answer 1

Como ya has observado, $$ \vdash \forall x(A\rightarrow B)\rightarrow (A\rightarrow \forall x B) $$ si $x$ es la única variable libre en $A, B$ por el teorema de la deducción. En el caso general, se puede ampliar el lenguaje con nuevas constantes y sustituir las variables libres adicionales (si las hay) por esas constantes para demostrar $$ \vdash \forall x(A(c_j)\rightarrow B(c_j,x))\rightarrow (A(c_j)\rightarrow \forall x B(c_j,x)) $$ de la misma manera. No es difícil demostrar, mediante una inducción sobre las pruebas formales, que esto implica lo que quieres, es decir, la versión de variable libre de esto.

El primer volumen de Tourlakis, Lectures in logic in set theory discute este material (en particular, utiliza casi la misma formalización); véase el Teorema I.4.15 allí.

Answer 2

Utilizando los consejos de Christian Remling, he podido formular la siguiente prueba explícita, que es bastante larga debido a la eliminación del uso del teorema de la deducción ( $\land$ tiene mayor precedencia que $\to$ ):

1 $\vdash \forall x(A \to B) \to (A \to B)$ (aax)

2 $\vdash (\forall x(A \to B) \to (A \to B)) \to (\forall x(A \to B) \land A \to B)) $ (foto)

3 $\vdash \forall x(A \to B) \land A \to B$ (mp 1 2)

4 $\vdash \forall x(A \to B) \land A \to \forall x B$ (aru, aplicable desde $x$ no libre en $\forall x(A \to B) \land A$ )

5 $\vdash (\forall x(A \to B) \land A \to \forall x B) \to (\forall x(A \to B) \to ( A \to \forall x B)) $ (foto)

6 $\vdash \forall x(A \to B) \to ( A \to \forall x B) $ (mp 4 5)