Skip to content

Desperately Seeking Integers

August 6, 2018
tags: , , , , , , , , , ,


A few twists on Turing’s proof of undecidability of predicate calculus

TuringBicycleRichLongmoreHiRes
By permission of Rich Longmore,
artist, blog source

Alan Turing presaged Stephen Cook’s proof of {\mathsf{NP}}-completeness of {\mathsf{SAT}.} Turing reduced the halting problem for his machines to the decision problem of the first-order predicate calculus, thus showing (alongside Alonzo Church) that the latter is undecidable. Cook imitated Turing’s reduction at the level of propositional calculus and with a nondeterministic machine.

Today we present a version of Turing’s proof and show how it answers a side issue raised in our previous post.

Completely aside from the ongoing work by Harvey Friedman previewed in that post, we—that is Dick and Ken—were interested in the boundary between decidable and undecidable theories in logic. We noted Michael Rabin’s theorem that the theory of the rationals with order {(\mathbb{Q},<)} is decidable with first-order quantifiers and second-order quantifiers allowed only over unary predicates—that is, over subsets of {\mathbb{Q}.} We sketched how quantifiers over ternary predicates—that is, over subsets of {\mathbb{Q}^3}—enable defining properties of {+} and {*} from which undecidability follows by the mentioned theorem of Julia Robinson.

This left the binary case. Most in particular, we were interested in the decision problem for second-order sentences of the form

\displaystyle \Phi = (\exists B_1(\cdot,\cdot))\cdots(\exists B_k(\cdot,\cdot))\phi,

where the only predicate symbols in {\phi} (besides {<} and {=}) are {B_1,\dots,B_k} and {\phi} has only first-order quantifiers. We were given references to papers by László Kalmár and William Quine but judging from this by Church and Quine (see page 183 and also this and this plus these slides) we wonder what extra is involved, for instance pairing. Our search for a crisp and brief proof led back to Turing’s first-order theorem.

Defining a Stairway

Our starting point is to build a predicate {A(x,y)} so that {Z(x) \equiv A(x,x)} will define a set with properties needed of the integers. Our intent is to make {A(x,y)} define a kind of ceiling function {a(x) =} the least “integer” {y \geq x.} The first rules we write say that {A(x,y)} is a functional relationship:

  1. For each {x} there is a unique {y} so that {A(x,y)}:

    \displaystyle \forall x \exists y \ A(x,y),

    and

    \displaystyle \forall x \forall y \forall z \ A(x,y) \wedge A(x,z) \rightarrow y=z.

    Thus {A} defines the desired function {a(x).} The further rules we need are:

  2. The function {a(x)} is non-decreasing.

    \displaystyle \forall x \forall y \ x \le y \rightarrow a(x) \le a(y).

  3. The function {a(x)} is a “step-like” function:

    \displaystyle \forall x \exists y>x \exists z \forall w \in (x,y) \ a(w) = z.

    This means that {a(w)} is constant on an interval.

  4. We add one more rule for good measure but it does not do all we might expect:

  5. The function {a(x)} tends to infinity:

    \displaystyle \forall x \exists y \ a(y) > x.

Now all we need is to define the successor relation via more rules and postulate an element {z} to act as zero. The rules for successor {S(x,y)} are:

\displaystyle A(x,x) \wedge A(y,y) \wedge (\forall w)\neg(A(w,w) \wedge x < w \wedge w < y).

Among several ways to handle {z} we find it most thematic is to leave it unquantified and assert {A(z,z).} This will be on the left-hand side of implications of the form {L \rightarrow R.} Any interpretation—that is, any assignment of a function on {\mathbb{Q}} for {a(\cdot)} and a value for {z}—that makes all the {L} parts true will make {z} the bottom of a stairway that has infinitely many steps above {z.} Let {\phi_A} be the conjunction of {A(z,z)} and all the above rules.

The last rule for {a(x)} might seem to imply the stairway climbs to infinity. As we’ll discuss, this is not enough to make a single “stairway to heaven.” But it does provide that any angel who climbs some number {k} of steps above {z} will need exactly {k} steps to get back down to {z.}

Encoding Computations

