S2S (mathematics)

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.

Basic properties

The first-order objects of S2S are finite binary strings. The second-order objects are arbitrary sets of finite binary strings. S2S has functions s↦''s0 and s''↦s1 on strings, and predicate 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) and S = T ⇔ ∀s ⇔ T).
In place of strings, one can use natural numbers with n↦2n+1 and n↦2n+2 but no other operations.
The set of all binary strings is denoted by ^*, using Kleene star.
Arbitrary subsets of ^* are sometimes identified with trees, specifically as a -labeled tree ^*; ^* 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.
For properties expressible in S2S, for each node, only O bits can be communicated between the left subtree and the right subtree and the rest.
For a fixed k, a function from strings to k can be encoded by a single set. Moreover, s,''t ⇒ s''01t where t doubles every character of t is injective, and s ⇒ is S2S definable. By contrast, by a communication complexity argument, in S1S a pair of sets is not encodable by a single set.

Weakenings of S2S: Weak S2S requires all sets to be finite. 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 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, sentences with k-fold quantifier alternation can decided in time corresponding to k+''O-fold exponentiation of the sentence length.
Axiomatization
WS2S can be axiomatized through certain basic properties plus induction schema.
S2S can be partially axiomatized by:

∃!s'' ∀t

∀s,''t ∀i''∈ ∀j∈

∀S ∧ ∀s ⇒ S ∧ S)⇒ ∀s ''S)

∃S'' ∀s ⇔ φ)
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'' ⇔ T). Since we have comprehension, induction can be a single statement rather than a schema.
The analogous axiomatization of S1S is complete. However, for S2S, completeness is open. While S1S has uniformization, there is no S2S definable choice function that given a non-empty set S returns an element of S, and comprehension schemas are commonly augmented with various forms of the axiom of choice. However, - is complete when extended with a determinacy schema for certain parity games.
S2S can also be axiomatized by Π¹₃ sentences. 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.

Theories related to S2S

For every finite k, the monadic second-order theory of countable graphs with treewidth ≤k is interpretable in S2S. For example, the MSO theory of trees or of series–parallel graphs is decidable. Here, we can also interpret the finiteness quantifier for a set of vertices, and also count vertices 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 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 linear orders is decidable, as is the MSO theory of countable trees with their Kleene–Brouwer orders. However, the MSO theory of is undecidable. The MSO theory of ordinals <ω₂ is decidable; decidability for ω₂ is independent of ZFC. Also, an ordinal is definable using monadic second-order logic on ordinals if and only if it can be obtained from definable regular cardinals by ordinal addition and multiplication.
S2S is useful for decidability of certain modal logics, with Kripke semantics naturally leading to trees.
S2S+U is undecidable if U is the unbounding quantifier: UX Φ if and only if Φ holds for arbitrarily large finite X. However, WS2S+U, even with quantification over infinite paths, is decidable, even with S2S subformulas that do not contain U.

Formula complexity

A set of binary strings is definable in S2S if and only if it is regular. In S1S, a predicate on sets is definable if and only if 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 φ, and finite tree of binary strings T, φ can be computed in time linear in |T|, but as noted above, the overhead can be iterated exponential in the formula size.
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 if and only if the highest priority seen infinitely often is odd.
For S2S, using tree automata, every formula is equivalent to a Δ¹₂ formula. Moreover, every S2S formula is equivalent to a formula with just four quantifiers, ∃S∀''T∃s''∀t.... For S1S, three quantifiers suffice, and for WS2S and WS1S, two quantifiers 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. RCA₀ + is equivalent to . Over a base theory, the schemas are equivalent to ∀S⊆ω ∃α₁<...<α_k L_α₁ ≺_Σ₁... ≺_Σ₁ L_{α_k} where L is the constructible universe . Due to limited induction, Π¹₂-CA₀ does not prove that all true Π¹₃ 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:

T is S2S definable from some set of binary strings polynomial time computable from S.

T can be computed from the set of winning positions for some game whose payoff is a finite boolean combination of Π⁰₂ sets.

T can be defined from S in arithmetic μ-calculus

T is in the least β-model containing S and satisfying all Π¹₃ consequences of in Π¹₂-CA₀.

Models of S1S and S2S

In addition to the standard model, there are other models for S1S and S2S, which use some rather than all subsets of the domain.
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.
This follows from relative recursiveness of S1S definable sets plus uniformization:

- φ can be computed from the parameters of φ and the values of φ for a finite set of s.

- A witness for ∃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. Also, by using lexicographically least shortest choices, there is an S1S formula φ' such that φ'⇒φ and ∃S φ ⇔∃!S φ' .
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 -labeled complete infinite binary tree. A labeled tree is regular if it can be obtained by unrolling a vertex-labeled finite directed graph with an initial vertex; a 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. There are nonregular models of S1S 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. An infinite tree automaton starts at the root and moves up the tree, and accepts if and only if every tree branch accepts. A nondeterministic tree automaton accepts if and only if player 1 has a winning strategy, where player 1 chooses an allowed pair of new states, 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, 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, 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, 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 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 assign the least ordinal α such that player 1 has a winning strategy with all entered priority k positions 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, 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 α lower initial position.
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 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, 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 or.
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 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, which is polynomial time when the number of priorities is small enough.
Theory of trees: For decidability of MSO logic on 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. 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, if a monadic relational model M is decidable, then so is its tree counterpart. For example, S2S is the tree counterpart of. 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' ⇔ P_i with P_i' false otherwise. The proof is similar to the S2S decidability proof. At each step, a automaton gets a tuple of M objects as input, and an M formula determines which state transitions are permitted. Player 1 chooses a mapping child⇒state that is permitted by the formula, and player 2 chooses the child to continue. To witness rejection by a non-deterministic automaton, for each pick a set of 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) 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, we can state ∀ ∀s ∃r∈''Ns'' f +_{N_s} r = 0_{N_s}. If M is S2S, 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 theory T, the theory T^M of M-products of T is decidable relative to a oracle, where a model of T^M uses an arbitrary disjoint model N_s of T for each s∈''M. The proof is by induction on formula complexity. Let v''_s be the list of free N_s variables, including f 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 to answer what is possible, and given a list possibilities, formulate a corresponding sentence in M.
Coding into extensions of S2S: Every decidable predicate on strings can be encoded for decidability of S2S together with the encoded predicate. Proof: Given a nondeterministic infinite tree automaton, we can partition the set of finite binary labeled trees 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. For example, assign trees to the same class if they have the same predicate that given initial_state and set Q of pairs returns whether player 1 can simultaneously force all branches to correspond to elements of Q. Now, for each k, pick a finite set of trees 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.