Logic grid puzzles and Beth's Definability Theorem

Logic Grid Puzzles are popular in magazines and newspapers. In such puzzles, the reader is asked to deduce an answer to a question from a set of clues in some scenario. For example, the scenario may be as follows: five guys are having drinks in a room. The clues are often information like "They all come from different countries", "The British is in blue" or "People in red don't drink alcohol". The question may be "What does the German drink?". The reader usually tries to deduce the answer by filling out a matrix with the clues, like the right one.
Puzzles of this kind involve turning an implicit characterisation (i.e. the clues) into an explicit one (i.e. a direct answer to the question). In formal logic, we may define a relation explicitly with a formula. More precisely, given a theory $S$ (i.e. a set of sentences), an n-ary relation $R(x_1,...,x_n)$ is explicitly defined by $\Phi$ w.r.t. $S$ if$$S \models \forall x_1,...,x_n: R(x_1,...,x_n)\equiv\Phi(x_1,...,x_n),$$where $\Phi(x_1,...,x_n)$ is a formula that doesn't refer to $R$. (If $A,B$ are theories, $A\models B$ means that every model of $A$ is also a model of $B.$) In contrast, a theory referring to a relation may not uniquely determine that relation. Intuitively, a theory characterises a relation $R$ iff we cannot find two models of the theory that are only different in their interpretations of the symbol $R$. More formally, if $S$ is a theory of vocabulary $\tau$, then $S$ implicitly defines a non-logical symbol $R\in\tau$ iff for all structures $A$ of vocabulary $\tau\setminus\{R\}$, there exist at most one relation $R^A$ over the domain of $A$ such that $A$ becomes a model of $S$ by interpreting $R$ to $R^A$. There are several equivalent ways to express this concept (e.g. this and this), but we shall use the following one for our convenience of proof:
Definition. A theory $S$ implicitly defines an n-ary relation $R(x_1,...,x_n)$ if$$S\cup S' \models \forall x_1,...,x_n: R(x_1,...,x_n)\equiv R'(x_1,...,x_n),$$where $S'$ is obtained by replacing every occurrence of $R$ in $S$ with a fresh relation symbol $R'$.
If a $R$ is explicitly defined by $\Phi$ w.r.t. $S$, then it is clear that $R$ can also be implicitly defined by $S$. The converse result is proved by Beth for first-order logic.
Theorem. (Beth's Definability Theorem for FOL) If a first-order property is implicitly definable then it can also be defined explicitly.
Beth's result is a corollary of Craig's Interpolation Theorem.
Lemma. If $A$ is a theory and $A\models \varphi$, then there is a finite set $A'\subseteq A$ such that $A'\models \varphi.$
Proof of lemma. Note that $A\models \varphi$ if and only if $A\cup \{\neg \varphi\}$ is unsatisfiable. By the compactness theorem, there is a finite subset $E\subseteq A\cup \{\neg \varphi\}$ that is unsatisfiable. If $\neg \varphi\not\in E$ then let $A' = E$. Otherwise, let $A' = E\setminus\{\neg \varphi\}$. Then $A'$ is the desired set. ◻
Proof of Beth's theorem. Suppose we have$$S\cup S' \models \forall x_1,...,x_n: R(x_1,...,x_n)\equiv R'(x_1,...,x_n).$$By the above lemma, we can assume w.l.o.g. that $S,S'$ are finite. Let $X=\bigwedge S$ and $X'=\bigwedge S'$. Our assumption implies that $$X\wedge X' \rightarrow \forall x_1,...,x_n: R(x_1,...,x_n)\equiv R'(x_1,...,x_n)$$is valid. By introducing fresh variables $p_1,...,p_n$, we can rewrite the above sentence to $X\wedge X' \rightarrow (R(p_1,...,p_n)\equiv R'(p_1,...,p_n))$, which is further equivalent to$$(X\wedge R(p_1,...,p_n)) \rightarrow (X' \rightarrow R'(p_1,...,p_n)).$$Since $X$ doesn't contain $R'$, and $X'$ doesn't contain $R$, by Craig's theorem there exist a formula $\Phi(p_1,...,p_n)$ containing neither $R$ nor $R'$, such that both$$(X\wedge R(p_1,...,p_n)) \rightarrow \Phi(p_1,...,p_n) \quad\mbox{and}\quad \Phi(p_1,...,p_n) \rightarrow (X' \rightarrow R'(p_1,...,p_n))$$ hold. Note that the latter can be rewritten to $\Phi(p_1,...,p_n) \rightarrow (X \rightarrow R(p_1,...,p_n))$ by replacing every occurrences of $R'$ with $R.$ It follows from the currying law that$$X \rightarrow (R(p_1,...,p_n) \rightarrow \Phi(p_1,...,p_n))\quad\mbox{and}\quad X \rightarrow (\Phi(p_1,...,p_n) \rightarrow R(p_1,...,p_n))$$are valid. Conjuncting the two formulas leads to $$X \rightarrow (R(p_1,...,p_n) \equiv \Phi(p_1,...,p_n)),$$ which further implies that $$S \models \forall x_1,...,x_n: R(x_1,...,x_n) \equiv \Phi(x_1,...,x_n).$$ This concludes the proof of the theorem. ◻
Craig's interpolation can be computed via syntactical transformation, as is shown in Craig's 1957 paper. Hence, we can always construct an explicit definition out of an implicit one. Since explicit definition is a syntactical notion (i.e. defined with a formula) while implicit definition tends to be more semantical (i.e. defined with a theory), Beth's theorem indicates that the syntactical definability of first-order logic is "complete" in some sense.

