Undecidability of Validity and Satisfiability

Logic and Proof Hilary 2016
Undecidability of Validity and Satisfiability

James Worrell
In this lecture we consider the computational problems of determining validity and satisfiability of
first-order formulas. We show that both validity and satisfiability are undecidable. On a positive
note, we show that validity is semi-decidable (or recursively enumerable). Intuitively this is because
a valid formula F has a finite witness of its validity—namely a finite resolution refutation of ¬F .
Satisfiability is not semi-decidable however. Intuitively, there need not be finite witness that a
given formula is satisfiable. In particular, there are satisfiable formulas that have no finite models.
1 Semi-Decidability of Validity
Theorem 1. Validity of first-order formulas is semi-decidable.
Proof. Recall that a semi-decision procedure for validity should halt and return “valid” when given
a valid formula as input, but otherwise may compute forever. Such a procedure is as follows. (Note
that there is no loss of generality in restricting to closed formulas since F is valid iff ∀xF is valid.)
Semi-Decision Procedure for Validity

Input: Closed formula F
Output: Either that F is valid or compute forever
Compute a Skolem-form formula G equisatisfiable with ¬F
Let G1 , G2 , . . . be an enumeration of the Herbrand expansion E(G)
for n = 1 to ∞ do
begin
if 2 ∈ Res∗ (G1 ∪ . . . ∪ Gn ) then stop and output “F is valid”
end
The procedure relies on the fact that F is valid if and only if ¬F is unsatisfiable. To show
unsatisfiability of ¬F we transform it into an equisatisfiable formula G in Skolem form. Then, by
the refutation completeness of ground resolution, G is unsatisfiable iff there is a ground resolution
refutation of G. If such a refutation exists it will eventually be discovered by the procedure. Note
that for each n the set of clauses Res∗ (G1 ∪ . . . ∪ Gn ) that can be derived by resolution from
G1 ∪ . . . ∪ Gn is computable in a finite amount of time. (Here we regard each Gi as a set of
clauses.)
In the above proof it was convenient to invoke the refutation completness of ground resolution.
However ulitmately the result relies on Herbrand’s Theorem and the Compactness Theorem for
propositional logic, which together guarantee that that F is valid if and only if some finite subset
of E(G) is unsatisfiable.
1
2 Undecidability of Validity and Satisfiability
In this section we recall the definition of Post’s Correspondence Problem (PCP), and show how to
transform a given instance of this problem into a first-order formula such that the instance has a
solution if and only if the formula is valid. It follows that the validity problem for first-order logic
is undecidable.
An instance of Post’s correspondence problem consists of a finite set of tiles. Each tile has a
bit-string on the top and a bit-string on the bottom. For example, we could have tiles

1 10 011
, ,
101 00 11
A solution to the problem is a sequence of tiles, allowing the same tile multiple times, such that
the top string equals the bottom string. In the above example a solution is

1 011 10 011
101 11 00 11
In general, an instance of Post’s correspondence problem is a finite set of pairs of bit-strings

P = {(x1 , y1 ), . . . , (xk , yk )}, where xi , yi ∈ {0, 1}∗ . A solution of P is a sequence i1 , i2 , . . . , in
such that xi1 xi2 . . . xin = yi1 yi2 . . . yin . In the above example one solution is the sequence 1, 3, 2, 3.
Clearly for each particular PCP instance, the set of potential solutions, i.e., sequences of tiles is
infinite. Thus solving an instance of PCP involves searching an infinite set.
We encode this problem in first-order logic using a signature with constant symbol e, two unary
function symbols f0 , f1 and a binary relation symbol P . The ground terms over this signature can
be considered as bit-strings, e.g., the term f1 (f1 (f0 (e))) represents the bit-string 110. In general,
for a bit-string b1 . . . bt ∈ {0, 1}∗ we denote the term fb1 (. . . (fbt (x)) . . .) by fb1 ...bk (x).
Our goal is to transform a given instance P of Post’s correspondence problem into a closed
formula F such that P has a solution if and only if F is valid. We first give the idea of the
construction in the above example. Consider the following three formulas:
F1 = P (f1 (e), f101 (e)) ∧ P (f10 (e), f00 (e)) ∧ P (f011 (e), f11 (e))
F2 = ∀u ∀v (P (u, v) → P (f1 (u), f101 (v)) ∧ P (f10 (u), f00 (v)) ∧ P (f011 (u), f11 (v)))
F3 = ∃u P (u, u) .
We claim that F1 ∧ F2 → F3 is valid if and only if the PCP instance has a solution.
Given a general instance P = {(x1 , y1 ), . . . , (xk , yk )} of PCP we have the formulas
k
^
F1 = P (fxi (e), fyi (e))
i=1
k
^
F2 = ∀u ∀v (P (u, v) → P (fxi (u), fyi (v)))
i=1
F3 = ∃u P (u, u) .
Proposition 2. P has a solution if and only if F1 ∧ F2 → F3 is valid.
2
Sketch. Suppose that F1 ∧ F2 → F3 is valid. Consider the Herbrand structure H for which
PH = {(fu (e), fv (e)) : ∃i1 . . . ∃it . u = xi1 . . . xit and v = yi1 . . . yit } .
Clearly H satisfies F1 ∧ F2 . Thus it must hold that H satisfies F3 . But this means that P has a
solution.
Conversely suppose that P has a solution. We show that F1 ∧ F2 → F3 is valid. To this end,
consider a structure A that satisfies F1 ∧ F2 . Then we can show by induction on t that for any
sequence of tiles i1 . . . it , A |= P (fu (e), fv (e)), where u = xi1 . . . xit and v = yi1 . . . yit . But since P
has a solution, A |= P (fu (e), fu (e)) for some string u. Thus A |= F3 .
Corollary 3. The satisfiability and validity problems for first-order logic are undecidable.
Proof. Undecidability of validity follows from undecidability of Post’s Correspondence Problem,

which was shown in the Models of Computation course. Furthermore, since F is valid if and only if
¬F is unsatisfiable, undecidability of satisfiability is immediate from undecidability of validity.
It follows from Theorem 1 and Corollary 3 that satisfiability is not even semi-decidable. Indeed
if satisfiability were semi-decidable then we could decide validity as follows. Given a formula F ,
either F is valid or ¬F is satisfiable. Thus we could decide validity of F by simultaneously running
a semi-decision procedure for validity on F and a semi-decision procedure for satisfiability on ¬F .
Corollary 4. Satisfiability of first-order formulas is not semi-decidable.

Undecidability of Validity and Satisfiability

Uploaded by

Copyright:

Available Formats

Undecidability of Validity and Satisfiability

Uploaded by

Document Information

Original Description:

Original Title

Copyright

Available Formats

Share this document

Share or Embed Document

Sharing Options

Did you find this document useful?

Is this content inappropriate?

Copyright:

Available Formats

Undecidability of Validity and Satisfiability

Uploaded by

Copyright:

Available Formats

Logic and Proof Hilary 2016

Undecidability of Validity and Satisfiability

Semi-Decision Procedure for Validity

In general, an instance of Post’s correspondence problem is a finite set of pairs of bit-strings

Proposition 2. P has a solution if and only if F1 ∧ F2 → F3 is valid.

Proof. Undecidability of validity follows from undecidability of Post’s Correspondence Problem,

Corollary 4. Satisfiability of first-order formulas is not semi-decidable.

You might also like