coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Eddy Westbrook <westbrook AT kestrel.edu>
- To: "coq-club AT inria.fr" <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 09:04:53 -0800
I would also recommend that you take a look at Coquand, Hancock, and Setzer, "Ordinals in Type Theory". I think this link works, but I can't check it on my phone:
They show how to define ordinals way beyond epsilon 0, and they do it with what would be an inductive type in Coq, so you get well-founded (in the inductive sense) for free.
-Eddy
Sent from my iPhone
Hello,
Paul Taylor has written about how to formulate ordinals in constructive
set theory in his paper "Intuitionistic Sets and Ordinals" [1].
The fixed point theorem Taylor mentions in the introduction to this
paper can be proved by the elegant argument of Pataraia (which Pataraia
himself never published, but Martin Escardo reproduced the proof in his
paper "Joins in the frame of nuclei" [2]).
Best,
Neel
[1] http://www.monad.me.uk/~pt/ordinals/intso.pdf
[2] http://www.cs.bham.ac.uk/~mhe/papers/hmj.pdf
On 29/01/15 14:59, roux cody wrote:Dear Vladimir,Coq is more than powerful enough to prove well ordering of epsilon zero,*for a constructive notion of well ordering*. This is usually defined by*accessibility*: if some property about ordinals is closed by successorand limits, then it holds for all ordinals.Sadly, this is not constructively equivalent to the fact that any subsetof ordinals has a least element.The n-lab seems to sum the situation up quite nicely:http://ncatlab.org/nlab/show/well-founded+relationWithout references I'm afraid.Note that the constructive formulation of well-foundedness is sufficientfor most applications! What application did you have in mind?Best,CodyOn Thu, Jan 29, 2015 at 7:46 AM, Vladimir Voevodsky <vladimir AT ias.edu<mailto:vladimir AT ias.edu>> wrote:If I recall correctly the ordinal numbers smaller than epsilon zerocan be represented by finite rooted trees (non planar). It is thennot difficult to describe constructively the ordinal partialordering on them. Gentzen theorem says that if this partial orderingis well-founded then Peano arithmetic is consistent.What can we prove about this ordering in Coq?Can it be shown that any decidable subset in the set of trees thatis inhabited has a smallest element relative to this ordering?If not then can the system of Coq me extended *constructively* (i.e.preserving canonicity) so that in the extended system such smallestelements can be found?Vladimir.
- [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] Gentzen proof and Kantor ordering, Neelakantan Krishnaswami, 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
- Re: [Coq-Club] Gentzen proof and Kantor ordering, roux cody, 01/29/2015
Archive powered by MHonArc 2.6.18.