References

1. Craig’s Interpolation Lemma and Beth’s Definability Theorem

2. Understanding Definability in First-Order Logic

A note on linking ideas in academic writing

Flow of information

Sentences and ideas should be ordered and linked to present information in a reasonable manner. Here reasonable means the reader can easily find what he expects to see as he reads. The following example shows how sentences can be re-ordered to improve readability. It is extracted from the first paragraph of an essay with title "The main sources of diversity in work values":

Original		Revised
The importance of education should be pointed out as one of the crucial sources of diversity in attitudes to work. The rising educational level has been perceived as one of the most significant investments in the general quality of life. Tertiary education in particular plays a very special role in this respect.		One of the crucial sources of diversity in attitudes to work is education. The rising educational level has been perceived as one of the most significant investments in the general quality of life. In this respect, tertiary education in particular plays a very special role.

Comments. It is preferred that the first sentence connects directly to the title, as that is what a reader expects when he starts reading the paragraph. The importance of education is redundant here because education is already pointed out as a crucial source. In this respect should be put at the beginning of a sentence since it serves as a linking phrase.

Text cohesion

Cohesion refers to the way in which elements of language are linked together to make a text. The sequence of given information followed by new information can contribute to the cohesion of a text because the new information of one sentence often becomes the given information of the next sentence. The following is an extract from a thesis about the construction of stance in academic writing. Words are colourised to show how old information is rephrased or repeated to improve smooth transitions to new information.

Passage		Comments
For the thesis writer, the construction of stance takes a distinctive form which derives from the nature of the thesis itself.		Clarify the subject of this passage and identify the expected target readers—the thesis writers.
As noted above, writers have to convince the supervisors and examiners to accept their research, which means that the thesis is inherently persuasive.		Clarify the goal of thesis writers to bring up the key characteristic of a thesis: being persuasive.
However, acceptance depends upon satisfying two quite distinct requirements.		The subject acceptance (of persuasion) follows logically from the key old info "being persuasive".
The first is that the thesis should make an original contribution to knowledge.		Introduce a claim.
In creating new knowledge and conveying it to other members of the discipline, the writer’s stance is that of a professional.		Rephrase the claim and reach a partial conclusion.
The second requirement is that the thesis must show mastery of the field.		Make another claim.
The display of established knowledge is required because the work will be assessed and thus the writer must also take a stance as a candidate.		Rephrase the claim and make another partial conclusion.
However combining the roles of candidate and professional can lead to considerable conflict and uncertainty.		Summarise the partial conclusions and start a new discussion.

As this example demonstrates, the new information of one sentence often becomes the given information of the next sentence. This sequence of given information → new information links the ideas of the text together and creates cohesion.

Devices to link ideas

We present more examples showing how ideas can be linked between sentences grammatically. In the second sentences of each example, the given information are referred using three kinds of grammar patterns. New ideas can be introduced by adding extra information to the given information.

