[FOM] 'Salvaging' Voevodsky's talk
Timothy Y. Chow
tchow at alum.mit.edu
Thu Jun 9 18:42:17 EDT 2011
Martin Davis wrote:
> What I have been trying to say over and over again is that Voevodsky has
> implied that his foundational views could provide a way out should PA be
> found to be inconsistent. And that this is silly given the now admitted
> fact that his systems prove con(PA).
A point of clarification. Voevodsky did not claim in his talk that any of
"his systems"---in the sense of any specific system that he had already
proposed and studied---would be a satisfactory "way out" should PA be
found to be inconsistent. Rather, he made a vague appeal to constructive
type theory and as-yet-unspecified procedures to isolate "reliable" proofs
that would be immune to an inconsistency in PA. Though this seems very
speculative and vague at this stage, it's not clear to me that it's
> He also suggested that serious efforts to prove the inconsistency of PA
> are worthwhile.
This part I agree is a fair representation of what Voevodsky said.
More information about the FOM