Asisten bukti untuk menulis matematika

Saya ingin menulis bukti matematika menggunakan beberapa asisten bukti. Semuanya akan ditulis menggunakan logika orde pertama (dengan kesetaraan) dan deduksi alami. Latar belakangnya adalah set theory (ZF). Misalnya, bagaimana saya bisa menulis bukti berikut?

Aksioma: $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$

Teorema: $\forall x\forall y(\forall z(z\notin x)\land\forall z(z\notin y)\rightarrow x=y)$

Artinya, set kosong itu unik.

Ini sepele bagi saya untuk menyelesaikannya dengan menggunakan kertas dan pena, tetapi yang benar-benar saya butuhkan adalah perangkat lunak untuk membantu saya memeriksa bukti kebenaran.

Terima kasih.

Coq dan Isabelle dapat melakukan ini.

[Coq] Berikut adalah makalah yang membahas cara menyandikan ZFC di CIC, yang menjadi dasar Coq.

Benjamin Werner: Set dalam Jenis, Jenis dalam Set (1997). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709

[Isabelle] Ada perpustakaan untuk ZF.

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/index.html

Pindah dari komentar atas saran Kaveh

Pertama, Anda perlu memilih asisten bukti. Coq adalah apa yang saya gunakan, tetapi ada banyak lainnya . Coq didasarkan pada logika tingkat tinggi (apa yang disebut Calculus of Inductive Constructions). Asisten pembuktian lainnya didasarkan pada logika urutan pertama, jadi mungkin lebih cocok dengan kebutuhan Anda (modulo komentar di atas).

Maka Anda perlu berkomitmen untuk mempelajari asisten bukti. Dokumen yang ditautkan adalah tutorial untuk memahami Coq. Menjadi seorang ahli Coq membutuhkan dedikasi dan praktik bertahun-tahun, tetapi teorema sederhana dapat dibuktikan dalam satu sore. Kunci untuk belajar Coq atau asisten bukti lainnya adalah melakukan bukti, seperti yang ada di kertas yang ditautkan. Hanya membaca makalah akan sangat sedikit membantu, karena seluruh pengalaman berinteraksi dengan asisten bukti tidak dapat disampaikan dengan baik di atas kertas.

Dalam beberapa hari Anda harus dapat menyandikan teorema sederhana, seperti yang di atas, dan membuktikannya. Jangan berharap kami akan melakukan ini untuk Anda. Anda tidak akan belajar apa-apa seperti itu.

Ketika Anda berhasil membuktikan teorema ini, jangan ragu untuk mengirimkan jawaban Anda di sini dan mungkin meninggalkan beberapa komentar tentang pengalaman Anda.

Apakah Anda siap menghadapi tantangan?

Ada banyak artikel matematika yang ditulis menggunakan asisten bukti Mizar: http://mizar.org/fm/

Dave Clarke menyarankan Coq, tapi sebenarnya Isabelle sepertinya ide yang jauh lebih baik, karena memiliki perpustakaan untuk ZF . Isabelle juga sangat dewasa dan memiliki beragam taktik dan ekstensi.

Saya belum pernah menggunakan Mizar secara pribadi, tetapi mungkin juga bagus.

bagaimana saya bisa menulis bukti berikut?

Di Isabelle / ZF Anda dapat menulis sesuatu seperti ini

theory csthquestion imports Main

begin

theorem empty_unique:
shows "\<forall> x.\<forall>y.(\<forall>z. (z\<notin>x)) \<and> (\<forall>z.(z\<notin>y)) \<longrightarrow> x=y"
    by auto

end

Seperti yang Anda lihat, Isabelle membuktikan ini secara otomatis. Tentu saja Anda dapat menulis bukti yang lebih rinci jika Anda benar-benar menginginkannya.

Teorema ini adalah contoh yang dikerjakan (lihat Contoh 11) dalam tutorial yang disertakan dengan perangkat lunak DC Proof 2.0 saya. Unduh secara gratis di situs web saya http://www.dcproof.com