Apakah teorema kekompakan untuk FOL telah diformalkan dalam Coq / Isabelle / etc?

15

Saya telah mencari formalisasi teorema kekompakan untuk FOL, tetapi belum menemukannya. Adakah yang tahu tentang perkembangan semacam itu atau pekerjaan terkait?

lo.logic coq Stefan Ciobaca
sumber
4
Sudahkah Anda mencoba bertanya pada milis Coq atau Isabelle?
Dave Clarke
2
Saya tidak yakin apakah ini cocok untuk cstheory, tetapi lihat ini . Kelengkapan ada di sana, dan kekompakan tidak jauh dari itu.
Kaveh
Lihat juga entri AFP untuk versi di Isabelle / HOL (dari 2004).
Makarius

Jawaban:

17

Teorema kekompakan untuk logika orde pertama klasik adalah konsekuensi langsung dari teorema kelengkapan, dan, sebenarnya, seseorang dapat membuktikan secara langsung Kekompakan dengan argumen gaya Henkin yang digunakan untuk Kelengkapan tanpa pernah menyebutkan derivasi.

Teorema Kelengkapan untuk FOL klasik sehubungan dengan model Tarski standar telah diresmikan di Mizar. Lihat serangkaian artikel di bawah http://fm.mizar.org/2005-13/fm13-1.html

Teorema kelengkapan yang sama, tetapi dengan bukti konstruktif, telah hampir diformalkan dalam asisten bukti Coq sendiri, lihat file zip di bawah https://sites.google.com/site/dankoilik/publications/phd-thesis

Saya katakan "hampir" karena ada satu titik teknis, yang membuktikan kebenaran algoritma penyortiran, bahwa saya belum punya waktu untuk menyelesaikannya, tetapi bahan utama (teorema ultra-filter konstruktif untuk bahasa yang dapat dihitung) diformalkan.

Seseorang juga dapat mempertimbangkan Kelengkapan, dan karenanya Kekompakan, untuk gagasan validitas non-standar, dan mendapatkan bukti konstruktif yang lengkap dan diformalkan.

Danko Ilik
sumber