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

Read More

Bukti Formal V.S. Bukti Informal

Pernahkah anda (khususnya mahasiswa matematika atau mereka yang pernah ikut olimpiade matematika) disuruh membuktikan suatu teorema matematika? PASTINYA! Kalo gak pernah saya ragu kalau anda adalah mahasiswa matematika :D

Ya, melakukan pembuktian adalah suatu hal yang rutin dilakukan oleh para mahasiswa matematika pada umumnya, karena (menurut saya) hal itu akan melatih pola berfikir sebagai calon matematikawan. Bukan matematikawan sejati yang tidak pernah sekalipun membuktikan satu teorema pun.

By the way, pertama saya akan menjelaskan apa itu teorema. Secara sederhana teorema adalah suatu pernyataan yang harus dibuktikan kebenarannya/dapat ditunjukkan kebenarannya. Berbeda dengan aksioma yang tidak perlu pembuktian sama sekali. Dalam hirarki pembuktian matematika, teorema berada di bawah aksioma dan postulat posisinya atau lebih rendah tingkatannya dibanding aksioma dan postulat. Cara-cara pembuktian teoerma sangat beragam, bisa bukti langsung, bukti tak-langsung atau reductio ad absurdum, bukti dengan kasus dan lain sebagainya. Jenis-jenis pembuktian ini akan dijelaskan pada postingan berikutnya.

Sekarang kita fokus kembali mengenai apa itu bukti formal dan bukti informal. Kebanyakan mahasiswa matematika tidak terlalu mengenal apa itu bukti formal dan apa itu bukti informal. Maka dari itu saya akan menjelaskan apa itu bukti formal terlebih dahulu.

Bukti Formal

Bukti formal secara sederhana merupakan suatu langkah pembuktian berdasarkan logika dari himpunan premis dan aksioma. Artinya pembuktian formal adalah pembuktian yang mengikuti aturan inferensi. Secara sederhana, aturan inferensi tampak seperti ini:

 

Dimana p merupakan premis-premis berhingga dan q merupakan konklusi atau kesimpulan. Perlu diketahui bahwa suatu kesimpulan yang benar diperoleh berdasarkan premis-premis yang benar. Hal ini dapat dilihat dari operasi biner . Jika salah satu premis salah maka nilai kebenaran dari  juga salah sehingga kesimpulan yang diperoleh juga salah. Hasil dari pembuktian yang mengikuti aturan inferensi haruslah berupa tautologi, artinya harus selalu bernilai benar.

Sekarang kembali fokus pada bukti formal. Bukti formal pada dasarnya berbentuk langkah-langkah logika, misalnya saya memiliki pernyataan A dan B dan ingin membuktikan bahwa kesimpulannya adalah TIDAK A, maka:

1. 
2.  

Konklusi: .

Pada pembuktian formal biasanya menggunakan komputer untuk mengklarifikasi kebenaran suatu teorema. Banyak sekali program pembuktian matematika yang disebut sebagai Automated Theorem Prover (Pembukti Teorema Otomatis) seperti Isabelle, HOL, Coq, Mizar dan lain sebagainya. Kali ini saya akan menunjukkan salah satu bukti formal mengenai pembuktian adalah bilangan irasional menggunakan Mizar Ver.6.1.11 - 3.33.722:

•  Sketsa Pembuktian Formal: Layout Informal

Theorem Th43: sqrt 2 is irrational :: PYTHAGORAS’STHEOREM
PROOF assume sqrt 2 is rational; consider a, b such that

4_3_1:                                     a^2 = 2 * b^2

and a,b are_relative_prime; a^2 is even; consider c such that a = 2 * c;
4 * c^2 = 2* b^2; 2 * c^2 = b^2; b is even; thus contradiction; END;

• Sketsa Pembuktian Formal: Layout Formal

theorem Th43: sqrt 2 is irrational
proof
  assume sqrt 2 is rational;
  consider a,b such that
4_3_1: a^2 = 2*b^2 and
  a,b are_relative_prime;
  a^2 is even;                                                        *4
  a is even;                                                 *4
  consider c such that a = 2*c;                              *4
  4*c^2 = 2*b^2;                                             *4
  2*c^2 = b^2;                                               *4
  b is even;                                                 *4
  thus contradiction;                                        *1
end;

• Bukti Formal

theorem Th43: sqrt 2 is irrational
proof
  assume sqrt 2 is rational;
  then consider a,b such that 
A1: b <> 0 and
A2: sqrt 2 = a/b and
A3: a,b are_relative_prime by Def1;
A4: b^2 <> 0 by A1,SQUARE_1:73;
 2 = (a/b)^2 by A2,SQUARE_1:def 4
  .= a^2/b^2 by SQUARE_1:69;
  then
4_3_1: a^2 = 2*b^2 by A4,REAL_1:43;
  a^2 is even by 4_3_1,ABIAN:def 1;
  then
A5: a is even by PYTHTRIP:2;
  then consider c such that
