[FOM] 'Salvaging' Voevodsky's talk

[Timothy Y. Chow]

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 
"silly."

> 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.

Tim