The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Here's how that looks with HIITs:
http://homotopytypetheory.org/2014/02/22/surreals-plump-ordinals/

On Thu, Jan 29, 2015 at 4:10 PM, Neelakantan Krishnaswami
<n.krishnaswami AT cs.bham.ac.uk>
 wrote:
> 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 successor
>> and limits, then it holds for all ordinals.
>>
>> Sadly, this is not constructively equivalent to the fact that any subset
>> of ordinals has a least element.
>>
>> The n-lab seems to sum the situation up quite nicely:
>>
>> http://ncatlab.org/nlab/show/well-founded+relation
>>
>> Without references I'm afraid.
>>
>> Note that the constructive formulation of well-foundedness is sufficient
>> for most applications! What application did you have in mind?
>>
>> Best,
>>
>> Cody
>>
>> On 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 zero
>>     can be represented by finite rooted trees (non planar). It is then
>>     not difficult to describe constructively the ordinal partial
>>     ordering on them. Gentzen theorem says that if this partial ordering
>>     is 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 that
>>     is 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 smallest
>>     elements can be found?
>>
>>     Vladimir.
>>
>>
>>
>