Second order monadic predicate logic

The second level monadic predicate logic, also called MSO for short after the English monadic second order logic , is a term from the field of mathematical logic . It is the fragment of the second- order predicate logic that only considers the single-digit predicates.

definition

For a signature, consider the language of the second order predicate logic. The formulas of the MSO are precisely those formulas in which all occurring relation variables are single-digit . This describes the syntax of the MSO. The semantics is the restriction of the semantics of the second order predicate logic. ${\displaystyle \sigma }$ ${\displaystyle L_{II}^{\sigma }}$ ${\displaystyle L_{II}^{\sigma }}$

Note that multi-digit relations can occur in the MSO, but these must then be part of the signature. This cannot be used to quantify.

Since single-digit relations are subsets of the basic set in every interpretation , statements about all subsets of the associated structures can be made in the MSO and quantified using these as required. You cannot quantify using function symbols or multi-digit relation symbols. ${\displaystyle \sigma }$

Examples

First order predicate logic

Every expression of the first-order predicate logic is an MSO expression, because such an expression does not contain any relation variables at all, especially no multi-place variables.

Induction axiom

As is well known, Peano arithmetic can be described with the signature , where 0 is a constant and a function symbol. The constant is interpreted as a zero element and s as a successor function. The so-called induction axiom ${\displaystyle \sigma =\{0,s\}}$ ${\displaystyle s}$

${\displaystyle \forall X((X0\land \forall x(Xx\rightarrow Xsx))\rightarrow \forall x\,Xx)}$

is apparently an MSO sentence.

Relationship between graphs

If for a two-digit relation symbol , then every structure is a graph , whereby this is the universe, i.e. the basic set, of the structure and the interpretation of the edge relation is on . Then ${\displaystyle \sigma =\{E\}}$ ${\displaystyle E}$ ${\displaystyle \sigma }$ ${\displaystyle G}$ ${\displaystyle G}$ ${\displaystyle E^{G}}$ ${\displaystyle E}$ ${\displaystyle G}$

${\displaystyle \forall X((\exists x\,Xx\land \exists x\,\neg Xx)\rightarrow \exists x\exists y\,(Xx\land \neg Xy\land Exy))}$

a syntactically correct MSO expression, because the only occurring relation variable is one-digit. The two-digit relation symbol belongs to the signature and is therefore not a relation variable. The semantics of this expression are: For every subset ( ) the following applies: if the subset is not empty ( ) and its complement is not empty either ( ), then there is an edge ( ) between it and its complement . This is obviously equivalent to the connection of the graph and we note that one can describe the connection of graphs in the MSO. This is not possible in the first level predicate logic, see locality (logic) , so that MSO proves to be genuinely more expressive through this example. ${\displaystyle X}$ ${\displaystyle E}$ ${\displaystyle \forall X}$ ${\displaystyle \exists x\,Xx}$ ${\displaystyle \exists x\,\neg Xx}$ ${\displaystyle \exists x\exists y(Xx\land \neg Xy\land Exy))}$

Even number of elements

For there is no MSO theorem that expresses on a set that is assumed to be finite that it is even. In the second level predicate logic this is possible by expressing, for example, that there is a subset and a bijective function of on its complement: ${\displaystyle \sigma =\emptyset }$ ${\displaystyle X}$ ${\displaystyle X}$

${\displaystyle \exists X\,\exists Y\,(''Y{\text{ ist Funktion}}''\,\land \,''X{\text{ ist Definitionsbereich von }}Y''\,\land \,''\neg X{\text{ ist Wertebereich von }}Y''\,\land \,''Y{\text{ ist bijektiv}}''\}}$,

It is clear that the sub-clauses enclosed in apostrophes can even be formulated in the first-order predicate logic. Since the two-digit relation variable is used here , it is not an MSO sentence. This example shows that second order predicate logic is genuinely more expressive than MSO. ${\displaystyle Y}$

MSO on words

Models of words

The second-order monadic predicate logic is suitable for the formulation of statements about words over a finite alphabet . For this we use as a signature , where the characters are of the alphabet and we formulate that <is a linear order on the universe and that form a partition of the universe. ${\displaystyle \Sigma }$ ${\displaystyle \sigma =\{<,P_{a},P_{b},\ldots \}}$ ${\displaystyle a,b,\ldots }$ ${\displaystyle P_{a},P_{b}\ldots }$

${\displaystyle \forall x\,\neg (x<x)\,\land \,\forall x\forall y\forall z\,(((x<y)\land (y<z))\rightarrow (x<z))\,\land \,\forall x\forall y\,((x=y)\lor (x<y)\lor (y<x))}$

expresses the linear order, and

${\displaystyle \forall x\,((P_{a}x\lor P_{b}x\lor P_{c}x)\land \neg (P_{a}x\land P_{b}x)\land \neg (P_{a}x\land P_{c}x)\land \neg (P_{b}x\land P_{c}x))}$

