[FOM] proof assistants and foundations of mathematics
Timothy Y. Chow
tchow at math.princeton.edu
Sat Aug 18 16:11:58 EDT 2018
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
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?
More information about the FOM