Examples		Comments
Contrast from differently doped regions immediately appears when the in-lens detector is switched on. This huge effect is believed to hold some important implications.		A comment (ie. the effect is huge) is implicitly introduced when the old information, which is a neutral description of a fact, is referred. It is preferable to separate description and evaluation clearly in academic writing.
It will be seen in the sample that the simulation is able to adapt again. The ability of this model to emulate changes in the characteristics of different sample types is cited as strong support for its validity.		The old information is rephrased by changing part of speech and inverting subject and object. By such rephrasing we avoid using "..., which ..." repeatedly for further explanation/elaboration.
In this analysis, "norm" refers to a prescribed or proscribed standard of behaviour. Such a definition is therefore broader than rules alone.		Using such a instead of this means that the author is going to generalise. In this case, the author intends to discuss a class of definitions instead of the definition of "norm".
The fact that the same British forces had to cover various commitments at once did stretch them to the limit, and perhaps beyond. The problem of over-stretch had emerged in the late 1950s.		The use of problem and over indicates the author's position in the following discussion on the aforementioned fact. Description and evaluation is cleanly separated.
For example, it would be interesting to find out if the active region contains more crystalline polymer as a result of operation. Such an investigation would involve using staining techniques.		The noun investigation is used to encapsulate the text to find out .... The use of such a indicates that the following discussion would not be restricted to that particular example.

Remark. The main device for linking ideas in these examples is called nominalisation, which is the use of a noun to express an idea that is previously expressed in the form of a clause or a sentence. Nominalisation is very useful in the construction of argument, as we can present what we already said in a shortened form and then move on to the new point following from that information. Here is an example:

I explained the results as such and such. This explanation is in agreement with earlier work.

We can add more details to the noun using prepositional phrases and clauses:

What I have sought to disprove is that there is an incompatibility between a "bad" nationalism and a "good" patriotism. The assertion that nationalism and patriotism are incompatible causes complete confusion when historians, even great ones, are confronted by past thinkers.

A note on useful decidable logics & theories

Note that this post discusses decidable fragments that allows at least some degree of quantifications, not decidable theories of ground formulas used in SMT solvers.

Decidable fragments of first-order logic

Monadic first-order logic. Also known as the relational monadic fragment (RMF) or the Löwenheim class [2], this fragment is a classical example of decidable first-order logic without equality. The RMF consists of the first-order formulas where all relation symbols are unary:$$\phi ::= R(x) \mid \neg \phi \mid \phi \vee \phi \mid \phi \wedge \phi \mid \exists x.\phi \mid \forall x.\phi.$$Note that equality is not allowed in this logic and there are no constant symbols. Satisfiability of the logic is first proved to be NE-complete [2], where NE = $\bigcup_c NTIME(2^{cn})$. Later it is shown that NE = NEXPTIME [1], and thus the problem is NEXPTIME-complete. The Löb-Gurevich class (cf. [8]) is a decidable extension of the RMF where unary function symbols are also allowed. Both of the classes enjoy the finite model property, cf [8].

Effectively propositional logic (EPR). [5] Also known as the Bernays-Schönfinkel class, this fragment consists of first-order formulas such that:
1. The vocabulary is restricted to constant and relation symbols.
2. The quantifier prefix is restricted to $\exists^*\forall^*$ for formulas in prenex normal form.
Condition 2 implies that EPR is not closed under negation. EPR enjoys the finite model property, meaning that a satisfiable formula is guaranteed to have a finite model. The satisfiability problem of EPR is NEXPTIME-complete.
We can extend EPR to allow quantifier alternation and function symbols while maintaining the same properties, as long as the formula in the extended logic is "stratified" [11]. More precisely, we define the quantifier alternation graph $G(\phi)$ for a formula $\phi$ as a directed graph where the set of vertices is the set of sorts, and for each function symbol $f : (s_1,\ldots, s_n) \to s$ in the skolem normal form of $\phi$, there is an edge $s_i \to s$ for $1 \le i \le n$. $\phi$ is called stratified if $G(\phi)$ does not contain a cycle through the sort of some universally quantified variable. For example, $\phi := \forall x. \exists y. f(x) = y$ is skolemized to $\forall x. f(x) = g(y)$ with $f,g : A \to B$. Hence $G(\phi)$ is acyclic and thus $\phi$ is in the decidable fragment.
Stratified formulas are also decidable, for there is no way to generate an infinite sequence of instantiation terms. By contrast, $\psi := \forall x. \exists y. f(y) = x$ is skolemized to $\forall x. f(g(x)) = x$ where $f: A \to B$ and $g: B \to A$. Hence $G(\psi)$ contains a cycle through the sort of $x$, and thus $\psi$ is not in the decidable fragment.
Formulas in the extended EPR can be effectively translated into propositional logic formulas through a instantiation process over a finite Henken domain, see e.g., [12,13]. Extended EPR is supported by first-order logic provers such as iProver (which is known as the most efficient solver for EPR), and by modern SMT solvers such as Z3.

