Logika konstruktivis adalah sistem yang menghilangkan Hukum Tengah yang Dikecualikan, serta Negasi Ganda, sebagai aksioma. Ini dijelaskan di Wikipedia di sini dan di sini . Secara khusus, sistem tidak memungkinkan pembuktian dengan kontradiksi.
Saya bertanya-tanya, apakah ada yang akrab dengan bagaimana ini mempengaruhi hasil mengenai Mesin Turing dan bahasa formal? Saya perhatikan bahwa hampir setiap bukti bahwa suatu bahasa tidak dapat ditentukan bergantung pada bukti oleh kontradiksi. Argumen Diagonisasi dan konsep reduksi bekerja dengan cara ini. Bisakah ada bukti "konstruktif" tentang keberadaan bahasa yang tidak dapat diputuskan, dan jika ya, seperti apa bentuknya?
EDIT: Untuk lebih jelasnya, pemahaman saya tentang pembuktian dengan kontradiksi dalam logika konstruktivisme salah, dan jawabannya telah menjelaskan hal ini.
Jawaban:
Iya nih. Anda tidak perlu perantara yang dikecualikan untuk mendapatkan kontradiksi. Secara khusus, diagonisasi masih berfungsi.
Berikut adalah argumen diagonalisasi khas oleh Conor McBride. Diagonisasi khusus ini adalah tentang ketidaklengkapan, bukan ketidakpastian, tetapi idenya sama. Poin penting yang perlu diperhatikan adalah bahwa kontradiksi yang didapatnya bukan dari bentuk "P dan bukan P", melainkan dari bentuk "x = x +1".
Tentu saja, sekarang Anda mungkin bertanya-tanya apakah logika konstruktif mengakui "x = x +1" sebagai suatu kontradiksi. Itu benar. Sifat utama dari suatu kontradiksi adalah bahwa segala sesuatu mengikuti dari suatu kontradiksi, dan menggunakan "x = x + 1", saya memang dapat secara konstruktif membuktikan "x = y" untuk dua bilangan alami.
Satu hal yang mungkin berbeda tentang bukti konstruktif adalah cara mendefinisikan "tidak dapat ditentukan". Dalam logika klasik, setiap bahasa harus dapat dipilih atau tidak dapat ditentukan; jadi "tidak diputuskan" hanya berarti "tidak dapat memutuskan". Namun, dalam logika konstruktif, "bukan" bukanlah operasi logis primitif, jadi kita tidak dapat mengungkapkan keraguan dengan cara ini. Alih-alih, kami mengatakan bahwa suatu bahasa tidak dapat diputuskan jika mengasumsikan bahwa bahasa itu dapat memutuskan mengarah pada kontradiksi.
Pada kenyataannya, meskipun "bukan" bukan primitif dalam logika konstruktif, kami biasanya mendefinisikan "bukan P" sebagai gula sintaksis untuk "P dapat digunakan untuk membangun kontradiksi", jadi bukti oleh kontradiksi sebenarnya satu-satunya cara untuk secara konstruktif buktikan pernyataan dalam bentuk "bukan P" seperti "bahasa L tidak dapat ditentukan".
sumber
Ketika berbicara tentang provabilitas pernyataan klasik secara konstruktif, seringkali penting bagaimana kita merumuskannya. Formulasi yang setara secara klasik tidak perlu sama secara konstruktif. Juga penting apa yang Anda maksud dengan bukti konstruktif, ada berbagai aliran konstruktivisme.
Misalnya, pernyataan yang menyatakan bahwa ada fungsi total yang tidak dapat dihitung tidak akan benar dalam rasa matematika konstruktif yang menganggap Tesis Gereja-Turing (yaitu setiap fungsi dapat dihitung) sebagai aksioma.
Di sisi lain, jika Anda berhati-hati Anda dapat merumuskannya sehingga dapat dibuktikan: untuk setiap penghitungan yang dapat dihitung dari fungsi penghitungan total, ada fungsi penghitungan total yang tidak ada dalam penghitungan.
Anda mungkin menemukan posting ini oleh Andrej Bauer menarik.
ps: Kita juga bisa melihat diagonalisasi dari perspektif teori kategori. Lihat
sumber
Saya pikir bukti kardinalitas masih berlaku, menunjukkan keberadaan bahasa yang bukan bahasa yang dapat dihitung (jadi pasti tidak dapat dipastikan).
Bukti langsung cukup lurus ke depan, itu hanya mengamati bahwa Mesin Turing dikodekan dalam beberapa alfabet hingga (mungkin juga biner), jadi ada banyak sekali, dan himpunan semua bahasa lebih dari alfabet tetap (mungkin juga biner lagi ) adalah himpunan semua himpunan bagian dari himpunan string di atas alfabet itu - yaitu himpunan daya himpunan yang dapat dihitung, dan harus tidak terhitung. Oleh karena itu ada lebih sedikit Mesin Turing daripada bahasa, jadi ada sesuatu yang tidak dapat dihitung.
Bagi saya ini tampaknya cukup konstruktif (meskipun tidak mungkin untuk mengejar secara fisik, ini memberi Anda cara untuk menunjuk pada beberapa bahasa dan mengetahui satu tidak dapat dihitung).
Kita kemudian mungkin bertanya apakah mungkin untuk menunjukkan bahwa set yang dapat dihitung dan tidak terhitung memiliki kardinalitas yang berbeda, khususnya, menghindari diagonisasi. Saya pikir ini masih mungkin. Argumen asli Cantor juga tampaknya sangat konstruktif.
Tentu saja, ini benar-benar perlu diperiksa oleh seseorang yang tahu lebih banyak tentang logika konstruktivis.
sumber
Saya pikir saya setuju dengan yang lain bahwa argumen diagonalisasi itu konstruktif, walaupun dari apa yang bisa saya katakan ada beberapa ketidaksepakatan tentang hal ini di beberapa kalangan.
Maksud saya, asumsikan bahwa kita sedang melihat kumpulan semua bahasa yang dapat dipilih. Saya dapat membuat bahasa yang tidak dapat ditentukan menggunakan diagonalisasi. Perlu dicatat bahwa saya tidak menganggap "konstruktivisme" dan "finitisme" sebagai hal yang sama sekali, meskipun secara historis saya pikir ini adalah busur terkait.
Pertama, saya pikir semua orang - bahkan konstruktivis - setuju bahwa seperangkat bahasa yang dapat ditentukan dapat dihitung. Karena seperangkat mesin Turing dapat dihitung (kami dapat menyandikan semua TM yang valid menggunakan string hingga), perjanjian ini cukup mudah diikuti.
Jadi secara teknis, kami telah membangun bahasa yang "tidak dapat memutuskan"; apakah seorang konstruktivis akan berargumen bahwa "tidak dapat memutuskan" tidak boleh dikacaukan dengan "tidak dapat dipastikan" adalah pertanyaan yang menarik, tetapi pertanyaan yang saya tidak siap untuk menjawab.
Untuk memperjelas, apa yang saya pikir ini tunjukkan adalah sebagai berikut: kita dapat secara konstruktif membuktikan bahwa ada bahasa yang tidak diputuskan oleh mesin Turing. Bagaimana Anda memilih untuk menafsirkan bahwa dalam kerangka kerja tertentu adalah pertanyaan yang lebih sulit.
sumber