Chapter IX

APPENDIX Why mathematicians need not lose sleep over automatic theorem provers

This appendix presents the technical fact that any creative set L has trivially describable (hence trivially recognizable) infinite recursive^{†} subsets such that any “verifier” for L—i.e., a ϕ_{i} such that L = W_{i}—takes an unreasonablyhorrendously-outrageously humongous amount of time to verify membership in such subsets.

More precisely, we will define a particular creative set L and show that for any choice of a recursive ϕ_{j_{0}}—e.g., one with a horrendously big run time, see Chapter 7—and for any ϕ_{i_{0}} such that L = W_{i_{0}} there is a “trivially recognizable” infinite subset T ⊆ L such that, \underline{for every x ∈ T}, the computation of ϕ_{i_{0}}(x) will take at least as many steps as that of ϕ_{j_{0}}(x).

We will then offer an interpretation of this fact in the context of recursively axiomatized theories such as Peano arithmetic and Set Theory.

1. A creative set

1.1 Definition. We define the set L as follows:

L = {⟨i, j, x⟩ : (ϕ_{i}(⟨i, j, x⟩) ↓ ∨ϕ_{j}(⟨i, j, x⟩) ↓ ) ∧
ϕ_{i}(⟨i, j, x⟩) needs at least as many steps as ϕ_{j}(⟨i, j, x⟩)}
□

1.2 Theorem. L defined above is creative.

Proof. (1) L is semi-recursive (r.e.). Indeed, let

g(i, j, x) =^{def} (μy)(T (i, ⟨i, j, x⟩, y) ∨ T (j, ⟨i, j, x⟩, y))

†Indeed under some mild assumptions, regular.

2 IX. APPENDIX Why mathematicians need not lose sleep over automatic theorem provers

Then,

⟨i, j, x⟩ ∈ L ↔(∃y)(T (i, ⟨i, j, x⟩, y) ∨ T (j, ⟨i, j, x⟩, y)) ∧
T (j, ⟨i, j, x⟩, g(i, j, x))

and we are done by strong projection, closure properties of P_{∗}, including the fact that P_{∗} is closed under substitution of P-functions into variables.^{†}

(2) Next we prove that \overline{L} is productive. We will argue that f = λi.⟨i, i, 0⟩ is a productive function for \overline{L}.^{‡}

Let then

W_{i} ⊆ \overline{L}  (2.1)

Question. Can it be ⟨i, i, 0⟩ ∈ L? Well, if yes, then, in particular, ϕ_{i}(⟨i, i, 0⟩) ↓, that is,^{§} ⟨i, i, 0⟩ ∈ W_{i} contradicting (2.1).

We conclude that ⟨i, i, 0⟩ ∈ \overline{L}.

Question. Can it be ⟨i, i, 0⟩ ∈ W_{i}? Well, if yes, then ϕ_{i}(⟨i, i, 0⟩) ↓. Moreover ϕ_{i}(⟨i, i, 0⟩) takes no more time to compute than ϕ_{i}(⟨i, i, 0⟩) (i.e., itself). Thus, the entrance requirement for L is met: ⟨i, i, 0⟩ ∈ L, contradicting (2.1) once more. Thus, ⟨i, i, 0⟩ ∉ W_{i} and we are done. □

With the theorem out of the way—for now—let us choose and fix any recursive ϕ_{j_{0}} whatsoever. Next, let us choose \underline{any verifier whatsoever}^{¶} ϕ_{i_{0}} for L. That is

L = W_{i_{0}}  (3)

Let also

T =^{def} {⟨i_{0}, j_{0}, x⟩ : x ∈ ℕ}  (4)

We will argue two things:

(I) T ⊆ L

(II) For all x ∈ ℕ, ϕ_{i_{0}}(⟨i_{0}, j_{0}, x⟩) takes at least as much time as ϕ_{j_{0}}(⟨i_{0}, j_{0}, x⟩) to compute.

OK, \underline{fix an arbitrary x} and let us pose and answer some questions:

Question. Can it be ϕ_{i_{0}}(⟨i_{0}, j_{0}, x⟩) ↑? If yes, then surely ϕ_{i_{0}}(⟨i_{0}, j_{0}, x⟩) takes at least as much time as ϕ_{j_{0}}(⟨i_{0}, j_{0}, x⟩) since the former is undefined and the latter is defined (recall that ϕ_{j_{0}} ∈ R). Thus the entrance conditions for L are met:

