Mengapa kita membutuhkan semantik formal untuk logika predikat?

Pertimbangkan pertanyaan ini diselesaikan. Saya tidak akan memilih jawaban terbaik karena mereka semua telah berkontribusi pada pemahaman saya tentang topik ini.

Saya tidak yakin manfaat apa yang kita miliki dengan secara formal mendefinisikan semantik logika predikat. Tetapi saya melihat nilai dalam memiliki kalkulus bukti formal. Maksud saya adalah bahwa kita tidak perlu semantik formal untuk membenarkan aturan inferensi kalkulus bukti.

Kita dapat mendefinisikan kalkulus yang meniru "hukum pemikiran", yaitu aturan inferensi yang telah digunakan oleh ahli matematika selama ratusan tahun untuk membuktikan teorema mereka. Kalkulus seperti itu sudah ada: deduksi alami. Maka kita akan mendefinisikan kalkulus ini menjadi sehat dan lengkap.

Ini dapat dibenarkan dengan menyadari bahwa semantik formal dari logika predikat hanyalah sebuah model. Ketepatan model hanya dapat dibenarkan secara intuitif. Dengan demikian, dengan menunjukkan bahwa deduksi alami baik dan lengkap dengan referensi ke semantik formal tidak menjadikan deduksi alami lebih "benar". Akan sama baiknya jika kita secara langsung membenarkan aturan pengurangan alami secara intuitif. Jalan memutar menggunakan semantik formal tidak memberi kita apa pun.

Kemudian, setelah deduksi alami didefinisikan sebagai suara dan lengkap, kita dapat menunjukkan kesehatan dan kelengkapan kalkuli lainnya dengan menunjukkan bahwa bukti yang mereka hasilkan dapat diterjemahkan ke deduksi alami dan sebaliknya.

Apakah refleksi saya di atas benar? Mengapa penting untuk membuktikan kesehatan dan kelengkapan kalkulus bukti dengan merujuk pada semantik formal?

Komentar kecil, dan jawaban yang lebih serius.

Pertama, tidak masuk akal untuk mendeklarasikan sistem deduksi alami lengkap dengan fiat. Deduksi alami menarik justru karena memiliki pengertian internal tentang konsistensi dan / atau kelengkapan - yaitu, eliminasi potong. Ini adalah teorema yang fantastis, dan IMO sepenuhnya membenarkan upaya untuk memberikan semantik teori-bukti murni (dan oleh korespondensi CH, itu juga membenarkan penggunaan metode operasional dalam bahasa pemrograman semantik). Tapi ini menarik justru karena menawarkan gagasan yang lebih halus untuk mendapatkan logika yang benar daripada konsistensi. Mengambil jalan teoretis bukti berarti Anda harus melakukan lebih banyak pekerjaan, tetapi sebagai gantinya Anda mendapatkan hasil yang lebih kuat.

Namun, kadang logika itu terjadi sendirimengambil peran sekunder. Kita dapat mulai dengan model (keluarga), dan kemudian mencari cara untuk berbicara secara sintaksis tentang mereka, menggunakan logika. Tingkat kesehatan dan kelengkapan logika sehubungan dengan keluarga model menunjukkan bahwa logika benar-benar menangkap semua hal yang menarik dan benar yang dapat Anda katakan tentang kelas model. Contoh konkret tentang kapan model lebih menarik daripada teori logis terjadi dalam analisis program dan pengecekan model. Di sana, hal yang biasa dilakukan adalah mengambil model Anda menjadi eksekusi program, dan logika menjadi beberapa fragmen logika temporal. Proposisi yang dapat Anda katakan dalam bahasa-bahasa ini (sengaja) tidak terlalu menarik - misalnya, null pointer dereferences tidak pernah terjadi - tetapi fakta bahwa itu berlaku untuk program aktual yang menjalankannya yang memberikan minat.

