Logic and Proof MT24, Decidability results for first-order logic
Flashcards
@State the results concerning the decidability of validity and satisfiability.
- Validity: Semi-decidable (i.e. $\text{RE}$, but not $\text{co-RE}$)
- Satisfiability: Not semi-decidable (in fact not $\text{RE}$, but $\text{co-RE}$)
@Prove that the validity problem for first-order formulas is semi-decidable.
This follows from the algorithm:
Input: Closed formula F
Output: Either that F is valid or compute forever
Compute a Skolem-form formula G equisatisfiable with (not F)
Let G _ 1, G _ 2, ... be enumeration of Herbrand expansion E(G)
for n = 1, 2... do:
if there is a resolution refutation from G _ 1, ..., G _ n, stop and output that F is valid
The correctness of this result follows from the soundness and completeness of ground resolution.
@Prove Church’s Theorem, i.e. that the satisfiability and validity problems for first-order logic are undecidable.
We need only consider the problem of validity, since if $F$ is valid iff $\lnot F$ is unsatisfiable.
We reduce from the Post correspondence problem. Let
\[\mathbf P = \\{ { x _ 1 \choose y _ 1 }, \ldots, { x _ k \choose y _ k } \\}\]where $x _ i, y _ i \in \{0, 1\}^\ast$ be an instance of the PCP. Recall a solution of $\mathbf P$ is a sequence $i _ 1, \ldots, i _ n$ such that
\[x _ {i _ 1} \cdots x _ {i _ n} = y _ {i _ 1} \cdots y _ {i _ n}\]To encode this in first-order logic, consider the signature $\sigma$ containing:
- One constant symbol $e$
- Two unary function symbols $f _ 0, f _ 1$
- Binary relation symbol $P$
The ground terms over this signature can be identified with bit-strings, e.g. $f _ 1(f _ 1(f _ 0(e)))$ (shortened to $f _ {110}(e)$) represents $110$.
Consider the following three formulas:
\[\begin{aligned} F _ 1 &= \bigwedge^k _ {i = 1} P(f _ {x _ i}(e), f _ {y _ i}(e)) \\\\ F _ 2 &= \forall u \forall v \bigwedge^k _ {i = 1} (P(u, v) \to P(f _ {x _ i}(u), f _ {y _ i}(v))) \\\\ F _ 3 &= \exists u P(u, u) \end{aligned}\]Then $\mathbf P$ has a solution iff $F _ 1 \land F _ 2 \to F _ 3$ is valid. (Does $F _ 1 = P(e, e)$ also suffice?)
If $F _ 1 \land F _ 2 \to F _ 3$ is valid, we can consider the Herbrand structure $\mathcal H$ where
\[P^\mathcal H = \\{ {f _ u(e) \choose f _ v(e)} : \exists i _ 1 \cdots \exists i _ t \text{ s.t. } u = x _ {i _ 1} \cdots x _ {i _ t}, v= y _ {i _ 1} \cdots y _ {i _ t}\\}\]Then $\mathcal H$ satisfies $F _ 1 \land F _ 2$, so by the validity of $F _ 1 \land F _ 2 \to F _ 3$ it follows that $\mathcal H$ satisfies $F _ 3$. This means that $\mathbf{P}$ has a solution.
Conversely, suppose $\mathbf P$ has a solution. Consider a structure $\mathcal A$ that satisfies $F _ 1 \land F _ 2 \to F _ 3$ Then by induction on $t$, for any sequence $i _ 1, \ldots, i _ t$,
\[\mathcal A \models P(f _ u(e), f _ v(e))\]where $u = x _ {i _ 1} \cdots x _ {i _ t}$, and $v = y _ {i _ 1} \cdots y _ {i _ t}$. But since $\mathbf P$ has a solution, it follows that
\[\mathcal A \models P(f _ u(e), f _ u(e))\]for some string $u$. Thus $\mathcal A \models F _ 3$.