[FOM] I\Sigma_1 + Con(I\Sigma_1)
Jeremy Avigad
avigad at cmu.edu
Sun Aug 25 15:38:07 EDT 2013
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
More information about the FOM
mailing list