[FOM] proof assistants and foundations of mathematics
José Manuel Rodriguez Caballero
josephcmac at gmail.com
Wed Aug 15 21:53:37 EDT 2018
>
> MK wrote:
> I detect two rather distinct concerns in Jose's comments:
> (1) What did Voevodsky mean when he criticized CIC as allegedly inadequate
> as
> far as foundations are concerned because CIC assumes the integers whereas
> apparently it shouldn't in Voevodsky's scheme of things;
Yes, this was my main concern after watching these two Voevodsky's
consecutive lectures. I recall that in Voevodsky's controversial lecture
about Peano arithmetic
https://video.ias.edu/voevodsky-80th
he mentioned the possibility of an infinite strictly decreasing sequence of
ordinals in order to violate Gentzen's consistency proof. Of course, such a
sequence do not exists neither in ZFC nor in CIC. I guess that Voevodsky
was thinking about hyperfinite sets:
https://en.wikipedia.org/wiki/Hyperfinite_set
CIC just assumes the standard model of natural numbers and non-standard
natural numbers are out. Maybe to use non-standard natural numbers was the
motivation of Voevodsky to reject CIC. Indeed, when I was learning UniMath
I was surprised to find the terminology standard finite sets:
https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/StandardFiniteSets.v
Voevodsky talked about these finite sets in his lecture at Oxford:
https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/141126-2.mp4
Kind Regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180815/d2a52860/attachment.html>
More information about the FOM
mailing list