Ilustrasi Teori Kategori: Logika (2021)

 (abuseofnotation.github.io)
2 poin oleh GN⁺ 2024-10-27 | 1 komentar | Bagikan ke WhatsApp
  • Logika berangkat dari proposisi atomik yang diterima sebagai benar, lalu membentuk proposisi yang lebih besar dengan operator seperti and, or, implies; seperti dalam teori kategori, komposisi adalah inti utamanya
  • Logika klasik menafsirkan proposisi sebagai nilai Boolean benar/salah, operator logika sebagai fungsi Boolean, dan membahas negasi, konjungsi, disjungsi, implikasi, serta ekuivalensi melalui tabel kebenaran
  • Interpretasi BHK dalam logika intuisionistik memandang proposisi sebagai objek yang memiliki bukti; A ∧ B ditafsirkan sebagai pasangan bukti, dan A → B sebagai fungsi yang mengubah bukti A menjadi bukti B
  • Dalam sebagian kategori, objek berkorespondensi dengan proposisi dan morfisme dengan bukti; dalam orde, ini muncul sebagai preorder atau partial order, dengan A ≤ B berarti A → B
  • Secara teori orde, logika intuisionistik berkorespondensi dengan Heyting algebra; secara teori kategori umum, dengan bicartesian closed category. Konjungsi, disjungsi, benar, salah, dan implikasi masing-masing berkorespondensi dengan meet/join, terminal/initial, dan exponential object

Logika yang Berawal dari Proposisi

  • Logika menangani aturan formal yang konsisten dengan dirinya sendiri terlepas dari observasi, dan merupakan sistem untuk menyimpulkan atau membuktikan bahwa sesuatu benar ketika sesuatu yang lain diketahui
  • Teori matematika dapat dipandang sebagai logika yang ditambahi definisi tambahan
    • Teori himpunan dapat didefinisikan dengan menambahkan konsep primitif relasi keanggotaan himpunan ke aksioma logika standar
  • Untuk memulai logika, diperlukan himpunan proposisi awal yang diterima sebagai benar atau salah
    • Ini disebut premis, proposisi atomik, atau primary proposition
  • Dua proposisi atau lebih menjadi satu proposisi majemuk melalui operator logika seperti and, or, implies/entails
    • ∧ berarti and
    • ∨ berarti or
    • → berarti follows atau implikasi
  • Proposisi majemuk juga dapat digabungkan lagi dengan proposisi lain, seperti proposisi atomik

Modus Ponens dan Tautologi

  • Modus ponens adalah pola logika lama: jika A benar dan A → B benar, maka B juga benar
    • Bentuknya adalah (A ∧ (A ⇒ B)) → B
    • Ini dapat dinyatakan dengan contoh seperti “Socrates adalah manusia, dan jika manusia pasti mati, maka Socrates pasti mati”
  • Logika tidak hanya menangani satu operasi, tetapi juga kombinasi dan relasi berbagai operasi logika
    • Relasi antara and dan implies tampak dalam modus ponens
    • Hukum distributif antara and dan or juga menjadi objek perhatian utama
  • Tautologi adalah proposisi yang selalu benar, terlepas dari nilai benar/salah proposisi-proposisi penyusunnya
    • Modus ponens selalu benar sebagai keseluruhan rumus, baik A maupun B benar atau salah
    • Proposisi yang selalu salah disebut kontradiksi
    • Jika not ditempelkan pada tautologi, hasilnya kontradiksi; jika not ditempelkan pada kontradiksi, hasilnya tautologi
  • Proposisi yang kebenarannya berubah bergantung pada nilai disebut contingent statement, dan berada di luar perhatian utama logika
  • Tautologi paling sederhana adalah hukum identitas, yaitu bahwa setiap proposisi mengimplikasikan dirinya sendiri

