Ini adalah pertanyaan lanjutan untuk
Apa perbedaan antara bukti dan program (atau antara proposisi dan tipe)?
Program apa yang sesuai dengan bukti non-konstruktif (klasik) dari bentuk ? (Asumsikan bahwa adalah beberapa hubungan menarik yang dapat dipilih misalnya eg -th TM tidak berhenti pada langkah .)
(ps: Saya memposting pertanyaan ini sebagian karena saya tertarik untuk belajar lebih banyak tentang apa yang dimaksud Neel dengan "terjemahan Godel-Gentzen adalah transformasi kelanjutan yang lewat" dalam komentarnya .)
Jawaban:
Ini pertanyaan yang menarik. Jelas seseorang tidak dapat berharap untuk memiliki program yang memutuskan untuk setiap apakah ∀ k T ( e , k ) berlaku atau tidak, karena ini akan memutuskan Masalah Pemutusan. Seperti yang telah disebutkan, ada beberapa cara untuk menafsirkan bukti secara komputasi: ekstensi Curry-Howard, realisasi, dialektika, dan sebagainya. Tetapi mereka semua akan menginterpretasikan secara teoretis teorema yang Anda sebutkan kurang lebih dengan cara berikut.e ∀kT(e,k)
Untuk kesederhanaan pertimbangkan teorema klasik yang setara
(1)∃i∀j(¬T(e,j)→¬T(e,i))
Ini (secara konstruktif) setara dengan yang disebutkan karena mengingat kita dapat memutuskan apakah ∀ k T ( e , k ) berlaku atau tidak dengan hanya memeriksa nilai ¬ T ( e , i ) . Jika ¬ T ( e , i ) tahan maka ∃ i ¬ T ( e , i ) dan karenanya ¬ ∀ i T ( e , i ) . Jika di sisi laini ∀kT(e,k) ¬T(e,i) ¬T(e,i) ∃i¬T(e,i) ¬∀iT(e,i) tidak berlaku oleh (1) kita memiliki ∀ j ( ¬ T ( e , j ) → ⊥ ) yang menyiratkan ∀ j T ( e , j ) .¬T(e,i) ∀j(¬T(e,j)→⊥) ∀jT(e,j)
Sekarang, sekali lagi kita tidak dapat menghitung dalam (1) untuk setiap e yang diberikan karena kita akan lagi menyelesaikan Masalah Pemutusan. Apa yang akan dilakukan oleh semua interpretasi yang disebutkan di atas adalah untuk melihat teorema yang setarai e
(2)∀f∃i′(¬T(e,f(i′))→¬T(e,i′))
Fungsi disebut fungsi Herbrand. Ia mencoba untuk menghitung contoh contoh j untuk setiap saksi potensial yang diberikan i . Jelas bahwa (1) dan (2) adalah setara. Dari kiri ke kanan ini konstruktif, cukup ambil i ′ = i pada (2), di mana i adalah saksi yang dianggap sebagai (1). Dari kanan ke kiri seseorang harus beralasan secara klasik. Asumsikan (1) itu tidak benar. Kemudian,f j i i′=i i
(3)∀i∃j¬(¬T(e,j)→¬T(e,i))
Biarkan menjadi fungsi menyaksikan ini, yaituf′
(4)∀i¬(¬T(e,f′(i))→¬T(e,i))
Sekarang, ambil dalam (2) dan kami memiliki ( ¬ T ( e , f ′ ( i ′ ) ) → ¬ T ( e , i ′ ) ) , untuk beberapa i ′ . Tetapi dengan mengambil i = i ′ dalam (4) kita memperoleh negasi dari itu, kontradiksi. Karenanya (2) menyiratkan (1).f=f′ (¬T(e,f′(i′))→¬T(e,i′)) i′ i=i′
Jadi, kita memiliki bahwa (1) dan (2) secara klasik setara. Tetapi yang menarik adalah bahwa (2) sekarang memiliki saksi konstruktif yang sangat sederhana. Ambil saja jika T ( e , f ( 0 ) ) tidak berlaku, karena kesimpulan (2) benar; atau ambil i ′ = 0 jika T ( e , f ( 0 ) ) berlaku, karena kemudian ¬ T ( e , f ( 0 )i′=f(0) T(e,f(0)) i′=0 T(e,f(0)) tidak berlaku dan premis (2) salah, menjadikannya kembali benar.¬T(e,f(0))
Oleh karena itu, cara untuk menginterpretasi secara teoretis suatu teorema klasik seperti (1) adalah dengan melihat formulasi setara (klasik) yang dapat dibuktikan secara konstruktif, dalam kasus kami (2).
Perbedaan penafsiran yang disebutkan di atas hanya berbeda pada cara fungsi muncul. Dalam hal realisasi dan interpretasi dialektika, ini secara eksplisit diberikan oleh interpretasi, ketika dikombinasikan dengan beberapa bentuk terjemahan negatif (seperti Goedel-Gentzen) Dalam kasus ekstensi Curry-Howard dengan call-cc dan operator lanjutan, fungsi f muncul dari kenyataan bahwa program diizinkan untuk "mengetahui" bagaimana nilai tertentu (dalam kasus kami i ) akan digunakan, jadi f adalah lanjutan dari program di sekitar titik di mana saya dihitung.f f i f i
Poin penting lainnya adalah bahwa Anda ingin bagian dari (1) ke (2) menjadi "modular", yaitu jika (1) digunakan untuk membuktikan (1 '), maka interpretasinya (2) harus digunakan dengan cara yang sama. untuk membuktikan interpretasi dari (1 '), katakanlah (2'). Semua interpretasi yang disebutkan di atas melakukan itu, termasuk terjemahan negatif Goedel-Gentzen.
sumber
Sudah cukup terkenal bahwa aritmatika klasik dan intuitionistic adalah sama.
Salah satu cara untuk menunjukkan ini adalah melalui "embeddings negatif" dari logika klasik menjadi logika intuitionistic. Jadi, misalkan adalah rumus aritmatika orde pertama klasik. Sekarang, kita dapat mendefinisikan formula logika intuitionistic sebagai berikut:ϕ
Perhatikan bahwa pada dasarnya adalah homomorfisme yang melekat pada yang tidak-tidak ada di mana-mana, kecuali bahwa pada disjungsi dan eksistensial, ia menggunakan dualitas de Morgan untuk mengubahnya menjadi konjungsi dan universal. (Saya cukup yakin ini bukan terjemahan Godel-Gentzen yang tepat, karena saya memasaknya untuk jawaban ini - pada dasarnya apa pun yang Anda tulis menggunakan double-negation + de Morgan dualitas akan berfungsi. Variasi ini sebenarnya ternyata penting untuk interpretasi komputasi logika klasik; lihat di bawah.)G(ϕ)
Pertama: Sudah jelas bahwa terjemahan ini mempertahankan kebenaran klasik, sehingga benar jika dan hanya jika ϕ adalah, secara klasik.G(ϕ) ϕ
Kedua: Ini kurang jelas, tetapi tetap demikian, bahwa untuk rumus di fragmen, provabilitas dalam logika intuitionistic dan klasik bertepatan. Cara untuk membuktikan ini adalah dengan pertama-tama melihat rumus yang diambil dari tata bahasa ini:∀,⟹,∧,¬
Dan kemudian kita dapat membuktikan sebagai lemma (dengan induksi pada ) bahwa G ( A )A dapat diturunkan secara intuisi. Jadi sekarang, kita dapat menunjukkan kesetaraan rumus-rumus negatif dengan melakukan induksi terhadap struktur buktinya (dalam, katakanlah, kalkulus berurutan) dan menggunakan lemma sebelumnya untuk mensimulasikan hukum tengah yang dikecualikan.G(A)⟹A
Jadi, bagaimana seharusnya Anda memikirkan hal ini secara intuitif?
Pertama, pandangan bukti-teoretis. Jika Anda melihat aturan kalkulus sekuens, Anda dapat melihat bahwa satu-satunya tempat logika klasik dan intuitionistic berbeda secara serius adalah aturan untuk disjungsi dan eksistensial. Jadi kami menggunakan fakta ini untuk menunjukkan bahwa bukti dalam satu logika formula ini dapat diterjemahkan ke bukti di yang lain. Ini menunjukkan bagaimana memikirkan logika konstruktif sebagai perluasan dari logika klasik dengan dua penghubung baru dan ∨ . Apa yang kita sebut "eksistensi klasik" dan "disjungsi klasik" hanyalah singkatan yang melibatkan ∀ , konjungsi, dan negasi, dan untuk membicarakan tentang keberadaan aktual kita perlu memperkenalkan penghubung baru.∃ ∨ ∀
Kedua, ada pandangan topologis. Sekarang, model logika klasik (sebagai keluarga set) adalah aljabar Boolean (yaitu, sekelompok himpunan bagian ditutup di bawah serikat, persimpangan, dan pelengkap yang berubah-ubah). Ternyata model logika intuitionsitic adalah sebagai ruang topologis , dengan proposisi ditafsirkan sebagai set terbuka. Mereka interpretasi dari negasi adalah interior komplemen, dan kemudian mudah untuk menunjukkan bahwa , yang berarti bahwa dua negasi mengirimkan kita ke terkecil clopen meliputi masing-masing terbuka --- dan clopens membentuk Aljabar Boolean.¬¬¬P=¬P
Sekarang, terima kasih kepada Curry-Howard, kami tahu bagaimana menafsirkan bukti dalam logika intuitionistic sebagai program fungsional. Jadi, satu jawaban yang mungkin (tetapi bukan satu-satunya) untuk pertanyaan "apa konten konstruktif dari bukti klasik?" adalah sebagai berikut:
Jadi mari kita lihat terjemahan . Jadi ini mengatakan bahwa konten konstruktif dari tengah yang dikecualikan sama dengan mengatakan bahwa itu bukan kasus yang ¬ P dan dan ¬ ¬ P tahan - yaitu, nonkontradiksi. Jadi dalam hal ini, sebenarnya tidak ada banyak konten komputasi dengan hukum dari perantara yang dikecualikan.G(A∨¬A)=¬(¬G(A)∧¬¬G(A)) ¬P ¬¬P
Untuk melihat apa itu secara konkret, ingatlah bahwa secara konstruktif, negasi didefinisikan sebagai . Jadi rumus ini adalah ( ( G ( A ))¬A==A⟹⊥ . Bit kode Ocaml berikut akan menggambarkan:((G(A)⟹⊥)∧((G(A)⟹⊥)⟹⊥))⟹⊥
Artinya, jika Anda tidak mendapatkan-A dan tidak-tidak-A, Anda bisa meneruskan negasi pertama ke yang kedua untuk mendapatkan kontradiksi yang Anda inginkan.
Sekarang, apa transformasi kelanjutan lewat gaya?
Sekarang,
Saya melihat "a" transformasi CPS, karena seperti yang saya sebutkan sebelumnya, ada banyak terjemahan negatif yang memungkinkan Anda membuktikan teorema ini, dan masing-masing sesuai dengan trasnformasi CPS yang berbeda. Dalam istilah operasional, setiap transformasi berhubungan dengan urutan evaluasi yang berbeda . Jadi tidak ada interpretasi komputasi unik dari logika klasik, karena Anda punya pilihan untuk dibuat dan pilihan perbedaan memiliki karakteristik operasional yang sangat berbeda.
sumber
Ada seluruh konferensi tentang masalah bukti non-konstruktif sebagai program , dan saya bukan ahli dalam hal ini. Di atas, Neel Krishnaswami menyinggung jawaban yang lebih lama ia persiapkan, yang, jika dilihat dari pekerjaannya di sini, akan sangat baik. Ini hanya rasa jawaban.
memberikan kode O'Caml:
Pengantar terbersih untuk hal ini yang saya lihat ada di Tim Griffin "Sebuah konsep formula-sebagai-jenis kontrol" .
sumber
callcc
ke Skemacallcc
. Maka Anda benar-benar dapat mencoba berbagai hal.