- What is second order logic in contrast to first order logic?
- What is monadic vs non monadic logic?
Monadic second-order logic is first-order logic plus quantification over sets. So, as well as being able to say that there exists a domain element with some property ($\exists x\dots$), you can also say that there exists a set of domain elements with some property. So, for example, we can define 3-colourability of graphs by saying
\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*}
In words, there are colours red, green and blue such that
- every vertex has a colour
- and no vertex has two colours
- and, if there's an edge between two vertices, those two vertices don't have the same colour.
General second-order logic allows not just quantification over sets but also over arbitrary relations over the domain. Recall that a relation is a set of $k$-tuples over the domain, for some $k$. Sets are just unary relations: $k=1$ and a $1$-tuple is just an element of the domain.
Why is it important for a second order logic to be monadic to be decidable OR why is this the wrong question?
Why is monadic second order logic decidable?
Honestly, I don't remember the decidability issues. A key point is that full second-order logic lets you quantify into existence a linear order of the domain
\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*}
That is, there exists a binary relation that is total, antisymmetric and transitive, i.e., is a linear order on the domain $D$. That implicitly gives you a linear order on $D^n$ for any $n$, and you can use relations on $D^n$ for large enough $n$ to simulate a Turing machine tape. But, with monadic SO, you can't do any of these things.
(I guess that, if your domain is infinite, you probably need to specify in addition that the linear order is discrete and has a minimal element; then you know that it has an initial segment that's isomorphic to the natural numbers, and that should be enough.)
On finite inputs, the existential fragment of SO – formulas of the form $\exists R_1\dots \exists R_k\,\varphi$, where the $R_i$ are relation symbols and $\varphi$ is first-order – defines exactly NP. Full second-order logic defines exactly the polynomial hierarchy. This is exactly because of the ability to encode Turing machines and the fact that quantifying a fixed collection of relations gives you a polynomial amount of stuff to play with.
- The relation to at least DFAs?
We can represent strings over some finite alphabet $\Sigma$ by relational structures. The vocabulary has a binary relation symbol $\leq$ that will be interpreted as a linear order, and a unany relation symbol $R_a$ for each character $a\in\Sigma$. Each element of the domain is a character in the string, the linear order tells you what order the characters appear in and the relations $R_a$ tell you what character appears in each position.
Now, suppose we have a DFA with $k$ states and let's assume we're dealing with finite strings, for now. We can write a formula that's broadly similar to the three-colourability formula above that says that our DFA accepts the string coded by its input. It says that there are sets (of domain elements, i.e., positions in the string) $Q_1, \dots, Q_k$, such that $Q_i$ will be the set of positions in the string at which the automaton is in state $i$. So assert that:
- each position $j$ is in exactly one of $Q_1, \dots, Q_k$;
- the first position is in $Q_1$ (assuming this is the start state);
- if the $j$th position is in $Q_i$ then the $(j+1)$th position is in whatever state the automaton's transition function says it should be;
- the final position is in an accepting state.
If this formula is true, the automaton must accept the string; if it's false, the automaton must reject. For NFAs, we just say that each position is in at least one state and the final state is in at least one accepting state. For infinite inputs, we can code, e.g., the Büchi condition by saying "for all positions $j$ in the input, if $j$ is in an accepting state, there's some $j'>j$ such that $j'$ is also in an accepting state.
Right now, I don't recall the proof of the converse (that everything definable in MSO can be recognized by an appropriate automaton). If I have time, I'll look that up and post a sketch.
Conversely, we can represent the meaning of MSO formulas by finite state automata inductively, following the construction of the automata. To do this we augment the alphabet of the automaton, by adding components that indicate the value of the free position variables $i$ and set variables $X$. If we read a string along the automaton we find exactly a single $1$ to indicate a certain postion $i$, and the positions in a set $X$ are marked likewise.
The basic formulas are $R_a(i)$ for "position $i$ has symbol $a$", $i\in X$ for "$i$ is an element of $X$" and $i<j$ for "position $i$ is before position $j$".
These formulas can be represented by the following simple finite state automata (over the augmented alphabet suited for the formula):
More complicated formulas are constructed using the Boolean connectives $\lor, \lnot$ and the existential quantifiers $\exists i, \exists X$. The intended meaning of these operators are easily translated to languages as the language operators union $\cup$, complement ${}^c$ and projection, which is the operation that removes the corresponding component from the augmented alphabet. For union we have to pay some attention to the augmented alphabets in case the two parts of the formula do not agree on the set of free variables. Projection is simple, but it will change a deterministic automaton into a nondeterministic one.
