Zrozumienie logiki najmniej ustalonego punktu

Aby lepiej zrozumieć artykuł, staram się krótko zrozumieć logikę najmniej ustalonego punktu. Utknąłem w kilku punktach.

Gdyby $G = (V,E)$ jest wykresem i

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

jest operatorem relacji binarnej $P$. Nie rozumiem, dlaczego najmniej ustalony punkt$P^*$ z $P$ jest przejściowym zamknięciem $E$. Przykład pochodzi z teorii modeli skończonych i jej zastosowań (s. 60).

Rozszerzając logikę pierwszego rzędu o najmniej ustalony operator wskaźnika, nie rozumiem, dlaczego symbol relacji $S_i$musi być pozytywny we wzorze. Pozytywne oznacza, że ​​każde wystąpienie$S_i$ we wzorze znajduje się w parzystej liczbie symboli negacji.

Czy ktoś ma pojęcie, co warto przeczytać, aby intuicyjnie zrozumieć logikę wskaźnika o najmniej ustalonych parametrach oraz jej składnię i semantykę?

Jeśli masz problem z koncepcją punktu o najmniej ustalonym punkcie, polecam poświęcić trochę czasu na zapoznanie się z bardziej ogólną teorią porządku.

Davey i Priestley, Wprowadzenie do krat i porządku to dobre wprowadzenie.

Aby zobaczyć, dlaczego zamknięcie przechodnie jest najmniej stałym punktem, wyobraź sobie budowanie zamknięcia z pustego zestawu, stosując logiczną formułę krok po kroku. Najmniej ustalony punkt pojawia się, gdy nie można dodać żadnych nowych krawędzi za pomocą formuły.

Wymóg, aby formuła była dodatnia, zapewnia, że ​​proces jest monotoniczny, tzn. Że rośnie na każdym etapie. Jeśli miałeś ujemną podformułę, możesz mieć przypadek, w którym na niektórych etapach zestaw krawędzi zmniejszy się, a to może prowadzić do niekończącej się oscylacji w górę i w dół, a nie do konwergencji do LFP.

Rozważmy algebrę logiczną utworzoną z zestawu sił skończonego zestawu $S$, uporządkowane według włączenia zestawu. Teraz rozważ operatora$P$ określony przez

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

Wyraźnie $P$ jest operatorem dodatnim.

1. Pokaż, że nie ma stałych punktów $\mu P$ takie, że $P(\mu P) = \mu P$. W rezultacie możesz to wywnioskować$\mu X.\;P(X)$ nie da się dobrze zdefiniować.

2. Udowodnij sobie twierdzenie Knaster-Tarksi. To znaczy, jeśli masz pełną sieć$L$oraz funkcja monotoniczna $f : L \to L$, a następnie zestaw stałych punktów $f$tworzy kompletną sieć. (W konsekwencji,$f$ ma najmniejszy i największy ustalony punkt.) Ten dowód jest bardzo krótki, ale jest to trochę porywacz głowy, gdy go zobaczysz po raz pierwszy, i monotoniczność $f$ ma kluczowe znaczenie dla argumentu.

3. Udowodnij, że dowolny operator zdefiniowany przez wyrażenie z dowolną zmienną $X$co występuje tylko pozytywnie, jest monotoniczne. Tak więc pozytywne występowanie jest warunkiem syntaktycznym wystarczającym do wymuszenia monotoniczności.

Uważam, że nie da się zastąpić wykonania tych dowodów dla siebie, naprawdę internalizując intuicję.

jest to bardzo stary post, więc być może już spotkałeś się z odpowiedzią zgodnie z życzeniem. Od ostatnich kilku miesięcy studiuję FO (LFP). Rozumiem trochę odpowiedzi, których potrzebujesz.

Aby odpowiedzieć na wymóg pozytywności, potrzeba wynika z faktu, że sprawdzenie, czy formuła przechwytuje operator monotoniczny, czy nie, jest nierozstrzygalne zarówno w modelach skończonych, jak i nieskończonych. Co rozumiem przez formułę przechwytującą operator monotoniczny? Załóżmy, że wypisujesz FO$[\sigma$] formuła z bezpłatną zmienną drugiego rzędu powiedz $\phi(\vec{x},X)$, gdzie $|\vec{x}|=ar(X)$, możemy zdefiniować odpowiedni operator $f_\phi$ : $\mathcal{P}(A^{ar(X)}) \mapsto \mathcal{P}(A^{ar(x)})$ gdzie ar (X) jest rodzajem zmiennej drugiego rzędu, a A jest domeną $\sigma$-Struktura $\mathbb{A}$ i $\mathcal{P}(Z)$ jest zestawem mocy zestawu Z. I $f_\phi(Z) = \{\ \vec{a} \in A^{ar(X)}\ |\ \mathbb{A},\vec{a},Z \models \phi\ \}$. Jeśli ten operator jest monotoniczny, wówczas możemy łatwo uchwycić punkt stały zarówno w strukturze skończonej, jak i nieskończonej, zgodnie z twierdzeniem Knastera Tarskiego o punkcie stałym wspomnianym w powyższych odpowiedziach. Problem polega jednak na sprawdzeniu, czy formuła wypisana z powyższego formularza koduje monotoniczny operator, czy nie jest nierozstrzygalna, więc musimy uzyskać następną najlepszą rzecz. Pozytywność w zmiennej swobodnej drugiego rzędu zapewnia spełnienie wymogu monotoniczności, jest to standardowa indukcja strukturalna potwierdzająca to zjawisko. Pytanie brzmi, czy to wystarczy?

Na to nie mam jeszcze solidnej odpowiedzi, ponieważ wciąż czytam. Mogę wskazać papiery na tym froncie. Przynajmniej jeden wyjaśniający pomysły, o których tu wspomniałem, pochodzi z pracy Monotone vs. Positive - Ajtai, Gurevich. Ponadto wspomina także o innym artykule Stałe punkty rozszerzeń logiki pierwszego rzędu autorstwa Gurewicza i Szelacha, który stwierdza, że ​​operator punktu stałego po zastosowaniu do formuły dodatniej nie traci mocy ekspresyjnej w porównaniu z aplikacją wykonywaną na dowolnych formułach monotonicznych.