Monadyczna logika drugiego rzędu dla manekinów

Jestem programistą z automatami, ale nie logiką.

Przeczytałem w artykułach, że te dwa są ze sobą ściśle powiązane. Deterministyczne automaty skończone (DFA), automaty drzewa i automaty z widocznym przesunięciem w dół są powiązane z logiką Monadic drugiego rzędu (MSO). Chociaż rozumiem automaty i ludzie (w dokumentach) próbowali mi wyjaśnić związek z MSO, zawsze zakładają silne zaplecze logiczne i zrozumienie MSO.

Kiedy patrzę na książki i kursy z logiki, przeważnie obsługują one tylko logikę pierwszego rzędu, która wydaje się dość prosta i składa się tylko z kilku pojęć: zmienne, lub, nie, sugeruje, dla wszystkich, istnieje itp.

Czy ktoś może mi wyjaśnić lub wskazać mi zasób, który może wyjaśnić:

Czym jest logika drugiego rzędu w przeciwieństwie do logiki pierwszego rzędu?
Czym jest logika monadyczna a nie monadyczna?
Dlaczego ważne jest, aby logika drugiego rzędu była monadyczna, aby można było o niej zadecydować LUB dlaczego to niewłaściwe pytanie?
Dlaczego rozstrzygająca jest logika monadyczna drugiego rzędu?
Relacja z przynajmniej DFA?

Jeśli jest to zasób, fajnie byłoby założyć, że jestem programistą, a nie logikiem. Oznacza to, że chciałbym zrozumieć, jak zaimplementuję go jako kod, ponieważ do tego czasu matematyka wydaje mi się magią;)

Dziękuję za wszelką pomoc, którą możesz mi udzielić. Byłbym bardzo wdzięczny.

automata finite-automata logic coq automated-theorem-proving Walter Schulze
źródło

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

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

Czym jest logika drugiego rzędu w przeciwieństwie do logiki pierwszego rzędu?

Czym jest logika monadyczna a nie monadyczna?

$\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*}$

Innymi słowy, istnieją takie kolory czerwony, zielony i niebieski, że

każdy wierzchołek ma kolor
i żaden wierzchołek nie ma dwóch kolorów
a jeśli między dwoma wierzchołkami znajduje się krawędź, te dwa wierzchołki nie mają tego samego koloru.

$k$ $k$ $k=1$ $1$

Dlaczego ważne jest, aby logika drugiego rzędu była monadyczna, aby można było o niej zadecydować LUB dlaczego to niewłaściwe pytanie?

Dlaczego rozstrzygająca jest logika monadyczna drugiego rzędu?

Szczerze mówiąc, nie pamiętam problemów rozstrzygalności. Kluczową kwestią jest to, że pełna logika drugiego rzędu pozwala określić ilościowo istnienie liniowego rzędu domeny

\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$

(Myślę, że jeśli twoja domena jest nieskończona, prawdopodobnie musisz dodatkowo określić, że porządek liniowy jest dyskretny i ma minimalny element; wtedy wiesz, że ma on początkowy segment, który jest izomorficzny do liczb naturalnych, i że powinno to być dość.)

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

Relacja z przynajmniej DFA?

$\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)$
ostateczna pozycja jest w stanie akceptacji.

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

W tej chwili nie przypominam sobie dowodu na odwrót (że wszystko, co można zdefiniować w MSO, może zostać rozpoznane przez odpowiedni automat). Jeśli będę miał czas, sprawdzę to i opublikuję szkic.

$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$

David Richerby
źródło

Dodano moją sugestię dotyczącą rozmowy. Oczekuje na zatwierdzenie przez @DavidRicherby

Hendrik Jan

Dziękuję za świetną odpowiedź. Nadal przetwarzam to wszystko i pracuję nad tym, szukam terminów, zastanawiam się, jak to zaimplementować itp. W międzyczasie myślę, że numer 3 był niewłaściwym pytaniem. Może raczej powinno tak być, dlaczego relacja między automatami i logiką jest tak ważna, że jest o tym mowa w wielu artykułach?

Walter Schulze

Dziękuję za doskonałą odpowiedź!

Klas.

Monadyczna logika drugiego rzędu dla manekinów

Odpowiedzi: