[FOM] Are the proofs of con(PA) circular?

[Martin Davis]

Some of this on-going discussion has in effect 
suggested that what Gentzen did amounts a proof 
of con(PA) from PA +  epsilon-0 induction.  That 
would be circular. But the proof can be carried 
out in PRA+ epsilon-0 induction.

Discussion of Gödel's beliefs should take note of 
the fact that he himself offered another proof of 
con(PA) via the equivalent con(HA) - his "Dialecta" interpretation.

Martin


Martin Davis
Professor Emeritus, Courant-NYU
Visiting Scholar, UC Berkeley
eipye + 1 = 0