[FOM] proof assistants and foundations of mathematics
Mario Carneiro
di.gama at gmail.com
Wed Aug 15 12:24:33 EDT 2018
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>
More information about the FOM
mailing list