Existential second-order logic (ESO) formulas have the form $$\Phi = \exists R_1 ... \exists R_k. \phi$$ where $R_1...R_k$ are relation symbols and $\phi$ is a FO formula, which can use the relation symbols $R_1...R_K$ as well as other relation symbols. My claim is that

$\Phi$ is satisfiable if and only if $\phi$ is satisfiable.

Indeed, satisfiability of a FO formula means finding a universe and an interpretation of all relation symbols. Therefore, we have an implicit quantification $\exists R_1 ... \exists R_k$ in front of the FO formula $\phi$, when considering satisfiability. (For validity, the claim does not hold.)

But the claim must be wrong since people study satisfiability of ESO separately from that of FO. What do I miss?


You're right: an ESO sentence is satisfiable iff its first-order "matrix" - with relation/function variables replaced with corresponding relation/function symbols - is satisfiable.

TI'm not an expert here, but I think what's going on is "linguistic convenience." There are other related questions where we don't get coincision. For example, checking whether a first-order sentence is true in a given finite structure is usually harder than checking whether one of its "second-orderizations" is true in that same structure${}$('s reduct). Similarly, as you say validity for ESO sentences is strictly more complicated than validity for FO sentences. In this way it may feel more consistent to talk about ESO satisfiability rather than FO satisfiability if we're also talking about ESO validity, ESO truth in a given structure, etc.


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.