Memahami logika titik paling tidak pasti

Untuk lebih memahami makalah saya mencoba untuk mendapatkan pemahaman singkat tentang logika titik paling tidak tetap. Ada beberapa poin di mana saya terjebak.

Jika adalah grafik dan$G = (V,E)$

$$\Phi(P) = \{(a,b) \mid G \models E(a,b) \lor P(a,b) \lor \exists z (E(a,z) \land P(z,b)) \}$$

adalah operator pada relasi biner . Saya tidak mengerti mengapa titik paling tetap P * dari P adalah penutupan transitif E . Contoh diambil dari Teori Model Hingga dan Aplikasinya (hlm. 60).$P$$P^*$$P$$E$

Ketika memperluas logika orde pertama dengan operator pointer paling tidak tetap saya tidak mengerti mengapa simbol relasi harus positif dalam rumus. Positif berarti bahwa setiap kemunculan S i dalam rumus berada dalam jumlah simbol negasi.$S_i$$S_i$

Apakah ada yang tahu apa yang baik untuk dibaca untuk pemahaman intuitif dari pointer pointer paling tidak tetap dan sintaks dan semantiknya?

Jika Anda mengalami masalah dengan konsep titik paling tidak tetap, saya akan merekomendasikan meluangkan waktu untuk mendapatkan latar belakang dalam teori urutan yang lebih umum.

Davey dan Priestley, Pengantar Lattices and Order adalah intro yang bagus.

Untuk melihat mengapa penutupan transitif adalah titik paling tidak tetap, bayangkan membangun penutupan dari set kosong, menerapkan rumus logis satu langkah pada satu waktu. Titik paling tidak tetap tiba ketika Anda tidak dapat menambahkan tepi baru menggunakan rumus.

Persyaratan agar formula menjadi positif memastikan bahwa prosesnya monoton, yaitu bahwa ia tumbuh pada setiap langkah. Jika Anda memiliki subformula negatif, Anda dapat memiliki kasus di mana pada beberapa langkah set tepi akan menurun, dan ini dapat menyebabkan osilasi non-terminasi ke atas dan ke bawah, daripada konvergensi ke LFP.

$S$$P$

$$P(X) = \lnot X$$

$P$

1. $\mu P$$P(\mu P) = \mu P$$\mu X.\;P(X)$

2. $L$$f : L \to L$$f$$f$$f$

3. $X$

Saya menemukan bahwa tidak ada pengganti untuk melakukan pembuktian ini untuk Anda sendiri karena benar-benar menginternalisasi intuisi.

ini adalah posting yang sangat lama sehingga Anda mungkin sudah menemukan jawaban yang diinginkan. Karena saya telah mempelajari FO (LFP) selama beberapa bulan terakhir. Saya memiliki beberapa pemahaman tentang jawaban yang Anda butuhkan.

$[\sigma$$\phi(\vec{x},X)$$|\vec{x}|=ar(X)$$f_\phi$$\mathcal{P}(A^{ar(X)}) \mapsto \mathcal{P}(A^{ar(x)})$$\sigma$$\mathbb{A}$$\mathcal{P}(Z)$$f_\phi(Z) = \{\ \vec{a} \in A^{ar(X)}\ |\ \mathbb{A},\vec{a},Z \models \phi\ \}$. Jika operator ini adalah monoton maka kita dapat dengan mudah menangkap titik tetap dalam struktur terbatas dan tak terbatas mengikuti teorema titik tetap knaster tarski yang disebutkan dalam jawaban di atas. Tetapi, masalahnya adalah menguji apakah formula yang ditulis dalam bentuk seperti di atas mengkodekan operator monoton atau tidak tidak dapat diputuskan sehingga kita perlu mendapatkan hal terbaik berikutnya. Kepositifan dalam variabel bebas orde kedua memastikan persyaratan monotonisitas terpenuhi, ini merupakan induksi struktural standar untuk membuktikan fenomena ini. Pertanyaannya, apakah sudah cukup?

Untuk itu, saya belum punya jawaban yang pasti, karena saya masih membaca. Saya bisa menunjukkan makalah di bagian depan ini. Setidaknya satu ide yang menjelaskan yang saya sebutkan di sini, berasal dari makalah, Monoton vs Positif - Ajtai, Gurevich. Ini juga lebih lanjut menyebutkan makalah lain ekstensi titik tetap dari logika urutan pertama oleh Gurevich dan Shelah yang menyatakan operator titik tetap ketika diterapkan pada formula positif tidak kehilangan daya ekspresif jika dibandingkan dengan aplikasi yang dilakukan melalui formula monoton sewenang-wenang.