coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Gentzen proof and Kantor ordering

From: Freek Wiedijk <freek AT cs.ru.nl>
To: coq-club AT inria.fr
Cc: Types list <types-list AT lists.seas.upenn.edu>
Subject: Re: [Coq-Club] Gentzen proof and Kantor ordering
Date: Thu, 29 Jan 2015 16:17:33 +0100

Hello,

The ordinals up to epsilon zero are one of the fundamental
notions in the ACL2 system. See for instance:

<http://www.ccs.neu.edu/home/pete/pub/acl2-ordinal-arithmetic-acl2.pdf>

Note that in the ACL2 representation of ordinals there is
no limit constructor, it's all about powers of omega (the
"finite rooted trees" that Vladimir was talking about).

Freek

[Coq-Club] Gentzen proof and Kantor ordering, Vladimir Voevodsky, 01/29/2015
- Re: [Coq-Club] Gentzen proof and Kantor ordering, roux cody, 01/29/2015
  - Re: [Coq-Club] Gentzen proof and Kantor ordering, Neelakantan Krishnaswami, 01/29/2015
    - Re: [Coq-Club] Gentzen proof and Kantor ordering, Freek Wiedijk, 01/29/2015
    - Re: [Coq-Club] Gentzen proof and Kantor ordering, Bas Spitters, 01/29/2015
    - Re: [Coq-Club] Gentzen proof and Kantor ordering, Eddy Westbrook, 01/29/2015
- Re: [Coq-Club] [TYPES] Gentzen proof and Kantor ordering, Martin Escardo, 01/29/2015
- Re: [Coq-Club] Gentzen proof and Kantor ordering, Frédéric Blanqui, 01/30/2015