Presburger arithmetic. The first-order theory of structure $(\mathbb N, +)$ can be decided by encoding $n\in \mathbb N$ in binary (LSB first), such that the atomic ternary-relation $+$ corresponds to a regular relation $+_2$ over this coding and $\mathbb N$ corresponds to the $\omega$-regular language $(0+1)^*0^\omega$. Buchi has shown in 1962 that given any formula $\phi(x_1,...,x_n)$ over ${\rm FO}(\mathbb N, +)$, one can effectively compute an $\omega$-automaton $A(x_1,...,x_n)$ that defines the same relation modulo convolution $\otimes$, namely, $\phi(x_1,...,x_n)$ holds iff $A$ accepts the $\omega$-word $x_1 \otimes \cdots \otimes x_n.$ Satisfiability problem for ${\rm FO}(\mathbb N, +)$ thus reduces to the emptiness problem for $\omega$-automata and is thus decidable. See [9] for a review of the algorithmic and computational complexity aspects of PA. Also see a recent historical review in this paper and its presentation.

A list of decidable theories can be found on Wikipedia.

References

1. Structural properties of complete problems for exponential time. 1997.
2. Complexity results for classes of quantification formulas. 2001.
3. Verification of randomised security protocols.
4. Decidability of second-order theories and automata on infinite trees. 1969.
5. Complexity results for classes of quantificational formulas. 1980.
6. The theory of ends, pushdown automata, and second-order logic. 1985.
7. Bisimulation through Probabilistic Testing. 1991.
8. The Classical Decision Problem. 2001.
9. A Survival Guide to Presburger Arithmetic. 2018.
10. Automata: From Logics to Algorithms. 2007.
11. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. 2009.
12. Deciding effectively propositional logic using DPLL and substitution sets. 2008.
13. Proof systems for effectively propositional logic. 2008.

A note on bisimulation and coinduction

