# Incompleteness Theorems for Limit-Computable Formal Systems

Godel’s First and Second Inconpleteness Theorems are about Peano Arithmetic, but their punchlines are respectively that “Any sufficiently expressive computable formal system cannot be complete and consistent” and that “Given a computable emulation of the proof theory of such a system inside itself, no proof consistency can be given, if the system is consistent”. In mathematics we like certainty (or something like it, for those of you with less objective dispositions), so this is a problem. However, practical considerations do not always need certainty. In this spirit, we might not require a computable formal system, but merely a limit-computable one. By this I mean that there is a theoretical machine $$m$$ which takes pairs of sentences $$s$$ of the system and natural numbers $$n$$ as inputs and outputs $$0$$ or $$1$$ assuming it halts. Provability of $$s$$ in the system is that $$\lim_{n\to\infty}m(s,n)=1$$ which just says that, for all but finitely many $$n$$, $$m$$ outputs $$1$$ on input $$(s,n)$$. In this way, if we accept the system, we can at least be sure that it will eventually tell us the right answer. Are there analogues of the Incompleteness Theorems for such systems? Or similar results?

• When you speak of "Limit-computable" are considering this concept or is it a new (your own) idea ? Commented Nov 12, 2020 at 10:54
• @Mauro ALLEGRANZA The concept of limit-computable is the same. I am not talking about the system in the paper specifically, even if it’s not computable. An example: we can prove the First Incompleteness Theorem from the Halting Problem. In any computable system which accurately describes computation, there is a machine m and an input i such that we cannot decide if m halts on i. But, we can just run the computation, give a value of 0 if it has not halted at time t, and a value of 1 if it does, and in the limit we will eventually know if m halts on i if in our system 1 is true and 0 is false. Commented Nov 12, 2020 at 11:30
• Maybe we have some issue with "in the limit we will eventually know". The gist of G's Theorem is that the usual concept of proof (that is a finite process) is not equiv to the "platonist" concept of truth (something objective and independent of time and humans and their capability to know it). If so, we already "know" that one of the Godel's pair of undecidable formulas: $G$ and $\lnot G$ is true. The issue is that, without a proof we do not know (inside the system) which one. What adds to this picture to say that an infinitely long computation will decide, but we do not know in what way ? Commented Nov 12, 2020 at 11:36
• Sorry, of course we will not eventually know. But we know that the answer will eventually be right. Suppose we are developing a formal system to represent something important. If we know it will eventually converge on the right answer, that’s some reason to do what it tells us at some point. It’s contrived, but suppose we live forever and at every time-step, we would like to say whether the machine halts. By guessing based on whether or not it’s halted, we ensure that we are right almost all of the time. Since we don’t live forever, errors would be proportionally larger, but still. Commented Nov 12, 2020 at 12:04

I'm going to focus on the first incompleteness theorem below, except for the final paragraph.

EDIT: the material here can all be found in Salehi/Seraji, Godel-Rosser's incompleteness theorems for non-recursively enumerable theories (although I was unaware of that paper when I wrote this answer). Additionally, note that Ishii, A note on the first incompleteness theorem claims a result contradicting the following, but that paper is incorrect and the error is addressed by Salehi/Seraji.

There are two problems with the theory you describe. The first is that, as you observe, it is not actually computable - and as finite entities, we can't really make that much use of limit computability. The second issue is that it is unsound: it is complete and consistent, but proves false sentences.

When we take soundness into account we see that there is indeed a version of the incompleteness theorem which "relativizes" to limit computation and beyond. Specifically, for each $$n>0$$ we have:

($$\mathsf{GIT_n}$$): Suppose $$T$$ is a consistent theory of arithmetic which contains Robinson arithmetic, is $${\bf 0^{(n-1)}}$$-computably axiomatizable, and is $$\Pi^0_n$$-sound. Then $$T$$ is incomplete.

(As usual this can be generalized substantially, but let's focus on this version for simplicity.)

• "$${\bf 0^{(n-1)}}$$" is the $$n-1$$th iterate of the Turing jump. The case $$n=1$$ corresponds to computably axiomatizable theories (= the original GIT).

• Using Craig's trick, we can replace "$${\bf 0^{(n-1)}}$$-axiomatizable" by "$$\Sigma_n$$-axiomatizable" (the usual version of Craig's trick is that computably axiomatizable and c.e. axiomatizable are equivalent, but it generalizes).

• "$$\Pi^0_n$$" is a particular class of sentences in the language of arithmetic - see here. "$$\Pi^0_n$$-soundness" is the property of only proving true $$\Pi^0_n$$ sentences. Note that when $$n=1$$ this is a redundant hypothesis, since every theory containing Robinson arithmetic proves all true $$\Sigma^0_1$$ sentences and so cannot prove any false $$\Pi^0_1$$ sentences without being inconsistent; this is why this additional hypothesis doesn't appear in the usual statement of the first incompleteness theorem.

• The two notions above are related to each other and to (a generalization of) limit computability: see Post's theorem and Shoenfield's limit lemma. In particular, we have "computable = $$\Delta^0_1$$ = $${\bf 0^{(0)}}$$-computable" and "limit computable = $$\Delta^0_2$$ = "$${\bf 0^{(1)}}$$-computable."

The $$\mathsf{GIT_n}$$s above can be proved by relativizing any of the computability-theoretic proofs of the usual incompleteness theorem; a useful trick here is that if $$T$$ satisfies the hypotheses of $$\mathsf{GIT_n}$$ then so does $$T$$ + the set of true $$\Sigma^0_n$$ sentences (this is a good exercise). Proof-theoretic arguments can also be used, but their relativizations are in my opinion less immediate.

[The second incompleteness theorem poses an interesting new difficulty, on the other hand; see an earlier edit of this question in conjunction with Andreas Blass' comment below.]

• Brilliant. In your note about redundancy, should the case be n=0? Commented Nov 13, 2020 at 1:02
• When you add all true $\Sigma^0_n$ sentences to $T$, the resulting theory, though able to prove each individual $\Sigma^0_n$ sentence, doesn't seem to know that it has this ability. That is, it doesn't seem to prove "all $\Sigma^0_n$ truths are provable." In the traditional $n=1$ case, that sort of knowledge is used, in the "difficult" Hilbert-Bernays derivability condition. So I don't see how your argument for the second incompleteness theorem avoids that. Commented Oct 25, 2021 at 16:23
• @AndreasBlass Ooh, that's a point - I'm not sure what I had in mind. I'll delete that part until I can fix it appropriately. Commented Oct 25, 2021 at 16:37