Sejak awal, logika matematika telah berkontribusi, dan telah dimotivasi oleh, studi tentang dasar matematika. Studi ini dimulai pada akhir abad ke-19
dengan pengembangan kerangka aksiomatik untuk geometri, aritmatika, dan analisis. Pada awal abad ke-20 itu dibentuk oleh program David Hilbert untuk membuktikan konsistensi teori dasar. Hasil dari Kurt Gödel, Gerhard Gentzen, dan lainnya memberikan resolusi parsial untuk program, dan mengklarifikasi masalah
yang terlibat dalam membuktikan konsistensi. Pekerjaan dalam teori himpunan menunjukkan bahwa hampir semua matematika biasa dapat diformalkan dalam bentuk himpunan, meskipun ada beberapa teorema
yang tidak dapat dibuktikan dalam sistem aksioma umum untuk teori himpunan. Pekerjaan kontemporer di dasar matematika sering berfokus pada penetapan bagian matematika mana
yang dapat diformalkan dalam sistem formal tertentu (seperti dalam matematika terbalik) daripada mencoba menemukan teori di mana semua matematika dapat dikembangkan.
Logika matematika diklasifikasikan menjadi empat subbidang. Mereka:
Nama-nama awal untuk logika matematika adalah logika simbolik (sebagai lawan dari logika filosofis) dan metamatematika. Istilah pertama masih digunakan (seperti dalam Asosiasi Logika Simbolik), tetapi istilah terakhir sekarang digunakan untuk aspek-aspek tertentu dari teori pembuktian.
Sejarah
Logika matematika adalah nama
yang diberikan oleh Giuseppe Peano untuk apa
yang juga dikenal sebagai logika simbolik. Dalam versi klasiknya, aspek dasarnya menyerupai logika Aristoteles, tetapi ditulis menggunakan notasi simbolik daripada bahasa alami. Upaya untuk memperlakukan operasi logika formal
dengan cara simbolis atau aljabar dilakukan oleh beberapa matematikawan
yang lebih filosofis, seperti Leibniz dan Lambert; tetapi kerja keras mereka tetap sedikit diketahui dan terisolasi. Adalah George Boole dan kemudian Augustus De Morgan, di pertengahan abad kesembilan belas,
yang menyajikan cara matematis
yang sistematis mengenai logika. Doktrin logika tradisional Aristotelian direformasi dan diselesaikan; dan darinya dikembangkan instrumen untuk menyelidiki konsep dasar matematika. Akan menyesatkan untuk mengatakan bahwa kontroversi mendasar
yang hidup pada periode 1900–1925 semuanya telah diselesaikan; tetapi filsafat matematika sangat diperjelas oleh logika "baru".
Sementara perkembangan logika Yunani sangat menekankan pada bentuk-bentuk argumen, sikap logika matematika saat ini dapat diringkas sebagai studi kombinatorial konten. Ini mencakup dimensi sintaksis dan semantik. Sintaksis berkaitan
dengan struktur
yang benar atau formal dari string simbol dalam bahasa formal, seperti, misalnya, mengirim string dari bahasa formal ke program compiler untuk menulisnya sebagai urutan instruksi mesin. Semantik berkaitan
dengan interpretasi atau penggunaan serangkaian simbol, seperti, misalnya, membangun model tertentu atau seluruh rangkaiannya, dalam teori model. Kajian matematika ini dari luar dikenal
dengan istilah metamatematika.
Beberapa publikasi penting adalah Begriffsschrift oleh Gottlob Frege, Studies in Logic oleh Charles Peirce, Principia Mathematica oleh Bertrand Russell dan Alfred North Whitehead, dan On Formal Undecidable Propositions of Principia Mathematica and Related Systems oleh Kurt Gödel.
Logika formal
Pada intinya, logika matematika berkaitan
dengan konsep matematika
yang diekspresikan menggunakan sistem logika formal. Sistem logika orde pertama adalah
yang paling banyak dipelajari karena penerapannya pada dasar matematika dan karena sifat-sifatnya
yang diinginkan. Logika klasik
yang lebih kuat seperti logika orde kedua atau logika infinitary juga dipelajari, bersama
dengan logika nonklasik seperti logika intuitionistic.
Bidang logika matematika
"Handbook of Mathematical Logic" karya Barwise (1977) membagi logika matematika menjadi empat bagian:
Teori himpunan adalah studi tentang himpunan,
yang merupakan kumpulan abstrak dari objek. Konsep dasar teori himpunan seperti himpunan bagian dan komplemen relatif sering disebut teori himpunan naif. Penelitian modern berada di bidang teori himpunan aksiomatik,
yang menggunakan metode logis untuk mempelajari proposisi mana
yang dapat dibuktikan dalam berbagai teori formal seperti teori himpunan Zermelo-Frankel,
yang dikenal sebagai ZFC, atau teori himpunan Yayasan Baru,
yang dikenal sebagai NF.
Teori pembuktian adalah studi tentang bukti formal dalam berbagai sistem deduksi logis. Bukti-bukti ini direpresentasikan sebagai objek matematika formal, memfasilitasi analisis mereka
dengan teknik matematika. Frege bekerja pada bukti matematis dan memformalkan gagasan tentang bukti.
Teori model mempelajari model dari berbagai teori formal. Himpunan semua model teori tertentu disebut kelas dasar. Teori model klasik berusaha untuk menentukan sifat-sifat model dalam kelas dasar tertentu, atau menentukan apakah kelas struktur tertentu membentuk kelas dasar. Metode eliminasi quantifier digunakan untuk menunjukkan bahwa model teori tertentu tidak bisa terlalu rumit.
Teori rekursi, juga disebut teori komputabilitas, mempelajari sifat-sifat fungsi
yang dapat dihitung dan derajat Turing,
yang membagi fungsi
yang tidak dapat dihitung menjadi himpunan
yang memiliki tingkat tidak dapat dihitung
yang sama. Bidang ini telah berkembang untuk memasukkan studi komputabilitas umum dan definabilitas. Di bidang ini, teori rekursi tumpang tindih
dengan teori bukti dan teori himpunan deskriptif
yang efektif.
Garis batas antara bidang-bidang ini, dan juga antara logika matematika dan bidang matematika lainnya, tidak selalu tajam; misalnya, teorema ketidaklengkapan Gödel menandai tidak hanya tonggak sejarah dalam teori rekursi dan teori pembuktian, tetapi juga mengarah pada teorema Loeb,
yang penting dalam logika modal. Bidang matematika teori kategori menggunakan banyak metode aksiomatik formal
yang mirip
dengan yang digunakan dalam logika matematika, tetapi teori kategori biasanya tidak dianggap sebagai subbidang logika matematika.
Ada banyak hubungan antara logika matematika dan ilmu komputer. Banyak pionir awal dalam ilmu komputer, seperti Alan Turing, juga matematikawan dan ahli logika.
Kajian teori komputabilitas dalam ilmu komputer erat kaitannya
dengan kajian komputabilitas dalam logika matematika. Namun ada perbedaan penekanan. Ilmuwan komputer sering fokus pada bahasa pemrograman konkret dan komputabilitas
yang layak, sementara peneliti dalam logika matematika sering fokus pada komputabilitas sebagai konsep teoritis dan noncomputability.
Studi tentang semantik bahasa pemrograman terkait
dengan teori model, seperti halnya verifikasi program (khususnya, pengecekan model). Isomorfisme Curry-Howard antara pembuktian dan program berhubungan
dengan teori pembuktian; logika intuitionistic dan logika linier
yang signifikan di sini. Kalkulus seperti kalkulus lambda dan logika kombinatori saat ini dipelajari terutama sebagai bahasa pemrograman
yang diidealkan.
Ilmu komputer juga berkontribusi pada matematika
dengan mengembangkan teknik untuk pemeriksaan otomatis atau bahkan menemukan bukti, seperti pembuktian teorema otomatis dan pemrograman logika.
Hasil terobosan
Teorema Löwenheim–Skolem (1919) menunjukkan bahwa jika himpunan kalimat dalam bahasa orde pertama
yang dapat dihitung memiliki model tak hingga, maka ia memiliki setidaknya satu model untuk setiap kardinalitas tak hingga.
Teorema kelengkapan Gödel (1929) menetapkan kesetaraan antara definisi semantik dan sintaksis konsekuensi logis dalam logika orde pertama.
Teorema ketidaklengkapan Gödel (1931) menunjukkan bahwa tidak ada sistem formal
yang cukup kuat
yang dapat membuktikan konsistensinya sendiri.
Ketidakterpecahan algoritmik dari Entscheidungsproblem,
yang didirikan secara independen oleh Alan Turing dan Alonzo Church pada tahun 1936, menunjukkan bahwa tidak ada program komputer
yang dapat digunakan untuk memutuskan
dengan benar apakah pernyataan matematis arbitrer itu benar.
Independensi hipotesis kontinum dari ZFC menunjukkan bahwa bukti dasar atau penolakan hipotesis ini tidak mungkin. Fakta bahwa hipotesis kontinum konsisten
dengan ZFC (jika ZFC sendiri konsisten) dibuktikan oleh Gödel pada tahun 1940. Fakta bahwa negasi hipotesis kontinum konsisten
dengan ZFC (jika ZFC konsisten) dibuktikan oleh Paul Cohen pada tahun 1963 .
Ketidakterpecahan algoritmik dari masalah kesepuluh Hilbert,
yang dibuat oleh Yuri Matiyasevich pada tahun 1970, menunjukkan bahwa tidak mungkin bagi program komputer mana pun untuk memutuskan
dengan benar apakah polinomial multivariat
dengan koefisien bilangan bulat memiliki akar bilangan bulat.
Posting Komentar