44
$\begingroup$

Given any reasonable formal system F (e.g., Peano Arithmetic or ZFC), we all know that one can construct a Turing machine that runs forever iff F is consistent, by enumerating the theorems of F and halting if it ever proves 0=1.

However, what interests me here is that the "obvious" such Turing machine will be an extremely complicated one. Besides the axioms of F, it will need to encode the symbols and inference rules of first-order logic, which (among other things) presumably requires writing a parser for context-free expressions. If you actually wrote the Turing machine out, it might have millions of states! Even in a high-level programming language, the task of writing a program that enumerates all the theorems of ZFC is not one that I'd casually give as homework.

Notice that this situation stands in striking contrast to that of universal Turing machines, which we've known since the 1960s how to construct with an extremely small number of states (albeit usually at the price of a complicated input encoding). It also contrasts with the observation that very small Turing machines can already exhibit "complicated, unpredictable" behavior: for example, the 5th Busy Beaver number is still unknown, and it seems like a plausible guess that the values of (say) BB(10) or BB(20) are independent of ZFC.

Thus my question:

Is any "qualitatively simpler" class of computer programs known, which can be proved to run forever iff ZFC is consistent? Here, by "qualitatively simpler," I mean doing something that looks much more straightforward than enumerating all the first-order consequences of the ZFC axioms, but that can nevertheless be proved by some nontrivial theorem to be equivalent to such an enumeration. Feel free to replace ZFC by ZF, PA, or any other system to which Gödel's Theorem applies if it makes a difference.

This question is clearly related to the well-known goal of finding "natural" or "combinatorial" statements that are provably independent of PA of ZFC, but it's not identical. For one thing, I don't demand that your statement have any independent mathematical interest---just that the computer program corresponding to your statement be easier to write than a program that enumerates all ZFC-theorems!

One concrete goal would be to find the smallest n for which you can prove that the value of BB(n) (the nth Busy Beaver number) is independent of ZFC. (It's clear that BB(n) is independent of ZFC for all n≥n0, where n0 is the number of states in a Turing machine that enumerates all ZFC-proofs and halts if it proves 0=1.)

As a first step, though, I'll be delighted to learn of any theorem that simplifies the task of writing proof-enumerating programs. (Even if the programs are still expressed in a high-level formalism, and are still horrendously complicated when compiled down to Turing machines.)

Improve this question
$\endgroup$
15
  • 1
    $\begingroup$ Scott, isn't the enumeration of all theorems of ZFC almost surely non-computable, though definable? I.e. the hard to program Turing Machine, you are suggesting would be of infinite length? $\endgroup$
    – Halfdan Faber
    Apr 24, 2011 at 23:44
  • 4
    $\begingroup$ No. There's certainly a finite TM that enumerates all the theorems of ZFC (for example, in increasing order of their Godel numbers). It's just a large finite TM. $\endgroup$
    – Scott Aaronson
    Apr 24, 2011 at 23:51
  • 1
    $\begingroup$ Scott: Just to make sure, there are combinatorial statements that are equivalent to (for example) the 1-consistency of PA (which is strictly stronger than its consistency), but that wouldn't be the sort of thing you are after, right? $\endgroup$
    – Andrés E. Caicedo
    Apr 25, 2011 at 0:23
  • 2
    $\begingroup$ Scott: Ok, I figured you were after $\Pi^0_1$ statements. That has actually been subject of recent work (by Friedman and others). The link I posted is then precisely in this direction (though perhaps still unsatisfactory). I'll try to expand this into an answer a bit later. $\endgroup$
    – Andrés E. Caicedo
    Apr 25, 2011 at 0:49
  • 4
    $\begingroup$ @Scott: In your first comment (replying to Halfdan Faber), the part in parentheses, about enumerating the theorems in order of Gödel numbers, is wrong. If you could do that, you'd have a decision procedure; to tell whether a given sentence S is a theorem of ZFC, start the enumeration, wait until something with larger Gödel number than S is enumerated, and see whether S has been enumerated by then. What can be done is to enumerate the theorems of ZFC in order of the (first) Gödel numbers of their proofs. $\endgroup$
    – Andreas Blass
    Apr 26, 2011 at 21:49

3 Answers 3

Reset to default
18
$\begingroup$

The discussion in the comments has helped clarify your question for me. I believe that it is closely related to the following remark by Harvey Friedman:

I am convinced that trying to take consistency statements like Con(ZFC + measurable cardinals) or Con(ZFC + rank into itself), Con(ZF + inaccessible rank into itself), etc., and force them into smaller and smaller Turing machines not halting, with demonstrable equivalence in an extremely weak system, is an open ended project, in the practical sense, that will create a virtually unlimited opportunity, in the practical sense, for a stream of ever and ever deeper mathematical ideas. Ideas that could come from unexpected sources, ideas that could have independent deep ramifications, ideas that -- well who knows what to expect. The benchmark is completely clear - how many quadruples? At the very least, deep ideas about set theory and large cardinals, but probably much more diverse deep ideas about, well, the unexpected. Any branch of mathematics whatsoever might prove useful, or even crucial, here. Whereas, we don't think that "any branch of mathematics" might be useful in logic problems, normally. This is different.

Other relevant postings from the FOM archives may be found here and here.

So Friedman's work, that Andres Caicedo alluded to in the comments, is probably the closest thing to what you want. I don't know of any other people who are working actively on this kind of project.

As a side remark, I believe that your intuition is correct that there is some kind of intrinsic "complexity" to the statement "ZFC is consistent," and roughly speaking it is because the totality of mathematical knowledge is a "complex" entity.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Btw, are we all certain that the required state count of a theorem-enumerating TM is essentially that of any context-free grammar generator? Might the first-order logic inference rules be easier/harder to apply? $\endgroup$
    – Liron
    Apr 26, 2011 at 14:21
  • $\begingroup$ Timothy, thanks so much for digging up that quote! Friedman beautifully expresses precisely what I was getting at with this question. $\endgroup$
    – Scott Aaronson
    Apr 26, 2011 at 16:15
  • $\begingroup$ As a side comment, I believe that Friedman's intuition is that the "complexity" here lies with the axioms, rather than with the rules of inference of classical first-order logic. It might be interesting to see how small a Turing machine is needed to check that there aren't two validities of first-order logic that are negations of each other. (Though thinking about it now, I guess we might want to pick a base theory that doesn't prove the consistency of first-order logic, and such a theory might be so weak that we can't prove much at all in it. I'm not sure.) $\endgroup$
    – Timothy Chow
    Apr 27, 2011 at 14:13
11
$\begingroup$

How about this: As discussed in

Does anyone know a polynomial whose lack of roots can't be proved?

there is a polynomial in several variables that has an integer root iff ZFC is inconsistent. In other words, if the polynomial has $n$ variables, you can enumerate all $n$-tuples of integers and plug them into the polynomial until the result is 0.
Since ZFC is consistent (as we all know), the computer program will run forever.

Improve this answer
$\endgroup$
16
  • 3
    $\begingroup$ "Since ZFC is consistent (as we all know)". Nice joke! $\endgroup$
    – SNd
    Apr 24, 2011 at 21:48
  • 2
    $\begingroup$ Ah, yes -- but as the author points out in the conclusion, that polynomial is extremely complicated (just like the Turing machine)! I'm looking for ideas/results from logic or other areas that could be used to cut down the complexity. $\endgroup$
    – Scott Aaronson
    Apr 24, 2011 at 21:52
  • 4
    $\begingroup$ To clarify: I don't see any reason to believe that writing a program to search for solutions to the polynomial would be simpler than the original task, of writing a program to search for contradictions in ZFC. (Maybe it will be, but I don't see why!) I know that there are many ways to transfer the complexity of the ZFC axioms + first-order logic from one setting to another. What interests me is that I've never seen a clear-cut way to reduce the complexity (but also know no reason why there shouldn't be one). $\endgroup$
    – Scott Aaronson
    Apr 24, 2011 at 22:01
  • 2
    $\begingroup$ I agree. The program is conceptually simple, just find the root of a given polynomial, but the complexity has been shifted into the list of coefficients. $\endgroup$
    – Stefan Geschke
    Apr 24, 2011 at 22:34
  • 5
    $\begingroup$ Andrey Bovykin has a research program involving short Diophantine expressions equiconsistent with various theories, you might want to check it out. $\endgroup$
    – Emil Jeřábek
    Apr 26, 2011 at 14:01
