# Prove or disprove: if $⊢_{FOL}\exists x\forall y\ \psi$ then $⊢_{FOL}\psi\{t/x\}$

Let $\psi$ be a formula without quantifiers in a language with at least one constant ,
such that $\exists x\forall y\ \psi$ is a sentence.
Prove or disprove:
If $⊢_{FOL}\exists x\forall y\ \psi$ then there's exist a closed term $t$ such that $⊢_{FOL}\psi\{t/x\}$

I think the claim is correct.
I tried proving it as follows:
$⊢_{FOL}\exists x\forall y\ \psi$ iff
$\forall x\exists y\ \neg\psi$ isn't satisfiable iff (by Skolem theorem)
$\forall x\ \neg\psi\{f(x)/y\}$ isn't satisfiable (where $f$ is a new function symbol)
then I tried to use Herbrand's theorem and I got stuck.

• closed term means that the language has constants; what about a language that has none ? – Mauro ALLEGRANZA Jul 13 '18 at 15:50
• The language has at least one constant – user11 Jul 13 '18 at 15:51
• I don't quite understand - I would think $\psi$ could have $y$ as a free variable, so then $\psi\{t/x\}$ would still have $y$ as a free variable. – Daniel Schepler Jul 13 '18 at 16:03
• yes, $\psi\{t/x\}$ would still have y as a free variable – user11 Jul 13 '18 at 16:05
• So then, what does $\vdash_{FOL} \psi\{t/x\}$ mean if $\psi\{t/x\}$ has free variables? – Daniel Schepler Jul 13 '18 at 16:06

I've found a counter example:
Let $\sigma=\{c,p\}$
Let $\psi=p(y)\vee\neg p(x)$

So:
$\vdash_{FOL}\exists x\forall y\ (p(y)\vee\neg p(x))$)
Because $\exists x\forall y\ (p(y)\vee\neg p(x)) \equiv (\forall y \ p(y))\vee (\neg \forall x \ p(x))$

But:
$\nvdash_{FOL}p(y)\vee\neg p(c)$
Because if we define:
$M=<\{0,1\},I>$ such that $I[p]=\{1\}\ ,I[c]=1$
and an assignment $v$ such that $v[y]=0$,
then $v[p(y)\vee\neg p(c)]=$f
and $c$ is the only closed term in the language

Yes, this is true.

I think it is most easily seen by using sequent calculus as your proof system for first order logic.

Sequent calculus has the nice property that everything that is provable has a cut-free proof -- and the only rule a cut-free proof of $\vdash \exists x\forall y\, \psi$ can end with is $\exists$R. ...

Ha! this is not true, as shown by the OP's counterexample where $\exists x \forall y. \psi$ is the Drinker Paradox. When one writes down a proof of the Drinker Paradox and eliminates cuts, what one ends up with is a proof where the last rule is not $\exists$R, but the right contraction rule. So my entire argument collapses.

(I'll let this this answer stand as a warning for the careless ...)

• Thanks for your answer, is there a way proving it without using sequent calculus? – user11 Jul 13 '18 at 16:40
• Actually, I believe the statement is not true. There is a correct counterexample in the OP's (deleted) answer, which will hopefully be undeleted soon. – Alex Kruckman Jul 13 '18 at 20:45
• @AlexKruckman: You're right and I'm horribly wrong. – hmakholm left over Monica Jul 13 '18 at 22:36