Notes - Logic and Proof MT24, Decidability results for first-order logic

Created: November 26, 2024
Updated: December 01, 2024

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.

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$> Then by induction on $t$, for any sequence of times $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$.



Related posts