A machine $(X,Y,S,\delta,\lambda)$ is a 5-tuple composed by an input alphabet $X$, an output alphabet $Y$, a state space $S$, a transition function $\delta:S\times X \rightarrow S$, and an output function $\lambda: S\rightarrow Y.$ We assume that $\delta$ is total without loss of generality. Also, its domain be extended to $X^*$ by defining $\delta^*(s,\epsilon)=s$ and $\delta^*(s,wx)=\delta(\delta^*(s,w),x).$ A bisimulation $R$ between two machines $M=(X,Y,S,\delta,\lambda)$ and $M'=(X,Y,S',\delta',\lambda')$ is a relation on $S\times S'$ defined recursively as $$R=\{(s,s'): \lambda(s)=\lambda'(s') \wedge \forall x\in X. (\delta(s,x),\delta'(s',x))\in R\}.$$ The union of all bisimulations is the greatest bisimulation and is often denoted by $\sim$. When $\sim$ is defined for one machine, it forms an equivalence relation and is called bisimilarity. Bisimilarity can be characterised inductively as follows. We define a sequence of equivalence relations $R_0 \supseteq R_1 \supseteq \cdots$ by letting $R_0 = S\times S$ and for $n\ge 1$, $(s, s') \in R_n$ iff for all $x\in X$, $\delta(s, x)$ implies $\exists x'\in X.\ (\delta(s, x), \delta(s', x')) \in R_{n-1}.$ It is easy to verify that the $R_n$ converges to the bisimilarity $\sim$, namely, $\bigcap_{n\ge 0} R_n=\sim$. (To see this, note that $\supseteq$ holds as $R_n \supseteq \sim$ for all $n\ge 0.$ Also, $\bigcap_{n\ge 0} R_n$ is a bisimulation and thus $\subseteq$ holds.) This inductive definition gives a simple fixpoint procedure for computing bisimilarity, see below.

Bisimulation and language equivalence

We call a machine a (deterministic) automaton if its output alphabet, denoted by $\mathcal{B}$, consists of only "rejected" and "accepted", denoted by $\bot$ and $\top$, respectively. It is interesting to note that a bisimulation $R$ between two automata $M$ and $M'$ over the same input alphabet $X$ can be itself described by an automaton $(X,\mathcal{B},R,\delta_R,\lambda_R)$, such that
1. $\delta_R((s,s'), x)=(\delta(s,x),\delta'(s',x))$ iff $(\delta(s,x),\delta'(s',x))\in R,$ and
2. $\lambda_R((s,s'))=\lambda(s)=\lambda'(s').$
Given an automaton $M=(X,Y,S,\delta,\lambda)$, the state language of a state $s$ of $M$ is defined as $L(s)=\{w\in X^{*}:\lambda\circ\delta^*(s,w)=\top\}.$ We call $L(s)$ the language of $M$ when $s$ is the initial state of $M$. The following implication can be shown by induction on the length of words:$$s\sim s' \implies L(s)=L(s').$$
Bisimulation equivalence is also called behavioural or observational equivalence by regarding the observable behaviours of a state as its state language. In the world of finite-state systems, two other notions of equivalence are often used in practice to prove language equivalence. The first notion is graph isomorphism. As the minimal automaton recognising a ($\omega$-)regular language is unique up to graph isomorphism, checking language equivalence amounts to checking graph isomorphism between their minimised automata. The second notion is trace equivalence, which relates two states iff they yield the same set of traces. Trace equivalence and bisimulation equivalence coincide on deterministic machines but the latter is finer in general (e.g. consider $a(b+c)$ v.s $ab+ac$). Here is a comparison among the three relations on finite machines:
Complexity: Bisimulation equivalence is $O(m\log n)$; Graph isomorphism is in NP; Trace equivalence is PSPACE-Complete.
Fineness: Graph isomorphism (w.o. minimisation) $\subseteq$ Bisimulation equivalence $\subseteq$ Trace equivalence $\subseteq$ Language equivalence

The proof principle of coinduction

Coinduction is a mathematical tool to define bisimulation. To demonstrate its use, we present here a technique that proves language equivalence using coinduction [1]. A $w$-derivative of a language $L\subseteq X^{*}$ is defined as $L_{w}=\{u\in X^{*}:wu\in L\}.$ The set of $\mathcal{L}$ languages on $X$ can be defined as an automaton $M_{\mathcal{L}}=(X^{*},\mathcal{L},\mathcal{B},\delta,\lambda)$ such that $\delta(L,x)=L_{x}$ and $\lambda(L)=\top$ iff $\epsilon\in L$. It turns out that $L(l)=l$ for all $l\in\mathcal{L}$, namely the state language of each state in $M_{\mathcal{L}}$ is the state itself. Hence we have$$L\sim L' \iff L=L'.$$This fact provides a uniform way to prove the equivalence of two languages. The more familiar method of proof by induction requires that one start from the equality of the base case (which is the pair of the minimal words in the two languages) and proceed to establish the equivalence of the pairs of longer words. Induction however doesn't work when the languages contain words of infinite length. In contrast, proof by coinduction starts from $\{(L,L')\}$ and continues to include more and more pairs via the transitions until a least fixed point is reached. This fixed point, whenever exists, is a bisimulation relation contained in the bisimilarity $\sim$ and thus implies that $L = L'.$
The principle of coinduction is not always effective—the process of constructing a bisimulation may not terminate even when the target languages are equivalent. This fact can be expected since otherwise the Halting problem would be solvable. On the other hand, the coinduction process always terminates when the two languages under consideration are regular: it either constructs a bisimilarity when they are equivalent, or finds a counterexample when they are not. In the case when the two languages are the same regular language, the process actually constructs the smallest finite automaton recognising them (more details later). This fact is a corollary of Kleene's Theorem, stating that a language is regular iff it is accepted by a finite automaton; see Section 8 of [1] for details. In fact, the most efficient equivalence checking algorithm for regular languages up to date is based on coinduction [4].

Bisimulation and fixed points

Given a machine $M = (X,Y,S,\delta,\lambda)$, one can define a monotone function $$F(A) := \{(s,s')\in S\times S : \forall x\in X\cup\{\epsilon\}.(\delta(s,x),\delta(s',x))\in A\}$$on lattice $(2^{S\times S},\subseteq).$ In the terminologies of fixed-point theory, bisimulations are the post-fixed points of $F$ and bisimilarity is the greatest post-fixed point $\nu X.~F(X).$ (Note: these fixed points collapse when $\delta$ defines deterministic transitions.) In this regard, proof by coinduction can be seen as showing that a property is closed under backward computation and contained in a coinductively defined set (ie. the greatest fixed point). In contrast, induction involves showing a property is closed under forward computation and containing an inductively defined set (ie. the least pre-fixed point). Intuitively, backward means that the set is obtained by keeping refine larger sets until the first (ie. the greatest) fixpoint is reached; and forward oppositely means that the set is obtained by keeping extend smaller sets until the first (ie. the smallest) fixpoint is reached.
The following procedure gives a naive fixpoint computation for the bisimilarity over a finite and non-deterministic machine. The bisimilarity is represented as a functional relation $\rho \subset S\times\mathbb N$ that maps states to labels of the equivalence classes induced by the bisimilarity.

Procedure ComputeBisimilarity
Begin
  Set $\rho := \{(s, 1) : s \in S\}$, $\rho' := \emptyset$
  While $\rho \neq \rho'$ do
    Set $\gamma := \{(s, \{ (x, \emptyset) : \delta(s,x)\in S \}) : s \in S \}$
    For all $s, x, s'$ such that $\delta(s,x) = s'$
      Set $\gamma(s)(x) := \gamma(s)(x) \cup \{ \rho(s') \}$
    Set $id := 0$, $A' := \mathbb N$, $\rho' := \emptyset$
    Let $L$ be a listing of $\gamma$ sorted by the second component
    For each $(s,A)$ in $L$ do
      If $A\neq A'$ then
        Set $A' := A$, $id := id + 1$
      Set $\rho' := \rho' \cup \{(s,id)\}$
  Output $\rho$ as the equivalence classes induced by the bisimilarity
 End

The procedure starts from a trivial binary relation where all states are equivalent. In each iteration, the algorithm computes a mapping $\gamma$ from each state to the labelling of its successors induced by the current bisimulation. A state will then be re-labelled according to the labelling of its successors changes. The refinement will continue until the labelling is stable, meaning that the greatest fixpoint (i.e. the unique largest bisimulation) is reached. See this paper for a survey of algorithms for computing bisimulations.
The fact that bisimulation relation can be constructed inductively implies that coinductive and inductive reasoning should yield the same results on inductively defined structures such as lists and trees, and make a difference only on structures that contain cycles or infinite paths. Further, while bisimulation coincides with bisimilarity on deterministic machines (such as $M_{\mathcal L}$), coinduction in general does not pinpoint bisimilarity for non-deterministic machines.

Bisimulation and minimisation

A homomorphism between two machines $M$ and $M'$ over the same input alphabets is any function $f:S\rightarrow S'$ satisfying $f(\delta(s,x))=\delta'(f(s),x)$, namely $$ \array{ S\times X &\overset{f\times id_X}{\longrightarrow}& S'\times X \\ \delta \downarrow & & \downarrow \delta' \\ S &\overset{f}{\longrightarrow}& S' }$$A homomorphism is called unique if given any homomorphism $g$ there exists an isomorphism $h$ such that $f=h\circ g$. The notion of unique homomorphisms is closely related to that of bisimulations. First, a mapping $f:S\rightarrow S'$ is a homomorphism iff $\{(s,f(s)):s\in S\}$ is a bisimulation between machines $M$ and $M'$. Furthermore, given a homomorphism $f:S\rightarrow S'$,
i) If $R$ is a bisimulation on $M$, then $f(R)=\{(f(u),f(v)):(u,v)\in R\}$ is a bisimulation on $M'$. [p.34, 5]
ii) If $R'$ is a bisimulation on $M'$, $f^{-1}(R')=\{(u,v):(f(u),f(v))\in R'\}$ is a bisimulation on $M$. [p.34, 5]
iii) $f$ is unique iff for any homomorphism $g:S\rightarrow S'$, the set $\{(f(s),g(s)):s\in S\}$ is a bisimulation on $M'$.
Unique homomorphism is a powerful utility to study languages and automata. For example, fix an automaton $M$ and consider a mapping $\phi: s \mapsto L(s)$ from $M$ to $M_{\mathcal L}.$ It is straightforward to check that $\phi$ is a unique homomorphism. One interesting fact about $\phi$ is that it identifies precisely the bisimilar states in $M$. That is, $$u\sim v \iff \phi(u)=\phi(v),$$which follows from the fact that $\{(u,v)\in S\times S: \phi(u)=\phi(v)\}$ is a bisimulation on $M$ and that $\{(\phi(u),\phi(v))\in \mathcal{L}\times \mathcal{L}:u\sim v\}$ is a bisimulation on $M_{\mathcal L}.$ Another amazing fact is that $\phi$ effectively minimises automata. To see this, let $\langle s \rangle_N$ (resp. $\langle S \rangle_N$) denote the sub-automaton generated by state $s$ (resp. sets of states $S$), i.e., the automaton induced by the states reachable from $s$ (resp. $S$), in automaton $N$. Also, we lift $\phi$ to a graph homomorphism such that given an automaton $N$, $\phi(N)$ is the sub-automaton of $M_{\mathcal L}$ generated by $\{\phi(s):s\in State(N)\}$. It turns out that$$\langle L(s) \rangle_{M_{\mathcal L}} = \langle \phi(s) \rangle_{M_{\mathcal L}} = \phi(\langle s \rangle_M).$$Since given $L$ we are free to choose any $s$ and $M$ satisfying $L(s)=L$, it follows that
i) If $L$ is regular, then $\langle L \rangle_{M_{\mathcal L}}$ is the canonical minimum automaton accepting $L$, and
ii) $\phi(\langle s \rangle_M)$ is the canonical minimisation of automaton $\langle s \rangle_M$.
In particular, $L$ is accepted by a finite automaton iff $\{L_w: w\in X^*\}$ is finite. This result is equivalent to the well-known characterisation of regular languages by Nerode and Myhill:
Theorem. (Nerode-Myhill) $L$ is accepted by a finite automaton if $R_L$ has a finite index. (Namely there are a finite number of classes in the equivalence relation $R_L$ on $L$ defined by $(u,v)\in R_L$ iff $\forall w\in L. (uw\in L \iff vw\in L).$)

