Deducción del Teorema y Cerrado Fórmulas

Question

¿Por qué en la Deducción del Teorema de qué se requiere un cerrado fórmula?

Deducción Del Teorema. Deje $A$ ser un cerrado fórmula en $T$. Para cada fórmula $B$ de $T$, $\vdash_T A \implies B$ iff $B$ es un teorema de $T[A]$.

No pude encontrar ningún contraejemplo.

Puede que me explique donde está el problema?

Editar:

He encontrado un contraejemplo.

si $A=C$ $B=\forall(x)C$

cuando Un no es un cerrado de la fórmula.

Answer 1

En el sistema de Joseph Shoenfield, la Lógica Matemática (1967) la restricción en $A$ ser cerrado que es necesario en la prueba de la Deducción del Teorema [consulte la página 33] con el fin de aplicar el $\exists$-introducción de la regla [se página 21] :

si $x$ no es libre en $B$, inferir $\exists x A \rightarrow B$$A \rightarrow B$.

Sin la condición de en $B$ en la regla, se puede derivar la inválida $\exists x (x=0) \rightarrow (x=0)$ de la tautología : $(x=0) \rightarrow (x=0)$.