Saya hanya akan menambahkan perspektif lain untuk menambah respons di atas. Pertama, refleksi ini bermanfaat, dan banyak orang memiliki ide serupa. Dalam filsafat ini kadang-kadang disebut "semantik teoritik-bukti", yang menarik untuk dikerjakan oleh Nuel Belnap, Dag Prawitz, Michael Dummett dan lainnya di tahun 60an dan 70an, yang dengan sendirinya menarik kembali karya Gentzen tentang deduksi alami. Per Martin-Löf dan Jean-Yves Girard juga tampaknya mengusulkan varian posisi ini dalam tulisan mereka. Dan berbicara sangat luas, dalam bahasa pemrograman ini adalah "pendekatan sintaksis untuk mengetik tingkat kesehatan".

Masalahnya adalah bahwa bahkan jika Anda menerima bahwa aturan logika tidak memerlukan penafsiran semantik yang terpisah, tidak terlalu menarik / berguna untuk mengatakan bahwa mereka dibenarkan sendiri dan membiarkannya begitu saja. Pertanyaannya adalah apa yang dicapai semantik formal, dan apakah mungkin untuk mencapai hal yang sama dengan jalan memutar yang lebih sedikit. Namun, proyek pemersatu teori model dengan teori bukti analitik adalah penting tetapi masih belum terselesaikan, sedang dikejar secara aktif di berbagai bidang termasuk logika kategoris, permainan semantik, dan "ludis" Girard. Sebagai contoh, di samping apa yang disebutkan oleh Charles, manfaat kualitatif lain dari memiliki model adalah kemampuan untuk memberikan contoh tandingan yang nyata kepada yang bukan-teorema, dan pertanyaannya adalah bagaimana memahami ini dalam pendekatan "langsung". Untuk satu jawaban yang diilhami orang ludis, lihat "Tentang arti kelengkapan logis" oleh Michele Basaldella dan Kazushige Terui.

Semantik formal memberikan makna langsung dari istilah dalam kalkulus secara independen dari aturan bukti sintaksis untuk memanipulasi mereka. Tanpa semantik formal bagaimana Anda bisa menyatakan apakah aturan deduksi itu benar (sehat) atau apakah Anda cukup memilikinya (kelengkapan)?

Ada "hukum pemikiran" yang diajukan sebelum deduksi alami terjadi. Silogisme Aristoteles adalah salah satu koleksi seperti itu. Jika kita mendefinisikannya sebagai suara dan lengkap, kita mungkin masih akan menggunakannya hari ini, daripada mengembangkan teknik logis yang lebih maju. Intinya adalah, jika silogisme sepenuhnya menangkap hukum pemikiran, mengapa kita perlu memikirkan logika lebih lanjut. Bagaimana jika mereka sebenarnya tidak konsisten? Memiliki semantik bersama dengan kalkulus resmi bukti dan kesehatan dan bukti kelengkapan menghubungkan mereka menyediakan tongkat pengukur untuk menilai nilai suatu sistem penalaran tersebut. Itu tidak lagi berdiri sendiri.

$X\lor \neg X$bahkan lebih jauh berargumen bahwa kita harus menerima bahwa tidak ada satu logika yang benar dan mengadopsi sikap pluralistik, menggunakan logika yang paling tepat untuk kesempatan itu. Mengingat banyaknya logika yang tersedia bagi para ilmuwan komputer (logika linier, logika pemisahan, logika konstruktif tingkat tinggi, banyak logika modal, semuanya dalam varietas klasik dan intuitionistic), mengadopsi sikap pluralistik adalah sesuatu yang kebanyakan dari kita mungkin belum memberikan yang kedua berpikir, karena logika adalah alat untuk menyelesaikan masalah tertentu dan kami mencoba untuk memilih yang paling tepat. Semantik formal adalah salah satu cara menilai kesesuaian logika.

