In mathematics, S2S is the monadic second order theory with two successors. It is one of the most expressive natural decidable theories known, with many decidable theories interpretable in S2S. Its decidability was proved by Rabin in 1969.^[1]

Basic properties

The first order objects of S2S are finite binary strings. The second order objects are arbitrary sets (or unary predicates) of finite binary strings. S2S has functions s→s0 and s→s1 on strings, and predicate s∈S (equivalently, S(s)) meaning string s belongs to set S.

Some properties and conventions:

• By default, lowercase letters refer to first order objects, and uppercase to second order objects.
• The inclusion of sets makes S2S second order, with "monadic" indicating absence of k-ary predicate variables for k>1.
• Concatenation of strings s and t is denoted by st, and is not generally available in S2S, not even s→0s. The prefix relation between strings is definable.
• Equality is primitive, or it can be defined as s = t ⇔ ∀S (S(s) ⇔ S(t)) and S = T ⇔ ∀s (S(s) ⇔ T(s)).
• In place of strings, one can use (for example) natural numbers with n→2n+1 and n→2n+2 but no other operations.
• The set of all binary strings is denoted by {0,1}^*, using Kleene star.
• Arbitrary subsets of {0,1}^* are sometimes identified with trees, specifically as a {0,1}-labeled tree {0,1}^*; {0,1}^* forms a complete infinite binary tree.
• For formula complexity, the prefix relation on strings is typically treated as first order. Without it, not all formulas would be equivalent to Δ¹₂ formulas.^[2]
• For properties expressible in S2S (viewing the set of all binary strings as a tree), for each node, only O(1) bits can be communicated between the left subtree and the right subtree and the rest (see communication complexity).
• For a fixed k, a function from strings to k (i.e. natural numbers below k) can be encoded by a single set. Moreover, s,t ⇒ s01t′ where t′ doubles every character of t is injective, and s ⇒ {s01t′: t∈{0,1}^*} is S2S definable. By contrast, by a communication complexity argument, in S1S (below) a pair of sets is not encodable by a single set.

