S2S can be axiomatized by:
- $∃!s ∀t \, (t0≠s ∧ t1≠s)$ (empty string, denoted by $ε$)
- $∀s,t \, ∀i∈\{0,1\} \, ∀j∈\{0,1\} \, (si=tj ⇒ s=t ∧ i=j)$ (tree successors; the use of $i$ and $j$ is an abbreviation; for $i=j$, 0 does not equal 1)
- $∀S \, (S(ε) ∧ ∀s \, (S(s) ⇒ S(s0) ∧ S(s1)) \,⇒\, ∀s \, S(s))$ (induction)
- (schema over $φ$) $∃S ∀s \, (S(s) ⇔ φ(s))$ (comprehension; $S$ not free in $φ$)
- (schema over $φ$) $∃(\text{maximal } f) \, ∀s∈\operatorname{dom}(f) \, ∃g⊆f \, (s∈\operatorname{dom}(g) ∧ φ(g))$ (choice)
For (5), $f$ and $g$ are partial boolean functions on strings (such a function can be represented by its domain and the set of inputs on which it is true). $g⊆f$ means $f$ extends $g$ (i.e. $∀s∈\operatorname{dom}(g) \, (s∈\operatorname{dom}(f) ∧ f(s)=g(s))$). $f$ is maximal for $ψ(f)$ iff $ψ(f) ∧ ∀g⊃f \; ¬ψ(g)$ ('$⊃$' means 'properly extends'). As usual, $φ$ may have free variables not shown, but with variable names not used in the schema.
Equality is only primitive for first order objects. By default, upper case letters denote sets (equivalently, unary predicates).
To see that (5) is true, repeatedly extend $f$ (using dependent choice) until you cannot. (5) makes (4) redundant except for a few basic constructs (in our formalization, just adjunction (empty set follows from (5) here)). Also, S2S allows pairing of sets (such as $S,T→\{s0:s∈S\}∪\{t1:t∈T\}$), so (5) extends to functions with a fixed finite range.
For S1S (which has one successor), the analog of 1-4 is complete. However, 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$. Thus, we plausibly need choice.
The paper A functional (Monadic) second-order theory of infinite trees (by Anupam Das and Colin Riba) (see also Toward Curry-Howard Approaches to MSO and Automata on Infinite Words and Trees (Riba 2019)) axiomatizes S2S by 1-4 and a certain determinacy schema (note: in a preliminary retracted version, the authors claimed that 1-4 suffices), so we only need to prove the determinacy described in the next paragraph.
Determinacy proof
A parity game is played on a possibly-infinite vertex-labeled (with a finite set of integer labels) directed graph with a distinguished initial vertex. The players take turns to move (or they lose), and after an infinite play, player 1 wins iff the highest label seen infinitely often is odd (alternatively, even). S2S does not interpret all graphs, but we only need graphs corresponding to runs of tree automata — bipartite graphs with vertices $(s,i)$ for a string $s$ and natural number $i<d$, with moves $(s,i)→(t,j)$ with $t∈\{s,s0,s1\}$. For them, we need to prove positional determinacy, where a positional strategy depends only on the current vertex.
We prove the determinacy by induction on the number of labels $k$ such that for each $k$ and $d$, the proof goes through in S2S. (I find it remarkable that we can reason like that in a decidable theory.)
Using choice, there is a positional strategy simultaneously winning from all positions with a positional winning strategy: Set $φ(f)$ if $f$ is a positional player 1 winning strategy for all vertices used in $f$. To extend $f$ to a vertex $v$, use a positional strategy for $v$, except that when we reach a vertex in $\operatorname{dom}(f)$, switch to $f$.
Next, suppose that the highest priority (i.e. label) is $k$ and has the right parity for player 2. Define the auxiliary game that ends when priority $k$ is reached (after one or more steps), or the original game ends (possibly after $ω$ moves); player 1 wins iff the winning condition is met or player 1 can positionally win from the final position. If player 1 positionally wins the auxiliary game, he can positionally win the original game since one can merge the auxiliary strategy with a universal positional strategy for the original game. Otherwise, by determinacy for $k-1$ (for the base case, games of length 1 are determined), player 2 positionally wins the auxiliary game. Using choice, let $f$ be a positional player 2 winning strategy for the auxiliary game for all positions in which player 2 wins that game. $f$ wins the original game for player 2 since either priority $k$ is hit infinitely often, or the final auxiliary win wins the original game.
Related theories
The axiomatization for $k$ successors is analogous (this does not immediately follow from the interpretability in S2S). The monadic theory of forests (as graphs) is axiomatizable using graph axioms, the absence of cycles (using the $Π^1_1$ formulation of connectivity), and (4)-(5).
Shelah-Stup theorem (which can be found for example here) extends as follows. Let $C$ be a class of monadic second order (MSO) structures of a given signature without functions or constants or 0-ary relations, and $T$ be the theory of $C$. Let the tree counterpart of $C$ consist of MSO models of 1,2,3,6 (below), with all models in (6) isomorphic to models in $C$. Then, (1)-(6) axiomatize its theory:
(1) $∃!a ∀b \, ¬t(a,b)$ (the root; denoted by $ε$; $t(a,b)$ means $b$ is a child of $a$)
(2) $b=d ∧ t(a,b) ∧ t(c,d) ⇒ a=c$ (tree successors)
(3) $∀S \, (S(ε) ∧ ∀a,b \, (t(a,b) ∧ S(a) ⇒ S(b))⇒ ∀a \, S(a))$ (induction)
(4)-(5) Same (as a schema) as axioms 4 and 5 for S2S.
(6) For every $a$, its children model $T$ (stated using one axiom per $T$ axiom). All atomic $T$-relations are false unless all distinct arguments are siblings. (The signature of the tree counterpart includes the signature of $T$, with a naming convention to avoid conflicts.)
The resulting theory is recursive in $T$, with an iterated-exponential-time many-to-one uniform reduction. Empty first order part is allowed in the theorem. For example, MSO models of trees (i.e. rooted trees with all nodes having finite depth) with a predicate for whether a set of siblings is finite (which can be used to define global finiteness) form the tree counterpart of MSO logic on zero or more elements with a predicate for whether a set of elements is finite.
For the proof, the above determinacy proof (and the rest) extends to tree automata using $T$-formulas for transitions (as in the Shelah-Stup theorem proof). A complication is that (5) only uses boolean functions (and we might not have pairing), but (5) suffices for well-founded subtrees (choosing nonlosing positions wins there), and for the remaining tree, we only need choice for branch points, and for each child of a branch point, we can store $O(1)$ bits at $O(1)$ higher depth.