Skema Aksioma dan Sistem Logika

  • Tautologi menjadi dasar bagi skema aksioma dan aturan inferensi
  • Skema aksioma adalah rumus yang berisi placeholder; dengan mengganti placeholder itu dengan proposisi, kita dapat membuat proposisi konkret
    • Jika warna atau proposisi konkret dihapus dari modus ponens, tersisa struktur umum
    • Dengan memasukkan proposisi atomik atau majemuk ke struktur itu, kita dapat membuat proposisi modus ponens tertentu
  • Aturan inferensi dapat digunakan dengan cara yang hampir sama seperti skema aksioma, dan skema aksioma juga dapat diterapkan seperti aturan inferensi
  • Semua tautologi dapat digunakan sebagai skema aksioma
  • Sistem logika atau sistem formal adalah kumpulan skema aksioma dan aturan inferensi, yang digunakan untuk menghasilkan semua proposisi yang mungkin
    • Sebagai contoh, disajikan sebuah sistem yang terdiri dari lima skema aksioma dan aturan inferensi modus ponens
    • Fakta bahwa sistem logika semacam ini lengkap berkaitan dengan teorema kelengkapan Gödel

Interpretasi Fungsi Kebenaran dalam Logika Klasik

  • Logika klasik didasarkan pada dikotomi bahwa proposisi adalah salah satu dari benar atau salah
  • Dalam interpretasi klasik, proposisi dan operator didefinisikan sebagai berikut
    • Proposisi adalah sesuatu yang benar atau salah seperti nilai Boolean
    • Operator logika adalah fungsi yang menerima satu atau lebih nilai Boolean dan mengembalikan nilai Boolean
  • Negasi ¬p adalah operasi uner yang mengubah benar menjadi salah dan salah menjadi benar
    • Hal yang sama dapat dinyatakan dengan tabel kebenaran
    • Eliminasi negasi ganda dibuktikan dengan cara bahwa menerapkan negasi dua kali mengembalikan nilai awal
  • and menerima dua nilai Boolean dan mengembalikan benar hanya ketika keduanya benar
    • p ∧ q → p
    • p ∧ q → q
  • or mengembalikan benar jika salah satu dari dua nilai Boolean benar
    • p → p ∨ q
    • q → p ∨ q
  • implies atau material condition ditulis sebagai p → q, dan salah hanya ketika p benar dan q salah
    • Dalam logika klasik, p → q sama dengan kasus ketika ¬p ∨ q benar
  • if and only if atau iff benar ketika dua proposisi memiliki nilai yang sama
    • P ↔ Q ekuivalen dengan P → Q ∧ Q → P
  • Selain dengan tabel kebenaran, ekuivalensi p → q dan ¬p ∨ q juga dapat dibuktikan dengan aksioma dan aturan inferensi
    • Bukti ekuivalensi penuh memerlukan pembuktian dua arah

Logika Intuisionistik dan Interpretasi BHK

  • Logika intuisionistik memandang bukti sebagai konstruksi, bukan penemuan kebenaran universal
  • Dari sudut pandang ini, dikotomi bahwa setiap proposisi pasti benar atau salah tidak dapat digunakan
    • Suatu proposisi bisa tidak terbukti bukan karena salah, melainkan karena berada di luar cakupan sistem logika yang diberikan
    • Konjektur prima kembar sering diajukan sebagai contoh seperti ini
  • Dalam interpretasi Brouwer–Heyting–Kolmogorov(BHK), bukti ditempatkan di pusat, bukan proposisi
    • Proposisi adalah sesuatu yang memiliki bukti
    • Operator logika adalah konstruksi yang membuat bukti dari bukti-bukti lain
  • Bukti A ∧ B adalah pasangan yang terdiri dari bukti A dan bukti B, yaitu product
  • A → B berarti ada fungsi yang mengubah bukti A menjadi bukti B
    • Himpunan bukti A → B dinyatakan sebagai himpunan fungsi dari A ke B, yaitu hom-set
    • Jika himpunan ini kosong, tidak ada cara untuk mengubah bukti A menjadi bukti B
  • Dalam interpretasi BHK tidak ada operator iff terpisah, tetapi ada panah
    • Ketika ada fungsi dari A ke B dan dari B ke A, kedua proposisi diperlakukan seperti ekuivalen
    • Dari sudut pandang himpunan, ini adalah situasi ketika himpunan bukti kedua proposisi isomorfik
  • Negasi bukan sekadar berarti tidak ada bukti; harus ditunjukkan bahwa jika A diasumsikan benar, maka akan tercapai kontradiksi
    • ⊥ berperan sebagai bukti untuk rumus yang tidak memiliki bukti, yaitu False atau bottom value
    • Dalam BHK, ¬A dibaca sebagai A → ⊥
    • Dalam teori himpunan, ⊥ dinyatakan sebagai himpunan kosong

