Lambda the Ultimate

Perhaps I'm trying too hard, but I was hoping for some sort of clear correspondence between logic and untyped computation so I could interpret incompleteness in a related computation problem; an untyped version of this clear Curry-Howard correspondance if you will.

But you're right, phrased as "undecidability -> incompleteness" makes perfect sense, and perhaps that's all I'll need. I'll mull it over, thanks!

I want to "formalizably" offer two concise proofs: that Goedel's essential result implies Turing's halting result, and vice versa.

Let ARITH_ORACLE be the name of a proposition that says there exists a (constructable) effective, complete, and consistent theory of arithmetic.

Let HALTING_ORACLE be the name of a proposition that says there exists an effective algorithm for deciding whether or not a given turing machine halts on a given input.

Let's say (crudely - "formalizably"): Goedel proved ARITH_ORACLE and Turing proved HALTING_ORACLE. I want to show that, talking in this abstract but formalizable way -- they proved the exact same thing.

In other words, I owe two proofs (proof sketches, really):

    Goedel-world case:
    Assume that:  (not ARITH_ORACLE)
    Show that: (not ARITH_ORACLE) implies (not HALTING_ORACLE)
    Therefore: (not HALTING_ORACLE)

and

    Turing-world case:
    Assume that:  (not HALTING_ORACLE)
    Show that: (not HALTING_ORACLE) implies (not ARITH_ORACLE)
    Therefore: (not ARITH_ORACLE)

The Goedel-world case:

We assume that ARITH_ORACLE is false - we have Goedel's proof but not Turing's.

Let's assume that HALTING_ORACLE is true. We know from Turing that it isn't but we're pretending we don't. The goal is to prove HALTING_ORACLE is false from just "(not ARITH_ORACLE)". We start by assuming HALTING_ORACLE is true, aiming to establish a contradiction:

Suppose that in arithmetic theory T we want to know if proposition P is true. We can write a program that enumerates all possible proofs in T, say from shortest to longer, looking for a proof of P. The program halts only if a proof is found.

The halting oracle, combined with that proof-search program, can instantly tell us if any particular proposition is true, or false, or undecidable in any particular arithmetic theory.

For any given arithmetic proposition, we can actually enumerate all possible arithmetic theories to find out if any exist that prove a given proposition or are at least consistent with that proposition. The halting oracle can, again, tell us if any given proposition is proved, disproved, or consistent with the axioms we have so far.

So, now we make a new program (using our imaginary halting oracle): It starts with some "revealed arithmetic axioms". The user types in propositions. The program spits out a proof, a disproof, or the confirmation that the proposition is, in fact, an axiom per some complicated schema. Which exact axiom set the program represents depends on what propositions you ask it about, in which order, but on any given run it is a complete, consistent, and effective axiom system.

The specification of that program comprises an ARITH_ORACLE kind of oracle. We assumed HALTING_ORACLE and then proved ARITH_ORACLE but we're in Goedel's world where we know for sure that "(not ARITH_ORACLE)" .... so ....

    (not ARITH_ORACLE) implies (not HALTING_ORACLE)

The Turing-world case:

This case is much easier. The halting question about any turing machine and input configuration can easily be expressed as a proposition about arithmetic. Essentially: if a given turing machine halts on a given input, then there exists an integer X which satisfies some arithmetic equation.

In other words, if ARITH_ORACLE then HALTING_ORACLE, for sure. Just convert every halting problem to arithmetic, trivially, and prove or disprove a theorem.

Well, we know from Turing that "(not HALTING_ORACLE)" and therefore, "(not ARITH_ORACLE)":

    (not HALTING_ORACLE) implies (not ARITH_ORACLE)

The technique underlying most of the proof sketch there is to make use of the fact that a halting oracle can turn any effectively enumerable set (including infinite sets) into a membership predicate oracle at least over domains that have an effective equality predicate.

That's a fulcrum that just never gives up for proving other interesting stuff.

Thomas nailed down the intra-convertibility quite well and even provided the proofs with enough rigor and technicality to introduce the vital concepts that I think help build the larger intuition. Rap my knuckles if I go to far in my attempt to build generalized intuition; it's been a few years.

Note that Thomas appealed several times to the enumeration of a set. He even singles it out in his postscript on the proof-theoretic power of a halting oracle being equivalent to a membership predicate upon such a set. If you crack open a text on computability, you'll see this idea encoded in various ways, most commonly under the terms "recursive" and "recursively enumerable". It behooves the scholar interested in this area to dig into those concepts, so I'll leave off continued exposition.

The rubber and road come together when you remember the equivalence of "math" and "computation". Really not that surprising to the programmer-- encoding math in computation is an everyday task. The reverse encoding may be less obvious, but again there are plenty of fairly accessible proofs about for confirmation. So let's restate the classes. "Recursive" is fully computable, in the sense that we have a guaranteed Yes/No answer to any proposition. "Recursively Enumerable" is computationally exhaustive, in the sense that we can perform an exhaustive search of the answer space. Naturally, spaces of unbounded cardinality (size) separate the latter class from the former. Thus everything can normalize to the same set of terms; the mathematical or computational versions simply become implementation perspectives. So, let's look at Goedel's first incompleteness theorem.

One can set up an enumerated set of proofs. So, what will be covered by that set? In this world of enumerations, GFIT becomes an assertion that (given certain conditions) there exist true propositions whose proof will never be ennumerated. The Decision Problem then becomes knowledge about a test of membership over this set, essentially equal to "does the enumeration reach element X?".