Weakenings of S2S: Weak S2S (WS2S) requires all sets to be finite (note that finiteness is expressible in S2S using Kőnig's lemma). S1S can be obtained by requiring that '1' does not appear in strings, and WS1S also requires finiteness. Even WS1S can interpret Presburger arithmetic with a predicate for powers of 2, as sets can be used to represent unbounded binary numbers with definable addition.

Decision complexity

S2S is decidable, and each of S2S, S1S, WS2S, WS1S has a nonelementary decision complexity corresponding to a linearly growing stack of exponentials. For the lower bound, it suffices to consider Σ¹₁ WS1S sentences. A single second order quantifier can be used to propose an arithmetic (or other) computation, which can be verified using first order quantifiers if we can test which numbers are equal. For this, if we appropriately encode numbers 1..m, we can encode a number with binary representation i₁i₂...i_m as i₁ 1 i₂ 2 ... i_m m, preceded by a guard. By merging testing of guards and reusing variable names, the number of bits is linear in the number of exponentials. For the upper bound, using the decision procedure (below), sentences with k-fold quantifier alternation can decided in time corresponding to k+O(1)-fold exponentiation of the sentence length (with uniform constants).

Axiomatization

WS2S can be axiomatized through certain basic properties plus induction schema.^[3]

S2S can be partially axiomatized by:
(1) ∃!s ∀t ( t0≠s ∧ t1≠s) (empty string, denoted by ε; ∃!s means "there is unique s")
(2) ∀s,t ∀i∈{0,1} ∀j∈{0,1} (si=tj ⇒ s=t ∧ i=j) (the use of i and j is an abbreviation; for i=j, 0 does not equal 1)
(3) ∀S (S(ε) ∧ ∀s (S(s) ⇒ S(s0) ∧ S(s1))⇒ ∀s S(s)) (induction)
(4) ∃S ∀s (S(s) ⇔ φ(s)) (S not free in φ)

(4) is the comprehension schema over formulas φ, which always holds for second order logic. As usual, if φ has free variables not shown, we take the universal closure of the axiom. If equality is primitive for predicates, one also adds extensionality S=T ⇔ ∀s (S(s) ⇔ T(s)). Since we have comprehension, induction can be a single statement rather than a schema.

The analogous axiomatization of S1S is complete.^[4] However, for S2S, completeness is open (as of 2021). While S1S has uniformization, there is no S2S definable (even allowing parameters) choice function that given a non-empty set S returns an element of S,^[5] and comprehension schemas are commonly augmented with various forms of the axiom of choice. However, (1)-(4) is complete when extended with a determinacy schema for certain parity games.^[6]

S2S can also be axiomatized by Π¹₃ sentences (using the prefix relation on strings as a primitive). However, it is not finitely axiomatizable, nor can it be axiomatized by Σ¹₃ sentences even if we add induction schema and a finite set of other sentences (this follows from its connection to Π¹₂-CA₀).

Theories related to S2S

For every finite k, the monadic second order (MSO) theory of countable graphs with treewidth ≤k (and a corresponding tree decomposition) is interpretable in S2S (see Courcelle's theorem). For example, the MSO theory of trees (as graphs) or of series-parallel graphs is decidable. Here (i.e. for bounded tree width), we can also interpret the finiteness quantifier for a set of vertices (or edges), and also count vertices (or edges) in a set modulo a fixed integer. Allowing uncountable graphs does not change the theory. Also, for comparison, S1S can interpret connected graphs of bounded pathwidth.

By contrast, for every set of graphs of unbounded treewidth, its existential (i.e. Σ¹₁) MSO theory is undecidable if we allow predicates on both vertices and edges. Thus, in a sense, decidability of S2S is the best possible. Graphs with unbounded treewidth have large grid minors, which can be used to simulate a Turing machine.

By reduction to S2S, the MSO theory of countable orders is decidable, as is the MSO theory of countable trees with their Kleene–Brouwer orders. However, the MSO theory of (${\displaystyle \mathbb {R} }$, <) is undecidable.^[7][8] The MSO theory of ordinals <ω₂ is decidable; decidability for ω₂ is independent of ZFC (assuming Con(ZFC + weakly compact cardinal)).^[9] Also, an ordinal is definable using monadic second order logic on ordinals iff it can be obtained obtained from definable regular cardinals by ordinal addition and multiplication.^[10]

S2S is useful for decidability of certain modal logics, with Kripke semantics naturally leading to trees.

S2S+U (or just S1S+U) is undecidable if U is the unbounding quantifier — UX Φ(X) iff Φ(X) holds for some arbitrarily large finite X.^[11] However, WS2S+U, even with quantification over infinite paths, is decidable, even with S2S subformulas that do not contain U.^[12]

Formula complexity

A set of binary strings is definable in S2S iff it is regular (i.e. forms a regular language). In S1S, a (unary) predicate on sets is (parameter-free) definable iff it is an ω-regular language. For S2S, for formulas that use their free variables only on strings not containing a 1, the expressiveness is the same as for S1S.

For every S2S formula φ(S₁,...,S_k), (with k free variables) and finite tree of binary strings T, φ(S₁∩T,...,S_k∩T) can be computed in time linear in |T| (see Courcelle's theorem), but as noted above, the overhead can be iterated exponential in the formula size (more precisely, the time is ${\displaystyle O(|T|k)+2_{O(|\phi |)}^{2}}$).

For S1S, every formula is equivalent to a Δ¹₁ formula, and to a boolean combination of Π⁰₂ arithmetic formulas. Moreover, every S1S formula is equivalent to acceptance by a corresponding ω-automaton of the parameters of the formula. The automaton can be a deterministic parity automaton: A parity automaton has an integer priority for each state, and accepts iff the highest priority seen infinitely often is odd (alternatively, even).

For S2S, using tree automata (below), every formula is equivalent to a Δ¹₂ formula. Moreover, every S2S formula is equivalent to a formula with just four quantifiers, ∃S∀T∃s∀t ... (assuming that our formalization has both the prefix relation and the successor functions). For S1S, three quantifiers (∃S∀s∃t) suffice, and for WS2S and WS1S, two quantifiers (∃S∀t) suffice; the prefix relation is not needed here for WS2S and WS1S.

However, with free second order variables, not every S2S formula can be expressed in second order arithmetic through just Π¹₁ transfinite recursion (see reverse mathematics). RCA₀ + (schema) {τ: τ is a true S2S sentence} is equivalent to (schema) {τ: τ is a Π¹₃ sentence provable in Π¹₂-CA₀ }.^[13][14] Over a base theory, the schemas are equivalent to (schema over k) ∀S⊆ω ∃α₁<...<α_k L_α1(S) ≺_Σ1 ... ≺_Σ1 L_αk(S) where L is the constructible universe (see also large countable ordinal). Due to limited induction, Π¹₂-CA₀ does not prove that all true (under the standard decision procedure) Π¹₃ S2S statements are actually true even though each such sentence is provable Π¹₂-CA₀.

Moreover, given sets of binary strings S and T, the following are equivalent:
(1) T is S2S definable from some set of binary strings polynomial time computable from S.
(2) T can be computed from the set of winning positions for some game whose payoff is a finite boolean combination of Π⁰₂(S) sets.
(3) T can be defined from S in arithmetic μ-calculus (arithmetic formulas + least fixed-point logic)
(4) T is in the least β-model (i.e. an ω-model whose set-theoretic counterpart is transitive) containing S and satisfying all Π¹₃ consequences of in Π¹₂-CA₀.

Models of S1S and S2S

In addition to the standard model (which is the unique MSO model for S1S and S2S), there are other models for S1S and S2S, which use some rather than all subsets of the domain (see Henkin semantics).

For every S⊆ω, sets recursive in S form an elementary submodel of the standard S1S model, and same for every non-empty collection of subsets of ω closed under Turing join and Turing reducibility.^[16]

This follows from relative recursiveness of S1S definable sets plus uniformization:
- φ(s) (as a function of s) can be computed from the parameters of φ and the values of φ(s′) for a finite set of s′ (with its size bounded by the number of states in a deterministic automaton for φ).
- A witness for ∃S φ(S) can be obtained by choosing k and a finite fragment of S′ of S, and repeatedly extending S′ such that the highest priority during each extension is k and that the extension can be completed into S satisfying φ without hitting priorities above k (these are permitted only for the initial S′). Also, by using lexicographically least shortest choices, there is an S1S formula φ' such that φ'⇒φ and ∃S φ(S) ⇔∃!S φ'(S) (i.e. uniformization; φ may have free variables not shown; φ' depends only on the formula φ).

The minimal model of S2S consists of all regular languages on binary strings. It is an elementary submodel of the standard model, so if an S2S parameter-free definable set of trees is non-empty, then it includes a regular tree. A regular language can also be treated as a regular {0,1}-labeled complete infinite binary tree (identified with predicates on strings). A labeled tree is regular if it can be obtained by unrolling a vertex-labeled finite directed graph with an initial vertex; a (directed) cycle in the graph reachable from the initial vertex gives an infinite tree. With this interpretation and encoding of regular trees, every true S2S sentence may already be provable in elementary function arithmetic. It is non-regular trees that may require nonpredicative comprehension for determinacy (below). There are nonregular (i.e. containing nonregular languages) models of S1S (and presumably S2S) (both with and without standard first order part) with a computable satisfaction relation. However, the set of recursive sets of strings does not form a model of S2S due to failure of comprehension and determinacy.

Decidability of S2S

The proof of decidability is by showing that every formula is equivalent to acceptance by a nondeterministic tree automaton (see tree automaton and infinite-tree automaton). An infinite tree automaton starts at the root and moves up the tree, and accepts iff every tree branch accepts. A nondeterministic tree automaton accepts iff player 1 has a winning strategy, where player 1 chooses an allowed (for the current state and input) pair of new states (p₀,p₁), while player 2 chooses the branch, with the transition to p₀ if 0 is chosen and p₁ otherwise. For a co-nondeterministic automaton, all choices are by player 2, while for deterministic, (p₀,p₁) is fixed by the state and input; and for a game automaton, the two players play a finite game to set the branch and the state. Acceptance on a branch is based on states seen infinitely often on the branch; parity automata are sufficiently general here.

For converting the formulas to automata, the base case is easy, and nondeterminism gives closure under existential quantifiers, so we only need closure under complementation. Using positional determinacy of parity games (which is where we need impredicative comprehension), non-existence of player 1 winning strategy gives a player 2 winning strategy S, with a co-nondeterministic tree automaton verifying its soundness. The automaton can then be made deterministic (which is where we get an exponential increase in the number of states), and thus existence of S corresponds to acceptance by a non-deterministic automaton.

Determinacy: Provably in ZFC, Borel games are determined, and the determinacy proof for boolean combinations of Π⁰₂ formulas (with arbitrary real parameters) also gives a strategy here that depends only on the current state and the position in the tree. The proof is by induction on the number of priorities. Assume that there are k priorities, with the highest priority being k, and that k has the right parity for player 2. For each position (tree position + state) assign the least ordinal α (if any) such that player 1 has a winning strategy with all entered (after one or more steps) priority k positions (if any) having labels <α. Player 1 can win if the initial position is labeled: Each time a priority k state is reached, the ordinal is decreased, and moreover in between the decreases, player 1 can use a strategy for k-1 priorities. Player 2 can win if the position is unlabeled: By the determinacy for k-1 priorities, player 2 has a strategy that wins or enters an unlabeled priority k state, in which case player 2 can again use that strategy. To make the strategy positional (by induction on k), when playing the auxiliary game, if two chosen positional strategies lead to the same position, continue with the strategy with the lower α, or for the same α (or for player 2) lower initial position (so we can switch a strategy finitely many times).

Automata determinization: For determinization of co-nondeterministic tree automata, it suffices to consider ω-automata, treating branch choice as input, determinizing the automaton, and using it for the deterministic tree automaton. Note that this does not work for nondeterministic tree automata as the determinization for going left (i.e. s→s0) can depend on the contents of the right branch; by contrast to nondeterminism, deterministic tree automata cannot even accept precisely nonempty sets. To determinize a nondeterministic ω-automaton M (for co-nondeterministic, take the complement, noting that deterministic parity automata are closed under complements), we can use a Safra tree with each node storing a set of possible states of M, and node creation and deletion based on reaching high priority states. For details, see ^[17] or.^[18]

Decidability of acceptance: Acceptance by a nondeterministic parity automaton of the empty tree corresponds to a parity game on a finite graph G. Using the above positional (also called memoryless) determinacy, this can be simulated by a finite game that ends when we reach a loop, with the winning condition based on the highest priority state in the loop. A clever optimization gives a quasipolynomial time algorithm,^[19] which is polynomial time when the number of priorities is small enough (which occurs commonly in practice).

Theory of trees: For decidability of MSO logic on trees (i.e. graphs that are trees), even with finiteness and modular counting quantifiers for first order objects, we can embed countable trees into the complete binary tree and use the decidability of S2S. For example, for a node s, we can represent its children by s1, s01, s001, and so on. For uncountable trees, we can use Shelah-Stup theorem (below). We can also add a predicate for a set first order objects having cardinality ω₁, and the predicate for cardinality ω₂, and so on for infinite regular cardinals. Graphs of bounded tree width are interpretable using trees, and without predicates over edges this also applies to graphs of bounded clique width.

Combining S2S with other decidable theories

Tree extensions of monadic theories: By Shelah-Stup theorem,^[20][21] if a monadic relational model M is decidable, then so is its tree counterpart. For example, (modulo choice of formalization) S2S is the tree counterpart of {0,1}. In the tree counterpart, the first order objects are finite sequences of elements of M ordered by extension, and an M-relation P_i is mapped to P_i'(vd₁,...,vd_k) ⇔ P_i(d₁,...,d_k) with P_i' false otherwise (d_j∈M, and v is a (possibly empty) sequence of elements of M). The proof is similar to the S2S decidability proof. At each step, a (nondeterministic) automaton gets a tuple of M objects (possibly second order) as input, and an M formula determines which state transitions are permitted. Player 1 (as above) chooses a mapping child⇒state that is permitted by the formula (given the current state), and player 2 chooses the child (of the node) to continue. To witness rejection by a non-deterministic automaton, for each (node, state) pick a set of (child, state) pairs such that for every choice, at least one of the pairs is hit, and such that all the resulting paths lead to rejection.

Combining a monadic theory with a first order theory: Feferman–Vaught theorem extends/applies as follows. If M is an MSO model and N is a first order model, then M remains decidable relative to a (Theory(M), Theory(N)) oracle even if M is augmented with all functions M→N where M is identified with its first objects, and for each s∈M we use a disjoint copy of N, with the language modified accordingly. For example, if N is (${\displaystyle \mathbb {R} }$,0,+,⋅), we can state ∀(function f) ∀s ∃r∈N_s f(s) +_Ns r = 0_Ns. If M is S2S (or more generally, the tree counterpart of some monadic model), the automata can now use N-formulas, and thereby convert f:M→N^k into a tuple of M sets. Disjointness is necessary as otherwise for every infinite N with equality, the extended S2S or just WS1S is undecidable. Also, for a (possibly incomplete) theory T, the theory T^M of M-products of T is decidable relative to a (Theory(M), T) oracle, where a model of T^M uses an arbitrary disjoint model N_s of T for each s∈M (as above, M is an MSO model; Theory(N_s) may depend on s). The proof is by induction on formula complexity. Let v_s be the list of free N_s variables, including f(s) if function f is free. By induction, one shows that v_s is only used through a finite set of N-formulas with |v_s| free variables. Thus, we can quantify over all possible outcomes by using N (or T) to answer what is possible, and given a list possibilities (or constraints), formulate a corresponding sentence in M.

Coding into extensions of S2S: Every decidable predicate on strings can be encoded (with linear time encoding and decoding) for decidability of S2S (even with the extensions above) together with the encoded predicate. Proof: Given a nondeterministic infinite tree automaton, we can partition the set of finite binary labeled trees (having labels over which the automaton can operate) into finitely many classes such that if a complete infinite binary tree can be composed of same-class trees, acceptance depends only on the class and the initial state (i.e. state the automaton enters the tree). (Note a rough similarity with the pumping lemma.) For example (for a parity automaton), assign trees to the same class if they have the same predicate that given initial_state and set Q of (state, highest_priority_reached) pairs returns whether player 1 (i.e. nondeterminism) can simultaneously force all branches to correspond to elements of Q. Now, for each k, pick a finite set of trees (suitable for coding) that belong to the same class for automata 1-k, with the choice of class consistent across k. To encode a predicate, encode some bits using k=1, then more bits using k=2, and so on.

References

Additional reference:
Weyer, Mark (2002). "Decidability of S1S and S2S". Automata, Logics, and Infinite Games. Lecture Notes in Computer Science. Vol. 2500. Springer. pp. 207–230. doi:10.1007/3-540-36387-4_12. ISBN 978-3-540-00388-5.