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

[Richard Heck]

On 05/18/2011 07:14 PM, Martin Davis wrote:
> 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.
>
The facts of course are the facts, and thanks for reminding us of them. 
But I still have to wonder in what sense a proof of con(PA) in PA + 
epsilon-0 induction is "circular". It's not circular in the 
straightforward sense of assuming its conclusion. Would (per 
impossibile) a proof of Con(PRA) in PRA necessarily have been circular? 
Or isn't it rather precisely one of the things for which Hilbert was 
looking?

> 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.
>
Presumably Gödel thought, then, that we had some other way of knowing 
that HA is consistent?

Richard Heck