Goedel's first incompleteness theorem, the omega rule, and Tennant's reflection rule

246 Views Asked by At

Typical discussions of Goedel's first incompleteness theorem note that PA can prove of each integer that it doesn't number the proof of the Goedel sentence $G$. They then note that using an omega rule to infer from the infinite conjunction of all of them would get you $G$ but this fails to yield a finitary proof. Neil Tennant has suggested that a reflection rule or axiom for primitive recursive functions/relations, such as the proof predicate, would legitimately get us to $G$. Apparently, he believes that PA can prove

for all integers $x$, $x$ is not the number of a proof of $G$

and then uses a reflection rule such as

if no integer numbers the proof of $G$, then $G$

to get (via modus ponens) $G$.

I find this appealing. What I don't get is how Tennant/one gets to the universal generalization about all integers. Is this simply good old mathematical induction? Obviously you get the base case. But how does one get from it holds for arbitrary integer $n$ to holding for $n+1$? Tennant must know he's doing but I sure don't. Someone explain or point me to a gentle explanation? Thanks in advance.

1

There are 1 best solutions below

5
On

No, it isn't "good old mathematical induction" that is supposed to get the arithmetical reasoner to accept a $\Pi_1$ reflection principle, so much as philosophical reflection(!) on the practice he is immersed in.

I have a shot at explaining what this is supposed to mean in §36.5 of (the second edition of) my Introduction to Gödel's Theorems. Here is a PDF of the relevant three pages. My discussion doesn't directly quote from Neil Tennant (or from Jeff Ketland, whose view appears in the para "You might protest..."). I didn't want to get into distracting exposition. But my discussion was intended to give the flavour of something close to Tennant's position, and as I recall he agreed with it.

(By the way, PA$\Pi$ is PA plus the $\Pi_1$ reflection principle which is easily shown to prove Con(PA) and hence the canonical Gödel sentence for PA.)