Kepuasan urutan pertama yang tidak memiliki model terbatas

Kita tahu dari teorema Gereja bahwa menentukan tingkat kepuasan pertama tidak dapat diputuskan secara umum, tetapi ada beberapa teknik yang dapat kita gunakan untuk menentukan tingkat kepuasan pertama. Yang paling jelas adalah mencari model yang terbatas. Namun, ada sejumlah pernyataan dalam logika urutan pertama yang dapat kami tunjukkan tidak memiliki model yang terbatas. Misalnya, domain apa pun di mana fungsi injeksi dan non-surjektif beroperasi tidak terbatas.

Bagaimana kita menunjukkan kepuasan untuk pernyataan urutan pertama di mana tidak ada model hingga atau keberadaan model terbatas tidak diketahui? Dalam pembuktian teorema otomatis kita dapat menentukan kepuasan beberapa cara:

1. Kita dapat meniadakan kalimat, dan mencari kontradiksi. Jika ditemukan, kami membuktikan validitas urutan pertama dari pernyataan dan dengan demikian memuaskan.
2. Kami menggunakan saturasi dengan resolusi dan kehabisan kesimpulan. Lebih sering daripada tidak, kita akan memiliki jumlah kesimpulan yang tak terbatas untuk dibuat, jadi ini tidak bisa diandalkan.
3. Kita dapat menggunakan pemaksaan, yang mengasumsikan keberadaan model dan juga konsistensi teori.

Saya tidak tahu ada orang yang menerapkan pemaksaan sebagai teknik mekanis untuk pembuktian teorema otomatis, dan itu tidak terlihat mudah, tetapi saya tertarik jika itu dilakukan atau dicoba, karena telah digunakan untuk membuktikan independensi untuk sejumlah pernyataan dalam teori himpunan, yang itu sendiri tidak memiliki model yang terbatas.

Apakah ada teknik lain yang dikenal untuk mencari kepuasan tingkat pertama yang berlaku untuk penalaran otomatis atau ada yang bekerja pada algoritma pemaksaan otomatis?

Inilah pendekatan yang lucu oleh Brock-Nannestad dan Schürmann:

Abstraksi Monadik Sejati

Idenya adalah untuk mencoba menerjemahkan kalimat tingkat pertama ke dalam logika tingkat pertama monadik , dengan "melupakan" beberapa argumen. Tentu saja terjemahannya tidak lengkap : ada beberapa kalimat yang konsisten yang menjadi tidak konsisten setelah terjemahan.

Namun, logika urutan pertama monadik adalah decidable . Karena itu, orang dapat memverifikasi jika terjemahan dari rumus konsisten:$\overline F$$F$

dapat diperiksa dengan prosedur keputusan, dan tersirat

Yang menyiratkan bahwa memiliki model, dengan teorema kelengkapan.$F$

Tema ini dapat berlaku agak lebih umum: mengidentifikasi sub-logika yang dapat diputuskan dari masalah Anda, kemudian menerjemahkan masalah Anda ke dalamnya, dengan cara yang menjaga kebenaran. Secara khusus pemecah SMT modern seperti Z3 telah menjadi sangat baik dalam membuktikan kepuasan formula dengan quantifiers (secara default , tetapi dapat bekerja dengan baik pada formula ). Π 0 $\Sigma^0_1$$\Pi^0_2$

Pemaksaan tampaknya jauh dari jangkauan metode otomatis saat ini.