Apakah ada semantik kategoris untuk logika non-monotonik?
Tampaknya jawaban sederhana untuk ini adalah "Tidak" karena gagasan jelas tentang komposisi gagal untuk model logika non-monotonik apa pun. Tetapi apakah ada model yang benar-benar berfungsi dengan gagasan komposisi yang didefinisikan dengan tepat?
ct.category-theory
semantics
denotational-semantics
David Boshton
sumber
sumber
Jawaban:
Logika non-monotonik adalah bidang yang luas - apakah Anda memiliki logika tertentu? Ngomong-ngomong, dengan asumsi asumsi :)
satu jawaban adalah bahwa Anda dapat memberikan semantik kategoris yang masuk akal untuk logika apa pun yang kalkulus berurutannya dengan eliminasi potong diketahui. Pada dasarnya, tipenya adalah objek, bentuk normal dari kalkulus berurutan adalah morfisme, dan cut-elimination memberi tahu Anda bagaimana menerapkan komposisi. Ini memberi Anda kategori awal dalam kategori model apa pun yang akhirnya Anda gunakan untuk membuktikan kesehatan dan kelengkapan.
Resep ini tidak tergantung pada monotonitas, sehingga dapat bekerja dengan baik bahkan untuk logika non-monotonik. Sebagai contoh, salah satu keberhasilan yang lebih penting dalam logika kategorikal adalah perlakuannya terhadap logika linier . Ini adalah logika di mana, secara intuitif, proposisi merujuk pada sumber daya , sehingga implikasi linear dapat dibaca sebagai " dapat dikonsumsi untuk menghasilkan ". Hubungan konsekuensi dari logika linier adalah non-monotonik (karena fakta bahwa dapat dikonsumsi untuk menghasilkan tidak berarti bahwa dan keduanya dapat dikonsumsi untuk menghasilkanA B A B A X BA⊸B A B A B A X B ). Namun, ia memiliki teori pembuktian yang sangat baik, dan model kategorikalnya terkait erat dengan teori kategori monoid.
sumber
[Permintaan maaf saya untuk menulis ini sebagai jawaban, meskipun pada dasarnya itu hanya komentar dari jawaban sebelumnya. Tapi saya tidak diperbolehkan memposting komentar di sana, karena saya tidak punya cukup "reputasi"]
Jawaban sebelumnya tidak benar. Logika linier (juga sistem substrukturalnya: MLL, MALL, MELL, ALL, apa pun yang Anda inginkan ...) sangat monoton .
Jawaban Neel membingungkan "relevansi" dan "non-monotonisitas".
Relevansi dapat dilihat sebagai non-monotonisitas dari konektor inferensi sistem . Logika linier relevan, dalam bahwa provability dari tidak berarti provability dari . Relevansi adalah semacam batin non-monotonisitas dari logika.⊢ X ⊗ A ⊸ B⊢A⊸B ⊢X⊗A⊸B
Di sisi lain, apa yang orang sebut logika non-monoton adalah sistem dimana provability sendiri dari sistem ini tidak monoton: menambahkan elemen baru ke set formula mengubah set formula dapat dibuktikan. Ini adalah bentuk meta non-monotonisitas, karena menyangkut provabilitas dan bukan penghubung kesimpulan. Logika linier adalah monoton: Anda dapat menambahkan apa pun yang Anda inginkan ke set rumus, dan setiap aksioma atau aturan inferensi baru ke sistem, tetapi jika Anda memiliki bukti dari sekuens sebelumnya, Anda akan masih memilikinya sekarang, karena Anda belum mengubah aturan inferensi lain kalkulus sekuens.Γ⊢M:A
Sejauh yang saya tahu, logika non-monotonik (nyata) sulit untuk diletakkan dalam bentuk kalkulus berurutan yang menikmati pemotongan-potong, atau jenis sistem bukti lainnya dengan gagasan yang sama untuk mengakhiri pengurangan-bukti. Inilah sebabnya mengapa pendekatan semantik kategoris tradisi hampir tidak akan berhasil bagi mereka.
sumber