The reverse case is more complicated, but I think more interesting. If one cannot guarantee a decision procedure for the enumeration of a particular element in the set, what does that mean for the eventual enumeration of a given element? Well, it turns out that the system is self-hosting; we can encode decideability right into the enumeration. So if we had to eventually emit proofs of all true propositions, we'd simply have to check for the proofs of "halts on X" and "never halts on X".

In sum, naasking is right; this tends not to get explored. I'm personally interested (and decently educated) in the subject, so I could put together this kind of explanation (with the immediate help of Thomas; thanks, your exposition was clear and helpful). But as with most mathematics, the discharge of any given theorem is not the enlightening step. The real meat is gaining some leverage of intuition over a domain. I find enumeration to be a mighty fine conceptual framework that has come in handy across math, logic, and computation. Biblio note: the best reference on my shelf for this is Hopcroft/Motwani/Ullman's Introduction to Automata Theory, Languages, and Computation, which I used to brush up for this. However, I can't speak for its approachability as a casual student as I got a thorough exposition in classroom lecture (thanks Dr. Friesen!).

See this: C. A. R. Hoare and D. C. S. Allison, Incomputability, Computing Surveys, pp. 169&em;178, September 1972. Draws a direct line from Russel to Turing.

Linky.

+20 :)

AFAIC, I also like to relate it to the (neverendingly) numerous forms of genuine creation of new formalisms that we layer, consciously or not, on top of our favourite legacies (pre-existing formalisms) that our brains pick up on their path to invention. Which is obviously the case in PL-related "hobbies". :)

Coincidentally, I've crafted my own small diagrammatic "toy-formalism" to picture to myself these important results re: (in-)completeness, (un-)decidability, and the (for sure-)layered language cakes they deal with. Just thought I could eventually share it here some time. Here it is, then:

ZFC axiomatic and acceptance of its offspring theories' incompleteness per Godel's Incompleteness Theorems (G):

+-------------------+       +-------------------+
|Axiom              |       |Creation           |
|  * => ZFC/0   ... |       |  ?    ZFC/G =>... |
|         ^         |       |       _____       |
+-----+   |   +-----+-------+-----+   |   +-----+
      |       |Use of the legacy: |       |
      |   G   |  ?     G/T => ZFC |  ZFC  |
      |       |       _____       |       |
      +-------+-----+   |   +-----+-------+
                    |       |
                    |   G   |
                    |       |
                    +-------+

Construction of N (Natural Numbers) in ZFC/Godel theoretical layers:
(classically built up from just ZFC's empty set)

+-------------------+       +-------------------+
|Axiom              |       |Creation           |
|  * =>  N/0    ... |       |  ?    N/ZFC =>... |
|         ^         |       |       _____       |
+-----+   |   +-----+-------+-----+   |   +-----+
      |       |Use of the legacy: |       |
      |  ZFC  |  ?    ZFC/G => N  |   N   |
      |       |       _____       |       |
      +-------+-----+   |   +-----+-------+
                    |       |
                    |  ZFC  |
                    |       |
                    +-------+

Construction of Turing Machines in N/ZFC theoretical layers:

+-------------------+       +-------------------+
|Axiom              |       |Creation           |
|  * => T.M/0   ... |       |  ?    T.M/N =>... |
|         ^         |       |       _____       |
+-----+   |   +-----+-------+-----+   |   +-----+
      |       |Use of the legacy: |       |
      |   N   |  ?    N/ZFC =>T.M |  T.M  |
      |       |       _____       |       |
      +-------+-----+   |   +-----+-------+
                    |       |
                    |   N   |
                    |       |
                    +-------+

Undecidability of the halting problem in T.M/N theoretical layers:

+-------------------+       +-------------------+
|Axiom              |       |Creation           |
|  * => H.P/0   ... |       |  ?    H.P/N =>... |
|         ^         |       |       _____       |
+-----+   |   +-----+-------+-----+   |   +-----+
      |       |Use of the legacy: |       |
      |  T.M  |  ?    T.M/N =>H.P |  H.P  |
      |       |       _____       |       |
      +-------+-----+   |   +-----+-------+
                    |       |
                    |  T.M  |
                    |       |
                    +-------+

Now, as Godel's incompleteness theorems state we cannot craft any kind of
a would-be both complete *and* consistent formal (theoretic) system appearing in this (would-be) schema:
(that one coined as, say, "NWF" : Not-Well-Founded)

+-------------------+       +-------------------+
|Axiom              |       |Creation           |
|  * => NWF/0   ... |       |  ?     NWF  =>NWF |
|         ^         |       |       _____       |
+-----+   |   +-----+-------+-----+   |   +-----+
      |   |   |(Hopeless...)      |   |   |
      |       |use of the legacy: |       |
      |  NWF  |  ?     NWF  =>NWF |  NWF  |
      |       |       _____       |       |
      +-------+-----+   |   +-----+-------+
                    |       |
                    |  NWF  |
                    |       |
                    +-------+

We can always try to invent such a NWF, but if it's axiomatized in itself and (supposedly) complete, then it'll always end up showing itself as inconsistent.
So that we're kind of "doomed" to have "to cope" forever with the ellipsis "..." (well, actually, just continue to humbly accept it) in those right-most T-boxes above, as far as theorem discovery/computational theory results go.

My 2 cts.

Great thread. It seems to cover this subject in depth, and even though I read it at the time, I didn't remember it having lacked the context I now have. Marc's sketch is the intuition I was starting to develop about the relationship, so I'll have to read it again more carefully to understand the dissenting opinions. Thanks!

...that the question probably somehow calls back to Binary Lambda Calculus and Combinatory Logic.