Satisfiability (first-order logic)
From Learning Logic for Computer Science
A first-order formula is satisfiable if there is a structure in which it is true under some variable assignment.
Formal definitions
Definition Let $\mathcal S$ be a signature. An $\mathcal S$-formula $\varphi$ is satisfiable if there exists an $\mathcal S$-structure $\mathcal A$ and an $A$-assignment $\beta$ such that $\mathcal A, \beta \mymodels \varphi$.
Example The formula $\exists x_0 P(x_0) \wedge \forall x_0 \neg P(f(x_0))$ is satisfiable, because it is true in the structure $\mathcal A$ with $A = \{0,1\}$, $P^\mathcal A = \{0\}$, and $f^\mathcal A = 1$.
The generalization to sets of formulas is straightforward.
Definition Let $\mathcal S$ be a signature. A set $\Phi$ of $\mathcal S$-formulas is satisfiable if there exists an $\mathcal S$-structure $\mathcal A$ and an $A$-assignment $\beta$ such that $\mathcal A, \beta \mymodels \varphi$ for every $\varphi \in \Phi$.
Example Let $\varphi_n = \bigwedge_{i<n} \neg x_i \doteq x_n$ for every $n \in \mathbf N$ and $\Phi = \{\varphi_n \colon n \in \mathbf N\}$. The $\Phi$ is satisfiable, because $\mathcal A, \beta \mymodels \Phi$ for $A = \mathbf N$ and $\beta$ defined by $\beta(x_i) = i$ for every $i \in \mathbf N$.
Undecidability
Satisfiability of first-order formulas is undecidable.
From the completeness theorem it follows that satisfiablity is co-r.e.