Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Bas Spitters <b.a.w.spitters AT gmail.com>
  • To: Coq Club <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 17:29:11 +0100

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



Archive powered by MHonArc 2.6.18.

Top of Page