Ramifikasi Teori Jenis Impredikatif

Kebanyakan tipe teori yang saya sadari adalah predikatif yang saya maksudkan

Void : Prop
Void = (x : Prop) -> x

tidak diketik dengan baik di sebagian besar pembuktian teorema karena tipe pi ini milik alam semesta yang sama Propdan tidak demikian halnya Prop : Prop. Ini menjadikannya predikatif dan tidak mengizinkan definisi tidak adil seperti di atas. Namun, banyak sekali "bahasa papan tulis" seperti System F atau CoC sebenarnya tidak berguna. Faktanya, impredicativitas ini sangat penting untuk mendefinisikan sebagian besar konstruksi yang tidak dimasukkan secara primitif dalam bahasa.

Pertanyaan saya adalah mengapa seseorang ingin berhenti dari impredicativity mengingat kekuatannya dalam mendefinisikan konstruksi logis? Saya pernah mendengar beberapa orang berkomentar bahwa impredicativity mengacaukan "perhitungan" atau "induksi" tetapi saya mengalami kesulitan menemukan penjelasan konkret.

lo.logic type-theory Daniel Gratzer
sumber

Apakah tipe teori predikatif, atau teorinya?

Andrej Bauer

Saya kira Coq bukan "teorema yang paling membuktikan" bagi Anda, karena ia menerima definisi di atas.

Andrej Bauer

@AndrejBauer Mengapa tidak keduanya? :) Saya kira coq memiliki alam semesta impredikatif dan juga prediksi. Saya kira pertanyaan saya adalah. "Kenapa tidak diatur tidak adil juga?" dalam konteks coq

Daniel Gratzer

Mengapa Type tidak bisa ditiru? > Periksa Jenis. Jenis: Jenis. Yah sialan :)

cody

Tidak perlu mengganggu pengembang! Impredicative Set cukup jahat, dan khususnya, hal itu bertentangan dengan prinsip-prinsip pilihan yang agak alami dan apa yang disebut "informatif dikecualikan tengah" forall P : Type, {P} + {~P}, karena ini + set impredicative menyiratkan bukti tidak relevan (dan natini bukan bukti yang tidak relevan). Lihat misalnya coq.inria.fr/library/Coq.Logic.ClassicalUniqueChoice.html dan coq.inria.fr/library/Coq.Logic.Berardi.html

cody

Jawaban:

Saya akan menguraikan komentar saya menjadi jawaban. Asal usul teori tipe predikatif hampir setua teori tipe itu sendiri, karena salah satu motivasi Russel adalah untuk melarang definisi "melingkar" yang diidentifikasi sebagai bagian dari sumber inkonsistensi dan paradoks abad XIX. Thierry Coquand memberikan ikhtisar tercerahkan di sini . Dalam teori ini, predikat atas "level" atau tipe, termasuk tipe-tipe level "selanjutnya", di mana terdapat jumlah level yang tak terbatas (dapat dihitung).

Sementara hierarki predikatif Russel (tampaknya) cukup untuk menghilangkan paradoks yang diketahui, ternyata sangat sulit untuk digunakan sebagai sistem dasar. Secara khusus, mendefinisikan sesuatu yang sesederhana sistem bilangan real sangat sulit, dan karenanya Russel mendalilkan aksioma, Aksioma Reducibilitas yang mendalilkan bahwa semua level "dikurangi" menjadi satu. Tidak perlu dikatakan, ini bukan perkembangan yang memuaskan.

Namun, bertentangan dengan pernyataan impredikatif "berbahaya" (seperti pemahaman tidak terbatas), aksioma ini tampaknya tidak memperkenalkan inkonsistensi. Formulasi selanjutnya dari teori-teori dasar (teori tipe sederhana , teori himpunan Zermelo ) menerimanya secara besar-besaran, membuat keluarga predikat (mengkuantifikasi kemungkinan seluruh semesta set), predikat pada tingkat yang sama.

Sekitar tahun 1971, Martin-Lof memperkenalkan teori tipe dependen di mana prinsip ini dan aksioma lebih lanjut Type : Typeberlaku. Sistem ini ternyata tidak konsisten karena alasan-alasan halus: paradoks Russel yang naif tidak dapat dimainkan (secara langsung), tetapi pengkodean yang cerdik tetap memungkinkan ditemukannya kontradiksi. Ini mendorong krisis iman yang serupa dengan Russel, menghasilkan teori tipe predikatif dengan alam semesta yang kita kenal dan cintai.

