Saya mencari untuk membangun notasi untuk tata cara yang dapat dihitung besar dengan "cara alami". Dengan "cara alami" yang saya maksudkan bahwa dengan memberikan data induktif tipe X, bahwa kesetaraan harus menjadi persamaan rekursif biasa (sama dengan yang deriving Eqdi Haskell akan hasilkan) dan urutannya haruslah urutan leksikografis rekursif biasa (sama dengan yang deriving Orddi Haskell akan menghasilkan ), dan ada predikat yang dapat ditentukan yang menentukan apakah anggota X adalah notasi ordinal yang valid atau tidak.
Misalnya, tata cara yang kurang dari ε 0 dapat diwakili oleh daftar yang diurutkan secara turun temurun dan memenuhi persyaratan ini. Tentukan X menjadi μα. μβ. 1 + α × β, alias daftar terbatas herediter. Tentukan isValiduntuk memeriksa bahwa X diurutkan dan semua anggota X adalah isValid. Anggota X yang valid semuanya adalah ordinal yang kurang dari ε 0 di bawah urutan leksikografis yang biasa.
Saya menduga bahwa μα 0. … Μα n . 1 + α 0 × ... × α n dapat digunakan untuk mendefinisikan ordinals kurang dari φ n + 1 (0), di mana φ adalah fungsi Veblen, dengan cara yang sama.
Seperti yang Anda lihat saya kehabisan μ bilangan di φ ω (0). Bisakah saya membuat notasi ordinal yang lebih besar untuk memenuhi persyaratan saya? Saya berharap untuk mencapai Γ 0 . Bisakah saya mendapatkan ordinal yang lebih besar jika saya membatalkan persyaratan decidability berdasarkan predikat validitas saya?
sumber
comparedi coq.inria.fr/pylons/contribs/files/Cantor/v8.3/… Dalam file yang sama, ada Lemmanf_introyang mungkin mencirikan validitas.Inductive lt : T2 -> T2 -> Proptidak tampak seperti pemesanan leksikografis kepada saya.Jawaban:
Hermann Ruge Jervel memiliki sistem yang bagus yang berjalan jauh ke ordinal Bachmann-Howard berdasarkan pohon berlabel. Lihat: http://folk.uio.no/herman/logsem.pdf
Saya juga suka bukunya tentang teori bukti, yang membahas sistem ini: http://folk.uio.no/herman/bevisteori.ps
sumber