# 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.