Estoy buscando construir anotaciones para ordinales contables grandes de una manera "natural". Por "forma natural" quiero decir que, dado un tipo de datos inductivo X, esa igualdad debería ser la igualdad recursiva habitual (lo mismo que deriving Eqen Haskell produciría) y el orden debería ser el orden lexicográfico recursivo habitual (lo mismo que deriving Orden Haskell produciría ), y hay un predicado decidible que determina si un miembro de X es una notación ordinal válida o no.
Por ejemplo, los ordinales menores que ε 0 pueden representarse mediante listas ordenadas hereditariamente finitas y satisfacen estos requisitos. Definir X para ser μα. μβ. 1 + α × β, también conocido como listas hereditariamente finitas. Defina isValidpara verificar que X esté ordenado y que todos los miembros de X lo estén isValid. Los miembros válidos de X son todos ordinales menores que ε 0 bajo el orden lexicográfico habitual.
Supongo que μα 0. … Μα n . 1 + α 0 ×… × α n se puede utilizar para definir ordinales menores que φ n + 1 (0), donde φ es la función Veblen, de manera similar.
Como puede ver, me quedo sin cuantificadores μ en φ ω (0). ¿Puedo construir anotaciones ordinales más grandes que satisfagan mis requisitos? Esperaba llegar hasta Γ 0 . ¿Puedo obtener ordinales más grandes si elimino mi requisito de capacidad de decisión en mi predicado de validez?
fuente
compareen coq.inria.fr/pylons/contribs/files/Cantor/v8.3/… En ese mismo archivo, hay un Lemanf_introque puede caracterizar la validez.Inductive lt : T2 -> T2 -> Propno me parece un pedido lexicográfico.Respuestas:
Hermann Ruge Jervel tiene un buen sistema que llega hasta el ordinal de Bachmann-Howard basado en árboles etiquetados. Ver: http://folk.uio.no/herman/logsem.pdf
También me gusta su libro sobre la teoría de la prueba, que analiza este sistema: http://folk.uio.no/herman/bevisteori.ps
fuente