Probar o refutar: si $⊢_{FOL}\exists x\forall y\ \psi$ y $⊢_{FOL}\psi\{t/x\}$

Question

Deje $\psi$ ser una fórmula sin cuantificadores en un idioma con al menos una constante ,
tal que $\exists x\forall y\ \psi$ es una pena.
Demostrar o refutar:
Si $⊢_{FOL}\exists x\forall y\ \psi$ entonces no existe un cerrado plazo $t$ tal que $⊢_{FOL}\psi\{t/x\}$

Creo que la afirmación es correcta.
Traté de demostrar de la siguiente manera:
$⊢_{FOL}\exists x\forall y\ \psi$ fib
$\forall x\exists y\ \neg\psi$ no es válido iff (por el teorema de Skolem)
$\forall x\ \neg\psi\{f(x)/y\}$ no es válido (donde $f$ es un nuevo símbolo de función)
entonces traté de usar el teorema de Herbrand y me quedé atrapado.

Answer 1

He encontrado un ejemplo contrario:
Que $\sigma={c,p}$
Que $\psi=p(y)\vee\neg p(x)$

Por lo tanto:
$\vdash_{FOL}\exists x\forall y\ (p(y)\vee\neg p(x))$)
Porque $\exists x\forall y\ (p(y)\vee\neg p(x)) \equiv (\forall y \ p(y))\vee (\neg \forall x \ p(x))$

Pero:
$\nvdash_{FOL}p(y)\vee\neg p(c)$
Porque si definimos:
$M=$ tal que $I[p]={1}\ ,I[c]=1$
y un % de la asignación $v$tal que $v[y]=0$,
entonces $v[p(y)\vee\neg p(c)]=$f
y $c$ es el término cerrado sólo en la lengua

Answer 2

Sí, esto es cierto.

Creo que se ve más fácilmente mediante el uso de sequent cálculo como la prueba del sistema de primer orden de la lógica.

Sequent cálculo tiene la propiedad de que todo lo que es comprobable tiene un corte libre de la prueba-y la única regla de un corte libre de la prueba de $\vdash \exists x\forall y\, \psi$ puede terminar con es $\exists$R. ...

Ja! esto no es cierto, como se muestra en el OP del contraejemplo donde $\exists x \forall y. \psi$ es el Bebedor de la Paradoja. Cuando uno escribe una prueba de que el Bebedor Paradoja y elimina los cortes, lo que uno termina con una prueba donde la última regla es no $\exists$R, pero el derecho de la contracción de la regla. Así que toda mi argumento se derrumba.

(Voy a dejar que esto esta respuesta de pie como una advertencia para los descuidados ...)