Proofs of Turing’s theorem such as this implicitly use relations like {S_0(x,y) \equiv y = x0} and {S_1(x,z) \equiv z = x1} for binary strings on Turing machine tapes, which numerically work out to {y = 2x} and {z = 2x+1.} We will use a universal two-counter machine instead. We don’t need the arithmetic details of why it is universal, such as Marvin Minsky’s coding trick. The machine input is in unary but we can just define it as a natural number {w.} To represent the current state and the counters at any time {t}, we use three more binary predicates:

  • {B_0(t,s) \equiv} the machine is in state {s} at time {t.}

  • {B_1(t,u) \equiv} counter 1 holds value {u} at time {t.}

  • {B_2(t,v) \equiv} counter 2 holds value {v} at time {t.}

We can write rules to make these functions of {t.} The program has a finite number of states and so we can (if we wish) use dedicated symbols {p,q,r,\dots} for them. We can take {z} as the start state. Following Minsky, we need only two kinds of instructions:

  • {I(p,i,q)}: If in state {p}, increment counter {i} and go to state {q.}

  • {J(p,i,q,r)}: If in state {p} and counter {i} is zero, go to state {r}, else decrement counter {i} and go to state {q.}

Each state has exactly one of these instructions except the halting state {f.} The rules corresponding to these instructions all have the form

\displaystyle (\forall s,s',t,t',u,u',v,v') [L \longrightarrow R],

where {L} is

\displaystyle \begin{array}{rcl} &&(s = p) \wedge B_0(t,s) \wedge B_i(t,u) \wedge B_{3-i}(t,v)\\ &\wedge &S(t,t') \wedge B_0(t',s') \wedge B_i(t',u') \wedge B_{3-i}(t',v'). \end{array}

In case the instruction for state {p} is {I(p,i,q)} we have {R} as

\displaystyle s' = q \wedge S(u,u') \wedge v' = v,

whereas in case the instruction is a conditional jump {J(p,i,q,r)} we get {R} as

\displaystyle \begin{array}{rcl} & &(u = z \wedge u' = u \wedge s' = r \wedge v' = v) \\ &\vee &(u > z \wedge S(u',u) \wedge s' = q \wedge v' = v). \end{array}

We conjoin all the machine rules into one finite formula {\phi_B.} The conditions to start in state {z} on a given input value {w} are:

\displaystyle \phi_0(w) = B_0(z,z) \wedge B_1(z,w) \wedge B_2(z,z).

Here we mean {w} to be a fixed natural number but we can’t say so literally, so what {\phi_0(w)} includes are terms {S(z,w_1),S(w_1,w_2),\dots} until we get to the fixed value {w.} Finally, the condition to halt eventually in state {f} is:

\displaystyle \phi_1 = (\exists t'') B_0(t'',f).

Turing’s Theorem

Now given any number {w}, take

\displaystyle \phi_w = (\phi_A \wedge \phi_B \wedge \phi_0(w)) \longrightarrow \phi_1.

We want to decide whether {\phi_w} is valid. Now {\phi_w} is first-order: we haven’t put in the existential quantifiers over the predicates yet. To be valid in our setting means that whatever relations on {\mathbb{Q}} are used for the four predicates {A,B_0,B_1,B_2} and whatever value is used for {z}, the resulting statement about rational numbers is true.

Theorem 1 The formula {\phi_w} is valid if and only if {M} on input {w} halts in state {f.} Hence first-order predicate calculus is undecidable.

Proof: First suppose {M(w)} halts. We need only consider interpretations that make {\phi_A \wedge \phi_B \wedge \phi_0(w)} true. Such interpretations set up the initial configuration of {M(w)} with {z} standing for zero and make every instance of the universally quantified implications implications in {\phi_B} true. The chain of those instances eventually yields {B_0(t'',f)} where {t''} is the number of steps {M} takes to halt. Thus {\phi_1} and hence {\phi_w} overall are made true.

Conversely, suppose {\phi_w} is valid. Then we can pick the interpretation that makes {A} the actual integer ceiling function and {z = 0.} This makes {\phi_A \wedge \phi_B \wedge \phi_0(w)} true so it must make {\phi_1} true with {t''} ranging over the positive integers, which means that {M(w)} must halt. \Box

We seem to have sacrificed some generality by basing on {(\mathbb{Q},<)}, but in fact we used nothing about the rationals except {<} being a total order (including trichotomy: {a < b \vee a = b \vee b < a}). We could axiomatize those properties too. Alternatively, we could forgo equality {=} in favor of having function symbols as in the Turing machine-based proof mentioned above.

