[FOM] proof assistants and foundations of mathematics

[Mario Carneiro]

On Wed, Aug 15, 2018 at 12:07 PM Timothy Y. Chow <tchow at math.princeton.edu>
wrote:

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

Note also that this relates primarily to the way induction is presented in
CIC, via a scheme rather than a finite collection of inductive types. If
you are only concerned with logical systems up to biinterpretability, then
CIC is finitely axiomatizable, so this is at best a concern with CIC as
traditionally construed and implemented in proof assistants, rather than
CIC the logical system.

 Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180815/2327bad6/attachment.html>