Понимание логики с наименьшей фиксированной точкой

Чтобы лучше понять статью, я пытаюсь получить краткое представление о логике с наименьшей фиксированной точкой. Есть несколько моментов, в которых я застрял.

Если $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)) \}$$

оператор бинарного отношения $P$, Я не понимаю, почему наименее фиксированная точка$P^*$ из $P$ является транзитивным закрытием $E$, Пример взят из теории конечных моделей и ее приложений (стр. 60).

При расширении логики первого порядка с помощью оператора наименьшего фиксированного указателя я не понимаю, почему символ отношения $S_i$должен быть положительным в формуле. Положительный означает, что каждый случай$S_i$ в формуле находится в четном числе символов отрицания.

Кто-нибудь знает, что хорошо читать для интуитивного понимания логики наименее фиксированного указателя и его синтаксиса и семантики?

Если у вас возникли проблемы с понятием наименьшей фиксированной точки, я бы порекомендовал потратить некоторое время на изучение основ более общей теории порядка.

Дейви и Пристли, Введение в Решетки и Порядок - хорошее введение.

Чтобы понять, почему транзитивное замыкание является наименьшей фиксированной точкой, представьте, что построение замыкания происходит из пустого набора, применяя логическую формулу по одному шагу за раз. Наименьшая фиксированная точка появляется, когда вы не можете добавить новые ребра, используя формулу.

Требование, чтобы формула была положительной, гарантирует, что процесс является монотонным, то есть, что он растет на каждом этапе. Если бы у вас была отрицательная субформула, у вас мог бы быть случай, когда на некоторых шагах набор ребер будет уменьшаться, и это может привести к непрекращающимся колебаниям вверх и вниз, а не к схождению в 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$что происходит только положительно, является монотонным. Таким образом, позитивный случай - это синтаксическое состояние, достаточное для обеспечения монотонности.

Я считаю, что ничто не заменит этих доказательств для того, чтобы действительно усвоить интуицию.

это очень старая запись, поэтому вы, возможно, уже нашли ответ на свой вопрос. Так как я изучал ФО (LFP) в течение последних нескольких месяцев. У меня есть понимание ответов, которые вам нужны.

Чтобы ответить требованию положительности, необходимо исходить из того факта, что проверка того, захватывает ли формула монотонный оператор или нет, неразрешима как в конечных, так и в бесконечных моделях. Что я имею в виду под формулой захвата монотонного оператора? Предположим, вы записываете FO$[\sigma$] формула со свободной переменной второго порядка скажем $\phi(\vec{x},X)$, где $|\vec{x}|=ar(X)$тогда мы можем определить соответствующий оператор $f_\phi$ : $\mathcal{P}(A^{ar(X)}) \mapsto \mathcal{P}(A^{ar(x)})$ где ar (X) - арность переменной второго порядка, а A - область $\sigma$-структура $\mathbb{A}$ а также $\mathcal{P}(Z)$ является набором мощности множества Z. И $f_\phi(Z) = \{\ \vec{a} \in A^{ar(X)}\ |\ \mathbb{A},\vec{a},Z \models \phi\ \}$, Если этот оператор является монотонным, то мы можем легко зафиксировать неподвижную точку как в конечной, так и в бесконечной структуре, следуя теореме Кнастера Тарского о неподвижной точке, упомянутой в ответах выше. Но проблема состоит в том, чтобы проверить, является ли формула, записанная в форме, описанной выше, кодирующим монотонный оператор, или нет, неразрешима, поэтому нам нужно получить следующую лучшую вещь. Позитивность в свободной переменной второго порядка обеспечивает выполнение требования монотонности, что является стандартной структурной индукцией для доказательства этого явления. Вопрос в том, достаточно ли этого?

На это у меня пока нет четкого ответа, так как я все еще читаю. Я могу указать на документы по этому вопросу. По крайней мере, одно объяснение идей, которые я упомянул здесь, взято из статьи « Монотон против позитива» - Айтай, Гуревич. В нем также упоминается еще одна статья « Фиксированные точки расширения логики первого порядка » Гуревича и Шелаха, в которой говорится, что оператор фиксированной точки при применении к положительной формуле не теряет выразительную силу по сравнению с приложением, выполненным над произвольными монотонными формулами.