Melihat Logika sebagai Kategori

  • Interpretasi BHK memberikan sudut pandang tingkat tinggi untuk menafsirkan logika dengan teori kategori
  • Sebagian kategori dapat dilihat seperti sistem logika
    • Objek adalah proposisi
    • Morfisme adalah bukti
  • Tidak semua kategori menjadi sistem logika; diperlukan syarat agar ada objek yang berkorespondensi dengan proposisi logika yang valid dan tidak ada objek yang berkorespondensi dengan proposisi yang tidak valid
  • Kategori yang memenuhi syarat seperti itu disebut bicartesian closed category
  • Sebagai kasus sederhana, jika terlebih dahulu melihat orde, sistem logika dan himpunan proposisi atomik membentuk kategori
    • Jika hanya ada satu cara dari A ke B, atau perbedaannya diabaikan, hasilnya menjadi preorder
    • Jika proposisi-proposisi yang saling mengikuti dipandang ekuivalen, hasilnya menjadi partial order
    • A ≤ B berarti A → B
  • Dalam diagram Hasse, ketika A berada di bawah B, maka A → B berlaku

Korespondensi Teoretis-Orde dari Operasi Logika

  • and dan or dalam logika muncul sebagai product dan sum dalam interpretasi BHK, dan dalam teori orde berkorespondensi dengan meet dan join
  • Agar menjadi sistem logika, sembarang dua proposisi harus dapat digabungkan dengan and atau or, sehingga orde harus memiliki meet dan join untuk semua elemen
    • Orde seperti ini disebut lattice
  • Hukum penting antara and dan or adalah distributivitas
    • Jika untuk semua A, B, C berlaku A ∧ (B ∨ C) ≅ (A ∧ B) ∨ (A ∧ C), maka itu adalah distributive lattice
  • Untuk merepresentasikan logika intuisionistik, lattice juga harus memiliki elemen yang berkorespondensi dengan True dan False
    • False ditulis sebagai ⊥, dan terkait dengan prinsip ledakan, yaitu jika ada bukti False maka proposisi apa pun dapat dibuktikan
    • True ditulis sebagai ⊤; ia mengikuti dari semua proposisi, tetapi dari dirinya sendiri tidak keluar isi yang bermakna
  • Dalam orde, True dan False masing-masing adalah greatest object dan least object
    • Dalam istilah teori kategori, keduanya berkorespondensi dengan terminal object dan initial object
    • Lattice yang memiliki least dan greatest disebut bounded lattice

Objek Implikasi dan Objek Eksponensial

  • Lattice yang merepresentasikan sistem logika memerlukan objek implikasi untuk setiap pasangan A, B, yaitu proposisi yang menyatakan bahwa A mengimplikasikan B
  • Objek ini didefinisikan melalui struktur modus ponens
    • A ∧ (A ⇒ B) → B harus berlaku
  • Syarat ini saja tidak cukup
    • Objek lain seperti A ⇒ B ∧ C atau A ⇒ B ∧ C ∧ D juga dapat masuk ke posisi yang sama
    • A ⇒ B yang sebenarnya adalah objek terbesar di antara X yang memenuhi A ∧ X → B
  • Dalam teori orde, A ⇒ B disebut exponential element atau relative pseudo-complement
    • Ini adalah X terbesar yang memenuhi A ∧ X ≤ B
  • Secara logis, X yang merupakan proposisi paling trivial yang memenuhi A ∧ X → B adalah proposisi implikasi A ⇒ B
  • Secara teori kategori, ini didefinisikan sebagai exponential object atau internal homomorphism object
    • Harus ada morfisme A × X → B
    • Dari objek kandidat lain dengan sifat yang sama, harus ada morfisme unik menuju objek eksponensial yang sebenarnya
  • Definisi objek implikasi ini sesuai dengan logika intuisionistik
    • Dalam logika klasik, karena hukum excluded middle, A ⇒ B disederhanakan menjadi ¬A ∨ B
  • Seperti meet, join, dan objek implikasi, A ⇒ B juga didefinisikan hingga isomorfisme unik