expresses the partition property.

A finite universe can then be assumed to be isomorphic , where <is interpreted as the natural order and an a is in the place of the , corresponding for and so on. ${\displaystyle \{1,2,\ldots ,n\}}$ ${\displaystyle P_{a}i}$ ${\displaystyle i}$ ${\displaystyle P_{b}i}$

Is, for example , the word defines a structure on the universe with the interpretations for , for , for and the natural order for <. The words from , that is, the finite strings above the alphabet , are exactly the models in this sense . ${\displaystyle \Sigma =\{a,b,c\}}$ ${\displaystyle s=aabcbca}$ ${\displaystyle \{<,P_{a},P_{b},P_{c}\}}$ ${\displaystyle M_{s}}$ ${\displaystyle \{1,2,3,4,5,6,7\}}$ ${\displaystyle \{1,2,7\}}$ ${\displaystyle P_{a}}$ ${\displaystyle \{3,5\}}$ ${\displaystyle P_{b}}$ ${\displaystyle \{2,4\}}$ ${\displaystyle P_{c}}$ ${\displaystyle \Sigma ^{*}}$ ${\displaystyle \Sigma }$ ${\displaystyle L_{II}^{\sigma }}$

MSO definability

Subsets of such character strings can now be described using MSO expressions. If an MSO sentence, i.e. an MSO formula without free variables, is ${\displaystyle \Phi }$

${\displaystyle L(\Phi ):=\{s\in \Sigma ^{*}|\,M_{s}\vDash \Phi \}}$

the set (language) of all words which are the model for , that is, which satisfy. A language of this form is called MSO-definable . ${\displaystyle \Phi }$ ${\displaystyle \Phi }$

For example, we can describe the language of all strings containing an even number of 's as follows: ${\displaystyle \Sigma =\{a,b,c\}}$ ${\displaystyle a}$

${\displaystyle \Phi =\exists X\exists Y\,{\big (}\forall x((P_{a}x\leftrightarrow (Xx\lor Yx))\land \neg (Xx\land Yx))}$

${\displaystyle \land \exists x(Xx\land \forall y\,(y<x\rightarrow \neg P_{a}x))}$

${\displaystyle \land \exists x(Yx\land \forall y\,(x<y\rightarrow \neg P_{a}x))}$

${\displaystyle \land \forall x\forall y\,((Xx\land Xy\land x<y)\rightarrow \exists z(Yz\land x<z\land z<y))}$

${\displaystyle \land \forall x\forall y\,((Yx\land Yy\land x<y)\rightarrow \exists z(Xz\land x<z\land z<y)){\big )}}$

In words that means

The 's are distributed over two sets and , which are disjoint, ${\displaystyle a}$ ${\displaystyle X}$ ${\displaystyle Y}$

and the first is in ${\displaystyle a}$ ${\displaystyle X}$

and the last one lies in ${\displaystyle a}$ ${\displaystyle Y}$

and between two different elements from there is one ${\displaystyle X}$ ${\displaystyle Y}$

and between two different elements from there is one . ${\displaystyle Y}$ ${\displaystyle X}$

It is then clear that this is the set of character strings that contains an even number of 's, that is, this language is MSO-definable. ${\displaystyle L(\Phi )}$ ${\displaystyle a}$

Theorem by Büchi

Büchi's theorem, named after Julius Richard Büchi , provides information about which languages ​​are MSO-definable:

• A language can be MSO defined if and only if it is regular .

This sentence, dating from 1960, establishes a very early connection between mathematical logic and theoretical computer science ; it is considered the first result of descriptive complexity theory . The phrase was also found independently by Boris Trakhtenbrot .

Analysis of the evidence shows that even using MSO expressions of the species

${\displaystyle \exists X_{1}\ldots \exists X_{n}\varphi }$

gets by, where an expression of the first-level predicate logic is in a signature extended by. The set of these expressions is called . For languages, therefore, regularity, MSO definability and definability are equivalent. ${\displaystyle \varphi }$ ${\displaystyle X_{1},\ldots ,X_{n}}$ ${\displaystyle M\Sigma _{1}^{1}}$ ${\displaystyle M\Sigma _{1}^{1}}$

Individual evidence

1. ↑ Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory , Springer-Verlag 1999, ISBN 3-540-28787-6 , Chapter 3.1: Second-Order Logic
2. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , sentence 7.14 for a more precise statement
3. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , sentence 7.12
4. ↑ JR Büchi: Weak second-order arithmetic and finite automota , Journal for mathematical logic and foundations of mathematics (1960), Volume 6, pages 66-92
5. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , sentence 7.21
6. ↑ B. Trahtenbrot: Finite automata and the logic of monadic predicates (Russian) , Sibirskij Mat. Zhurnal (1962), Volume 3, pages 103-131
7. ↑ Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory , Springer Verlag 1999, ISBN 3-540-28787-6 , sentence 6.2.3