References and further reading

1. Automata and Coinduction (An Exercise in Coalgebra)
2. Introduction to Bisimulation and Coinduction (book) (slides)
3. An introduction to (co)algebra and (co)induction
4. Checking NFA Equivalence with Bisimulations up to Congruence
5. Universal Coalgebra: A Theory of Systems
6. Bisimulation and Language Equivalence

A note on useful decidable temporal logics

Subclasses of FO(LTL)

In the following, we assume that non-constant function symbols and equality are not allowed. The addition of them can lead to the loss of decidability for any of the subclasses introduced here.

Monadic FO(LTL), proposed by Hodkinson et al. [1] in 2000, is the first non-trivial decidable subclass of FO(LTL). This class contains all sub-formulas beginning with a temporal operator (Since or Until) have at most one free variable. Thus, we can talk about objects in the intended domain using the full power of first-order logic; however, temporal operators may be used to describe the development in time of only one object (two are enough to simulate the behaviour of Turing machines). The satisfiability problem for formulas in this class can be reduced to fragments of classical two-sorted first-order logics in which one sort is intended for temporal reasoning. The decidability results also hold for the temporal logics with finite domains.

Remark. FO(LTL) provides only ‘implicit’ access to time: quantification over points in time in the sense of first-order logic is not permitted, and the only means of expressing temporal properties is by the temporal operators Since and Until. It turns out that monadic FO(LTL) is weaker than the two-sorted first-order language, where one sort of which refers to points in time and the other to the first-order domain. For example, the formula $∃t_1 ∃t_2 (t_1 < t_2 ∧ ∀x(P(t_1, x) ↔ P(t_2, x)))$ is not expressible in FO(LTL) over any interesting class of linear time structures [2, 3].

