Comprender la lógica de punto menos fijo

Para comprender mejor un artículo, estoy tratando de obtener una breve comprensión de la lógica de punto menos fijo. Hay algunos puntos donde estoy atrapado.

Si $G = (V,E)$ es un gráfico y

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

es un operador en la relación binaria . No entiendo por qué el punto mínimo fijo de es el cierre transitivo de . El ejemplo está tomado de la teoría de modelos finitos y sus aplicaciones (p. 60).P ∗ P $P$$P^*$$P$$E$

Al extender la lógica de primer orden con el operador de puntero menos fijo, no entiendo por qué el símbolo de relación debe ser positivo en la fórmula. Positivo significa que cada de en la fórmula está dentro de un número par de símbolos de negación.$S_i$$S_i$

¿Alguien tiene idea de lo que es bueno leer para una comprensión intuitiva de la lógica de puntero menos fijo y su sintaxis y semántica?

Si tiene problemas con el concepto de punto menos fijo, le recomendaría pasar algún tiempo obteniendo antecedentes en una teoría del orden más general.

Davey y Priestley, Introducción a los enrejados y el orden es una buena introducción.

Para ver por qué el cierre transitivo es el punto menos fijo, imagine construir el cierre a partir de un conjunto vacío, aplicando la fórmula lógica paso a paso. El punto menos fijo llega cuando no puede agregar bordes nuevos con la fórmula.

El requisito de que la fórmula sea positiva asegura que el proceso sea monótono, es decir, que crezca en cada paso. Si tuviera una subformula negativa, podría tener el caso de que en algunos pasos el conjunto de aristas disminuiría, y esto podría conducir a una oscilación sin terminación hacia arriba y hacia abajo, en lugar de una convergencia a la LFP.

Considere el álgebra booleana formada a partir del conjunto de potencia de un conjunto finito , ordenado por inclusión de conjunto. Ahora, considere el operador P definido por$S$$P$

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

Claramente, es un operador no positivo.$P$

1. Muestran que no hay puntos fijos tal que P ( μ P ) = μ P . Como resultado, se puede concluir que μ X $\mu P$$P(\mu P) = \mu P$ no puede estar bien definido.$\mu X.\;P(X)$

2. Prueba el teorema de Knaster-Tarksi por ti mismo. Es decir, si tiene una red completa y una función monótona f : L → L , entonces el conjunto de puntos fijos de f forma una red completa. (Como consecuencia, f tiene un punto fijo mínimo y máximo.) Esta prueba es muy corta, pero es un rasguño de cabeza la primera vez que la ve, y la monotonicidad de f es crítica para el argumento.$L$$f : L \to L$$f$$f$$f$

3. Demuestre usted mismo que cualquier operador definido por una expresión con una variable libre que ocurre solo positivamente es monótono. Entonces, la ocurrencia positiva es una condición sintáctica que es suficiente para imponer la monotonicidad.$X$

Me parece que no hay sustituto para hacer estas pruebas por ti mismo para realmente internalizar la intuición.

Esta es una publicación muy antigua, por lo que es posible que ya haya encontrado la respuesta deseada. Desde que he estado estudiando FO (LFP) durante los últimos meses. Tengo cierta comprensión de las respuestas que necesita.

$[\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\ \}$. Si este operador es monótono, podemos capturar fácilmente el punto fijo en la estructura finita e infinita siguiendo el teorema del punto fijo de knaster tarski mencionado en las respuestas anteriores. Pero, el problema es probar si la fórmula escrita en el formulario anterior codifica un operador monótono o no es indecidible, por lo que debemos obtener la siguiente mejor opción. La positividad en la variable libre de segundo orden asegura que se cumple el requisito de monotonicidad, es una inducción estructural estándar para probar este fenómeno. La pregunta es, ¿es suficiente?

Para eso, todavía no tengo una respuesta sólida, ya que todavía estoy leyendo. Puedo señalar documentos en este frente. Al menos la que explica las ideas que mencioné aquí, son del artículo, Monotone vs Positive - Ajtai, Gurevich. También menciona otro documento Extensiones de punto fijo de lógica de primer orden por Gurevich y Shelah que establece que el operador de punto fijo cuando se aplica a la fórmula positiva no pierde poder expresivo en comparación con la aplicación que se realiza sobre fórmulas monótonas arbitrarias.