[FOM] Are the proofs of con(PA) circular?
Richard Heck
rgheck at brown.edu
Wed May 18 21:36:17 EDT 2011
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
More information about the FOM
mailing list