[FOM] proof assistants and foundations of mathematics

[Timothy Y. Chow]

Jose Manuel Rodriguez Caballero wrote:

> Rather than worried about the consistency of CIC (calculus of inductive 
> constructions), I'm worried about the fact that I do not understand why 
> Voevodsky said that CIC was no cleanly defined from the point of view of 
> the foundations of mathematics.

I listened to part of this talk, which may be found here:

https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/VTS_01_1.mp4
https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/VTS_01_2.mp4

The remark that Jose alludes to occurs at the end of the first video clip 
and the beginning of the second video clip.

Voevodsky was pointing out that CIC has an infinite list of operations and 
axioms, which he regards as not "clean" since he prefers a finite list. 
As far as I can tell, this was a taste judgement, and he was not 
suggesting that CIC might be inconsistent, or that proofs based on CIC 
might be unreliable.

Tim