[FOM] proof assistants and foundations of mathematics

[José Manuel Rodriguez Caballero]

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