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

[[Course - Logic and Proof MT24]]^U

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

Flashcards

Related posts