A6: a = 2*c by ABIAN:def 1;
A7: 4*c^2 = (2*2)*c^2
  .= 2^2*c^2 by SQUARE_1:def 3
  .= 2*b^2 by A6,4_3_1,SQUARE_1:68;
2*(2*c^2) = (2*2)*c^2 by AXIOMS:16
  .= 2*b^2 by A7;
then 2*c^2 = b^2 by REAL_1:9;
then b^2 is even by ABIAN:def 1;
then b is even by PYTHTRIP:2;
then 2 divides a & 2 divides b by A5,Def2;
then
A8: 2 divides a gcd b by INT_2:33;
  a gcd b = 1 by A3,INT_2:def 4;
  hence contradiction by A8,INT_2:17;
end;

Bukti Informal

Setelah mengetahui apa yang dimaksud dengan bukti formal, apakah anda sudah bisa menebak seperti apa bukti informal? Ya! Bukti informal adalah pembuktian dengan kata-kata sehari-hari seperti "Akan gue buktiin..." atau "Dengan semau gue..." atau "Nah lo bisa liat bahwa terjadi kontradiksi di sini dan di situ". #PLAK #PLAK #WADEZIG! Sori-sori becanda :3 Sebenarnya yang dimaksud dengan bukti informal adalah suatu bentuk pembuktian yang bertujuan untuk menyimpulkan pernyataan baru berdasarkan pernyataan yang sudah diketahui sebelumnya. Bedanya pada pembuktian informal lebih cenderung kepada penulisan bukti dalam bentuk paragraf dibanding hanya bentuk-bentuk logika. Pembuktian dengan bukti informal sangat sering digunakan pada umumnya bagi mereka yang berkecimpung di dunia matematika. Dari bukti informal, seorang ahli matematika/ahli komputer dapat mengkonstruksi bukti formal untuk dibuktikan kebenarannya menggunakan komputer, walaupun untuk mengkonstruksi bukti informal ke bukti formal pada prinsipnya membutuhkan waktu yang cukup lama melelahkan.

Berikut merupakan salah satu bukti informal mengenai pembuktian adalah bilangan irasional oleh G.H. Hardy dan E.M. Wright dalam buku yang berjudul An Introduction to the Theory of Numbers. 4th edition.

Teorema 43 (Teorema Phytagoras). adalah bilangan irasional.
Bentuk pembuktian ini adalah sebagai berikut. Jika adalah rasional, maka persamaan:

                                                            
                                                                            (4.3.1)

memiliki solusi dalam bilangan bulat a, b dengan (a, b) = 1. Karena genap, maka a juga bilangan genap. Jika a = 2c, maka , , dan b juga genap, kontradiksi dengan hipotesis bahwa (a, b) = 1.

Sumber: Nine Formal Proof Sketches oleh Freek Wiedijk, University of Nijmegen

Read More

Mengenai Argumen: Suatu Pendahuluan Logika Simbolik

sumber: blogs.ubc.ca

Misalkan saya memiliki sebuah pernyataan seperti berikut:

Saya percaya bahwa...

        ... Soekarno adalah salah satu presiden Indonesia.

        ... Hukum fisika mengenai kelembaman ditemukan oleh Newton.

        ... Dunia sedang mengalami gejala pemanasan global.

Saya rasa hampir semua orang setuju dengan pernyataan saya. Jelas bahwa Soekarno adalah salah satu presiden Indonesia, bahwa hukum fisika mengenai kelembaman ditemukan oleh Newton dan lain sebagainya. Tapi perlu diketahui bahwa tidak semua hal yang kita percayai mutlak benar.

Beberapa orang mungkin tidak percaya atau tidak setuju dengan pernyataan saya, tentunya dengan berbagai alasan. Misalnya saja bahwa dunia sebenarnya tidak mengalami pemanasan global, bahwa pemanasan global hanyalah teori konspirasi gila yang entah apa tujuannya (kalau penasaran dengan pendapat ini, anda bisa melihatnya disini). Beberapa orang mungkin tidak tahu mengenai apa yang anda pikirkan mengenai orang-orang tersebut, atau anda berfikir bahwa pernyataan mereka jelas salah. Untuk menerima pernyataan mereka, anda membutuhkan sebuah argumen.

Misalnya, saya memiliki sebuah argumen berikut:

"Jika 1/1 = 1, 2/2 = 1, 3/3 = 1 maka setiap n/n = 1. Dan jika n/n = 1, maka 0/0 haruslah sama dengan 1. Sehingga jika 1/1 = 1, 2/2 = 1, 3/3 = 1 maka 0/0 haruslah sama dengan 1"

Saya telah memberikan sebuah argumen, apa yang bisa anda lakukan dengan argumen berikut?

• Jika anda menerima argumen ini, maka anda harus setuju dengan kesimpulan/konklusi argumen (yaitu "... maka 0/0 haruslah sama dengan 1");
• Jika anda tidak menerimanya, maka anda bisa menguji argumen saya dengan beberapa cara.

