Misplaced Pages

#182817

59-575: In mathematics, S2S is the monadic second order theory of the infinite complete binary tree . S2S may also refer to: S2S (mathematics) 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 → s 0 and s → s 1 on strings, and predicate s ∈ S (equivalently, S ( s )) meaning string s belongs to set S . Some properties and conventions: Weakenings of S2S: Weak S2S (WS2S) requires all sets to be finite (note that finiteness

118-403: A (Theory( M ), T ) oracle, where a model of T 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

177-400: 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. 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

236-403: 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 Δ 2 formula. Moreover, every S2S formula is equivalent to

295-487: 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

354-417: 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

413-530: A finite set of other sentences (this follows from its connection to Π 2 -CA 0 ). 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

472-850: 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. 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 . Series-parallel graph In graph theory , series–parallel graphs are graphs with two distinguished vertices called terminals , formed recursively by two simple composition operations. They can be used to model series and parallel electric circuits . In this context,

531-529: 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 Π 1 transfinite recursion (see reverse mathematics ). RCA 0 + (schema) {τ: τ

590-580: 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. S2S can be partially axiomatized by: (1) ∃! s ∀ t ( t 0≠ s ∧ t 1≠ s ) (empty string, denoted by ε; ∃! s means "there

649-489: A linearly growing stack of exponentials. For the lower bound, it suffices to consider Σ 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 i 1 i 2 ... i m as i 1 1 i 2 2 ... i m m , preceded by

SECTION 10

#1732851514183

708-461: 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 (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

767-416: A model of certain types of electric networks, these graphs are of interest in computational complexity theory , because a number of standard graph problems are solvable in linear time on SP-graphs, including finding of the maximum matching , maximum independent set , minimum dominating set and Hamiltonian completion . Some of these problems are NP-complete for general graphs. The solution capitalizes on

826-458: A modification of the above (3)⇒(2) and even without requiring positionality; see the reference). In turn, their existence (using (4)⇒(3)) gives the desired Σ 1 elementary chains. 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

885-448: 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 1 ,..., vd k ) ⇔ P i ( d 1 ,..., d k ) with P i ' false otherwise ( d j ∈ M , and v

944-473: 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 Π 3 sentences (using the prefix relation on strings as a primitive). However, it is not finitely axiomatizable, nor can it be axiomatized by Σ 3 sentences even if we add induction schema and

1003-402: 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 ( R {\displaystyle \mathbb {R} } , <)

1062-412: 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 (also called memoryless) determinacy, this can be simulated by a finite game that ends when we reach

1121-444: A smaller label outside the least fixed point, player 2 can use it (abandoning the auxiliary game), otherwise (using monotonicity) player 2 can use an auxiliary game strategy that assumes that the set of smaller labels in the original game will equal the least fixed point.) For (4)⇒(3), we use monotonic induction to build an initial segment of the constructible hierarchy above a given real number r . This works as long as each ordinal α

1180-404: 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 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 of M -products of T is decidable relative to

1239-413: 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

SECTION 20

#1732851514183

1298-408: Is a finite boolean combination of Π 2 ( 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 Π 3 consequences of in Π 2 -CA 0 . For (3)⇒(2), define a game where player 1 attempts to show that

1357-491: 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 ( R {\displaystyle \mathbb {R} } ,0,+,⋅), we can state ∀(function f ) ∀ s ∃ r ∈ N s f ( s ) + N s r = 0 N s . If M

1416-463: Is a graph that may be constructed by a sequence of series and parallel compositions starting from a set of copies of a single-edge graph K 2 with assigned terminals. Definition 1 . Finally, a graph is called series–parallel (SP-graph) , if it is a TTSPG when some two of its vertices are regarded as source and sink. In a similar way one may define series–parallel digraphs , constructed from copies of single-arc graphs, with arcs directed from

1475-527: Is a series–parallel graph. The maximal series–parallel graphs, graphs to which no additional edges can be added without destroying their series–parallel structure, are exactly the 2-trees . 2-connected series–parallel graphs are characterised by having no subgraph homeomorphic to K 4 . Series parallel graphs may also be characterized by their ear decompositions . SP-graphs may be recognized in linear time and their series–parallel decomposition may be constructed in linear time as well. Besides being

1534-439: Is a true S2S sentence} is equivalent to (schema) {τ: τ is a Π 3 sentence provable in Π 2 -CA 0 }. 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, Π 2 -CA 0 does not prove that all true (under

1593-440: 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 1 ,..., S k ), (with k free variables) and finite tree of binary strings T , φ( S 1 ∩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

1652-454: 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

1711-483: 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

1770-415: Is identified by some appropriately expressible property of α so that we can encode α by a natural number and continue. Now, suppose that we built L α (r) and the inductive step (which uses L α (r) as a parameter) allows examining L β (r). If a new Σ 1 fact appears between α and β, we can use it to label α and continue. Otherwise, we get the above Σ 1 elementary chains whose length corresponds to

1829-402: Is infinite or player 2 wins the last auxiliary game. In the auxiliary game, player 1 attempts to show that the last element picked by player 2 is a valid inductive step using elements with smaller labels. Now, if s is not in the least fixed-point, then the set of labels is ill-founded, or an inductive step is wrong, and (using monotonicity) this can be picked up by player 2. (If player 1 plays

S2S - Misplaced Pages Continue

1888-587: 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

1947-420: Is undecidable if U is the unbounding quantifier — U X Φ( X ) iff Φ( X ) holds for some arbitrarily large finite X . However, WS2S+U, even with quantification over infinite paths, is decidable, even with S2S subformulas that do not contain U. 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

2006-473: 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 iff 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)

2065-458: 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 ( s 0) ∧ S ( s 1))⇒ ∀ 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

2124-516: 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

2183-411: 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

2242-413: 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

2301-606: The complete binary tree and use the decidability of S2S. For example, for a node s , we can represent its children by s 1, s 01, s 001, 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 ω 1 , and the predicate for cardinality ω 2 , 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 . Tree extensions of monadic theories: By Shelah-Stup theorem, if

2360-403: The desired element s is inside the least fixed point. Player 1 gradually labels elements including s with rational numbers, intended to correspond to ordinal stages of the monotonic induction (any countable ordinal is embeddable into Q {\displaystyle \mathbb {Q} } ). Player 2 plays elements with strictly descending labels (and he can pass) and wins iff the sequence

2419-425: The determinacy proof for boolean combinations of Π 2 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

S2S - Misplaced Pages Continue

2478-421: The determinization for going left (i.e. s → s 0) 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

2537-406: 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

2596-520: The fact that if the answers for one of these problems are known for two SP-graphs, then one can quickly find the answer for their series and parallel compositions. The generalized series–parallel graphs (GSP-graphs) are an extension of the SP-graphs with the same algorithmic efficiency for the mentioned problems. The class of GSP-graphs include the classes of SP-graphs and outerplanar graphs . GSP graphs may be specified by Definition 2 augmented with

2655-447: 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. Σ 1 ) MSO theory is undecidable if we allow predicates on both vertices and edges. Thus, in

