Paradigma apa yang membuktikan teorema otomatis yang sesuai untuk formalisasi Principia Mathematica-style?

Saya memiliki sebuah buku, yang diilhami oleh Principia Mathematica (PM) Russell dan positivisme logis, berupaya memformalkan domain tertentu dengan menentukan aksioma dan menyimpulkan teorema dari mereka. Singkatnya, ia mencoba melakukan untuk domainnya apa yang PM coba lakukan untuk matematika. Seperti PM, itu ditulis sebelum pembuktian teorema otomatis (ATP) dimungkinkan.

Saya mencoba untuk mewakili aksioma-aksioma ini dalam sistem ATP modern, dan mencoba untuk menyimpulkan teorema, awalnya yang disimpulkan oleh penulis (dengan tangan). Saya belum pernah menggunakan sistem ATP sebelumnya, dan diberi banyak pilihan (HOL, Coq, Isabelle, dan banyak lagi), masing-masing dengan kekuatan, kelemahan, dan aplikasi yang dimaksudkan, terbukti sulit untuk memutuskan mana yang tepat untuk spesifik saya. tujuan.

Formalisme penulis erat mencerminkan PM. Ada kelas (set?), Kelas kelas, dan seterusnya hingga 6 tingkat hierarki. Ada urutan pertama, dan mungkin logika urutan lebih tinggi. Mengingat hubungannya dengan PM, saya awalnya menyelidiki Metamath, karena beberapa teorema PM telah dibuktikan di MetaMath oleh orang lain. Namun, Metamath tentu saja merupakan pembuktian bukti dan bukan sistem ATP.

Melihat deskripsi berbagai sistem ATP, saya melihat beberapa karakteristik, seperti implementasi teori tipe Gereja, teori tipe konstruktif, teori tipe intuitionistic, teori himpunan diketik / tidak diketik, deduksi alami, jenis kalkulus lambda, polimorfisme, teori fungsi rekursif, dan adanya persamaan (atau tidak). Singkatnya, setiap sistem tampaknya menerapkan bahasa yang sangat berbeda, dan harus sesuai untuk memformalkan hal-hal yang berbeda. Saya berasumsi bahwa perpustakaan yang ada untuk memformalkan matematika tidak relevan dengan tujuan saya.

Setiap saran mengenai karakteristik yang harus saya cari dalam memilih ATP, atau saran lain yang mungkin Anda miliki setelah membaca pertanyaan ini, akan sangat dihargai. Untuk referensi, ini adalah halaman contoh dari buku. Sayangnya, seperti PM, itu dalam notasi Peano-Russell.

Buku -

"Metode Aksiomatik dalam Biologi" (1937), JH Woodger, A. Tarski, WF Floyd

Aksioma dimulai dengan mereologis. Sebagai contoh,

1.1.2 $x$ adalah jumlah dari $\alpha$ jika $\alpha$ terkandung dalam bagian-bagian $x$ , dan jika ketika $y$ adalah bagian dari $x$ selalu ada $z$ milik $\alpha$ memiliki bagian-bagian yang sama dengan bagian-bagian dari $y$ :

$$S{ = }_{ Df }\hat { x } \hat { \alpha } \{ \alpha \subset \vec { { P }^{ ‘ } } x:.(y):yPx.\supset .(\exists z).z\in \alpha .\vec { { P }^{ ‘ } } y\cap \vec { { P }^{ ‘ } } z\neq \Lambda \}$$

Sekali lagi, perhatikan bahwa ini adalah notasi Peano-Russell (notasi Principia).

Aksioma belakangan memiliki konten biologis, seperti,

7.4.2 Ketika gamet dari dua anggota kelas Mendel bersatu berpasangan untuk membentuk zigot, probabilitas setiap pasangan yang disatukan sama dengan yang ada pada pasangan lainnya.

Ini, dari apa yang saya mengerti, adalah postulat genetika Mendel.

Saya menghilangkan notasi untuk ini karena panjangnya tiga baris, dan dibangun berdasarkan konten yang telah ditentukan sebelumnya.

Contoh teorema -

