[FOM] I\Sigma_1 + Con(I\Sigma_1)

[Jeremy Avigad]

Richard Heck wrote:

> Obviously, I\Sigma_1 + Con(I\Sigma_1) is a sub-theory of I\Sigma_2,
> since I\Sigma_2 proves Con(I\Sigma_1). I am guessing (a) that it is a
> proper sub-theory and (b) that it does not even interpret I\Sigma_2.
> Yes? References?
>
> Does the same hold for I\Sigma_n + Con(I\Sigma_{n+k})?
>
> Thanks in advance,
> Richard Heck
Indeed, adding any true Pi_1 sentence to a theory does not change the 
theory's "provably total computable functions." So I\Sigma_1 + Con(T) 
does not prove I\Sigma_2 for any consistent T, and similarly for 
I\Sigma_n and I\Sigma_{n+k}. I believe this observation is due to Kreisel.

The argument (in the case of I\Sigma_1) goes like this. Suppose phi(x) 
and psi(x,y) are primitive recursive and

   I\Sigma_1 + forall y phi(y)  proves  forall x exists y psi(x,y).

Then

   I\Sigma_1 proves forall x exists y (psi(x, y) or not phi(y)).

By the well-known result due to Parsons, Mints, and Takeuti 
(independently), this implies that there is a primitive recursive 
function that for every x returns a y such that either psi(x, y) or not 
phi(y). But phi(y) is always true, so this is just a y such that psi(x, y).

Now, I\Sigma_2 proves the totality of Ackermann's function. This can be 
written in the form "forall x exists y psi(x, y)", where psi says that y 
is a halting computation sequence for a particular Turing machine that 
computes Ackermann's function on input x. If I\Sigma_1 plus forall y 
phi(y) proved I\Sigma_2, by the argument above there would be a 
primitive recursive function returning such a halting computation 
sequence for each x, contradicting the fact that Ackermann's function is 
not primitive recursive.

As far as interpretability goes, this says that any interpretation 
cannot preserve Pi_2 sentences. But in general, with the assumption 
con(T), you can "arithmetize" the completeness theorem and write down a 
formula describing a model of T, giving rise to an interpretation. This 
works in fairly weak theories of arithmetic. Harvey is an expert here, 
but as I recall these issues are also treated in the book by Hájek and 
Pudlák on the metamathematics of arithmetic.

Best wishes,

Jeremy