⟨i_{0}, j_{0}, x⟩ ∈ L

But ϕ_{i_{0}}(⟨i_{0}, j_{0}, x⟩) ↑ means

⟨i_{0}, j_{0}, x⟩ ∉ W_{i_{0}}

†If Q(y, x⃗) ∈ P_{∗} and λz⃗.f(z⃗) ∈ P, then Q(f(z⃗), x⃗) ∈ P_{∗} since Q(f(z⃗), x⃗) ↔ (∃y)(y = f(z⃗) ∧ Q(y, x⃗)). Now use the fact that the graph of f is in P_{∗}, and closure under ∧ and ∃.

‡So is λi.⟨i, i, k⟩ for any k ∈ ℕ.

§Recall the definition: W_{i} = dom(ϕ_{i}).

¶Recall the terminology “verifier”. It means that if z ∈ L then ϕ_{i_{0}}(z) ↓—i.e., “program”

i_{0} verifies membership—else ϕ_{i_{0}}(z) ↑, i.e., program i_{0} runs forever.

Supplementary Lecture Notes, C5111/C4111 (Winter 2002)\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

contradicting (3). Thus,

ϕ_{i_{0}}(⟨i_{0}, j_{0}, x⟩) ↓  (5)

By (3), ⟨i_{0}, j_{0}, x⟩ ∈ L, establishing (I).

Now for (II):

Question. Can it be that ϕ_{i_{0}}(⟨i_{0}, j_{0}, x⟩) ↓ in strictly fewer steps than ϕ_{j_{0}}(⟨i_{0}, j_{0}, x⟩) ↓?

NO. Otherwise, we have the entrance sub-condition (for L) to the left of “∧” true, but the sub-condition to the right false. Hence ⟨i_{0}, j_{0}, x⟩ ∉ L (yet ⟨i_{0}, j_{0}, x⟩ ∈ W_{i_{0}}) contradicting (3) again. Thus, (II) is proved.

Since we can arrange to pick a ϕ_{j_{0}} that runs horrendously-outrageously-humongously slowly (Ch.7), what we have proved is that for any such ϕ_{j_{0}} and any choice of verifier “program” i_{0} for L, we can build an infinite subset T (see (4)) of L that, despite being trivially recognizable on its own, the verifier

i_{0} for L will be horrendously-impractically-slow on \underline{every} input in T.

Let us now bring into the discussion the fact that L is creative. We cite two facts without proof (for proofs see Ch.9 of “Computability”).

By the way, we can hope for no more than a verifier for a creative set. We can have no yes/no recognizer (that is, decider) since such a set is not recursive (its complement is productive, i.e., effectively non-r.e.).

Fact 1. The set of theorems of each of Peano arithmetic and (axiomatic) Set Theory is creative.

Fact 2. Any two creative sets, A and B are recursively isomorphic. This means that there is a recursive 1-1 and onto function f : ℕ → ℕ such that f[A] = B.

Thus, there is, essentially, only one creative set. In particular, L can be thought (within two-way 1-1 recursive encoding) that it is the set of all theorems of Peano arithmetic.

Select now, as above, a very-very-very slowly computable total ϕ_{j_{0}} and pick any verifier ϕ_{i_{0}} for L.

Consider the associated set T. This is a (sub)set of theorems (an infinite one at that) of Peano arithmetic, since T ⊆ L. Now, “humanly” speaking, the T -theorems are trivial to recognize, since we can tell at a glance if a number has the form ⟨i_{0}, j_{0}, x⟩—i.e., 2^{i_{0}+1}3^{j_{0}+1}5^{x+1}—or not.

On the other hand, our arbitrary verifier ϕ_{i_{0}} will have loads of trouble on every theorem in T: it will take more time on each such than what ϕ_{j_{0}} needs.

Mathematicians (and computer scientists who prove theorems) will sleep easy tonight.

If we think of natural numbers as strings over {0, 1}, that is, if we identify ℕ with {0, 1}^{∗}, then the set of theorems T is a regular language over the alphabet {0, 1, (,),; } where “;” represents “,”. I mean, we can think of “⟨i_{0}, j_{0}, x⟩” as the string “(i_{0}; j_{0}; x)”, x ∈ {0, 1}^{∗}.

Supplementary Lecture Notes, C5111/C4111 (Winter 2002)\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis