Монадическая логика второго порядка для чайников

Я программист с автоматом, но не с логикой.

Я читал в газетах, что они очень тесно связаны. Детерминированные конечные автоматы (DFA), древовидные автоматы и автоматы видимого нажатия - все они связаны с монадической логикой второго порядка (MSO). Хотя, я понимаю, что автоматы и люди (в статьях) пытались объяснить мне отношение к MSO, они всегда берут сильный фон в логике и понимании MSO.

Когда я смотрю на книги и курсы по логике, они в основном работают только с логикой первого порядка, которая кажется довольно простой и состоит только из нескольких понятий: переменные, или, что не подразумевается, для всех, существует и т. Д.

Может кто-нибудь объяснить или указать мне на ресурс, который может объяснить:

Что такое логика второго порядка в отличие от логики первого порядка?
Что такое монадическая и не монадическая логика?
Почему важно, чтобы логика второго порядка была монадической, чтобы ее можно было разрешить ИЛИ почему это неправильный вопрос?
Почему монадическая логика второго порядка разрешима?
Отношение хотя бы к ДФА?

Если это ресурс, было бы неплохо, если бы он предполагал, что я программист, а не логик. Это означает, что я хотел бы понять, как я реализовал бы это как код, потому что до тех пор математика кажется мне волшебством;)

Спасибо за любую помощь, которую вы можете оказать мне. Я был бы очень признателен.

automata finite-automata logic coq automated-theorem-proving Вальтер Шульце
источник

«Почему важно, чтобы логика второго порядка была монадической, чтобы ее можно было разрешить ИЛИ почему это неправильный вопрос?» если вы разрешите количественное определение по двоичному предикату, например,

затем вы сразу же получаете всю мощь логики первого порядка с помощью одного двоичного предиката, который уже неразрешим (даже без функций арности> 0 и без равенства) [Kalmar, Suranyi, 1950]

\exists M [. . . M (x, y) . . .]

$\exists M[...M(x,y)...]$

Vor

Что такое логика второго порядка в отличие от логики первого порядка?

Что такое монадическая и не монадическая логика?

Монадическая логика второго порядка - это логика первого порядка плюс квантификация по множествам. Таким образом, помимо возможности сказать, что существует элемент домена с некоторым свойством ( ), вы также можете сказать, что существует набор элементов домена с некоторым свойством. Так, например, мы можем определить 3-окрашиваемость графов, сказав $\exists x\dots$

\begin{aligned} \exists R \exists G \exists B [ & \forall x (x \in R \lor x \in G \lor x \in B) \\ \land \neg \exists x ((x \in R \land x \in G) \lor (x \in G \land x \in B) \lor (x \in B \land x \in R)) \\ \land \forall x \forall y (E (x, y) \to \neg ((x \in R \land y \in R) \lor (x \in G \land y \in G) \\ \lor (x \in B \land y \in B)))] . \end{aligned}

$\begin{align*} \exists R\,\exists G\,\exists B\, \big[&\forall x\,\big(x\in R\lor x\in G\lor x\in B\big)\\ &\land \neg\exists x\,\big((x\in R\land x\in G) \lor (x\in G\land x\in B) \lor (x\in B\land x\in R)\big)\\ &\land \forall x\,\forall y\,\big(E(x,y)\rightarrow \neg \big((x\in R\land y\in R)\lor (x\in G\land y\in G)\\ &\qquad\qquad\qquad\qquad\qquad\quad\lor (x\in B\land y\in B)\big)\big)\big]\,. \end{align*}$

На словах есть красный, зеленый и синий цвета, такие, что

каждая вершина имеет цвет
и ни у одной вершины нет двух цветов
и, если есть ребро между двумя вершинами, эти две вершины не имеют одинаковый цвет.

Общая логика второго порядка допускает не только количественную оценку по множествам, но и по произвольным отношениям по области. Напомним, что отношение - это набор кортежей по области для некоторого . Множества - это просто унарные отношения: а кортеж - это просто элемент области. $k$ $k$ $k=1$ $1$

Почему важно, чтобы логика второго порядка была монадической, чтобы ее можно было разрешить ИЛИ почему это неправильный вопрос?

Почему монадическая логика второго порядка разрешима?

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

\begin{aligned} \exists R \forall x \forall y \forall z [ & (R (x, y) \lor R (y, x)) \\ ((R (x, y) \land R (y, x)) \to x = y) \\ ((R (x, y) \land R (y, z)) \to R (x, z))] . \end{aligned}

$\begin{align*} \exists R\,\forall x\,\forall y\,\forall z\,\big[&(R(x,y)\lor R(y,x)\big)\\ &\big((R(x,y)\land R(y,x))\rightarrow x=y\big)\\ &\big((R(x,y)\land R(y,z))\rightarrow R(x,z)\big)\big]\,. \end{align*}$

$D$ $D^n$ $n$ $D^n$ $n$

(Я предполагаю, что если ваш домен бесконечен, вам, вероятно, нужно дополнительно указать, что линейный порядок дискретен и имеет минимальный элемент; тогда вы знаете, что у него есть начальный сегмент, который изоморфен натуральным числам, и это должно быть довольно.)

$\exists R_1\dots \exists R_k\,\varphi$ $R_i$ $\varphi$

Отношение хотя бы к ДФА?

$\Sigma$ $\leq$ $R_a$ $a\in\Sigma$ $R_a$

$k$ $Q_1, \dots, Q_k$ $Q_i$ $i$

$j$ $Q_1, \dots, Q_k$
$Q_1$
$j$ $Q_i$ $(j+1)$
окончательная позиция находится в состоянии принятия.

$j$ $j$ $j'>j$ $j'$

Прямо сейчас я не вспоминаю доказательство обратного (что все определяемое в MSO может быть распознано соответствующим автоматом). Если у меня будет время, я посмотрю это и опубликую эскиз.

$i$ $X$ $1$ $i$ $X$

$R_a(i)$ $i$ $a$ $i\in X$ $i$ $X$ $i<j$ $i$ $j$

$\lor, \lnot$ $\exists i, \exists X$ $\cup$ ${}^c$

Дэвид Ричерби
источник

Добавил мое предложение для обратного. В ожидании одобрения @DavidRicherby

Хендрик янв

Спасибо за отличный ответ. Я все еще обрабатываю все это и прорабатываю, выискиваю термины, думаю, как бы это реализовать и т. Д. В то же время я думаю, что вопрос № 3 был неправильным вопросом. Может быть, лучше было бы объяснить, почему связь между автоматами и логикой так важна, что она упоминается во многих статьях?

Вальтер Шульце

Спасибо за отличный ответ!

Клас.

Монадическая логика второго порядка для чайников

Ответы: