Tipos indutivos para grandes notações ordinais contáveis.

28

Estou procurando criar notações para grandes ordinais contáveis ​​de uma "maneira natural". Por "caminho natural", quero dizer que, dado um tipo de dados indutivo X, essa igualdade deve ser a igualdade recursiva usual (a mesma que deriving Eqem Haskell produziria) e a ordem deve ser a ordem lexicográfica recursiva usual (a mesma que deriving Ordem Haskell produziria ) e existe um predicado decidível que determina se um membro de X é uma notação ordinal válida ou não.

Por exemplo, ordinais menores que ε 0 podem ser representados por listas ordenadas hereditariamente finitas e atendem a esses requisitos. Defina X como μα. μβ. 1 + α × β, também conhecidas como listas hereditariamente finitas. Defina isValidpara verificar se X está classificado e todos os membros de X estão isValid. Os membros válidos de X são todos ordinais menores que ε 0, na ordem lexicográfica usual.

Eu conjecturo que μα 0. … Μα n . 1 + α 0 ×… × α n pode ser usado para definir ordinais menores que φ n + 1 (0), onde φ é a função Veblen, de maneira semelhante.

Como você pode ver, os quantificadores μ estão em φ ω (0). Posso criar notações ordinais maiores que atendam aos meus requisitos? Eu esperava chegar até 0 . Posso obter ordinais maiores se eu abandonar meu requisito de decidibilidade no meu predicado de validade?

Russell O'Connor
fonte
1
Você viu o Cantor nos contribs do Coq? coq.inria.fr/pylons/pylons/contribs/view/Cantor/v8.3 Parece-me intuitivo que a forma normal do Veblen seja "natural" da maneira que você especificar. Não é esse o caso?
Jbapple #
O que a teoria diz, até onde você pode chegar com a igualdade decidível? Em algum momento, você precisa renunciar à decidibilidade e se satisfazer com a semidecidibilidade.
Andrej Bauer
O tipo que codifica o formulário Veblen tem pedidos decidíveis, mas não tenho certeza se a validade é decidível. o pedido está compareem coq.inria.fr/pylons/contribs/files/Cantor/v8.3/… Nesse mesmo arquivo, existe um lema nf_introque pode caracterizar a validade.
Jbapple #
@ jbapple: isso parece muito com a resposta, talvez você deva publicá-la como resposta.
Andrej Bauer
@jbapple Inductive lt : T2 -> T2 -> Propnão parece um pedido lexicográfico para mim.
Russell O'Connor

Respostas:

4

O Hermann Ruge Jervel tem um bom sistema que vai até o ordinal de Bachmann-Howard com base em árvores rotuladas. Veja: http://folk.uio.no/herman/logsem.pdf

Também gosto do seu livro sobre a teoria da prova, que discute esse sistema: http://folk.uio.no/herman/bevisteori.ps

solrizar
fonte
Eu não acho que este é "natural" na forma especificada na questão - ver lâminas 7 e 8.
jbapple
O link não funciona mais
Łukasz Lew