[FOM] proof assistants and foundations of mathematics
Timothy Y. Chow
tchow at math.princeton.edu
Wed Aug 15 00:03:44 EDT 2018
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
More information about the FOM
mailing list