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.

  • $\begingroup$ closed term means that the language has constants; what about a language that has none ? $\endgroup$ – Mauro ALLEGRANZA Jul 13 '18 at 15:50
  • $\begingroup$ The language has at least one constant $\endgroup$ – user11 Jul 13 '18 at 15:51
  • $\begingroup$ 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. $\endgroup$ – Daniel Schepler Jul 13 '18 at 16:03
  • $\begingroup$ yes, $\psi\{t/x\}$ would still have y as a free variable $\endgroup$ – user11 Jul 13 '18 at 16:05
  • $\begingroup$ So then, what does $\vdash_{FOL} \psi\{t/x\}$ mean if $\psi\{t/x\}$ has free variables? $\endgroup$ – 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)$

$\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))$

$\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 ...)

  • $\begingroup$ Thanks for your answer, is there a way proving it without using sequent calculus? $\endgroup$ – user11 Jul 13 '18 at 16:40
  • 1
    $\begingroup$ 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. $\endgroup$ – Alex Kruckman Jul 13 '18 at 20:45
  • $\begingroup$ @AlexKruckman: You're right and I'm horribly wrong. $\endgroup$ – Henning Makholm Jul 13 '18 at 22:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.