Kapan (atau seharusnya) CS Teoritis peduli dengan bukti intuitionistic?

Dari apa yang saya mengerti (yang sangat sedikit, jadi tolong perbaiki saya di mana saya salah!), Teori bahasa pemrograman sering berkaitan dengan bukti "intuitionistic". Dalam interpretasi saya sendiri, pendekatan itu menuntut kita untuk menganggap serius konsekuensi perhitungan logika dan kemampuan. Bukti tidak dapat ada kecuali ada algoritma yang membangun konsekuensi dari hipotesis. Kita dapat menolak sebagai aksioma prinsip tengah yang dikecualikan, misalnya, karena menunjukkan beberapa objek, yang dapat berupa atau ¬ X , secara tidak konstruktif.$X$$\lnot X$

Filosofi di atas mungkin mengarahkan kita untuk lebih memilih bukti yang valid secara intuisi dari pada yang tidak. Namun, saya belum melihat adanya kekhawatiran tentang benar-benar menggunakan logika intuitionistic dalam makalah di bidang lain dari CS teoritis. Kami sepertinya senang membuktikan hasil kami menggunakan logika klasik. Misalnya, orang mungkin membayangkan menggunakan prinsip tengah yang dikecualikan untuk membuktikan bahwa suatu algoritma benar. Dengan kata lain, kami peduli dan menganggap serius alam semesta yang dibatasi secara komputasi dalam hasil kami, tetapi tidak harus dalam bukti kami atas hasil ini.

1. Apakah peneliti dalam CS teoretis pernah khawatir tentang menulis bukti yang valid secara intuisi? Saya dapat dengan mudah membayangkan subbidang ilmu komputer teoretis yang berusaha memahami ketika hasil TCS, terutama yang algoritmik, bertahan dalam logika intuitionistic (atau lebih menarik, ketika mereka tidak). Tapi saya belum menemukan apa pun.

2. Adakah argumen filosofis yang harus mereka miliki? Sepertinya orang bisa mengklaim bahwa hasil ilmu komputer harus dibuktikan secara intuisi ketika mungkin, dan kita harus tahu hasil mana yang membutuhkan misalnya PEM. Adakah yang mencoba membuat argumen seperti itu? Atau mungkin ada konsensus bahwa pertanyaan ini tidak begitu penting?

3. Sebagai pertanyaan sampingan, saya ingin tahu contoh-contoh kasus di mana ini benar-benar penting: Apakah ada hasil TCS yang penting diketahui berpegang pada logika klasik tetapi tidak dalam logika intuitionistic? Atau diduga tidak memegang logika intuitionistic.

Permintaan maaf atas kelembutan pertanyaan! Mungkin diperlukan penulisan ulang atau interpretasi ulang setelah mendengar dari para ahli.

Seperti yang saya katakan di komentar, logika intuitionist bukanlah poin utama. Poin yang lebih penting adalah memiliki bukti konstruktif. Saya pikir teori tipe Martin-Löf jauh lebih relevan dengan teori bahasa pemrograman daripada logika intuitionistic dan ada ahli yang berpendapat bahwa karya Martin-Löf adalah alasan utama untuk membangkitkan kembali minat umum dalam matematika konstruktif.

Interpretasi komputabilitas dari konstruktif adalah satu perspektif yang mungkin, tetapi bukan satu-satunya perspektif. Kita harus berhati-hati di sini ketika kita ingin membandingkan bukti konstruktif dengan bukti klasik. Meskipun keduanya mungkin menggunakan simbol yang sama, apa yang mereka maksudkan dengan simbol-simbol itu berbeda.

Itu selalu baik untuk diingat bahwa bukti klasik dapat diterjemahkan menjadi bukti intuitionistic. Dengan kata lain, dalam arti tertentu, logika klasik adalah subsistem dari logika intuitionistic. Oleh karena itu Anda dapat menyadari (katakanlah menggunakan fungsi yang dapat dihitung) bukti klasik dalam arti tertentu. Di sisi lain, kita dapat menganggap matematika konstruktif sebagai beberapa sistem matematika dalam lingkungan klasik.

$A \lor B$$A \lor B$$\lor$

$\forall x \ \exists y \ \varphi(x,y)$$x$$y$$\varphi(x,y)$$y$$y$$x$$A$$x$$\varphi(x,A(x))$$A$

Sekarang mengapa kita tidak menggunakan logika intuitionist dalam praktiknya? Ada beberapa alasan. Sebagai contoh, kebanyakan dari kita tidak dilatih dengan pengaturan pikiran itu. Juga menemukan bukti klasik dari sebuah pernyataan mungkin jauh lebih mudah daripada menemukan bukti yang konstruktif. Atau kita mungkin peduli tentang detail tingkat rendah yang disembunyikan dan tidak dapat diakses dalam pengaturan yang konstruktif (lihat juga logika linier ). Atau kita mungkin tidak tertarik untuk mendapatkan barang-barang tambahan yang disertai dengan bukti konstruktif. Dan meskipun ada alat untuk mengekstrak program dari bukti alat ini umumnya membutuhkan bukti yang sangat rinci dan belum cukup user-friendly untuk teori umum. Singkatnya, terlalu banyak rasa sakit untuk manfaat yang terlalu sedikit.

