Bisakah kita membuktikan normalisasi yang lemah untuk Sistem F dengan induksi secara ordinal yang tidak terbatas

16

Normalisasi yang lemah untuk kalkulus lambda yang diketik sederhana dapat dibuktikan (Turing) dengan induksi pada . Kalkulus lambda diperpanjang dengan rekursi pada bilangan asli (Gentzen) memiliki strategi normalisasi yang lemah dengan induksi pada . $\omega^2$ $\epsilon_0$

Bagaimana dengan Sistem F (atau lebih lemah)? Apakah ada bukti normalisasi yang lemah dalam gaya ini? Jika tidak, dapatkah itu dilakukan?

lo.logic type-theory lambda-calculus proof-theory normalization Kaveh
sumber

1

Ini mungkin berguna untuk berkomentar bahwa setiap konsisten (dihitung) teori dengan ekspresi yang cukup memiliki "bukti"-teori ordinal lebih rendah dari

didefinisikan sebagai ordinal dihitung terkecil yang tidak provably beralasan dalam teori yang diberikan. Kuncinya adalah menggambarkan ordinal itu dengan cara "alami".

ω_{C K}

$\omega_{\mathrm{CK}}$

cody

10

Survei paling komprehensif tentang hubungan antara teori bukti konstruktif (yang terkait erat dengan teori ordinals konstruktif) dan aritmatika impredikatif orde kedua (yang ditunjukkan oleh Ulrik setara dalam kekuatannya dengan Sistem F) adalah Girard (1989). Di sana ia membangun teorinya tentang dilator (1981), yang sebenarnya tidak saya ikuti, tetapi saya pikir pada dasarnya memberikan teori nonkonstruksi Skolemisation tingkat tinggi.

Pemahaman saya adalah bahwa Anda tidak bisa mengungkapkan formula konstruktif dalam arti Uskup-Martin-Lof, karena mereka impredicative dengan cara Anda tidak dapat menghilangkan dengan menambahkan apapun skema induksi orde pertama. $\Sigma^1_2$

Saya ingat menyarankan kepada ahli teori ordinal bahwa seseorang dapat dengan mudah menetapkan bahwa Anda dapat mendasari konstruktivisme impredikatif dalam teori tipe yang didasarkan pada kalkulus lambda polimorfik, dan menggunakan teknik kandidat reduksi dari bukti SN Girard untuk Sistem F untuk memaksakan urutan total yang masuk akal pada alam semesta konstruksi, menyebut kelas-kelas kesetaraan yang Anda dapatkan dari ini tata cara; dia mengatakan sesuatu yang cerdas yang saya anggap sebagai Anda mungkin berhasil, tetapi itu akan memiliki semua keuntungan pencurian daripada kerja keras yang jujur. Untuk membuatnya bekerja, itu tidak cukup baik bahwa Anda dapat membuktikan dalam teori himpunan keberadaan ordinansi semacam itu, Anda akan membutuhkan bukti konstruktif dari trikotomi untuk pesanan.

Singkatnya, dengan gagasan konstruksi intuitionistic yang teratur karena Uskup — Martin-Löf, literatur yang saya tahu dengan kuat menyarankan tidak. Jika Anda enggan bekerja keras jujur dan akan merangkul konstruktivisme impredikatif, maka dugaan saya adalah bahwa itu mungkin bisa dilakukan. Anda tentu saja memerlukan teori yang lebih kuat bahwa Sistem F untuk secara konstruktif membuktikan trikotomi yang diperlukan, tetapi Kalkulus Konstruksi Induktif memberikan kandidat yang jelas.

Referensi

$\Pi^1_2$
Girard (1989) Teori Bukti dan Kompleksitas Logis, vol. I , Napoli: Bibliopolis. Tidak ada volume II.

Charles Stewart
sumber

13

$\Pi^0_2$ $\omega^2$

$\varepsilon_0$ $\Gamma_0$

Mudah-mudahan suatu hari seseorang akan datang dengan notasi ordinal untuk aritmatika orde kedua yang semua orang akan setuju adalah alami, dan kemudian yang dapat digunakan dengan cara jujur untuk membuktikan normalisasi yang lemah untuk Sistem F.

Ulrik Buchholtz
sumber

11

$\mathbb{N} \to \mathbb{N}$

Lebih jauh, saya pikir aritmatika orde kedua cukup kuat dan belum ada batas atas konstruktif yang dikenal dengan "teoritik pembuktian teoretisnya" ( Seni analisis ordinal, bagian 3 ).

Saya pikir ikatan ordinal konstruktif inilah yang diperlukan untuk melakukan induksi yang Anda minta.

jbapple
sumber

Bisakah kita membuktikan normalisasi yang lemah untuk Sistem F dengan induksi secara ordinal yang tidak terbatas

Jawaban:

Referensi