[FOM] Provability in PA

[Richard Heck]

Charles Parsons wrote:
> At 11:11 AM -0400 8/17/06, Studtmann, Paul wrote:
>   
>> Let I-Sigma-n be Peano Arithmetic (PA) with the induction schema restricted
>> to Sigma-n formulas.  Can anyone tell me whether the following is true or
>> false:
>>
>> (*) There is some n such that for all Sigma-2 sentences, s, if PA |- s, then
>> I-sigma-n |- s.
>>
>> I am in fact interested in the general case but (*) is easier to state and
>> read.
>>
>> If it is known that (*) is true or that it is false, I would like to know
>> whether it can be proven to be true, if true, or false, if false, within PA.
>> And of course I would be interested to know where I can find the proofs.
>>     
> For each n we can thus exhibit a sigma-2 (in fact pi-1) sentence that 
> is provable in PA and prove in PA that it is not provable in 
> I-sigma-n. But the generalization can't be provable in PA, because it 
> would imply that for every n there is a sentence not provable in 
> I-sigma-n, thus that the latter is consistent for every n. But that 
> implies the consistency of PA.
>   
To elaborate Charles's remark just slightly, for each n, PA proves
Con(I\Sigma_n), which is of course \Pi_1. PA also proves that each
I\Sigma_n is subject to the second incompleteness theorem: PA proves
that, for each n, if I\Sigma_n proves Con(I\Sigma_n), then I\Sigma_n is
inconsistent. Hence, for each n, PA proves that I\Sigma_n does not prove
Con(I\Sigma_n), so, for each n, PA proves: Con(I\Sigma_n), and PA proves
Con(I\Sigma_n), but I\Sigma_n does not prove Con(I\Sigma_n).

So, for each n, PA proves: There exists a \Pi_1 sentence S such that PA
proves S and I\Sigma_n does not proves S. (As Charles said, PA cannot
prove the generalization, only each instance.)

This could be strengthened a bit, since Con(I\Sigma_n) is provable in, I
believe, I\Sigma_{n+2}. Is that right? My copy of Hajek and Pudlak is at
the office....

Richard Heck

-- 
==================================================================
Richard G Heck, Jr
Professor of Philosophy
Brown University
http://bobjweil.com/heck/
==================================================================
Get my public key from http://sks.keyserver.penguin.de
Hash: 0x1DE91F1E66FFBDEC
Learn how to sign your email using Thunderbird and GnuPG at:
http://dudu.dyn.2-h.org/nist/gpg-enigmail-howto