References

1. Decidable fragments of first-order temporal logics.
2. Temporal Logic. Part I & Part II. Clarendon Press, Oxford.
3. Temporal connectives versus explicit timestamps in temporal query languages.

A note on useful decidable logics & theories - Part II

Decidable fragments of second-order logic

(Weak) MSO with one successor. The monadic second-order theory of structure $(\mathbb N, <)$ (denoted by S1S) is decidable. Buchi showed in 1962 that given any formula $\phi(x_1,...,x_n)$ over ${\rm MSO}(\mathbb N, <)$, one can effectively compute an $\omega$-automaton $A(x_1,...,x_n)$ defining the same relation modulo convolution. There is a similar connection between weak $MSO(\mathbb N, <)$ (denoted by WS1S) and finite-word automata. See [10] for a historical survey.

MSO over binary trees. The structure of infinite binary trees is $T_2 := (\{1,2\}^*,S_1,S_2)$ with $S_i := \{(v,vi) : v \in \{1,2\}^*\}$. Rabin's Tree Theorem [4] states that the MSO-theory of the infinite binary tree (denoted by S2S) is decidable, or in other terminology: that model-checking the binary tree with respect to MSO-properties is decidable. In [4], Rabin also proved the decidability of a bunch of theories using interpretation in $T_2$, such as MSO over n-ary trees (see below). Note that Rabin's theorem is subsumed by a more general result stating that MSO over the prefix-rewriting systems is decidable [?].

