[FOM] proof assistants and foundations of mathematics

[Timothy Y. Chow]

Jose M wrote:

> Also, Voevodsky evidently studied such a proof before his lecture, I 
> quote him:

Yes, if you read the paper I linked to, you'll see that I discussed this 
remark of Voevodsky in some detail.  As others have pointed out, there has 
been much discussion of what Voevodsky meant, and it is very hard, even on 
a very charitable reading, to turn it into a coherent objection.

One way to interpret his appeal to Goedel's theorem is as a blanket 
objection to all consistency proofs.  But if we do that, then the 
criticism applies equally to Voevodsky's own proposed foundations.  Later 
in the lecture he talks about "reliable" proofs, but it is completely 
unclear what he means by this; in particular, his own arguments can be 
turned against him to "prove" that Goedel's theorem shows that his 
so-called "reliable" arguments cannot be shown to be reliable.

There is no doubt that Voevodsky was a great mathematician.  That does not 
mean that we should stand in awe of him and assume that what he says is 
always correct.  His arguments should be evaluated on their merits, not on 
his reputation, which is what you seem to be doing.

> my modest case, I take the infinitely large strictly decreasing sequence 
> of ordinals as a property of ZFC or CIC, but not as something factually 
> true.

What does "factually true" mean?  Is it "factually true" that the square 
root of 2 is irrational?  What about Fermat's Last Theorem?  If so, why 
are these factually true while other proven theorems are not?

Tim