Are there "Godel encodings" for non-arithmetic theories?

Question

This is probably a very naive question, but is there something about Godel encoding that is essentially arithmetical, or is it possible to construct analogous mappings between the objects studied in a theory and statements in the theory itself for non-arithmetical theories (i.e, theories whose objects of study are not numbers). Are there any notable examples of this being done?

Answer 1

Here is a proof sketch of the (first) incompleteness theorem which does not (overtly) use numbers, instead using Turing machines (but any Turing-equivalent model of computation will suffice as long as it can take strings as inputs):

1. As a prerequisite, prove that the Halting Problem is unsolvable. This means that there does not exist a Turing machine H which can decide whether any given (input) Turing machine will halt on any given input. As this is a well-known and fairly straightforward proof, I will not explain it in full detail here, but the general idea is that you could use H to construct another machine which halts if and only if it does not halt, producing a contradiction.
2. Whatever proof system you are using must already have some way of formally representing a proof as a sequence of symbols, and some algorithm or procedure for deciding whether a given proof (sequence of symbols) is valid. If it lacks either of those things, then it's not really much of a proof system in the first place (i.e. it has not been sufficiently formalized to function as an object of study). As a further prerequisite, we're going to impose three additional requirements:
   • The procedure for deciding whether a proof is valid must be Turing-computable. Under the Church-Turing thesis, it is generally accepted that there is no other reasonable notion of computability that we could appeal to instead, so if your proof validation is not Turing-computable, then (again) it's not much of a system.
   • Either the alphabet of your proof system must be finite, or failing that, the set of all strings that can be interpreted as proofs is recursively enumerable. In practice, "the alphabet is finite" is by far the more common state of affairs (which automatically implies recursive enumerability because the Kleene star of a finite set is always recursively enumerable).
     • Most interpretations of Turing machines assume a finite alphabet. If you really want an infinite alphabet, you need a means of encoding it into some finite alphabet, or you need to redo a lot of computation theory.
   • Your proof system has a means of encoding the statements "Turing machine X halts on input Y" and "Turing machine X does not halt on input Y" for any suitable values of X and Y, and it never proves either statement unless it is true (i.e. it will never "prove" that X halts when in fact X does not halt, or vice-versa).
     • If you want to nitpick, you can also impose a requirement that this encoding can be computed from some (other) encoding of X and Y (as used in the Halting Problem), but we can also rewrite the proof of the Halting Problem to directly use the encoding of our proof system, and then this requirement can be dropped.
3. We can now construct a Turing machine M which will do the following:
   1. For each string which can be interpreted as a proof, check whether that string is a valid proof of the input statement or of its negation.
   2. If it's a valid proof of the input statement, halt with a 1 on the tape (or whatever symbol is convenient instead of "1").
   3. If it's a valid proof of the negation, halt with a 0 (or whatever symbol is convenient and different from the previous symbol).
   4. Continue running indefinitely until one of those two criteria is met.
4. Assume that M always halts.
5. If we want to solve the Halting Problem, then we can write an encoding of "machine X halts on input Y" for any values of X and Y, submit it to M, and wait for M to halt. By assumption, this always works, so M solves the Halting Problem.
6. But the Halting Problem is unsolvable, so this is a contradiction. Therefore, there must be some inputs for which M does not halt.
7. The only way for M to never halt on some input is if that input has no proof or disproof in the system we are considering.
8. Furthermore, we know that at least one such input (for which M doesn't halt) must be of the form "Turing machine X [halts/does not halt]," or else the contradiction would still go through. That implies that there exist Turing machines whose (non-)halting does not admit a proof in our system (for at least one input).
   • In practice, a machine that actually does halt can be proved to halt in the vast majority of "real" systems that we might be studying, so those machines are generally of the non-halting variety.

Some important considerations:

• Gödel's original formulation assumed the system "knows about" numbers well enough to do basic arithmetic. This proof instead assumes the system "knows about" Turing machines. These assumptions are not equivalent, so the statement we have proved is not identical to the statement that Gödel proved.
  • In general, that sort of assumption cannot be removed entirely, because there are very simple systems that don't "know" enough math to run into problems.
• In practice, most working mathematicians use systems powerful enough to do both arithmetic and computation theory, so it makes little difference to them which way we prove their system incomplete. But it's important to keep in mind if you care about things like model theory or provability.
• The Category Theorists will tell you that this is just one example of a broader pattern of diagonalization arguments, which also include things like Cantor's diagonal argument (showing that the reals are uncountable). They might also point out that this presentation of the proof actually hides the diagonalization inside the Halting Problem, itself another example of this pattern. It can be argued that "hiding the ball" in this fashion makes the proof more approachable but less pedagogically useful.
• As far as I can tell, this argument is originally due to Kleene (1943). The proof begins in part III, on page 58 (going by the original page numbers), and is quite a bit more formal than what is presented above.