Chcę budować notacje dla dużych policzalnych porządków w „naturalny sposób”. Przez „naturalny sposób” rozumiem, że biorąc pod uwagę typ danych indukcyjnych X, równość ta powinna być zwykłą rekurencyjną równością (ta sama, deriving Eqktórą wytworzyłby Haskell), a kolejność powinna być zwykłym rekurencyjnym porządkiem leksykograficznym (tym samym, co deriving Ordw Haskell dałby ), i istnieje rozstrzygalny predykat, który określa, czy element X jest prawidłową notacją porządkową, czy nie.
Na przykład liczby porządkowe mniejsze niż ε 0 mogą być reprezentowane przez dziedzicznie posortowane listy posortowane i spełniają te wymagania. Zdefiniuj X na μα. μβ. 1 + α × β, czyli dziedzicznie skończone listy. Zdefiniuj, isValidaby sprawdzić, czy X jest posortowane, a wszyscy członkowie X są isValid. Prawidłowymi elementami X są wszystkie rzędne mniejsze niż ε 0 w zwykłym porządku leksykograficznym.
Przypuszczam, że μα 0. … μα n . 1 + α 0 ×… × α n można użyć do zdefiniowania rzędnych mniejszych niż φ n + 1 (0), gdzie φ jest funkcją Veblena, w podobny sposób.
Jak widać zabrakło mi kwantyfikatorów μ w φ ω (0). Czy mogę budować większe notacje porządkowe spełniające moje wymagania? Miałem nadzieję, że dojdę do far 0 . Czy mogę uzyskać większe porządki, jeśli porzucę wymóg rozstrzygalności w predykacie ważności?
comparew coq.inria.fr/pylons/contribs/files/Cantor/v8.3/... W tym samym pliku znajduje się lemat, nf_introktóry może charakteryzować ważność.
Inductive lt : T2 -> T2 -> Propnie wygląda dla mnie na porządek leksykograficzny.