Let there be some formula $\phi$, is there an algorithm to construct a closed formula $\phi'=\exists x_1...\exists x_n \psi$ where $\psi$ does not have any quantifiers and $\phi$ is satiable iff $\phi'$ is satiable?

My idea is that it is wrong, and if we assume that it is true, then we can convert $\phi '$ to Skolem normal form to a closed formula $\phi ''$ with no quantifiers, so if we look at Herbrand's theorem, we only have one closed instance of $\phi ''$ which is the formula itself so we have an always halting algorithm to check whether a formula is satiable in first order logic. Is there any theorem that says the language of satiable FOL formulas is undecidable or something like that?


edit: I found in Wikipedia that validity is undecidable and you can solve validity of $\phi$ by checking that $\lnot \phi$ is not satiable, so I guess this solves it. If anyone can comment whether I made a mistake along the way I'd appreciate it.

  • $\begingroup$ $\phi'$ is a Skolem normal form of $\phi$. Why do you think Skolemisation will eliminate the quantifiers from it? $\endgroup$ – Rob Arthan Aug 19 '18 at 22:40
  • $\begingroup$ @RobArthan No, the $\phi ''$ is the Skolem normal form of $\phi '$, and that has only existential quantifiers so all of the variables will be replaced by constant symbols. $\endgroup$ – Eloo Aug 20 '18 at 6:25
  • $\begingroup$ @Eldo: sorry. I misread your question as saying "where $\psi$ does not have any existential quantifiers". Skolem normal form gives you a $\psi$ that does have quantifiers but they are all universal. $\endgroup$ – Rob Arthan Aug 20 '18 at 20:54

Your Answer

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

Browse other questions tagged or ask your own question.