Ini tampaknya membawa interpretasi yang bermakna dalam genetika Mendel, yang, tidak menjadi sejarawan biologi, saya tidak mengerti. Dalam buku itu, disimpulkan dengan tangan.

Terima kasih!

Principia Mathematica sebagian besar merupakan respons terhadap berbagai paradoks yang ditemukan dalam logika matematika pada pergantian abad ke-20. Namun karya itu sendiri, yang sering dipuji sebagai 'maha karya yang tak terbaca' agak canggung dan fondasi yang lebih modern telah dibuat. Untuk menggambarkan sebagian besar matematika, Anda memiliki beberapa pilihan: teori kategori adalah satu, teori jenis telah populer di beberapa proyek sebagai perpanjangan dari kalkulus lambda, tetapi yang paling dipahami dan paling mendasar mungkin adalah teori yang ditetapkan.

Teori himpunan memiliki beberapa formulasi yang berbeda; Zermelo Frankel menetapkan teori dengan aksioma pilihan adalah yang paling ortodoks, dengan penuh cinta disebut sebagai oleh para penggemar teori himpunan. Teori himpunan Tarski-Grothendiek adalah teori lain yang sebagian besar mirip dengan yang mencakup aksioma Tarski untuk alasan tentang kategori besar. Ini menarik untuk verifikasi, tetapi agak lebih sulit untuk membuktikan teorema otomatis karena skema aksioma penggantian mengakui jumlah aksioma yang tak terbatas yang mewakili tantangan untuk implementasi. Sementara dasar-dasar ini sangat masuk akal untuk sistem verifikasi bukti seperti Mizar untuk Tarski-Grothendiek teori set dan Metamath untukZ F C Z F $\sf ZFC$$\sf\ ZFC$$\sf ZFC$, untuk sistem pembuktian teorema yang sebenarnya, alangkah baiknya untuk memiliki aksiomatisasi terbatas.

Landasan yang mungkin paling tepat untuk itu adalah teori himpunan Von Neumann – Bernays-Gödel, atau , yang mengakui aksioma terbatas dengan menjadi dua teori yang diurutkan yang memiliki ontologi kelas yang tepat serta set. Lebih lanjut, telah terbukti bahwa adalah perpanjangan konservatif dari , sehingga setiap teorema adalah teorema dariN B G Z F C N B G Z F $\sf NBG$$\sf NBG$$\sf ZFC$$\sf NBG$$\sf ZFC$. Alasan bahwa teori ini adalah yang paling tepat untuk penalaran otomatis menurut pendapat saya adalah ekspresif dalam logika urutan pertama, yang mengakui kalkulus bukti yang efektif, masuk akal dan lengkap, dan aksiomatisasi terbatas berarti dapat digunakan dengan resolusi urutan pertama yang memberi kita hasil rapi: Jika suatu pernyataan dapat diputuskan, bukti pada akhirnya akan ditemukan.

Logika proposisional tidak cukup ekspresif, dan logika orde tinggi, sementara jauh lebih ekspresif, tidak mengakui kalkulus bukti yang efektif, sehat dan lengkap. Logika orde pertama dengan teori himpunan memungkinkan Anda untuk mewakili dan memetakan teori-teori logis orde tinggi, jadi untuk yayasan itulah sweet spot ... kecuali untuk kemungkinan pernyataan yang tidak dapat ditentukan (terima kasih kepada Gödel.) Yang merupakan alasan mengapa teori orde pertama dari peringkat quantifier yang memadai sering digambarkan sebagai semi-decidable.

Art Quaife melakukan beberapa hal dalam hal ini di: Pengembangan Otomatis Teori Matematika Fundamental, di mana ia mengimplementasikan dalam logika urutan pertama dalam bentuk klausa sehingga dapat digunakan oleh teorema teorema berbasis resolusi (Otter) dan referensi exellent untuk menangani dasar untuk pekerjaan semacam ini adalah Pengantar Matematika Logika Elliott Mendelson .$\sf NBG$