Ada cara untuk memperbaiki teori untuk memungkinkan impredicativitas "tidak bersalah" ala teori Zermelo, menghasilkan teori tipe seperti Calculus of Constructions, tetapi kerusakan telah terjadi, dan "sekolah Swedia" teori tipe cenderung menolak impredicativitas.

Beberapa poin:

Apa hubungannya ini dengan matematika intuitionistic? Jawabannya tidak banyak. Pada pergantian abad ke-XX, matematikawan cenderung mengacaukan penggunaan prinsip sirkular / impredikatif dengan penalaran non-konstruktif (intuisi adalah bahwa penalaran impredikatif tampaknya mengasumsikan alam semesta matematika yang sudah ada sebelumnya , seperti halnya penggunaan tengah yang dikecualikan). Namun, ada teori impredikatif intuitionistic sempurna (seperti IZF ). Orang-orang yang tertarik dengan intuitionism masih cenderung tertarik pada predicativisme karena beberapa alasan (tentu saja saya bersalah).
Apa yang dapat Anda lakukan dalam matematika predikatif? Sebagaimana Martin tunjukkan dalam jawabannya, Hermann Weyl (jangan dikelirukan dengan Andre Weil) memulai program yang mencoba mengeksplorasi kekuatan ekspresif sistem predikatif, dengan mengambil titik awal bahwa sistem predikatif memiliki kekuatan ekspresif antara Aritmatika Peano dan Orde Kedua. Aritmatika , yang cukup banyak disetujui untuk menjadi impredikatif oleh sebagian besar standar (dan dapat dibandingkan dengan Sistem F di sisi teori jenis). Program ini kemudian dijuluki "membalikkan matematika" karena mencoba untuk mengklasifikasikan kekuatan teorema matematika yang dikenal dalam hal aksioma yang diperlukan untuk membuktikannya (kebalikan dari pendekatan yang biasa). Ituhalaman wikipedia memberikan ikhtisar yang baik; program ini cukup berhasil, karena sebagian besar abad XIX matematika dapat dengan mudah ditampung dalam sistem yang sangat lemah. Masih merupakan pertanyaan terbuka apakah program ini dapat meningkatkan hasil yang lebih baru dalam, katakanlah, teori kategori yang lebih tinggi (kecurigaannya adalah bahwa jawabannya adalah "ya, dengan usaha keras").

cody
sumber

Posting Anda yang bagus berisi komentar samping yang sangat menarik: "cukup disetujui untuk menjadi tidak adil oleh sebagian besar standar ". Ini menunjuk pada sesuatu yang halus, yaitu bahwa tidak jelas di mana tepatnya batas antara predikatif dan impredikatif harus ditarik.

Martin Berger

{P A}_{2}

$\mathrm{PA}_2$

Satu dimensi adalah tipe inferensi. Inferensi tipe sistem F misalnya tidak dapat ditentukan, tetapi beberapa fragmen predikatifnya memiliki inferensi tipe (sebagian) yang dapat ditentukan.

Dimensi lain adalah konsistensi sebagai logika. Para pemikir yang terhormat secara historis merasa sedikit mual karena memiliki dasar matematika yang tidak baik. Bagaimanapun, ini adalah bentuk penalaran melingkar. Saya pikir H. Weyl mungkin yang pertama atau, salah satu yang pertama, yang mencoba merekonstruksi sebanyak mungkin matematika dengan cara predikatif ... hanya untuk berada di sisi yang aman. Kita telah belajar bahwa lingkaran-lingkaran impredicativity tidak bermasalah dalam matematika klasik, dalam arti bahwa tidak ada kontradiksi yang pernah diperoleh dari definisi impredikatif 'jinak'. Seiring waktu, kami belajar untuk memercayai mereka. Perhatikan bahwa ini (tidak adanya paradoxa) adalah empirispengamatan! Namun, sebagian besar pengembangan teori pembuktian, dengan konstruksi ordinalnya yang aneh memiliki tujuan akhir yaitu keinginan untuk membangun semua matematika 'dari bawah', yaitu tanpa definisi impredikatif. Program ini belum selesai. Dalam beberapa tahun terakhir, minat pada dasar predikatif matematika telah bergeser dari kekhawatiran tentang paradoxa ke konten perhitungan bukti, yang menarik karena berbagai alasan. Ternyata definisi impredikatif membuat sulit untuk mengekstraksi konten komputasi. Sudut lain dalam kekhawatiran tentang konsistensi berasal dari tradisi Curry-Howard. Teori tipe orisinal Martin-Lof adalah tidak masuk akal ... dan tidak sehat. Menyusul kejutan itu, ia mengusulkan hanya sistem predikatif, tetapi dikombinasikan dengan tipe data induktif untuk mendapatkan kembali banyak kekuatan impredikatif.

