First Incompleteness via computation: an explicit construction

[Anatoly Vorobey]

Dear FOM,

It's standard by now in popular books and undergraduate courses to see the
first Incompleteness Theorem proved through
a computation-based argument. However, details matter, and details include
the strength of the assumptions on a theory T as well as whether we get a
constructive incompleteness proof. In addition to T assumed recursively
axiomatizable and appropriately strong, the usual choices are:

A. T assumed sound.
B. T assumed omega-consistent.
C. T assumed consistent.

1. We get a nonconstructive proof by contradiction that T is incomplete.
2. We get a specific sentence W, in principle constructible from axioms of
T,
such that T doesn't decide W.

With this terminology, I believe the original proof by Godel is B2, and the
"Rosser's trick" upgrades it to C2. On the other hand, the simplest and
most frequent computation-based proof is A1, when we say "Given that T is
complete and sound, enumerate all proofs in T to decide the Halting
Problem".

I'm used to seeing computation-based proofs that assume soundness, but this
isn't an inherent limitation. A few years ago, Scott Aaronson wrote a
blogpost on a computation-based proof that merely assumes T is consistent
(he did not claim it was new and in fact clarified that Kleene's 1967
textbook contains a variant of it):
https://www.scottaaronson.com/blog/?p=710

However, the proof in Aaronson's post is still nonconstructive, i.e. it's a
C1 proof while it'd be nice to have a C2 proof.

Recently I was struck to discover just such a proof laid out in a long note
on Stack Overflow, by a pseudonymous contributor calling themselves
'user21820'. This is the note:
https://math.stackexchange.com/questions/2486348/computability-viewpoint-of-godel-rossers-incompleteness-theorem
I want to bring this proof to the attention of FOM and ask whether it's new
and/or appears in any standard references/textbooks. I'm not an expert in
the field, merely an enthusiastic reader. The proof is entirely due to
'user21820', who is not me.

That text deals with several different topics and doesn't isolate a
self-contained 'C2' proof, although it can be easily gleaned out of the
text. Let me next sketch this proof briefly.

Assume some standard computation framework, e.g. Turing machines, where a
program P run on input I may halt, and if it halts, produces some output O.
We say that T "can reason about programs" if the following is true (this
definition is key to the proof):

If a program P, when run on input I, halts and produces output O, then:
- T proves "P run on I halts and produces O"
- for any O' != O, T refutes "P run on I halts and produces O' ".

This definition of "can reason about programs" is similar to, but different
from, strong representation. If it's known in the literature and has a
name/reference, please let me know.

I believe the usual candidates for Godel's First theorem, e.g. Robinson's
Q, indeed "can reason about programs" in this sense. Proving "P run on I
halts and produces O" is easy via exhibiting a trace M which includes all
the computation steps. Refuting "P run on I halts and produces O' " is
possible because if the "true" trace M contains N steps, then any candidate
trace M' which ends in a halt state can be shown in T to coincide with M on
each of the first N steps one-by-one due to the deterministic behavior of
P, and so T can prove that any possible trace starting with I must end with
O.

Now assume T "can reason about programs" and is consistent. Let a program
P, given input I, look through all proofs in T lexicographically, searching
for a proof or a refutation of the sentence "I, when run on I as input,
halts and outputs 1". If P finds a proof, it halts and outputs 0, and if it
finds a refutation, it halts and outputs 1.
We claim that W="P run on P halts and outputs 1" is a sentence that
exhibits the incompleteness of T. When we run P on input P, it searches for
a proof or a refutation of W in T. If P halts and outputs 1, T must be able
to prove W because it "can reason about programs", but P also found a
refutation of W, contradicting the consistency of T. If P halts and outputs
0, T must be able to refute W because of the second clause in "can reason
about programs", but P also found a proof of W, again the same
contradiction. Therefore P never halts when run on P, meaning neither a
proof nor a refutation of W exist in T.

Note that we never relied on T being sound, and that W can be in principle
explicitly constructed from the axioms of T, which appear in the part of
the program P that verifies whether an arbitrary string is a proof in T.

As mentioned above, I'd appreciate any references to this proof, as well as
to the notion "can reason about programs", in existing
textbooks/literature, any further clarification that places it in some
proper context, etc.

Thanks,
Anatoly Vorobey.
-- 
Anatoly Vorobey, avorobey at gmail.com
http://avva.livejournal.com (Russian)
http://www.lovestwell.org (English)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210919/472c6fc2/attachment-0001.html>