Teori Pembuktian: Sebuah Kajian Pembuktian dengan Logika, Filsafat, Semantik dan Aljabar

BENDA apa itu Teori Pembuktian? 

Teori Pembuktian mungkin sangat asing di Indonesia dikarenakan topik yang satu ini lebih booming di negara seberang dibanding negara sendiri. Apalagi di Indonesia ilmu logika matematika lebih diteliti dalam segi penerapannya dibanding perluasan teorinya, juga sangat jarang matematikawan Indonesia yang berkecimpung di cabang Landasan Matematika, padahal di negeri seberang ilmu seperti Teori Pembuktian sudah berkembang jauh dari sekedar teori sampai penerapannya pada mesin belajar dan kecerdasan buatan. Baik, sekarang kita fokus dalam membahas apa itu teori pembuktian. 

Teori Pembuktian (Proof Theory), secara sederhana, adalah salah satu kajian dalam matematika dalam mempelajari struktur pembuktian matematika. Menurut Wikipedia, teori pembuktian merupakan cabang dari logika matematika yang menunjukkan pembuktian layaknya objek matematika secara formal, memfasilitasi analisisnya dengan teknik matematika. Menurut S. Buss dalam bukunya, Handbook of Proof Theory, dijelaskan bahwa Teori Pembuktian adalah bidang matematika yang mempelajari konsep pembuktian matematika dan keterbuktian matematika.

Pada dasarnya, pembuktian matematika ditunjukkan sebagai struktur data yang didefinisikan secara induktif misalnya seperti daftar, pohon (pohon seperti dalam teori graf), atau lainnya, yang dikonstruksi berdasarkan aksioma dan aturan inferensi dalam sistem logika. Karena 'pembuktian' memegang peranan penting dalam matematika sebagai sarana dalam mencapai kebenaran atau kesalahan suatu proposisi matematika; Teori Pembuktian, pada prinsipnya, studi dasar semua matematika. Tentu saja, penggunaan Teori Pembuktian sebagai dasar matematika tampak aneh karena Teori Pembuktian sendiri merupakan subbidang matematika. Bersama dengan Teori Model, Teori Himpunan Aksiomatik, dan Teori Rekusi, Teori Pembuktian adalah salah satu dari 4 pilar landasan matematika.

Teori Pembuktian sangat penting dalam filsafat logika, dimana ketertarikan utamanya adalah ide sebuah Pembuktian Teoritik Semantik, sebuah ide yang bergantung pada ide-ide teknis dalam Teori Pembuktian Struktural untuk menjadi layak.

Sejarah Teori Pembuktian

 Sumber: http://singularityweblog.zippykid.netdna-cdn.com

Pada pergantian abad kesembilan belas, matematika menunjukkan gaya berargumentasi yang lebih eksplisit ke arah komputasional daripada yang umum saat ini. Selama abad ini, pengenalan metode aljabar abstrak membantu menyatukan perkembangan dalam analisis, teori bilangan, geometri, dan teori persamaan, dan pekerjaan oleh matematikawan seperti Dedekind, Cantor, dan Hilbert menjelang akhir abad ini memperkenalkan bahasa himpunan teoritik dan metode penyatuan yang berfungsi untuk mengecilkan atau menekan sisi komputasional matematika. Pergeseran dalam penekanan dari perhitungan memunculkan kekhawatiran apakah metode tersebut bermakna, atau sesuai dengan matematika. Penemuan paradoks yang berasal dari penggunaan terlalu naif bahasa himpunan teoretik dan metode menyebabkan bahkan lebih mendesak kekhawatiran mengenai apakah metode modern bahkan konsisten. Hal ini menyebabkan perdebatan sengit di awal abad kedua puluh dan apa yang kadang-kadang disebut "krisis landasan (crisis of foundation)".

Dalam ceramahnya pada 1922, David Hilbert memperkenalkan Beweistheorie, atau Teori Pembuktian (Proof Theory), yang bertujuan membenarkan penggunaan metode modern untuk menyelesaikan masalah yang sangat mendasar untuk selamanya. Hal ini, menurut Hilbert, dapat dicapai dengan hal-hal berikut:

• Pertama, sebagai bagian dari abstrak, infinitary penalaran matematika dalam pertanyaan menggunakan sistem aksiomatik formal, yang menentukan sebuah bahasa formal yang ditetapkan dan mempresisikan aturan inferensi.
• Lalu melihat bukti dalam sistem ini sebagai objek kombinatorik, finit, dan membuktikan konsistensinya. Misalnya fakta bahwa tidak terdapat cara untuk men-derivasi sebuah kontradiksi - menggunakan argumen 'konkrit tidak objektif (unobjectionable).

Dengan begitu, menurut Hilbert, "...kita bergerak menuju tingkat tinggi dari kontemplasi (kebulatan pikiran), dari yang mana aksioma-aksioma, formula-formula, dan bukti-bukti teori matematika adalah dirinya sendiri sebagai objek sebuah investigasi contentional. Tapi untuk tujuan ini ide konsensus biasa dari teori matematika harus digantikan oleh formula dan aturan-aturan, dan ditiru oleh formalisme. Dengan kata lain, kita harus memiliki formalisasi ketat dari keseluruhan teori matematika... Dalam cara ini pemikiran kontentual (yang mana tentu saja tidak bisa sepenuhnya bisa dihilangkan) disingkirkan sebagaimana mestinya; dan diwaktu yang sama hal ini menjadi mungkin untuk menarik perbedaan yang tajam dan sistematis dalam matematika antara rumus dan bukti-bukti resmi di satu sisi, dan ide-ide kontentual di sisi lainnya."

Saat ini, Teori Pembuktian bisa diperlihatkan sebagai studi umum mengenai sistem deduktif formal. Perlu diketahui bahwa sistem formal ini bisa digunakan untuk memodelkan tipe inferensi yang lebih luas - modal, temporal, probabilistik, induktif, defisibel, deontic, dan lain-lain - pekerjaan dalam bidang ini sangat luas dan bervariasi. Disini, kita memfokuskan bahwa Teori Pembuktian dari Penalaran Matematis, tapi walaupun dengan batasan ini, bidang ini sangat 'luas'.

Sumber:
en.wikipedia.org/wiki/proof_theory
http://plato.stanford.edu/entries/proof-theory-development/#LatDevAppSeqCal
Jeremy Avigad, Proof Theory