Индуктивные типы для больших исчисляемых порядковых обозначений.

28

Я пытаюсь построить нотацию для больших счетных ординалов "естественным образом". Под «естественным путем» я подразумеваю, что при индуктивном типе данных X это равенство должно быть обычным рекурсивным равенством (таким же, как deriving Eqв Haskell), а порядок должен быть обычным рекурсивным лексикографическим порядком (таким же, как deriving Ordв Haskell; ), и существует разрешимый предикат, который определяет, является ли член X действительным порядковым обозначением или нет.

Например, порядковые номера, меньшие ε 0, могут быть представлены наследственно конечными отсортированными списками и удовлетворяют этим требованиям. Определите X как µα. μβ. 1 + α × β, то есть наследственно конечные списки. Определите, isValidчтобы проверить, что X отсортирован и все члены X являются isValid. Действительными членами X являются все порядковые числа меньше ε 0 в обычном лексикографическом порядке.

Я предполагаю, что μα 0. … Μα n . 1 + α 0 ×… × α n может использоваться для определения ординалов, меньших φ n + 1 (0), где φ - функция Веблена, аналогичным образом.

Как видите, я исчерпал µ квантификаторов при φ ω (0). Могу ли я построить более крупные порядковые обозначения, удовлетворяющие моим требованиям? Я надеялся добраться до 0 . Могу ли я получить ординалы большего размера, если откажусь от требования разрешимости для моего предиката достоверности?

Рассел О'Коннор
источник
1
Вы видели Кантора в списках Coq? coq.inria.fr/pylons/pylons/contribs/view/Cantor/v8.3 Мне кажется интуитивно понятным, что нормальная форма Веблена является "естественной" в том смысле, в котором вы указываете. Разве это не так?
Jbapple
Что говорит теория, как далеко вы можете пойти, имея решительное равенство? В какой-то момент вы должны отказаться от решимости и быть удовлетворенным полуразрешимостью.
Андрей Бауэр
Тип, который кодирует форму Веблена, имеет разрешимое упорядочение, но я не уверен, что допустимость допустима. порядок находится compareв coq.inria.fr/pylons/contribs/files/Cantor/v8.3/… В этом же файле есть лемма, nf_introкоторая может характеризовать действительность.
JBapple
@jbapple: это очень похоже на ответ, возможно, вам следует опубликовать его как ответ.
Андрей Бауэр
@jbapple Inductive lt : T2 -> T2 -> Propне похож на лексикографический порядок для меня.
Рассел О'Коннор

Ответы:

4

У Германа Руге Джервела есть хорошая система, которая идет вплоть до ординала Бахмана-Ховарда, основанного на помеченных деревьях. Смотрите: http://folk.uio.no/herman/logsem.pdf

Мне также нравится его книга по теории доказательств, в которой обсуждается эта система: http://folk.uio.no/herman/bevisteori.ps

solrize
источник
Я не думаю, что это «естественно», как указано в вопросе - см.
Слайды
Ссылка больше не работает
Łukasz Lew