MSO over n-ary trees. The decidability results of MSO-theory over binary trees $T_2$ can be extended to $n$-ary branching trees $T_n$ with vertices in $[1..n]^*$ by encoding a vertex $a_1 a_2 \dots a_k$ of $T_n$ by a vertex $1^{a_1} 2 1^{a_2} 2 \dots 2 1^{a_k} 2$ of $T_2$. The translation of MSO-formulas is straightforward.

MSO over pushdown automata. Let $G := (V,E)$ denote the configuration graph of a pushdown automaton, where $V\subseteq Q\times\Sigma^*$. Let $n := \max(|Q|,|\Sigma|).$ One can MSO-interpret $G$ in $T_n$ by representing the configuration $(q, s_1,...,s_k)$ as the vertex $s_1...s_k\ q$ of $T_n$. Each step between the configurations in $G$ is translated in MSO to a local move from one vertex to another in $T_n$. Decidability of MSO over binary trees hence subsumes the fundamental result of Muller and Schupp [6] that checking MSO properties is decidable for the configuration graph of a pushdown automaton.

Decidable modal logic

Probabilistic modal logic (PML). Let $\Sigma$ be a finite set of actions. The syntax of the logic is defined as follows:$$\phi ::= \top \mid \bot \mid \phi\vee\phi \mid \neg\phi \mid (\phi)_a\ {\rm op}~p,$$where $a \in \Sigma$, ${\rm op}\in \{=,<\}$, and $0\le p\le 1$. The semantics of PML is defined over a discrete non-deterministic probabilistic transition system such that for $s\in S$, e.g.,$$s \models (\phi)_a \le p \quad {\rm iff} \quad \Pr(s' \models \phi \mid s\xrightarrow{a} s') \le p.$$Larsen and Skou [7] show that, when the transition probabilities are rational and bounded above zero, given any PML formula $\phi$ and fixed $0<\epsilon<1$, one can compute an experiment $t_{\epsilon,\phi}$ and an observation $o_{\epsilon,\phi}$ such that $s \models \phi$ iff $\Pr(o_{\epsilon,\phi}$ is observed by running $t_{\epsilon,\phi}$ on $s) \ge 1-\epsilon$, and $s \not\models \phi$ iff $\Pr(o_{\epsilon,\phi}$ is observed by running $t_{\epsilon,\phi}$ on $s) \le \epsilon$. Such experiments can be computed, executed and observed in polynomial time. Larsen and Skou show that PML characterises probabilistic bisimulation in the following sense: two states are probabilistic bisimilar iff they satisfy exactly the same set of PML formulas.

Misc

Reduction of decidability. Suppose that model checking $L$-theory of structure $S$ is known to be decidable. The model checking problem for a structure $S'$ with respect to $L'$-theory is decidable if we can give an $L$-description of $S'$ within structure $S$. That is, we characterise structure $S'$ using $L$-formulas over $S$. In other words, we provide a satisfiability-preserving translation of any $L'$-formulas $\phi$ into $L$-formula $\psi$ such that $S'\models \phi$ iff $S\models \psi$. Hence $L'$-theory over structure $S'$ is also decidable.

References

1. Structural properties of complete problems for exponential time. 1997.
2. Complexity results for classes of quantification formulas. 2001.
3. Verification of randomised security protocols.
4. Decidability of second-order theories and automata on infinite trees. 1969.
5. Complexity results for classes of quantificational formulas. 1980.
6. The theory of ends, pushdown automata, and second-order logic. 1985.
7. Bisimulation through Probabilistic Testing. 1991.
8. The Classical Decision Problem. 2001.
9. A Survival Guide to Presburger Arithmetic. 2018.
10. Automata: From Logics to Algorithms. 2007.
11. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. 2009.