1443:. 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 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.
1439:
strings). A labeled tree 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
1237:). Player 2 plays elements with strictly descending labels (and he can pass) and wins iff the sequence 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
2063:
Every decidable predicate on strings can be encoded (with linear time encoding and decoding) for decidability of S2S (even with 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
1492:
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 is where we need impredicative comprehension), non-existence of player 1
2064:(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 the automaton enters the tree). (Note a rough similarity with the
1241:
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 a smaller label outside the least fixed point, player 2 can use it (abandoning the auxiliary game), otherwise (using
1758:
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 the child (of the node) to continue. To witness rejection by a non-deterministic automaton, for each (node,
670:
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
1438:
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
1459:). An infinite tree automaton starts at the root and moves up 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 (
1612:
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 the complete binary tree and use the decidability of S2S. For example, for a node
1489:) 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.
1557:), 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 α (or for player 2) lower initial position (so we can switch a strategy finitely many times).
318:
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
1602:. Using the above positional (also called memoryless) 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
1563:
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
1308:+S2S gives us a determinacy schema that gives existence of least fixed points (by 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 Σ
914:
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).
682:) 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
1656:
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
1519:
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
371:, 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
1497:, 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
1532:
has the right parity for player 2. For each position (tree position + state) assign the least ordinal α (if any) such that player 1 has a winning strategy with all entered (after one or more steps) priority
568:
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
1576:
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
1159:
See and, but briefly the proof runs as follows. (1)⇒(2) follows from the below decidability proof using tree automata. (2)⇒(1) follows by converting the game associated with a binary string
1249:. This works as long as each ordinal α 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
603:
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)
897:
1322:
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
1637:, 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
727:)). 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.
20:
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
1844:
1235:
713:
32:
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
1759:
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.
1337:
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.
1629:
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 ω
1242:
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.)
2072:
of (state, highest_priority_reached) pairs returns whether player 1 (i.e. nondeterminism) can simultaneously force all branches to correspond to elements of
209:
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.
1163:
into a tree parity game with a fixed number of priorities and then merging these trees into a single tree (the binary trees can be merged here using
287:: 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.
212:
For formula complexity, the prefix relation on strings is typically treated as first order. Without it, not all formulas would be equivalent to Δ
2348:
2068:.) For example (for a parity automaton), assign trees to the same class if they have the same predicate that given initial_state and set
630:
sentences (using the prefix relation on strings as a primitive). However, it is not finitely axiomatizable, nor can it be axiomatized by Σ
2114:
769:. For S2S, for formulas that use their free variables only on strings not containing a 1, the expressiveness is the same as for S1S.
298:). S1S can be obtained by requiring that '1' does not appear in strings, and WS1S also requires finiteness. Even WS1S can interpret
1580:(for co-nondeterministic, take the complement, noting that deterministic parity automata are closed under complements), we can use a
1215:
with rational numbers, intended to correspond to ordinal stages of the monotonic induction (any countable ordinal is embeddable into
1451:
The proof of decidability is by showing that every formula is equivalent to acceptance by a nondeterministic tree automaton (see
753:. However, WS2S+U, even with quantification over infinite paths, is decidable, even with S2S subformulas that do not contain U.
2435:, Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore, vol. 15, pp. 193–205,
938:... (assuming that our formalization has both the prefix relation and the successor functions). For S1S, three quantifiers (∃
314:
decision complexity corresponding to a linearly growing stack of exponentials. For the lower bound, it suffices to consider Σ
2798:
2448:
2232:
1245:
For (4)⇒(3), we use monotonic induction to build an initial segment of the constructible hierarchy above a given real number
961:
However, with free second order variables, not every S2S formula can be expressed in second order arithmetic through just Π
689:
By reduction to S2S, the MSO theory of countable orders is decidable, as is the MSO theory of countable trees with their
1606:
algorithm, which is polynomial time when the number of priorities is small enough (which occurs commonly in practice).
1750:). The proof is similar to the S2S decidability proof. At each step, a (nondeterministic) automaton gets a tuple of
2053:) to answer what is possible, and given a list possibilities (or constraints), formulate a corresponding sentence in
302:
with a predicate for powers of 2, as sets can be used to represent unbounded binary numbers with definable addition.
634:
sentences even if we add induction schema and a finite set of other sentences (this follows from its connection to Π
1541:
state is reached, the ordinal is decreased, and moreover in between the decreases, player 1 can use a strategy for
1537:
positions (if any) having labels <α. Player 1 can win if the initial position is labeled: Each time a priority
2165:
2753:
1100:
can be computed from the set of winning positions for some game whose payoff is a finite boolean combination of Π
820:), but as noted above, the overhead can be iterated exponential in the formula size (more precisely, the time is
823:
2674:
1440:
2821:
2311:
1553:
state, in which case player 2 can again use that strategy. To make the strategy positional (by induction on
565:
2183:
A model theoretic proof of completeness of an axiomatization of monadic second-order logic on infinite words
1415:). Also, by using lexicographically least shortest choices, there is an S1S formula φ' such that φ'⇒φ and ∃
2181:
2816:
2209:
1765:
1481:
otherwise. For a co-nondeterministic automaton, all choices are by player 2, while for deterministic, (p
219:
For properties expressible in S2S (viewing the set of all binary strings as a tree), for each node, only
1304:, while the rest (in terms of proving S2S sentences) can be done in a weak base theory. Conversely, RCA
1269:
elementary chains whose length corresponds to the nesting depth of the monotonic inductive definitions.
1927:
with equality, the extended S2S or just WS1S is undecidable. Also, for a (possibly incomplete) theory
17:
2291:(A preliminary 2015 version erroneously claimed proof of completeness without the determinacy schema.)
1265:
fact appears between α and β, we can use it to label α and continue. Otherwise, we get the above Σ
690:
224:
1827:
1218:
696:
79:
By default, lowercase letters refer to first order objects, and uppercase to second order objects.
2255:
Das, Anupam; Riba, Colin (2020). "A functional (monadic) second-order theory of infinite trees".
1903:
is S2S (or more generally, the tree counterpart of some monadic model), the automata can now use
1456:
1431:) (i.e. uniformization; φ may have free variables not shown; φ' depends only on the formula φ).
1050:
910:
arithmetic formulas. Moreover, every S1S formula is equivalent to acceptance by a corresponding
724:
570:
294:
Weak S2S (WS2S) requires all sets to be finite (note that finiteness is expressible in S2S using
2080:, pick a finite set of trees (suitable for coding) that belong to the same class for automata 1-
1588:, and node creation and deletion based on reaching high priority states. For details, see or.
1046:
817:
766:
663:
532:
922:
formula. Moreover, every S2S formula is equivalent to a formula with just four quantifiers, ∃
223:(1) bits can be communicated between the left subtree and the right subtree and the rest (see
2778:
667:
311:
299:
2540:
600:)). Since we have comprehension, induction can be a single statement rather than a schema.
1603:
8:
966:
295:
2735:
2727:
2709:
2653:
2620:
2619:. 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06). pp. 255–264.
2592:
Kołodziejczyk, Leszek; Michalewski, Henryk; Pradic, Pierre; Skrzypczak, Michał (2019).
2519:
2492:
2468:
2406:
2398:
2330:
2282:
2264:
2238:
1545:-1 priorities. Player 2 can win if the position is unlabeled: By the determinacy for
1193:). The below determinacy proof (in the decidability section) also leads to (2)⇒(3). Π
2794:
2739:
2650:
Determinization of Büchi
Automata: Unifying the Approaches of Safra and Muller-Schupp
2444:
2425:
2410:
2228:
1594:
Acceptance by a nondeterministic parity automaton of the empty tree corresponds to a
1119:
118:
2334:
2286:
2278:
2242:
1207:
For (3)⇒(2), define a game where player 1 attempts to show that the desired element
678:
By contrast, for every set of graphs of unbounded treewidth, its existential (i.e. Σ
619:. However, (1)-(4) is complete when extended with a determinacy schema for certain
2786:
2719:
2630:
2574:
2436:
2390:
2320:
2274:
2220:
2190:
2146:
1435:
1364:(with its size bounded by the number of states in a deterministic automaton for φ).
1340:
This follows from relative recursiveness of S1S definable sets plus uniformization:
1323:
1133:
765:). In S1S, a (unary) predicate on sets is (parameter-free) definable iff it is an
762:
731:
82:
The inclusion of sets makes S2S second order, with "monadic" indicating absence of
21:
2785:. Lecture Notes in Computer Science. Vol. 2500. Springer. pp. 207–230.
2617:
From
Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata
2224:
2194:
1549:-1 priorities, player 2 has a strategy that wins or enters an unlabeled priority
1090:
is S2S definable from some set of binary strings polynomial time computable from
616:
604:
2673:
Calude, Cristian; Jain, Sanjay; Khoussainov, Bakhadyr; Li, Wei; Stephan, Frank.
2140:
391:
WS2S can be axiomatized through certain basic properties plus induction schema.
2578:
2555:
2440:
2302:
1789:
1452:
1211:
is inside the least fixed point. Player 1 gradually labels elements including
973:+ (schema) {τ: τ is a true S2S sentence} is equivalent to (schema) {τ: τ is a Π
683:
2694:
2371:
911:
2810:
2790:
2150:
2065:
2045:| free variables. Thus, we can quantify over all possible outcomes by using
1065:
S2S statements are actually true even though each such sentence is provable Π
615:, and comprehension schemas are commonly augmented with various forms of the
761:
A set of binary strings is definable in S2S iff it is regular (i.e. forms a
1638:
2167:
An axiom system for the weak monadic second order theory of two successors
737:
S2S+U (or just S1S+U) is undecidable if U is the unbounding quantifier — U
2634:
2518:. LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science.
1595:
1512:
620:
383:(1)-fold exponentiation of the sentence length (with uniform constants).
203:
2591:
918:
For S2S, using tree automata (below), every formula is equivalent to a Δ
2731:
2402:
2325:
2306:
2219:, Lecture Notes in Computer Science, vol. 4646, pp. 161–176,
1129:
2115:"Decidability of second-order theories and automata on infinite trees"
1061:
does not prove that all true (under the standard decision procedure) Π
662:(and a corresponding tree decomposition) is interpretable in S2S (see
2593:
958:) suffice; the prefix relation is not needed here for WS2S and WS1S.
672:
655:
2723:
2394:
183:
In place of strings, one can use (for example) natural numbers with
2714:
2658:
2524:
2473:
2349:"What is the Turing degree of the monadic theory of the real line?"
2269:
985:}. Over a base theory, the schemas are equivalent to (schema over
2625:
2497:
375:-fold quantifier alternation can decided in time corresponding to
1923:
sets. Disjointness is necessary as otherwise for every infinite
654:, the monadic second order (MSO) theory of countable graphs with
1350:) can be computed from the parameters of φ and the values of φ(
1644:
1473:), while player 2 chooses the branch, with the transition to p
730:
S2S is useful for decidability of certain modal logics, with
2463:
Bojańczyk, Mikołaj; Parys, Paweł; Toruńczyk, Szymon (2015),
1501:
corresponds to acceptance by a non-deterministic automaton.
2370:
Gurevich, Yuri; Magidor, Menachem; Shelah, Saharon (1993).
1820:, with the language modified accordingly. For example, if
666:). For example, the MSO theory of trees (as graphs) or of
1993:). The proof is by induction on formula complexity. Let
1568:
tree automata as the determinization for going left (i.e.
1515:, and the determinacy proof for boolean combinations of Π
1508:
715:, <) is undecidable. The MSO theory of ordinals <ω
310:
S2S is decidable, and each of S2S, S1S, WS2S, WS1S has a
202:
The set of all binary strings is denoted by {0,1}, using
2513:
2142:
On the
Structure of the Monadic Logic of the Binary Tree
1396:
such that the highest priority during each extension is
2462:
2594:"The logical strength of Büchi's decidability theorem"
1652:
By Shelah-Stup theorem, if a monadic relational model
2369:
1830:
1763:
Combining a monadic theory with a first order theory:
1221:
826:
699:
2489:
Weak MSO+U with path quantifiers over infinite trees
1132:(i.e. an ω-model whose set-theoretic counterpart is
950:) suffice, and for WS2S and WS1S, two quantifiers (∃
323:, we can encode a number with binary representation
2672:
2553:
2514:Kołodziejczyk, Leszek; Michalewski, Henryk (2016).
2509:
2507:
2210:"MSO on the Infinite Binary Tree: Choice and Order"
1808:is identified with its first objects, and for each
1584:with each node storing a set of possible states of
1493:winning strategy gives a player 2 winning strategy
2554:Heinatsch, Christoph; Möllerfeld, Michael (2010).
1838:
1229:
891:
792:free variables) and finite tree of binary strings
707:
2122:Transactions of the American Mathematical Society
2088:. To encode a predicate, encode some bits using
1754:objects (possibly second order) as input, and an
2808:
2504:
1118:in arithmetic μ-calculus (arithmetic formulas +
2516:How unprovable is Rabin's decidability theorem?
124:Equality is primitive, or it can be defined as
2300:
1746:is a (possibly empty) sequence of elements of
1404:satisfying φ without hitting priorities above
2676:Deciding parity games in quasipolynomial time
2538:
2207:
2084:, with the choice of class consistent across
1400:and that the extension can be completed into
242:) can be encoded by a single set. Moreover,
2465:The MSO+U theory of (N, <) is undecidable
1524:priorities, with the highest priority being
2754:"The generalization of Shelah–Stup theorem"
1645:Combining S2S with other decidable theories
902:For S1S, every formula is equivalent to a Δ
2539:Kołodziejczyk, Leszek (October 19, 2015).
2208:Carayol, Arnaud; Löding, Christof (2007),
1408:(these are permitted only for the initial
906:formula, and to a boolean combination of Π
892:{\displaystyle O(|T|k)+2_{O(|\phi |)}^{2}}
749:) holds for some arbitrarily large finite
723:is independent of ZFC (assuming Con(ZFC +
645:
2713:
2657:
2647:
2624:
2523:
2496:
2486:
2472:
2324:
2307:"The monadic theory and the "next world""
2268:
1832:
1434:The minimal model of S2S consists of all
1223:
701:
2614:
1780:remains decidable relative to a (Theory(
1317:
1253:(r) and the inductive step (which uses L
2254:
2163:
2023:is free. By induction, one shows that
1076:Moreover, given sets of binary strings
812:∩T) can be computed in time linear in |
2809:
2692:
2423:
2138:
1446:
1257:(r) as a parameter) allows examining L
2776:
2112:
2032:is only used through a finite set of
1633:, and the predicate for cardinality ω
756:
109:generally available in S2S, not even
2783:Automata, Logics, and Infinite Games
2179:
1650:Tree extensions of monadic theories:
394:S2S can be partially axiomatized by:
2598:Logical Methods in Computer Science
2433:Computational Prospects of Infinity
2257:Logical Methods in Computer Science
1943:is decidable relative to a (Theory(
1617:, we can represent its children by
27:
13:
2648:Löding, Christof; Pirogov, Anton.
2426:"Monadic definability of ordinals"
420:) (empty string, denoted by ε; ∃!
14:
2833:
2541:"Question on Decidability of S2S"
1955:uses an arbitrary disjoint model
1846:,0,+,⋅), we can state ∀(function
1205:monotonic induction, so (3)⇒(4).
75:Some properties and conventions:
2567:Annals of Pure and Applied Logic
1796:is augmented with all functions
1768:extends/applies as follows. If
1292:the positional determinacy with
719:is decidable; decidability for ω
626:S2S can also be axiomatized by Π
2746:
2686:
2666:
2641:
2608:
2585:
2547:
2532:
2480:
2456:
2417:
1907:-formulas, and thereby convert
1084:, the following are equivalent:
1053:). Due to limited induction, Π
693:. However, the MSO theory of (
2556:"The determinacy strength of Π
2363:
2341:
2294:
2248:
2201:
2173:
2157:
2139:Janin, David; Lenzi, Giacomo.
2132:
2106:
2061:Coding into extensions of S2S:
1441:elementary function arithmetic
1374:) can be obtained by choosing
879:
875:
867:
863:
849:
842:
834:
830:
1:
2779:"Decidability of S1S and S2S"
2383:The Journal of Symbolic Logic
2312:Israel Journal of Mathematics
2099:
1776:is a first order model, then
1661:ordered by extension, and an
234:, a function from strings to
121:between strings is definable.
86:-ary predicate variables for
2693:Shelah, Saharon (Nov 1975).
2225:10.1007/978-3-540-74915-8_15
2195:10.1007/978-3-642-33475-7_22
1839:{\displaystyle \mathbb {R} }
1230:{\displaystyle \mathbb {Q} }
734:naturally leading to trees.
708:{\displaystyle \mathbb {R} }
671:connected graphs of bounded
238:(i.e. natural numbers below
48:1 on strings, and predicate
7:
2487:Bojańczyk, Mikołaj (2014),
1951:) oracle, where a model of
1592:Decidability of acceptance:
1389:, and repeatedly extending
1296:priorities is provable in Π
1189:doubles every character of
965:transfinite recursion (see
607:that given a non-empty set
268:doubles every character of
199:+2 but no other operations.
18:monadic second order theory
16:In mathematics, S2S is the
10:
2838:
2579:10.1016/j.apal.2010.04.012
2441:10.1142/9789812796554_0010
1816:we use a disjoint copy of
1272:For the equivalence of RCA
2695:"Monadic theory of order"
2279:10.23638/LMCS-16(4:6)2020
2092:=1, then more bits using
1561:Automata determinization:
1378:and a finite fragment of
93:Concatenation of strings
2791:10.1007/3-540-36387-4_12
2372:"The monadic theory of ω
2151:10.1007/3-540-48340-3_28
1980:is an MSO model; Theory(
772:For every S2S formula φ(
478:is an abbreviation; for
225:communication complexity
2113:Rabin, Michael (1969).
1766:Feferman–Vaught theorem
1457:infinite-tree automaton
1120:least fixed-point logic
1051:large countable ordinal
725:weakly compact cardinal
646:Theories related to S2S
424:means "there is unique
2615:Piterman, Nir (2006).
2217:Computer Science Logic
2164:Siefkes, Dirk (1971),
1840:
1357:) for a finite set of
1333:⊆ω, sets recursive in
1231:
1047:constructible universe
977:sentence provable in Π
893:
709:
668:series-parallel graphs
611:returns an element of
2774:Additional reference:
2702:Annals of Mathematics
2424:Neeman, Itay (2008),
2011:variables, including
1841:
1318:Models of S1S and S2S
1232:
894:
710:
691:Kleene–Brouwer orders
486:, 0 does not equal 1)
300:Presburger arithmetic
2822:Computability theory
2777:Weyer, Mark (2002).
2635:10.1109/LICS.2006.28
2180:Riba, Colin (2012).
2002:be the list of free
1828:
1772:is an MSO model and
1604:quasipolynomial time
1477:if 0 is chosen and p
1346:) (as a function of
1219:
1144:consequences of in Π
1140:and satisfying all Π
1114:can be defined from
824:
697:
566:comprehension schema
1729:' false otherwise (
1447:Decidability of S2S
1312:elementary chains.
967:reverse mathematics
888:
818:Courcelle's theorem
664:Courcelle's theorem
306:Decision complexity
2817:Mathematical logic
2326:10.1007/BF02760646
1836:
1598:on a finite graph
1511:, Borel games are
1227:
889:
855:
767:ω-regular language
757:Formula complexity
705:
292:Weakenings of S2S:
272:is injective, and
64:)) meaning string
2800:978-3-540-00388-5
2573:(12): 1462–1470.
2450:978-981-279-654-7
2234:978-3-540-74914-1
2076:. Now, for each
1436:regular languages
1366:- A witness for ∃
650:For every finite
2829:
2804:
2768:
2767:
2765:
2763:
2758:
2750:
2744:
2743:
2717:
2699:
2690:
2684:
2683:
2681:
2670:
2664:
2663:
2661:
2645:
2639:
2638:
2628:
2612:
2606:
2605:
2604:(2): 16:1–16:31.
2589:
2583:
2582:
2564:
2551:
2545:
2544:
2536:
2530:
2529:
2527:
2511:
2502:
2501:
2500:
2484:
2478:
2477:
2476:
2460:
2454:
2453:
2430:
2421:
2415:
2414:
2380:
2367:
2361:
2360:
2358:
2356:
2345:
2339:
2338:
2328:
2301:Gurevich, Yuri;
2298:
2292:
2290:
2272:
2252:
2246:
2245:
2214:
2205:
2199:
2198:
2188:
2177:
2171:
2170:
2161:
2155:
2154:
2136:
2130:
2129:
2119:
2110:
2036:-formulas with |
1989:) may depend on
1919:into a tuple of
1845:
1843:
1842:
1837:
1835:
1610:Theory of trees:
1566:nondeterministic
1414:
1395:
1384:
1363:
1356:
1324:Henkin semantics
1261:(r). If a new Σ
1236:
1234:
1233:
1228:
1226:
1188:
1181:
1128:is in the least
898:
896:
895:
890:
887:
882:
878:
870:
845:
837:
763:regular language
732:Kripke semantics
714:
712:
711:
706:
704:
470:) (the use of
286:
267:
260:
28:Basic properties
2837:
2836:
2832:
2831:
2830:
2828:
2827:
2826:
2807:
2806:
2801:
2775:
2772:
2771:
2761:
2759:
2756:
2752:
2751:
2747:
2724:10.2307/1971037
2697:
2691:
2687:
2679:
2671:
2667:
2646:
2642:
2613:
2609:
2590:
2586:
2562:
2560:-comprehension"
2559:
2552:
2548:
2537:
2533:
2512:
2505:
2485:
2481:
2461:
2457:
2451:
2428:
2422:
2418:
2395:10.2307/2273556
2378:
2375:
2368:
2364:
2354:
2352:
2347:
2346:
2342:
2303:Shelah, Saharon
2299:
2295:
2253:
2249:
2235:
2212:
2206:
2202:
2186:
2178:
2174:
2162:
2158:
2137:
2133:
2117:
2111:
2107:
2102:
2096:=2, and so on.
2044:
2031:
2010:
2001:
1988:
1963:
1898:
1897:
1884:
1883:
1866:
1831:
1829:
1826:
1825:
1737:
1728:
1719:
1712:
1705:
1696:
1689:
1682:
1673:
1647:
1636:
1632:
1518:
1488:
1484:
1480:
1476:
1472:
1465:
1449:
1412:
1393:
1382:
1365:
1361:
1354:
1341:
1320:
1315:
1314:
1311:
1307:
1303:
1299:
1287:
1283:
1279:
1275:
1268:
1264:
1260:
1256:
1252:
1222:
1220:
1217:
1216:
1204:
1200:
1196:
1186:
1179:
1157:
1151:
1147:
1143:
1123:
1109:
1103:
1095:
1085:
1072:
1068:
1064:
1060:
1056:
1040:
1039:
1029:
1028:
1022:
1021:
1011:
1010:
1002:
996:
984:
980:
976:
972:
964:
921:
909:
905:
883:
874:
866:
859:
841:
833:
825:
822:
821:
811:
802:
787:
778:
759:
722:
718:
700:
698:
695:
694:
681:
648:
641:
637:
633:
629:
617:axiom of choice
605:choice function
561:not free in φ)
536:
487:
429:
395:
367:
358:
351:
344:
335:
329:
317:
284:
265:
258:
215:
119:prefix relation
68:belongs to set
56:(equivalently,
30:
12:
11:
5:
2835:
2825:
2824:
2819:
2799:
2770:
2769:
2745:
2708:(3): 379–419.
2685:
2665:
2652:. ICALP 2019.
2640:
2607:
2584:
2557:
2546:
2531:
2503:
2479:
2455:
2449:
2416:
2389:(2): 387–398.
2373:
2362:
2351:. MathOverflow
2340:
2319:(1–3): 55–68.
2293:
2247:
2233:
2200:
2172:
2156:
2131:
2104:
2103:
2101:
2098:
2040:
2027:
2019:) if function
2006:
1997:
1984:
1959:
1893:
1889:
1879:
1875:
1862:
1834:
1733:
1724:
1717:
1710:
1701:
1694:
1687:
1678:
1669:
1646:
1643:
1634:
1630:
1516:
1486:
1482:
1478:
1474:
1470:
1463:
1453:tree automaton
1448:
1445:
1319:
1316:
1309:
1305:
1301:
1297:
1288:⊢φ}, for each
1285:
1281:
1277:
1273:
1266:
1262:
1258:
1254:
1250:
1225:
1202:
1198:
1194:
1158:
1155:
1154:
1149:
1145:
1141:
1101:
1070:
1066:
1062:
1058:
1054:
1035:
1033:
1026:
1024:
1019:
1017:
1008:
1006:
998:
994:
982:
978:
974:
970:
962:
919:
907:
903:
886:
881:
877:
873:
869:
865:
862:
858:
854:
851:
848:
844:
840:
836:
832:
829:
807:
800:
783:
776:
758:
755:
720:
716:
703:
684:Turing machine
679:
647:
644:
639:
635:
631:
627:
571:extensionality
387:Axiomatization
363:
356:
349:
340:
333:
327:
315:
289:
288:
228:
217:
213:
210:
207:
200:
181:
122:
101:is denoted by
91:
80:
29:
26:
9:
6:
4:
3:
2:
2834:
2823:
2820:
2818:
2815:
2814:
2812:
2805:
2802:
2796:
2792:
2788:
2784:
2780:
2755:
2749:
2741:
2737:
2733:
2729:
2725:
2721:
2716:
2711:
2707:
2703:
2696:
2689:
2678:
2677:
2669:
2660:
2655:
2651:
2644:
2636:
2632:
2627:
2622:
2618:
2611:
2603:
2599:
2595:
2588:
2580:
2576:
2572:
2568:
2561:
2550:
2542:
2535:
2526:
2521:
2517:
2510:
2508:
2499:
2494:
2490:
2483:
2475:
2470:
2466:
2459:
2452:
2446:
2442:
2438:
2434:
2427:
2420:
2412:
2408:
2404:
2400:
2396:
2392:
2388:
2384:
2377:
2366:
2350:
2344:
2336:
2332:
2327:
2322:
2318:
2314:
2313:
2308:
2304:
2297:
2288:
2284:
2280:
2276:
2271:
2266:
2262:
2258:
2251:
2244:
2240:
2236:
2230:
2226:
2222:
2218:
2211:
2204:
2196:
2192:
2185:
2184:
2176:
2169:
2168:
2160:
2152:
2148:
2145:. MFCS 1999.
2144:
2143:
2135:
2127:
2123:
2116:
2109:
2105:
2097:
2095:
2091:
2087:
2083:
2079:
2075:
2071:
2067:
2066:pumping lemma
2062:
2058:
2056:
2052:
2048:
2043:
2039:
2035:
2030:
2026:
2022:
2018:
2014:
2009:
2005:
2000:
1996:
1992:
1987:
1983:
1979:
1975:
1971:
1967:
1962:
1958:
1954:
1950:
1946:
1942:
1939:-products of
1938:
1934:
1931:, the theory
1930:
1926:
1922:
1918:
1914:
1910:
1906:
1902:
1896:
1892:
1887:
1882:
1878:
1873:
1869:
1865:
1861:
1857:
1853:
1849:
1823:
1819:
1815:
1811:
1807:
1803:
1799:
1795:
1791:
1787:
1783:
1779:
1775:
1771:
1767:
1764:
1760:
1757:
1753:
1749:
1745:
1741:
1736:
1732:
1727:
1723:
1716:
1709:
1704:
1700:
1693:
1686:
1681:
1677:
1674:is mapped to
1672:
1668:
1664:
1660:
1655:
1651:
1642:
1640:
1628:
1624:
1620:
1616:
1611:
1607:
1605:
1601:
1597:
1593:
1589:
1587:
1583:
1579:
1575:
1571:
1567:
1562:
1558:
1556:
1552:
1548:
1544:
1540:
1536:
1531:
1527:
1523:
1514:
1510:
1506:
1502:
1500:
1496:
1490:
1469:
1462:
1458:
1454:
1444:
1442:
1437:
1432:
1430:
1426:
1422:
1418:
1411:
1407:
1403:
1399:
1392:
1388:
1381:
1377:
1373:
1369:
1360:
1353:
1349:
1345:
1338:
1336:
1332:
1327:
1325:
1313:
1295:
1291:
1270:
1248:
1243:
1240:
1214:
1210:
1192:
1185:
1178:
1174:
1170:
1166:
1162:
1156:Proof sketch:
1153:
1139:
1136:) containing
1135:
1131:
1127:
1121:
1117:
1113:
1107:
1099:
1093:
1089:
1083:
1079:
1074:
1052:
1048:
1044:
1038:
1032:
1015:
1005:
1001:
992:
988:
968:
959:
957:
953:
949:
945:
941:
937:
933:
929:
925:
916:
913:
900:
884:
871:
860:
856:
852:
846:
838:
827:
819:
815:
810:
806:
799:
795:
791:
786:
782:
775:
770:
768:
764:
754:
752:
748:
744:
740:
735:
733:
728:
726:
692:
687:
685:
676:
674:
669:
665:
661:
657:
653:
643:
624:
622:
618:
614:
610:
606:
601:
599:
595:
591:
587:
583:
579:
575:
572:
567:
562:
560:
556:
552:
548:
544:
540:
534:
530:
527:
523:
519:
515:
511:
507:
503:
499:
495:
491:
485:
481:
477:
473:
469:
465:
461:
457:
453:
449:
445:
441:
437:
433:
427:
423:
419:
415:
411:
407:
403:
399:
392:
389:
388:
384:
382:
378:
374:
370:
366:
362:
355:
348:
343:
339:
332:
326:
322:
313:
312:nonelementary
308:
307:
303:
301:
297:
296:Kőnig's lemma
293:
283:
279:
275:
271:
264:
257:
253:
249:
245:
241:
237:
233:
229:
226:
222:
218:
211:
208:
205:
201:
198:
194:
190:
186:
182:
179:
175:
171:
167:
163:
159:
155:
151:
147:
143:
139:
135:
131:
127:
123:
120:
116:
112:
108:
104:
100:
96:
92:
89:
85:
81:
78:
77:
76:
73:
71:
67:
63:
59:
55:
51:
47:
43:
39:
35:
25:
23:
19:
2782:
2773:
2762:November 14,
2760:. Retrieved
2748:
2705:
2701:
2688:
2682:. STOC 2017.
2675:
2668:
2649:
2643:
2616:
2610:
2601:
2597:
2587:
2570:
2566:
2549:
2534:
2515:
2488:
2482:
2464:
2458:
2432:
2419:
2386:
2382:
2365:
2355:November 14,
2353:. Retrieved
2343:
2316:
2310:
2296:
2260:
2256:
2250:
2216:
2203:
2189:. TCS 2012.
2182:
2175:
2166:
2159:
2141:
2134:
2125:
2121:
2108:
2093:
2089:
2085:
2081:
2077:
2073:
2069:
2060:
2059:
2054:
2050:
2046:
2041:
2037:
2033:
2028:
2024:
2020:
2016:
2012:
2007:
2003:
1998:
1994:
1990:
1985:
1981:
1977:
1973:
1969:
1965:
1960:
1956:
1952:
1948:
1944:
1940:
1936:
1932:
1928:
1924:
1920:
1916:
1912:
1908:
1904:
1900:
1894:
1890:
1885:
1880:
1876:
1871:
1867:
1863:
1859:
1855:
1851:
1847:
1821:
1817:
1813:
1809:
1805:
1801:
1797:
1793:
1785:
1781:
1777:
1773:
1769:
1762:
1761:
1755:
1751:
1747:
1743:
1739:
1734:
1730:
1725:
1721:
1714:
1707:
1702:
1698:
1691:
1684:
1679:
1675:
1670:
1666:
1662:
1658:
1653:
1649:
1648:
1639:clique width
1626:
1622:
1618:
1614:
1609:
1608:
1599:
1591:
1590:
1585:
1581:
1577:
1573:
1569:
1565:
1560:
1559:
1554:
1550:
1546:
1542:
1538:
1534:
1529:
1525:
1521:
1507:Provably in
1505:Determinacy:
1504:
1503:
1498:
1494:
1491:
1467:
1460:
1450:
1433:
1428:
1424:
1420:
1416:
1409:
1405:
1401:
1397:
1390:
1386:
1379:
1375:
1371:
1367:
1358:
1351:
1347:
1343:
1339:
1334:
1330:
1328:
1321:
1293:
1289:
1276:+S2S with {Π
1271:
1246:
1244:
1238:
1212:
1208:
1206:
1190:
1183:
1176:
1172:
1168:
1164:
1160:
1137:
1125:
1115:
1111:
1105:
1097:
1091:
1087:
1081:
1077:
1075:
1042:
1036:
1030:
1013:
1003:
999:
997:<...<α
990:
986:
960:
955:
951:
947:
943:
939:
935:
931:
927:
923:
917:
901:
813:
808:
804:
797:
793:
789:
784:
780:
773:
771:
760:
750:
746:
742:
738:
736:
729:
688:
677:
659:
651:
649:
625:
621:parity games
612:
608:
602:
597:
593:
589:
585:
581:
577:
573:
563:
558:
554:
550:
546:
542:
538:
528:
525:
521:
517:
513:
509:
505:
501:
497:
493:
489:
483:
479:
475:
471:
467:
463:
459:
455:
451:
447:
443:
439:
435:
431:
425:
421:
417:
413:
409:
405:
401:
397:
393:
390:
386:
385:
380:
376:
372:
368:
364:
360:
353:
346:
341:
337:
330:
324:
320:
309:
305:
304:
291:
290:
281:
277:
273:
269:
262:
255:
251:
247:
243:
239:
235:
231:
230:For a fixed
220:
196:
192:
188:
184:
177:
173:
169:
165:
161:
157:
153:
149:
145:
141:
137:
133:
129:
125:
114:
110:
106:
102:
98:
94:
87:
83:
74:
69:
65:
61:
57:
53:
49:
45:
41:
37:
33:
31:
15:
1976:(as above,
1596:parity game
1528:, and that
912:ω-automaton
564:(4) is the
204:Kleene star
2811:Categories
2715:2305.00968
2659:1902.02139
2525:1508.06780
2474:1502.04578
2270:1903.05878
2100:References
1784:), Theory(
1665:-relation
1582:Safra tree
1513:determined
1329:For every
1134:transitive
1049:(see also
1041:(S) where
2740:122129926
2626:0705.2205
2498:1404.7278
2411:120260712
1968:for each
872:ϕ
788:), (with
673:pathwidth
656:treewidth
533:induction
216:formulas.
105:, and is
24:in 1969.
2335:15807840
2305:(1984).
2287:76666389
2243:14580598
1792:even if
1201:proves Δ
745:) iff Φ(
446:∈{0,1} (
442:∈{0,1} ∀
2732:1971037
2403:2273556
1720:) with
1130:β-model
1108:) sets.
1045:is the
969:). RCA
816:| (see
803:∩T,...,
496:(ε) ∧ ∀
191:+1 and
152:)) and
117:. The
2797:
2738:
2730:
2543:. FOM.
2447:
2409:
2401:
2333:
2285:
2241:
2231:
1899:. If
1804:where
1790:oracle
1742:, and
1182:where
553:) ⇔ φ(
531:(s)) (
524:1))⇒ ∀
396:(1) ∃!
359:2 ...
261:where
90:>1.
40:0 and
2757:(PDF)
2736:S2CID
2728:JSTOR
2710:arXiv
2698:(PDF)
2680:(PDF)
2654:arXiv
2621:arXiv
2563:(PDF)
2520:arXiv
2493:arXiv
2469:arXiv
2429:(PDF)
2407:S2CID
2399:JSTOR
2379:(PDF)
2331:S2CID
2283:S2CID
2265:arXiv
2263:(4).
2239:S2CID
2213:(PDF)
2187:(PDF)
2118:(PDF)
1713:,...,
1690:,...,
1423:) ⇔∃!
1023:... ≺
993:⊆ω ∃α
779:,...,
537:(4) ∃
516:0) ∧
488:(3) ∀
430:(2) ∀
22:Rabin
2795:ISBN
2764:2022
2445:ISBN
2357:2022
2229:ISBN
2049:(or
1824:is (
1697:) ⇔
1625:01,
1455:and
1342:- φ(
1280:φ: Π
1124:(4)
1110:(3)
1096:(2)
1086:(1)
1080:and
796:, φ(
592:) ⇔
557:)) (
508:) ⇒
474:and
172:) ⇔
144:) ⇔
97:and
2787:doi
2720:doi
2706:102
2631:doi
2575:doi
2571:161
2437:doi
2391:doi
2321:doi
2275:doi
2221:doi
2191:doi
2147:doi
2126:141
1964:of
1947:),
1935:of
1888:= 0
1874:) +
1850:) ∀
1788:))
1621:1,
1509:ZFC
1427:φ'(
1385:of
1326:).
1300:-CA
1284:-CA
1197:-CA
1148:-CA
1069:-CA
1057:-CA
1016:) ≺
989:) ∀
981:-CA
899:).
642:).
638:-CA
580:⇔ ∀
345:as
336:...
319:1..
276:⇒ {
180:)).
160:⇔ ∀
132:⇔ ∀
107:not
2813::
2793:.
2781:.
2734:.
2726:.
2718:.
2704:.
2700:.
2629:.
2602:15
2600:.
2596:.
2569:.
2565:.
2506:^
2491:,
2467:,
2443:,
2431:,
2405:.
2397:.
2387:48
2385:.
2381:.
2329:.
2317:49
2315:.
2309:.
2281:.
2273:.
2261:16
2259:.
2237:,
2227:,
2215:,
2124:.
2120:.
2057:.
1692:vd
1685:vd
1683:'(
1641:.
1485:,p
1419:φ(
1370:φ(
1175:01
1171:⇒
1152:.
1073:.
741:Φ(
686:.
675:.
623:.
462:∧
454:⇒
452:tj
448:si
428:")
416:1≠
412:∧
408:0≠
404:(
352:1
280:01
254:01
250:⇒
227:).
195:→2
187:→2
156:=
128:=
113:→0
103:st
72:.
2803:.
2789::
2766:.
2742:.
2722::
2712::
2662:.
2656::
2637:.
2633::
2623::
2581:.
2577::
2558:2
2528:.
2522::
2495::
2471::
2439::
2413:.
2393::
2376:"
2374:2
2359:.
2337:.
2323::
2289:.
2277::
2267::
2223::
2197:.
2193::
2153:.
2149::
2128:.
2094:k
2090:k
2086:k
2082:k
2078:k
2074:Q
2070:Q
2055:M
2051:T
2047:N
2042:s
2038:v
2034:N
2029:s
2025:v
2021:f
2017:s
2015:(
2013:f
2008:s
2004:N
1999:s
1995:v
1991:s
1986:s
1982:N
1978:M
1974:M
1972:∈
1970:s
1966:T
1961:s
1957:N
1953:T
1949:T
1945:M
1941:T
1937:M
1933:T
1929:T
1925:N
1921:M
1917:N
1915:→
1913:M
1911::
1909:f
1905:N
1901:M
1895:s
1891:N
1886:r
1881:s
1877:N
1872:s
1870:(
1868:f
1864:s
1860:N
1858:∈
1856:r
1854:∃
1852:s
1848:f
1833:R
1822:N
1818:N
1814:M
1812:∈
1810:s
1806:M
1802:N
1800:→
1798:M
1794:M
1786:N
1782:M
1778:M
1774:N
1770:M
1756:M
1752:M
1748:M
1744:v
1740:M
1738:∈
1735:j
1731:d
1726:i
1722:P
1718:k
1715:d
1711:1
1708:d
1706:(
1703:i
1699:P
1695:k
1688:1
1680:i
1676:P
1671:i
1667:P
1663:M
1659:M
1654:M
1635:2
1631:1
1627:s
1623:s
1619:s
1615:s
1600:G
1586:M
1578:M
1574:s
1572:→
1570:s
1555:k
1551:k
1547:k
1543:k
1539:k
1535:k
1530:k
1526:k
1522:k
1517:2
1499:S
1495:S
1487:1
1483:0
1479:1
1475:0
1471:1
1468:p
1466:,
1464:0
1461:p
1429:S
1425:S
1421:S
1417:S
1413:′
1410:S
1406:k
1402:S
1398:k
1394:′
1391:S
1387:S
1383:′
1380:S
1376:k
1372:S
1368:S
1362:′
1359:s
1355:′
1352:s
1348:s
1344:s
1335:S
1331:S
1310:1
1306:0
1302:0
1298:2
1294:k
1290:k
1286:0
1282:2
1278:3
1274:0
1267:1
1263:1
1259:β
1255:α
1251:α
1247:r
1239:s
1224:Q
1213:s
1209:s
1203:2
1199:0
1195:2
1191:t
1187:′
1184:t
1180:′
1177:t
1173:s
1169:t
1167:,
1165:s
1161:s
1150:0
1146:2
1142:3
1138:S
1126:T
1122:)
1116:S
1112:T
1106:S
1104:(
1102:2
1098:T
1094:.
1092:S
1088:T
1082:T
1078:S
1071:0
1067:2
1063:3
1059:0
1055:2
1043:L
1037:k
1034:α
1031:L
1027:1
1025:Σ
1020:1
1018:Σ
1014:S
1012:(
1009:1
1007:α
1004:L
1000:k
995:1
991:S
987:k
983:0
979:2
975:3
971:0
963:1
956:t
954:∀
952:S
948:t
946:∃
944:s
942:∀
940:S
936:t
934:∀
932:s
930:∃
928:T
926:∀
924:S
920:2
908:2
904:1
885:2
880:)
876:|
868:|
864:(
861:O
857:2
853:+
850:)
847:k
843:|
839:T
835:|
831:(
828:O
814:T
809:k
805:S
801:1
798:S
794:T
790:k
785:k
781:S
777:1
774:S
751:X
747:X
743:X
739:X
721:2
717:2
702:R
680:1
660:k
658:≤
652:k
640:0
636:2
632:3
628:3
613:S
609:S
598:s
596:(
594:T
590:s
588:(
586:S
584:(
582:s
578:T
576:=
574:S
559:S
555:s
551:s
549:(
547:S
545:(
543:s
541:∀
539:S
535:)
529:S
526:s
522:s
520:(
518:S
514:s
512:(
510:S
506:s
504:(
502:S
500:(
498:s
494:S
492:(
490:S
484:j
482:=
480:i
476:j
472:i
468:j
466:=
464:i
460:t
458:=
456:s
450:=
444:j
440:i
438:∀
436:t
434:,
432:s
426:s
422:s
418:s
414:t
410:s
406:t
402:t
400:∀
398:s
381:O
379:+
377:k
373:k
369:m
365:m
361:i
357:2
354:i
350:1
347:i
342:m
338:i
334:2
331:i
328:1
325:i
321:m
316:1
285:′
282:t
278:s
274:s
270:t
266:′
263:t
259:′
256:t
252:s
248:t
246:,
244:s
240:k
236:k
232:k
221:O
214:2
206:.
197:n
193:n
189:n
185:n
178:s
176:(
174:T
170:s
168:(
166:S
164:(
162:s
158:T
154:S
150:t
148:(
146:S
142:s
140:(
138:S
136:(
134:S
130:t
126:s
115:s
111:s
99:t
95:s
88:k
84:k
70:S
66:s
62:s
60:(
58:S
54:S
52:∈
50:s
46:s
44:→
42:s
38:s
36:→
34:s
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.