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 Δ 2 1 {\displaystyle \Delta _{2}^{1}} 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 Σ 1 1 {\displaystyle {\Sigma }_{1}^{1}} 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. 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).
… excerpt ends here. Continue reading the full article.
