[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


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:

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:

Voevodsky talked about these finite sets in his lecture at Oxford:

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