Ups and Downs in the Second-Order Case

Now we put the second-order quantifiers on the predicates in order to prove our desired theorem:

Theorem 2 Consider sentences of the form

\displaystyle \Phi = (\exists A) (\exists B_{0}) (\exists B_{1}) (\exists B_{2})\; \phi(A,B_{0},B_{1},B_{2}),

where {\phi} is first-order. The problem of deciding whether {\Phi} is true in {(\mathbb{Q},<)} is undecidable.

A natural impulse is to take {\phi = \phi_w} for a given input {w} as before. This leads to a notable issue, one that Ronald Fagin reminded us of. If {M(w)} halts, we get that {\Phi} (for that {w}) is true. Indeed—and this is a first hint that wires are crossed from the above proof—we can use the genuine integer ceiling function for the “{(\exists A)}” part and the rest follows.

Conversely, suppose {M(w)} does not halt. The rub is that we can still make {\Phi} true. Take {A} such that the derived set {Z}, our set of “integers,”includes {\{1 - 1/n : n \in \mathbb{N}^+\} \cup \{1\}.} Take {z = 0.} Then {1 - 1/(n+1)} is the successor of {1 - 1/n} for all {n} but {1} is not the successor of anything. Although the values of {B_0(t,s)} for {t = 1 - 1/n} are fixed for all {n} by actions of the machine, nothing prevents us from blithely defining {B_0(1,f)} to be true. This makes {\Phi} true too.

We forgot about the rule that {a(x)} grows unboundedly but it doesn’t help: we can just add the rest of the natural numbers to {Z.} Attempts to fix this by running {M} backwards from state {f} are forestalled by the possibility of adding {1 + 1/n} to {Z} for all {n} as well—our axioms are too weak to prevent having infinitely many predecessors.

The upshot is that although we can will into existence multiple infinite staircases, we cannot guarantee a single staircase that goes to heaven. In broad terms, we cannot rule out {M(w)} taking a nonstandard integer number of steps to halt (for connections to {\mathsf{P = NP}} start here). But in this situation we can fix the problem by a simple twist (used also here).

Proof: Define {\Phi_w} by asserting instead that {M(w)} doesn’t halt. That is, take

\displaystyle \phi_w = \phi_A \wedge \phi_B \wedge \phi_0(w) \wedge \neg \phi_1.

If {M(w)} doesn’t halt, then the standard assignment to {A} giving {z = 0} and {Z = \mathbb{Z}} works for that as well. The converse is now to suppose that {M(w)} does halt in state {f.} We need to show that there is no way to instantiate the four binary predicates and {z} to make the resulting sentence {\phi_w} true. By {\phi_0(w)} it sets up the initial configuration. The {\phi_B} part leans only on features of {\phi_A} that the instantiation must make true. Thus successive configurations are forced by the implications in {\phi_B} to follow correctly, so that {B_0(t,f)} is made true for some {t} that does belong to the staircase above {z.} This immediately contradicts of {\neg\phi_1.} So {\Phi_w} is false.

Thus {\Phi_w} is true if and only if {M(w)} does not halt. \Box

This finally answers the last post’s desire for showing concretely that second-order existential is undecidable with binary predicates, needing no reference other than Turing (OK: and Minsky). We would still like to trace this historically through the above-mentioned references to Kalmár and Quine and perhaps others. In contrast to great past attention to minimizing the alternation and number of quantifiers, we are curious also about minimizing the number of binary predicates. We note how this 1984 paper by Warren Goldfarb gets the number of binary predicates down to one but at a greater cost in unary predicates, of which above we’ve used none. We are also not sure how our setting with domain {\mathbb{Q}} and a fixed meaning for {<} plays in the tradeoffs.

Open Problems

What is the best reference? Is there a nice and clean proof for the case of just one dyadic predicate? What other tradeoffs, such as between function symbols and predicates using equality (or exists-unique quantifiers), are in play here?

[added reference to Goldfarb paper and changed next sentence; changed picture at top with permission notice]

from → All Posts, History, Ideas, Oldies, Proofs, Teaching

Leave a Reply

Discover more from Gödel's Lost Letter and P=NP

Subscribe now to keep reading and get access to the full archive.

Continue reading