Bagaimana caranya menguji sebuah argumen? Terdapat 2 cara bagaimana sebuah argumen diuji. Anda bisa menguji argumen berdasarkan isi argumen tersebut, atau berdasarkan bentuknya.

Menguji Argumen Berdasarkan Isi Argumen

Menguji suatu isi argumen artinya adalah anda ragu bahwa argumen ini bernilai benar. Sebagai cotoh, anda mungkin berargumen:

"Menurut anda bahwa karena 1/1 = 1, 2/2 = 1, 3/3 = 1 lantas anda  menyimpulkan bahwa 0/0 = 1. Menurut saya itu tidak masuk akal dan saya tidak setuju dengan pernyataan anda. Walaupun secara umum suatu bilangan jika dibagi dengan bilangan itu sendiri menghasilkan 1, tidak berarti itu berlaku untuk 0/0 karena 0/0 merupakan bentuk tak terdefinisi."

Kita semua mungkin sepakat bahwa argumen ini benar (mungkin juga tidak di beberapa "sisi"). Karena kita fokus pada mengklaim bahwa argumen ini benar, kita katakan bahwa ini argumen yang digunakan untuk menguji isi argumen sebelumnya.

Perlu dicatat bahwa pada logika simbolik kita tidak memfokuskan pada isi argumen.

Menguji Argumen Berdasarkan Bentuknya

Cara lain untuk menguji isi suatu argumen adalah dengan menguji berdasarkan bentuk/susunan argumen tersebut. Misalnya seperti:

"Misalkan untuk setiap n/n = 1 maka 0/0 = 1. Sehingga

karena 0/0 = 1 maka

Hal ini tidak mungkin karena 0 jika dikali 0 maka menghasilkan 0 juga, maka argumen sebelumnya tidak benar berdasarkan metode inferensi."

Argumen ini mencoba memberi tahu bahwa walaupun suatu klaim dibuat dari argumen yang benar, maka kesimpulan atau konklusinya bisa saja bernilai salah. Bisa dilihat bahwa argumen uji ini tidak memfokuskan pada isi argumen, tapi pada bentuk dari argumen itu sendiri.

Sebagai catatan, logika simbolik merupakan studi mengenai bentuk dari argumen.

Kembali fokus pada argumen kita mengenai 0/0. Argumen ini memiliki 2 pernyataan (atau bisa disebut sebagai premis), dan sebuah konklusi/kesimpulan:

Premis 1: Jika 1/1 = 1, 2/2 = 1, 3/3 = 1 maka setiap n/n = 1. 

Premis 2: Jika n/n = 1, maka 0/0 haruslah sama dengan 1.

Konklusi: Jika 1/1 = 1, 2/2 = 1, 3/3 = 1 maka 0/0 haruslah sama dengan 1.

Argumen uji yang digunakan untuk menguji argumen diatas adalah: Tidak semua premis bernilai benar, maka kesimpulannya tidak bisa dijamin benar. Walau begitu, argumen diatas dapat dikatakan sebagai argumen yang valid. Mengapa? Hal ini karena walaupun argumen diatas memiliki kesimpulan yang salah, tapi argumen ini mengikuti salah satu kaidah yang benar yaitu silogisme (mengenai silogisme akan dijelaskan pada postingan selanjutnya).

Bentuk Argumen Pada Umumnya

Berikut merupakan bentuk argumen yang sangat umum dijumpai (selanjutnya penulis akan menjelaskan lebih detail mengenai bentuk-bentuk argumen dalam postingan lainnya). Karena dalam logika simbolik kita tidak mementingkan isi dari suatu argumen, kita menggunakan huruf A dan B untuk mewakili suatu pernyataan, semisal:

1. Jika A benar, maka B benar.
2. A benar.

Maka, B benar.

atau bentuk seperti berikut:

1. A benar atau B benar.
2. Ternyata A salah.

Maka, B benar.

Semua argumen yang memiliki bentuk berikut dikatakan sebagai argumen yang valid. Jadi untuk menguji suatu argumen selain dari bentuknya, anda harus menguji berdasarkan isinya.

Sampai disini kita masuk ke definisi argumen,

Definisi: Argumen

Sebuah argumen adalah himpunan berhingga dari pernyataan yang dinamakan premis, bersama dengan pernyataan tunggal dinamakan konklusi, yang mana kebenarannya didukung berdasarkan kebenaran dari premis-premisnya.

Pada argumen diatas kita memiliki 2 premis dan sebuah konklusi:

Premis 1: Jika 1/1 = 1, 2/2 = 1, 3/3 = 1 maka setiap n/n = 1. 

Premis 2: Jika n/n = 1, maka 0/0 haruslah sama dengan 1.

Jika 1/1 = 1, 2/2 = 1, 3/3 = 1 maka 0/0 haruslah sama dengan 1.

Simbol  digunakan untuk mengindikasikan konklusi dari suatu argumen, dibaca "sehingga".

Read More