0
$\begingroup$

Maybe I understand the question wrong, but I think you should specify the logic in which the equivalence is proven. This is a little bit similar to relative consistency. Then you have three logics. The two logics that you compare and the logic in which you prove the relative consistency.

If your logic that proves the equivalence, can prove Con(PA), then the equivalent Turing machine is quite simple. Just a Turing machine that runs forever.

About the question itself. One reason why making a program that enumerates the theorems is hard, is because a logic is non-deterministic (you have choices in the axioms and inference rules you use) and a programming language (and a Turing machine) is deterministic. The task becomes much easier if you take a non-deterministic language.

To show that with a simple example. Take the last theorem of Fermat. To encode that as a halting problem, you have to diagonalize over a, b, c and n. This require some amount of coding. However, in a non-deterministic language, you just take a, b, c and n non-deterministic. A much simpler program.

Finally, the tricky part of programming the axioms and inference rules of a logic, is the variable substitution and the problem when variables are used multiple times. I think it should be possible to get fully rid of variables, which makes it easier to program, but less readable for humans.

Lucas

Improve this answer
$\endgroup$
3
  • $\begingroup$ Lucas, in order to talk about Turing machines we need something like PA or even a weak fragment of it. Most results in mathematics (like the incompleteness theorems, for example) can actually be proved within such a framework. That would be a reasonable starting point if you want to formalize things. $\endgroup$
    – Stefan Geschke
    Apr 28, 2011 at 20:02
  • $\begingroup$ Stefan you write "want to formalize things". The point I tried to make is that the question requires the formalization. Without it, it is not a proper question. $\endgroup$
    – Lucas K.
    Apr 28, 2011 at 20:11
  • 1
    $\begingroup$ I was imagining the equivalence would be provable in a weak fragment of PA, like most other "ordinary" mathematical statements. $\endgroup$
    – Scott Aaronson
    Apr 29, 2011 at 4:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.