Matematika memiliki banyak simbol. Beberapa mungkin mengatakan terlalu banyak simbol. Jadi mari kita lakukan matematika dengan gambar.
Mari kita punya kertas, yang akan kita gambar. Untuk memulai kertas kosong, kita akan mengatakan itu setara dengan atau true .
Jika kita menulis hal-hal lain di atas kertas itu juga akan benar.
Sebagai contoh
Menunjukkan bahwa klaim dan Q benar.
Sekarang mari kita katakan bahwa jika kita menggambar lingkaran di sekitar pernyataan, pernyataan itu salah. Ini tidak logis.
Sebagai contoh:
Menunjukkan bahwa salah dan Q benar.
Kami bahkan dapat menempatkan lingkaran di sekitar beberapa sub-pernyataan:
Karena bagian di dalam lingkaran biasanya dibaca sebagai dengan meletakkan lingkaran di sekitarnya itu berarti tidak ( P dan Q ) . Kita bahkan dapat membuat lingkaran sarang
Ini berbunyi .
Jika kita menggambar lingkaran dengan tidak ada di dalamnya, itu mewakili atau salah .
Karena ruang kosong itu benar, maka negasi yang benar itu salah.
Sekarang menggunakan metode visual sederhana ini, kita sebenarnya dapat mewakili pernyataan apa pun dalam logika proposisional.
Bukti
Langkah selanjutnya setelah dapat mewakili pernyataan adalah mampu membuktikannya. Sebagai bukti, kami memiliki 4 aturan berbeda yang dapat digunakan untuk mengubah grafik. Kita selalu mulai dengan lembaran kosong yang seperti kita ketahui adalah kebenaran yang kosong dan kemudian menggunakan aturan yang berbeda ini untuk mengubah lembaran kertas kosong kita menjadi teorema.
Aturan inferensi pertama kami adalah Penyisipan .
Insersi
Kami akan menyebut jumlah negasi antara sub-grafik dan tingkat atas adalah "kedalaman". Insersi memungkinkan kita untuk memperkenalkan pernyataan apa pun yang kita inginkan pada kedalaman yang aneh.
Berikut adalah contoh kami melakukan penyisipan:
Penghapusan
Aturan inferensi berikutnya adalah Erasure . Penghapusan memberi tahu kita bahwa jika kita memiliki pernyataan yang pada kedalaman yang sama kita dapat menghapusnya sepenuhnya.
Berikut adalah contoh penghapusan yang diterapkan:
bersarang tingkat.
Potong ganda
Double Cut adalah persamaan. Yang berarti, tidak seperti kesimpulan sebelumnya, itu juga dapat dibalik. Potong ganda memberi tahu kita bahwa kita dapat menggambar dua lingkaran di sekitar sub-grafik, dan jika ada dua lingkaran di sekitar sub-grafik, kita bisa menghapus keduanya.
Berikut adalah contoh dari Double Cut yang digunakan
Perulangan
Iterasi adalah kesetaraan juga. 1 Itu terbalik disebut Deiterasi Jika kita memiliki pernyataan dan potongan pada tingkat yang sama, kita dapat menyalin pernyataan itu di dalam potongan.
Sebagai contoh:
Deiterasi memungkinkan kita untuk membalik Iterasi . Pernyataan dapat dihapus melalui Deiterasi jika ada salinannya di tingkat berikutnya.
Format representasi dan bukti ini bukan dari penemuan saya sendiri. Mereka adalah modifikasi kecil dari logika diagram yang disebut Alpha Existential Graphs . Jika Anda ingin membaca lebih lanjut tentang ini, tidak ada banyak literatur, tetapi artikel yang terhubung adalah awal yang baik.
Tugas
Tugas Anda adalah membuktikan teorema berikut:
Ini, ketika diterjemahkan ke dalam simbolisasi logika tradisional
.
Juga dikenal sebagai Aksioma Łukasiewicz-Tarski .
Ini mungkin tampak terlibat tetapi grafik eksistensial sangat efisien dalam hal panjang bukti. Saya memilih teorema ini karena saya pikir itu adalah panjang yang sesuai untuk teka-teki yang menyenangkan dan menantang. Jika Anda mengalami masalah dengan yang satu ini saya akan merekomendasikan mencoba beberapa teorema yang lebih dasar terlebih dahulu untuk memahami sistem. Daftar ini dapat ditemukan di bagian bawah posting.
Ini adalah golf bukti sehingga skor Anda akan menjadi jumlah total langkah dalam bukti Anda dari awal hingga selesai. Tujuannya adalah untuk meminimalkan skor Anda.
Format
Format untuk tantangan ini fleksibel, Anda dapat mengirimkan jawaban dalam format apa pun yang dapat dibaca dengan jelas, termasuk format yang dibuat sendiri atau dirender. Namun untuk kejelasan saya sarankan format sederhana berikut:
Kami mewakili potongan dengan tanda kurung, apa pun yang kami potong dimasukkan ke dalam parens. Potongan kosong hanya akan menjadi
()
contoh.Kami mewakili atom hanya dengan surat-surat mereka.
Sebagai contoh di sini adalah pernyataan sasaran dalam format ini:
(((A((B(A))))(((((C)((D((E)))))(((C((D(F))))(((E(D))((E(F))))))))(G))))((H(G))))
Format ini bagus karena dapat dibaca oleh manusia dan mesin, jadi memasukkannya dalam posting Anda akan menyenangkan.
Sedangkan untuk pekerjaan Anda yang sebenarnya, saya merekomendasikan pensil dan kertas saat berolahraga. Saya menemukan bahwa teks tidak seintuitif kertas ketika menyangkut grafik eksistensial.
Contoh bukti
Dalam contoh bukti ini kita akan membuktikan teorema berikut:
Bukti:
Praktekkan Teorema
Berikut adalah beberapa teorema sederhana yang dapat Anda gunakan untuk berlatih sistem:
Xiukasiewicz 'Aksioma Kedua
Aksioma Meredith
1: Sebagian besar sumber menggunakan versi Iterasi yang lebih canggih dan kuat , tetapi untuk menyederhanakan tantangan ini, saya menggunakan versi ini. Mereka setara secara fungsional.
sumber
Jawaban:
19 langkah
(())
[potong ganda](AB()(((G))))
[insersi](AB(A)(((G))))
[perulangan](((AB(A)))(((G))))
[potong ganda](((AB(A))(((G))))(((G))))
[perulangan](((AB(A))(((G))))((H(G))))
[insersi](((AB(A))(((G)(()))))((H(G))))
[potong ganda](((AB(A))(((DE()(C)(F))(G))))((H(G))))
[insersi](((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G))))
[perulangan](((AB(A))(((DE(CD(F))(DE(C))(F))(G))))((H(G))))
[perulangan](((AB(A))(((E(CD(F))(DE(C))(F)((D)))(G))))((H(G))))
[potong ganda](((AB(A))(((E(CD(F))(DE(C))(E(D))(F))(G))))((H(G))))
[perulangan](((AB(A))(((G)((CD(F))(DE(C))(E(D))((E(F)))))))((H(G))))
[potong ganda](((AB(A))(((G)((CD(F))(DE(C))(((E(D))((E(F)))))))))((H(G))))
[potong ganda](((AB(A))(((G)((C((D(F))))(DE(C))(((E(D))((E(F)))))))))((H(G))))
[potong ganda](((AB(A))(((G)((DE(C))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[potong ganda](((AB(A))(((G)((D(C)((E)))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[potong ganda](((AB(A))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[potong ganda](((A((B(A))))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[potong ganda]Praktekkan teorema
Aksioma kedua Łukasiewicz: 7 langkah
(())
[potong ganda](A()(B)(C))
[insersi](A(A(B))(B)(C))
[perulangan](A(AB(C))(A(B))(C))
[perulangan]((AB(C))(A(B))((A(C))))
[potong ganda]((AB(C))(((A(B))((A(C))))))
[potong ganda]((A((B(C))))(((A(B))((A(C))))))
[potong ganda]Aksioma Meredith: 11 langkah
(())
[potong ganda](()(D(A)(E)))
[insersi]((D(A)(E))((D(A)(E))))
[perulangan]((D(A)(E))((D(A)(E(A)))))
[perulangan]((D(A)(E))(((E(A))((D(A))))))
[potong ganda](((E)((D(A))))(((E(A))((D(A))))))
[potong ganda](((E)((C)(D(A))))(((E(A))((D(A))))))
[insersi](((E)((C)(D(A)(C))))(((E(A))((D(A))))))
[perulangan](((E)((C)((A)(C)((D)))))(((E(A))((D(A))))))
[potong ganda](((E)((C)((A)(((C)((D)))))))(((E(A))((D(A))))))
[potong ganda](((E)((C)((A(B))(((C)((D)))))))(((E(A))((D(A))))))
[insersi]Pencari bukti Haskell
(Apa, kamu pikir aku akan melakukannya dengan tangan? :-P)
Ini hanya mencoba penyisipan, pengantar pemotongan ganda, dan iterasi. Jadi masih mungkin solusi ini bisa dikalahkan dengan menggunakan penghapusan, eliminasi potongan ganda, atau deiterasi.
sumber
22 Langkah
(((())(())))
(((AB())(CDE(F)()))H(G))
(((AB(A))(CDE(F)(CD(F)))(G))H(G))
(((A((B(A))))(((((C))DE(F)(C((D(F)))))(G))))((H(G))))
(((A((B(A))))(((((C)DE)DE(F)(C((D(F)))))(G))))((H(G))))
(((A((B(A))))(((((C)((D((E)))))((((((D))E(F)))(C((D(F)))))))(G))))((H(G))))
(((A((B(A))))(((((C)((D((E)))))((((((D)E)E(F)))(C((D(F)))))))(G))))((H(G))))
(((A((B(A))))(((((C)((D((E)))))((((((D)E)((E(F)))))(C((D(F)))))(G))))))((H(G))))
Beberapa hal yang saya pelajari dari menyelesaikan puzzle ini:
Kurangi representasi yang disediakan. Ini melibatkan membalikkan pemotongan ganda dan iterasi. Misalnya, aksioma ini berkurang
(((AB(A))(((C)DE)(CD(F))(E(D))(E(F)))(G))H(G))
setelah membalikkan pemotongan ganda, dan(((AB(A))(()CDE(F)))H(G)))
setelah membalikkan iterasi.Cari atom yang tersesat. Misalnya, H digunakan sebagai variabel dummy, dan dengan demikian dapat dimasukkan pada titik mana pun.
Praktik Solusi Teorema:
Solusi untuk Aksioma Kedua Łukasiewicz ': [8 Langkah]
(())
(()AB(C))
((AB(C))AB(C))
((A((B(C))))A((B))(C))
((A((B(C))))A(A(B))(C))
((A((B(C))))(((A(B))((A(C))))))
Solusi untuk Aksioma Meredith: [12 Langkah]
(())
(()(A)D(E))
(((A)D(E))(A)D(E(A)))
(((((A)D))(E))(A)D(E(A)))
(((((A(B))D)(C))(E))(A)D(E(A)))
(((((A(B))(C)D)(C))(E))(A)D(E(A)))
(((((A(B))(((C)((D)))))(C))(E))(((((A)D))(E(A)))))
sumber
\$
sebagai awal / akhir yang saya pikir akan membuat solusi Anda lebih mudah dibaca. Saya harap Anda bersenang-senang di sini :)