[Coq-Club] Gentzen proof and Kantor ordering

[Vladimir Voevodsky]

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.

[roux cody]

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

Post by Vladimir Voevodsky
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.

[Neelakantan Krishnaswami]

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

Post by roux cody
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.
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
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.

[Freek Wiedijk]

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

[Bas Spitters]

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

Post by Neelakantan Krishnaswami
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

Post by roux cody
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.
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
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.

[Eddy Westbrook]

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:

http://www.cse.chalmers.se/~coquand/ordinal.ps

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

Post by Neelakantan Krishnaswami
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

Post by roux cody
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.
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
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.

[Martin Escardo]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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?

In a weak fragment of dependent type theory, it is possible to define
epslon0 and higher.

Here I did it in Agda, with comments explaining what is (not) needed:

http://www.cs.bham.ac.uk/~mhe/papers/ordinals/ordinals.html

Martin

[Frédéric Blanqui]

Hello. Some developments about ordinals in Coq have been done by Pierre
Castéran. See his web page http://www.labri.fr/perso/ :


Ordinal notations and rpo
<http://www.labri.fr/%7Ecasteran/Cantor/Kantor.tar.gz>: A contribution
for Coq (8.1) <http://coq.inria.fr>, (joint work with Evelyne Contï¿œjean
<http://www.lri.fr/%7Econtejea> and Florian Hatat). This development
(work in progress !) includes:

* Proof of termination of the rpo with status
* Some results about Hilbert's epsilon operator
* An extension of the Ensembles library : denumerable sets
* Ordinal notations based on Cantor and Veblen normal forms
* Axiomatic definition of countable ordinals (after K. Schï¿œtte)


This development is about termination proofs and ordinal numbers.

It will also serve as a corpus for studying the relationship between Coq
and the mathematical language.

This work is still unfinished, and we hope it will remain so, as the
doamin is very rich.


Table of modules :



prelude/

Some preliminary definitions and results (Pierre Castï¿œran,
Evelyne Contï¿œjean)


hilbert/
Introducing in Coq Hilbert's epsilon operator (Pierre Castï¿œran)


denumerable/
Denumerable sets (Florian Hatat)


rpo/
About the recursive path ordering (Evelyne Contï¿œjean)



epsilon0/
Ordinals in Cantor Normal Form (Pierre Castï¿œran)


gamma0/
Ordinals in Veblen Normal Form (Pierre Castï¿œran)


schutte/
Axiomatic presentation of denumerable ordinals, after K. Schï¿œtte
(Pierre Castï¿œran)


misc/
Computing the length of the Goodstein sequence starting from 4 (in base 2)
(Pierre Castï¿œran)


SCHROEDER/
Slight modification of the contribution by Hugo Herbelin (Florian Hatat)

Post by Vladimir Voevodsky
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.

[Thomas Streicher]

Post by Vladimir Voevodsky
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?

Already intuitionisti second order arithmetic does the job and thus so
does Coq.
Pure MLTT without universes wan't do it unless you have sufficient W-types.
But such a pure MLTT cannot even prove not(0 = suc(x)). However,
adding a constant for that is possible and we'd arrive at a system of
the strength of HA whih can't recognize indutivity of epsilon_0.

thomas