Sekarang asisten pembuktian modern sering kurang peduli dengan fondasi dari paradigma Principia Mathematia dan lebih berguna untuk pembuktian teorema untuk pekerjaan sehari-hari, sehingga mereka memiliki beberapa dukungan untuk fragmen-fragmen logika tingkat tinggi, penyelesaian SAT / SMT, teori tipe, dan lainnya. pendekatan yang lebih informal dan kurang mendasar. Tetapi jika Anda mencoba melakukan sesuatu seperti Principia Mathematica, sebuah prover teorema resolusi orde pertama dengan teori orde pertama yang dapat diterima secara aksial sangat ideal.

Untuk beberapa contoh tentang bagaimana teorema otomatis menyerang masalah dari yayasan-yayasan ini, situs Ribuan Masalah untuk Teorema Provers ( TPTP ) memiliki sejumlah masalah yang bagus, dan Anda akan mencatat bahwa banyak masalah mendasar dalam teori bilangan ditemukan di menetapkan teori. Jika Anda punya waktu, periksa NUM006-1.p di situs mereka: dugaan Goldbach. Anda dapat mencoba menjalankannya, dan jika itu layak, bukti akhirnya akan ditemukan.$\sf NBG$

Teorema dalam buku Anda hampir pasti akan menjadi teorema mengingat bahwa mereka ditulis dalam bahasa teori himpunan. Aksioma genetika dalam buku itu hampir pasti akan direpresentasikan sebagai definisi predikat teoretis, seperti halnya aritmetika Peano diwakili dalam sebagai definisi predikat. Dari sana Anda mengikuti prosedur resolusi di ATP apa pun. Pilih pernyataan yang ingin Anda buktikan, negasikan, konversikan ke bentuk normal Skolem, lalu ke bentuk klausa, dan ikuti resolusi. Ketika Anda menemukan klausa kosong, Anda telah menemukan kontradiksi, membuktikan pernyataan itu.N B $\sf NBG$$\sf NBG$

Tugas yang Anda miliki jika Anda ingin mencoba untuk mendefinisikan teori dalam hal teori himpunan, adalah menemukan definisi predikat relasional yang terpisah dari teori himpunan, yang akan memungkinkan Anda untuk membuat predikat dalam hal teori himpunan. Sekali lagi, contoh dari ini adalah bagaimana kita mendefinisikan aritmetika Peano dalam teori himpunan, yang dengan sendirinya tidak memiliki definisi angka, penambahan, perkalian, atau bahkan kesetaraan. Sebagai contoh definisi teoritis tentang hubungan seperti kesetaraan, kita dapat mendefinisikannya dalam hal keanggotaan:

∀ ∈ ↔ ∈ $\forall$ xy ( z (z x z y) x = y)$\forall$$\in$$\leftrightarrow$$\in$$\leftrightarrow$

Sedikit peringatan: kurva pembelajaran untuk ini memang sangat curam. Jika Anda bermaksud mengejar ini, Anda mungkin menemukan diri Anda beberapa tahun sebelum memahami masalah penuh, seperti pengalaman saya. Anda mungkin ingin memeriksa teori dari pendekatan yang kurang mendasar sebelum mengambil tugas besar menanamkannya dalam bahasa dasar untuk semuanya. Anda tidak, setelah semua, tentu perlu alasan tentang set terhitung gen pencampuran.

Beberapa poin:

1. $\in$$\cap, \subset$

2. Setiap asisten bukti interaktif modern pasti akan memiliki ekspresi untuk memformalkan dan membuktikan pernyataan Anda, seperti yang disarankan Andrej. Bahkan, karena tampaknya ada beberapa pernyataan termasuk aritmatika, akan lebih bijaksana untuk menggunakan sistem seperti Isabelle , Coq atau HOL yang sudah memiliki teori yang luas untuk menangani pernyataan aritmatika. Penekanan saya pada modern bukanlah kebetulan: langkah besar dalam kegunaan telah dibuat sejak Automath, dan saya benar-benar berpikir Anda akan merugikan diri sendiri dengan menggunakan apa pun yang belum dikembangkan secara aktif sejak tahun 90-an (jika Anda bahkan bisa mendapatkannya) bekerja!)

3. $\LaTeX$