Heyting Algebra dan Bicartesian Closed Category

  • Logika intuisionistik terdiri dari True, False, and, or, implies
  • Jika direpresentasikan sebagai orde, hasilnya adalah Heyting algebra
    • Memiliki join dan meet
    • Memiliki objek greatest dan least
    • Memiliki objek implikasi
  • Sistem logika intuisionistik dapat dilihat sebagai Heyting algebra
    • and dan or adalah meet dan join
    • True dan False adalah greatest dan least object
    • implies adalah exponential object
  • Jika definisi yang sama diubah agar sesuai dengan kategori umum, hasilnya adalah bicartesian closed category
    • Memiliki product dan coproduct
    • Memiliki initial dan terminal object
    • Memiliki exponential object
  • Sistem logika intuisionistik juga dapat dilihat sebagai bicartesian closed category
    • and dan or adalah product dan coproduct
    • True dan False adalah terminal dan initial object
    • implies adalah exponential object
  • Lattice yang mengikuti logika klasik harus complemented selain bounded dan distributive
    • Untuk setiap proposisi A, ada ¬A yang unik dan memenuhi A ∨ ¬A = 1, A ∧ ¬A = 0
    • Lattice seperti ini disebut Boolean algebra

Bukti Sederhana dari Sudut Pandang Logika Kategoris

  • A ∨ ⊤ ≅ ⊤ langsung mengikuti dari definisi join
    • Join adalah batas atas terkecil yang lebih besar dari atau sama dengan dua objek
    • Karena satu-satunya objek yang lebih besar dari atau sama dengan ⊤ adalah ⊤ itu sendiri, join dari sembarang A dan ⊤ adalah ⊤
    • Secara logis, ini adalah tautologi “sembarang A atau True adalah True”
  • Jika ada A → B, maka A ∨ B = B
    • Jika salah satu dari dua objek berada di atas yang lain, join adalah objek yang lebih atas
    • Ini dapat dilihat sebagai generalisasi dari A ∨ ⊤ = ⊤
    • Sebab untuk semua objek A, selalu berlaku A → ⊤
  • Hukum identitas juga dibuktikan dengan objek implikasi
    • A ⇒ A adalah X terbesar yang memenuhi A ∧ X → A
    • Syarat ini berlaku untuk semua X, sehingga menjadi objek terbesar ⊤
    • Karena itu A → A selalu benar
  • Jika A adalah semantic consequence A ⊨ B, yaitu mengimplikasikan B di semua model, maka A ⇒ B juga berkorespondensi dengan ⊤
    • Karena A sendiri sudah mengimplikasikan B, A ∧ X → B berlaku untuk semua X
    • Ini juga disebut deduction theorem

Membuat Logika dengan Free Heyting Algebra

  • Untuk menjalankan logika, pertama-tama pilih proposisi atomik yang akan digunakan sesuai domain masalah
  • Jika jenis logika yang dipilih adalah logika intuisionistik, proposisi majemuk seperti A ∧ B dan A ∨ B untuk semua A, B harus digambarkan sebagai graf
  • Karena komposisi dari proposisi majemuk juga harus dimasukkan kembali, daftar keseluruhannya menjadi tak hingga
  • Proposisi mana yang mengimplikasikan proposisi lain diperiksa dengan mengikuti jalur panah yang keluar dari proposisi awal
  • Menjalankan logika adalah proses mencari jalur dari hal yang sudah diketahui menuju hal yang ingin dibuktikan, atau menyusun bukti dengan memanipulasi bukti yang sudah dimiliki
  • Dalam logika intuisionistik, umumnya sulit membuktikan bahwa suatu fakta tidak dapat dicapai dari aksioma, yaitu bahwa fakta itu tidak dapat dibuktikan

Bacaan terkait