Alasan lain untuk memiliki semantik formal adalah bahwa ada lebih banyak logika daripada predikat kalkulus. Banyak dari logika ini dirancang untuk alasan tentang jenis sistem tertentu. (Saya sedang berpikir tentang modal logika). Di sini kelas sistem diketahui dan logika datang kemudian (walaupun, secara historis, ini juga tidak benar). Sekali lagi, kesehatan memberi tahu kita apakah aksioma logika dengan benar menangkap "perilaku" sistem, dan kelengkapan memberi tahu kita apakah kita memiliki cukup aksioma. Tanpa semantik, bagaimana kita tahu apakah aturan deduksi sudah cukup dan bukan omong kosong?

Salah satu contoh logika yang didefinisikan murni secara sintaksis dan pekerjaan masih berlangsung untuk menyediakannya dengan semantik formal adalah logika BAN untuk alasan tentang protokol kriptografi. Aturan inferensi logis tampak masuk akal, jadi mengapa memberikan semantik formal? Sayangnya, logika BAN dapat digunakan untuk membuktikan bahwa suatu protokol sudah benar, namun serangan terhadap protokol tersebut mungkin ada. Oleh karena itu aturan deduksi salah , setidaknya sehubungan dengan semantik yang diharapkan.

Saya setuju dengan supercooldave, tetapi ada alasan lain yang lebih pragmatis untuk menginginkan lebih dari beberapa aturan inferensi lain yang mencirikan logika: seperangkat aturan inferensi tertentu cenderung tidak baik untuk menjawab jenis masalah yang dihadapi saat meletakkan logika menggunakan.

Jika Anda memiliki logika yang ditentukan oleh daftar aksioma dan beberapa aturan sebagai sistem Hilbert, biasanya akan menjadi kerja keras untuk mencari cara untuk membuktikan teorema yang diberikan dalam sistem, dan tanpa wawasan teoritis, Anda tidak akan pergi untuk dapat membuktikan bahwa proposisi yang diberikan tidak dapat dibuktikan dalam sistem. Model tradisional baik untuk membuktikan sifat yang berlaku untuk keseluruhan logika dengan induksi.

Empat jenis alat berguna untuk memecahkan masalah yang ingin diselesaikan oleh sebagian besar ahli logika, disusun dari yang paling tidak sampai yang paling semantik:

1. Sistem gaya Hilbert baik untuk mengkarakterisasi hubungan konsekuensi logis dari suatu logika, dan mereka biasanya baik untuk mengkategorikan beberapa logika, seperti logika modal saingan;
2. Sistem Tableau baik untuk memformalkan algoritma keputusan. Biasanya jika suatu logika dapat diputuskan, seseorang dapat menemukan sistem tablo terminating sebagai algoritma keputusan, dan jika tidak seseorang dapat menemukan sistem tablo yang berpotensi non-terminating yang menyediakan prosedur semi-keputusan. Jika seseorang ingin menunjukkan batas atas kompleksitas decidability (yaitu, kelas kompleksitas logika), sistem tablo umumnya tempat pertama yang terlihat.
3. Teori bukti analitik, seperti deduksi alami dan kalkulus sekuel Gentzen, memberikan representasi bukti yang baik untuk penalaran, dan menawarkan gagasan bukti analitik, yang berguna untuk membuktikan sifat-sifat yang berguna seperti interpolasi untuk sebuah teori.
4. Teori model gaya Tarski seringkali lebih baik untuk alasan tentang logika, karena mereka hampir sepenuhnya abstrak jauh dari rincian sintaksis logika. Dalam logika modal dan teori himpunan, mereka jauh lebih baik dalam memberikan hasil sehingga para ahli logika cenderung memiliki minat yang sangat terbatas dalam teori tablo dan bukti analitik.

Karena supercooldave menyebutkan logika intuitionistic: tanpa aturan dari kalangan menengah yang dikecualikan, teori model menjadi jauh lebih rumit, dan teori bukti analitik menjadi lebih penting, biasanya semantik pilihan. Teknik aljabar, seperti teori kategori, menjadi lebih disukai untuk abstrak jauh dari kompleksitas sintaksis.