In mathematics, S2S is the monadic second-order theory with two successors. Its first-order objects are finite binary strings. 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 (or unary predicates) of finite binary strings. S2S has functions s↦s0 and s↦s1 that add one more character to a string, and a predicate s∈S (equivalently, S(s)) meaning string s belongs to set S. The two strings s0 and s1 are the two successors of s from which this theory is named.

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. 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 i1i2...im as i1 1 i2 2 ... im 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 be 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.

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. 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, 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. (A preliminary 2015 version erroneously claimed proof of completeness without the determinacy schema.)

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

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 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 <ω2 is decidable; decidability for ω2 is independent of ZFC (assuming Con(ZFC + weakly compact cardinal)). 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 (or just S1S+U) is undecidable if U is the unbounding quantifier: UX Φ(X) if and only if Φ(X) 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 (i.e. forms a regular language). In S1S, a (unary) predicate on sets is (parameter-free) 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 φ(S1,...,Sk), (with k free variables) and finite tree of binary strings T, φ(S1∩T,...,Sk∩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 ).

For S1S, every formula is equivalent to a Δ11 formula, and to a boolean combination of Π02 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 (alternatively, even).

For S2S, using tree automata (below), every formula is equivalent to a Δ12 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 Π11 transfinite recursion (see reverse mathematics). RCA0 + (schema) {τ: τ is a true S2S sentence} is equivalent to (schema) {τ: τ is a Π13 sentence provable in Π12-CA0 }. Over a base theory, the schemas are equivalent to (schema over k) ∀S⊆ω ∃α1<...<αk Lα1(S) ≺Σ1 ... ≺Σ1 Lαk(S) where L is the constructible universe (see also large countable ordinal). Due to limited induction, Π12-CA0 does not prove that all true (under the standard decision procedure) Π13 S2S statements are actually true even though each such sentence is provable Π12-CA0.

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 Π02(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 Π13 consequences of in Π12-CA0.

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.

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 φ).