1 komentar

 
GN⁺ 2024-10-27
Komentar Hacker News

  • Halaman ini benar-benar luar biasa, dan saya beberapa kali menemukannya saat mempelajari materi terkait
    Meski begitu, saya lebih memilih belajar dari Milewski. Mempelajari ini adalah sebuah perjalanan, dan penulis ct-illustrated tampaknya masih berada di tengah perjalanan itu
    Milewski sudah menempuh jalan itu berkali-kali, jadi buku dan blognya merupakan titik awal yang bagus
    https://github.com/hmemcpy/milewski-ctfp-pdf Buku
    https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • Saya membaca belasan bab awal Milewski; beberapa bab pertama benar-benar bagus, tetapi gaya penulisannya yang tidak memberikan definisi dan notasi yang presisi makin lama makin menjengkelkan
      Sepertinya ia menganggap apa pun jadi lebih mudah dipahami jika ditulis dalam prosa yang ringan dan tidak presisi, tetapi akibatnya hampir tidak berguna sebagai buku referensi
      Sama sekali tidak begitu¹
      ¹) https://news.ycombinator.com/item?id=41756286
    • Karena saya tidak mengerti apa yang dikatakan bartoszmilewski, buku itu tampaknya tidak berguna bagi saya
      Namun di tempat kerja, saya menggunakan teori kategori untuk seluruh model domain saya

  • Ini dulu sudah pernah dibahas di URL lain
    https://news.ycombinator.com/item?id=28660131 (2 komentar)
    https://news.ycombinator.com/item?id=28660157 (112 komentar)

  • Di bagian awal buku, saat membandingkan matematika dengan sains atau rekayasa, saya menemukan kalimat keren seperti ini
    “Karena itu, matematikawan berada dalam posisi yang aneh, bahkan bisa dibilang unik, di mana mereka harus terus-menerus membela apa yang mereka lakukan dari sudut pandang nilainya bagi bidang studi lain. Perlu ditegaskan lagi, untuk bidang studi lain mana pun, hal seperti ini akan dianggap absurd.”
    Ini konsep yang bisa dipahami siapa pun yang pernah mempelajari bidang yang tidak langsung menghasilkan uang, dan menyenangkan mendengar bahwa orang-orang berbakat di bidang angka pun harus berhadapan dengan pisau cukur Milton Friedman

    • Kalau begitu, syukurlah banyak proyek dalam “kajian budaya” sebenarnya didanai langsung oleh Departemen Pertahanan dan Departemen Luar Negeri AS
      Seluruh kajian “pascakolonial” saat ini tidak lebih dari backend soft power Amerika Serikat, dan jika perang pecah, mungkin juga akan menjadi backend hard power

  • Diagram lingkaran di dalam lingkaran tidak akan bertahan baik saat diskalakan jika lingkaran-lingkaran di bagian dalam selalu ditempatkan di tengah secara vertikal

  • Apakah ada kisah sukses yang menggunakan teori kategori untuk menyelesaikan masalah CS/SWE secara bermanfaat yang sebelumnya tidak bisa diselesaikan tanpa teori kategori? Monad tidak termasuk. Karena itu sesuatu yang akan tercipta secara alami jika situasinya memang membutuhkannya
    Saya mempelajarinya selama 1 tahun di pascasarjana, tetapi akhirnya menyerah

    • Tidak ada masalah yang tidak bisa dimodelkan tanpa teori kategori
      Salah satu teorema paling mendasar dalam teori kategori, lemma Yoneda, secara langsung mengatakan bahwa setiap masalah yang dinyatakan dalam bahasa kategori dapat diterjemahkan ke dalam bahasa himpunan dan fungsi. Hal yang sama berlaku untuk semua objek matematika yang didefinisikan sebagai himpunan, sehingga nama apa pun selalu bisa diganti dengan definisinya
      Kontribusi bahasa kategoris terhadap kerangka implisit suatu teori tidak mungkin lebih besar daripada definisi “kategori” itu sendiri, dan definisi itu sangat kecil. Ini mirip dengan bertanya mengapa memakai grup jika “operasi pada himpunan yang memiliki asosiativitas, ketertutupan, identitas, dan invers” terasa lebih mudah didekati
      Aljabar abstrak didasarkan pada pustaka definisi untuk tipe-tipe operasi pada himpunan yang cukup sederhana hingga cukup sering muncul. Alat atau teknik bukanlah sesuatu yang bisa ditemukan di dalam definisi
      Ring, ruang vektor, dan modul biasanya langsung diterima begitu saja, tetapi kategori memecah orang menjadi yang percaya dan yang tidak. Saya penasaran mengapa itu terjadi
    • Contoh paling dekat yang saya tahu adalah pekerjaan pada UMAP
      Saat saya mewawancarai Leland McInnes, ia menjelaskan secara rinci bahwa meski teori kategori tidak mutlak diperlukan dalam kode aktual dari hasil akhirnya, teori kategori berperan besar dalam menghubungkan banyak titik
      Melihat peningkatan relatifnya dibanding teknik mutakhir sebelumnya, t-SNE, ini satu-satunya contoh yang membuat saya meninjau ulang kritik saya terhadap cara teori kategori dibicarakan dalam perangkat lunak
      https://arxiv.org/abs/1802.03426
    • Ini mirip dengan bertanya, “Apakah ada kisah sukses pergi ke tempat dengan mobil yang tidak bisa dicapai dengan berjalan kaki?”
      Teori kategori adalah bahasa sekaligus alat, jadi apa yang bisa dikatakan dalam bahasa teori kategori juga bisa dikatakan dalam bahasa lain
      Seperti mobil, jika Anda belajar mengemudikannya—dan kurva belajarnya memang sangat curam—Anda bisa sampai lebih cepat. Pada prinsipnya, tidak ada tempat yang benar-benar tidak bisa dicapai dengan berjalan kaki tanpa menyebut konsep teori kategori secara eksplisit
    • Jika sesuatu yang sudah dipahami dirumuskan ulang dalam kerangka yang lebih umum, Anda bisa melihat lebih jelas apa arti sebenarnya dan memisahkan esensi dari detail-detail yang berantakan
      Sejauh pemahaman saya yang sangat terbatas, mencirikan objek melalui sifat universal adalah bagian penting dari teori kategori
      Kegunaan praktis lain dari teori kategori adalah memberikan bahasa bersama bagi ilmuwan komputer, matematikawan, dan fisikawan. Kolaborasi tidak mudah jika semua orang menyebut pola yang sama dengan nama berbeda dan definisi yang sedikit tidak kompatibel
    • Topos Institute sedang membuat perangkat lunak baru yang diharapkan terlihat jauh lebih transparan bagi orang-orang yang belum meminum Kool-Aid teori kategori
      Pra-alfa saat ini terutama untuk pemodelan dinamika sistem, tetapi saya rasa fondasi kategoris esensial untuk cakupan pekerjaan yang dituju. Saya senang mendengar pendapat siapa pun
      https://topos.site/blog/2024-10-02-introducing-catcolab/

  • Saya pikir teori kategori berguna, tetapi sepertinya belum untuk komputasi
    Jika tidak benar-benar membutuhkannya, wajar saja terasa sulit. Apakah Anda benar-benar perlu memahami sifat universal, funktor adjungsi, dan lemma Yoneda? Jika tidak perlu, Anda akan kesulitan mempelajari apa itu semua
    Menariknya, pengalaman pemrograman fungsional membantu memahami teori kategori, tetapi sebaliknya tidak terlalu. Misalnya, polimorfisme parametrik memberi intuisi tentang transformasi natural, dan transformasi natural adalah inti dari semua penerapan teori kategori
    Penerapan teori kategori yang meyakinkan sangat matematis. Bisa ditemukan dalam topologi aljabar, teori representasi, geometri aljabar, dan logika nonklasik

  • Ada kesalahan
    “Modus ponens adalah proposisi yang terdiri dari dua proposisi lain, di sini ditandai sebagai A dan B, dan mengatakan bahwa jika proposisi A benar dan proposisi A --> B juga benar, yaitu jika A mengimplikasikan B, maka B juga benar. Misalnya, jika kita tahu ‘Sokrates adalah manusia’ dan ‘manusia itu mati’, maka kita juga tahu ‘Sokrates itu mati’.”
    Contoh ini bukan kasus modus ponens, aturan dalam logika proposisional, melainkan silogisme kategoris yang membutuhkan logika predikat

  • Di sini dikatakan “logika adalah ilmu tentang yang mungkin”, tetapi bukankah logika seharusnya menjadi ilmu tentang yang pasti?
    Menurut saya intinya adalah memungkinkan kita mengatakan secara pasti apa yang valid dan apa yang tidak

  • Notasi diagramnya menarik
    Apakah penulis juga menyajikan aturan inferensi untuk transformasi diagram yang mempertahankan kebenaran?