Je cherche à construire des notations pour les grands ordinaux dénombrables d'une «manière naturelle». Par "voie naturelle", je veux dire que, étant donné un type de données inductif X, cette égalité devrait être l'égalité récursive habituelle (la même que celle deriving Eqde Haskell produirait) et l'ordre devrait être l'ordre lexicographique récursif habituel (la même que celle deriving Ordde Haskell produirait ), et il existe un prédicat décidable qui détermine si un membre de X est une notation ordinale valide ou non.
Par exemple, des ordinaux inférieurs à ε 0 peuvent être représentés par des listes triées héréditairement finies et satisfont à ces exigences. Définissez X comme μα. μβ. 1 + α × β, alias listes héréditairement finies. Définissez isValidpour vérifier que X est trié et que tous les membres de X le sont isValid. Les membres valides de X sont tous des ordinaux inférieurs à ε 0 dans l'ordre lexicographique habituel.
Je suppose que μα 0. … Μα n . 1 + α 0 ×… × α n peut être utilisé pour définir des ordinaux inférieurs à φ n + 1 (0), où φ est la fonction Veblen, d'une manière similaire.
Comme vous pouvez le voir, je manque de quantificateurs μ à φ ω (0). Puis-je créer des notations ordinales plus grandes répondant à mes exigences? J'espérais aller jusqu'à Γ 0 . Puis-je obtenir des ordinaux plus gros si je laisse tomber mon exigence de décidabilité sur mon prédicat de validité?
la source
compareen coq.inria.fr/pylons/contribs/files/Cantor/v8.3/… Dans ce même fichier, il y a un lemmenf_introqui pourrait caractériser la validité.Inductive lt : T2 -> T2 -> Propne ressemble pas à un ordre lexicographique pour moi.Réponses:
Hermann Ruge Jervel a un joli système qui va jusqu'à l'ordinal de Bachmann-Howard basé sur des arbres étiquetés. Voir: http://folk.uio.no/herman/logsem.pdf
J'aime aussi son livre sur la théorie de la preuve, qui traite de ce système: http://folk.uio.no/herman/bevisteori.ps
la source