Martin Berger
sumber

Agar adil, Russel adalah salah satu yang pertama mencoba . Dia agak mengakui kekalahan (dengan aksioma reducibilitas).

cody

@cody Saya tidak terlalu akrab dengan sejarah upaya ini. Seberapa sukses Weyl (dan S. Feferman) dalam upaya mereka? MLTT / HOTT pasti berhasil, kataku.

Martin Berger

Pada dasarnya, Weyl sangat sukses, yaitu sebagian besar kumpulan analisis dapat diformalkan tanpa menarik matematika orde 2 (impredikatif). Tubuh kerja telah menjadi bagian dari Matematika Terbalik yang secara tepat menghitung seberapa banyak "ketidaktepatan" yang Anda butuhkan.

cody

Tidak benar bahwa teori pembuktian dapat "dengan konstruksi ordinalnya yang aneh" membangun semua matematika tanpa definisi yang tidak benar. Masalahnya adalah bahwa teori pembuktian tidak dilakukan dalam ruang hampa, tetapi dalam suatu sistem formal, yang dengan sendirinya memiliki beberapa bukti teoritik-teoretis bahwa teori pembuktian tidak mampu membuktikan beralasan. Jadi pengejaran ini pasti tidak akan pernah bisa mencapai 'dasar'. Beberapa ahli logika berpikir bahwa Γ [0] adalah ordinal impredikatif pertama, dan jika demikian maka Anda terjebak pada dan tidak dapat secara predikatif membenarkan ATR0. Jika tidak, maka Anda perlu menjustifikasi bahwa Γ [0] adalah predikatif. Bagaimana Anda akan

user21820

@ user21820 Saya tidak mengatakan bahwa semua matematika dapat dibangun tanpa definisi impredikatif, itu pertanyaan terbuka.

Martin Berger

Jenis-jenis teori cenderung ke arah predicativity terutama alasan sosial-teknis.

Pertama, konsep informal impredicativity dapat diformalkan dalam (setidaknya) dua cara berbeda. Pertama, kita mengatakan bahwa teori tipe seperti Sistem F adalah impredikatif karena kuantifikasi tipe dapat berkisar pada semua tipe (termasuk tipe yang dimiliki quantifier). Jadi kita dapat mendefinisikan operator identitas dan komposisi umum:

\begin{array}{lclll} saya d & : & \forall Sebuah . Sebuah \to Sebuah & = & Λ Sebuah . λ x . x \\ c Hai m hal Hai s e & : & \forall Sebuah, b, c . (Sebuah \to b) \to (b \to c) \to (Sebuah \to c) & = & Λ Sebuah, b, c . λ f, g . λ x . g (f x) \end{array}

$\begin{array}{lclll} \mathit{id} & : & \forall a.\; a \to a & = & \Lambda a.\;\lambda x.\;x\\ \mathit{compose} & : & \forall a, b, c.\; (a \to b) \to (b \to c) \to (a \to c) & = & \Lambda a,b,c.\lambda f, g. \lambda x. g(f\;x) \end{array}$

Namun, perhatikan bahwa dalam teori himpunan standar (misalnya, ZFC), operasi ini tidak dapat didefinisikan sebagai objek . Tidak ada yang namanya "fungsi identitas" dalam teori himpunan, karena fungsi adalah hubungan antara himpunan domain dan himpunan kode, dan jika fungsi tunggal bisa berupa fungsi identitas, maka Anda dapat menggunakannya untuk membuat himpunan dari semua set. (Ini pada dasarnya bagaimana John Reynolds menunjukkan bahwa polimorfisme gaya System-F tidak memiliki model set-teoretis.)

$X$ $S$ $P$ $X$ $P$ $X$

Jadi impredicativity gaya-F tidak sesuai dengan pandangan naif tentang tipe sebagai set. Jika Anda menggunakan teori tipe sebagai asisten pembuktian, itu baik untuk dapat mem-porting matematika standar dengan mudah ke alat Anda, dan sebagian besar orang yang menerapkan sistem seperti itu hanya menghilangkan impredicativity. Dengan cara ini semuanya memiliki pembacaan set-theoretic dan type-theoretic, dan Anda dapat menafsirkan tipe dengan cara apa pun yang paling nyaman bagi Anda.

Neel Krishnaswami
sumber

N

$\mathbb{N}$

N

$\mathbb{N}$