2714-411: The formula size (more precisely, the time is O ( | T | k ) + 2 O ( | ϕ | ) 2 {\displaystyle O(|T|k)+2_{O(|\phi |)}^{2}} ). For S1S, every formula is equivalent to a Δ 1 formula, and to a boolean combination of Π 2 arithmetic formulas. Moreover, every S1S formula is equivalent to acceptance by

2773-402: 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

2832-399: 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

2891-413: The nesting depth of the monotonic inductive definitions. For the equivalence of RCA 0 +S2S with {Π 3 φ: Π 2 -CA 0 ⊢φ}, for each k the positional determinacy with k priorities is provable in Π 2 -CA 0 , while the rest (in terms of proving S2S sentences) can be done in a weak base theory. Conversely, RCA 0 +S2S gives us a determinacy schema that gives existence of least fixed points (by

2950-401: 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

3009-410: 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

SECTION 50

#1732851514183

3068-426: The source to the sink. The following definition specifies the same class of graphs. Definition 2 . A graph is an SP-graph, if it may be turned into K 2 by a sequence of the following operations: Every series–parallel graph has treewidth at most 2 and branchwidth at most 2. Indeed, a graph has treewidth at most 2 if and only if it has branchwidth at most 2, if and only if every biconnected component

3127-441: The sources of X and Y to create the source of Pc and merging the sinks of X and Y to create the sink of Pc . The series composition Sc = Sc(X,Y) of two TTGs X and Y is a TTG created from the disjoint union of graphs X and Y by merging the sink of X with the source of Y . The source of X becomes the source of Sc and the sink of Y becomes the sink of Sc . A two-terminal series–parallel graph (TTSPG)

3186-496: 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

3245-400: The standard decision procedure) Π 3 S2S statements are actually true even though each such sentence is provable Π 2 -CA 0 . 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

3304-446: The term graph means multigraph . There are several ways to define series–parallel graphs. The following definition basically follows the one used by David Eppstein . A two-terminal graph (TTG) is a graph with two distinguished vertices, s and t called source and sink , respectively. The parallel composition Pc = Pc(X,Y) of two TTGs X and Y is a TTG created from the disjoint union of graphs X and Y by merging

3363-550: The third operation of deletion of a dangling vertex (vertex of degree 1). Alternatively, Definition 1 may be augmented with the following operation. An SPQR tree is a tree structure that can be defined for an arbitrary 2-vertex-connected graph . It has S-nodes, which are analogous to the series composition operations in series–parallel graphs, P-nodes, which are analogous to the parallel composition operations in series–parallel graphs, and R-nodes, which do not correspond to series–parallel composition operations. A 2-connected graph

3422-450: 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 0 , p 1 ), while player 2 chooses the branch, with the transition to p 0 if 0 is chosen and p 1 otherwise. For a co-nondeterministic automaton, all choices are by player 2, while for deterministic, (p 0 ,p 1 )

3481-452: 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

#182817