[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I don't know exactly if this can be useful but Pierre Castéran (with parts also done by Évelyne Contejean) formalized ordinals and proved the termination of hydra's problem usinng them there: http://www.labri.fr/perso/casteran/hydra-ludica/index.html This is work in progress but the proofs for hydra is finished as far as I know. Best regards, Pierre Courtieu 2018-01-10 16:45 GMT+01:00 Paolo Giarrusso <[email protected]>: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Since I (and maybe others) understand structural induction better than > transfinite induction, I now wonder if one can use structural induction to > understand better both specific uses of transfinite induction and > proof-theoretic ordinal analysis. > > Has anybody written, say, an introduction to ordinals for the Coq programmer > or some such thing? Googling found little,* maybe because this seems > pointless to people who do understand ordinals. But maybe such a presentation > would be more accessible to computer scientists used to proof assistants? > > For instance: > > (1) can one define the proof-theoretic strength of an inductive datatype, > such as Richard’s example? > (2) Gentzen’s proof of consistency for PA translates derivations in PA to > infinitary derivations in PA_\omega [1], and then requires transfinite > induction up to \epsilon_0. Could one just use as structural induction on an > inductive type of PA_\omega infinitary derivations? > > (2b) In fact, if I try to encode PA_\omega derivations in Coq (pseudocode) > naively, the result looks similar to Richard’s datatype (though more indexed) > — there’s one premise with an argument per natural: > > Inductive derivation Gamma Delta := > | omegaR : forall F Gamma Delta, (forall n, derivation Gamma (F n : Delta)) > -> derivation Gamma ((Forall x, F x) : Delta) > | omegaL : > forall F Gamma Delta, (forall n, derivation (F n : Gamma) Delta) -> > derivation ((Exists x, F x) : Gamma) Delta > > * Forall x, F x > > *The best answer seems to be Emil Jeřábek at > https://mathoverflow.net/a/61045/36016, saying (IIUC) that ordinals can be > understood as trees, but pointing out those trees are more complex. But some > still prefer structural recursion even when it can be translated to induction > on naturals, so maybe the same applies here. > > [1] I’m following the presentation in > https://www1.maths.leeds.ac.uk/~rathjen/Sepp-chiemsee.pdf. > >> On Wed, 10 Jan 2018 at 11:45, Frédéric Blanqui <[email protected]> >> wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> Hello. >> >> Well, it is if you define the height as a transfinite ordinal. In case >> of an infinitely branching constructor like Mk : (nat -> ty) -> ty, >> height(Mk f) = sup{height(f n) | n in nat} + 1. >> >> Frédéric. >> >> >> Le 09/01/2018 à 17:14, Xavier Leroy a écrit : >> > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >> > ] >> > >> > On 07/01/2018 17:41, Xavier Leroy wrote: >> > >> >> As your example shows, the tree can contain infinitely-branching nodes, >> >> hence the size can be infinite, but all paths are finite, hence the >> >> height is finite. >> > I was confused. All paths in this tree are finite indeed, and that's why >> > it induces a well-founded ordering. But in the presence of >> > infinitely-branching nodes, the height can still be infinite and is not an >> > appropriate justification for structural induction. >> > >> > Sorry for the noise, >> > >> > - Xavier Leroy >>