$\Pi^0_2$$PA$$PA$$PA$

Saya ingat bahwa Douglas S. Bridges dalam pengantar buku teori komputabilitasnya berpendapat bahwa kita harus membuktikan hasil kita secara konstruktif. Dia memberikan contoh yang IIRC pada dasarnya adalah sebagai berikut:

Asumsikan bahwa Anda bekerja untuk perusahaan perangkat lunak besar dan manajer Anda meminta program untuk menyelesaikan masalah. Apakah bisa diterima untuk kembali dengan dua program dan memberi tahu manajer Anda salah satu dari dua pemecahan ini dengan benar, tetapi saya tidak tahu yang mana?

Pada akhirnya, kita harus ingat bahwa meskipun kita menggunakan simbol yang sama untuk logika klasik dan intuitionistic, simbol-simbol ini memiliki makna yang berbeda, dan yang digunakan tergantung pada apa yang ingin kita ungkapkan.

Untuk pertanyaan terakhir Anda, saya pikir teorema Robertson-Seymour akan menjadi contoh teorema yang kita tahu itu benar secara klasik tetapi kami tidak memiliki bukti konstruktif tentang itu. Lihat juga

• Apakah ada bukti keberadaan algoritma yang tidak konstruktif?

Perlu dipikirkan mengapa logika intuistionistik adalah logika alami untuk perhitungan, karena terlalu sering orang tersesat dalam rincian teknis dan gagal memahami esensi masalah.

Sederhananya, logika klasik adalah logika informasi yang sempurna: semua pernyataan dalam sistem diasumsikan diketahui atau dapat diketahui sebagai benar atau salah, tidak salah lagi.

Logika intuistionistik, di sisi lain, memiliki ruang untuk pernyataan dengan nilai kebenaran yang tidak diketahui dan tidak diketahui. Ini penting untuk perhitungan, karena, berkat ketidakpastian pemutusan dalam kasus umum, tidak akan selalu pasti berapa nilai kebenaran beberapa pernyataan, atau bahkan apakah nilai kebenaran bisa diberikan pada pernyataan tertentu atau tidak. .

$\neg\neg P \implies P$

Menurut pendapat saya, alasan "semantik" ini adalah motivasi yang jauh lebih penting untuk penggunaan logika intuistionistik untuk perhitungan daripada alasan teknis lainnya yang dapat dikemukakan.

Fungsi hash kriptografi dunia nyata seperti MD5 & SHA tidak memiliki key. Karena itu, cukup sulit untuk menerapkan teknik-teknik dari kriptografi teoretis sebagai alasan keamanannya. Alasan sederhana mengapa: untuk fungsi hash keyless, ada program / musuh yang sangat kecil yang menghasilkan tabrakan di bawah fungsi hash; yaitu, program yang memiliki tabrakan seperti itu - yang harus ada! - kode keras.

Makalah Phil Rogaway Memformalisasikan Ketidaktahuan Manusia: Hashing Tabrakan-Tahan tanpa Kunci berurusan dengan masalah ini. Di dalamnya ia menunjukkan bahwa beberapa teorema yang sangat standar untuk fungsi hash utama (seperti konstruksi Merkle-Damgård & paradigma hash-then-sign) dapat diadaptasi dan dibuktikan kembali dengan pernyataan teorema "ramah intuisi-ramah" yang berlaku untuk fungsi hash yang tidak dikunci.

di sini ada bab bagus tentang Intuitionistic Logic dari buku online komprehensif Logic for Computer Science , 300pp. [1] sec 9.5, p210, ringkasan pada p220:

Logika intuitionistic muncul dari gerakan konstruktivisme dalam matematika yang menolak bukti keberadaan non-konstruktif atau yang didasarkan pada hukum tengah yang dikecualikan. Baru-baru ini hubungan antara matematika dan pemrograman intuitionistic telah keluar dari pengamatan bahwa proposisi dan tipe (dalam arti pemrograman) adalah setara. Pengembangan algoritma dalam sistem formal ini, yang didasarkan pada deduksi alami, terdiri dari penulisan spesifikasi dalam notasi logis dan kemudian, dengan mempertimbangkan ini sebagai tipe, membuktikan bahwa itu tidak kosong. Karena logika yang mendasari adalah bukti konstruktif, jika dapat dilakukan,

Perspektif terdekat lainnya berasal dari tulisan TCSist Andrej Bauer tentang "Matematika dan komputasi; matematika untuk komputer" [2] yang pada dasarnya mengusulkan bahwa "matematika intuitionistic baik untuk fisika". presentasi terutama dalam hal fisika, tetapi bagi mereka yang menganggap CS erat dengan fisika ideologi umumnya akan dibawa ke TCS.

Interpretasi komputasi. Ini adalah interpretasi dari logika intuitionistic yang biasa disajikan dalam ilmu komputer. Kami melihat semua set sebagaimana diwakili oleh struktur data yang cocok — sudut pandang yang masuk akal bagi seorang ilmuwan komputer. Maka sebuah pernyataan dianggap benar jika ada program (bukti komputasi) yang menyaksikan kebenarannya.

[1] Logika untuk Ilmu Komputer, Reeves dan Clark

[2] Matematika intuitionistic untuk fisika Bauer