PaperlayerView exact revision on arXiv

Source-linked AI summary

Twin-width IV: ordered graphs and matrices

Édouard Bonnet, Ugo Giocanti, Patrice Ossona de Mendez, Pierre Simon, Stéphan Thomassé, Szymon Toruńczyk

arXiv:2102.03117v3math.COcs.CCcs.DMcs.DScs.LO

TL;DR

For hereditary ordered binary structures, the paper seeks characterizations of bounded twin-width and an efficient way to obtain the witnesses used in model checking. It establishes a dichotomy linking twin-width to structural, growth, and logical properties, and gives a polynomial-time witness algorithm for ordered graphs of bounded twin-width.

  • Problem

    For bounded-twin-width classes, it was unknown whether a low-twin-width witness could be computed efficiently for every such class.

    Source: §1 · p. 2

  • Method

    The paper proves multiple equivalent characterizations of bounded twin-width for hereditary ordered graphs and computes bounded-twin-width witnesses in polynomial time.

    Source: §1 · p. 2

  • Results

    Hereditary ordered graph classes either have bounded twin-width, bounded grid rank, growth 2^O(n), and FPT first-order model checking, or have unbounded twin-width, contain specified obstruction classes, and have growth at least P⌊n/2⌋.

    Source: §1 · p. 4

  • Takeaways & Limitations

    For ordered graph classes of bounded twin-width, polynomial-time witness computation yields fixed-parameter tractable first-order model checking.

    Source: §1 · p. 2

    The converse between bounded twin-width and fixed-parameter tractability is established under common complexity-theoretic assumptions.

    Source: §1 · p. 2

Abstract

from arXiv · show

We establish a list of characterizations of bounded twin-width for hereditary, totally ordered binary structures. This has several consequences. First, it allows us to show that a (hereditary) class of matrices over a finite alphabet either contains at least $n!$ matrices of size $n \times n$, or at most $c^n$ for some constant $c$. This generalizes the celebrated Stanley-Wilf conjecture/Marcus-Tardos theorem from permutation classes to any matrix class over a finite alphabet, answers our small conjecture [SODA '21] in the case of ordered graphs, and with more work, settles a question first asked by Balogh, Bollob\'as, and Morris [Eur. J. Comb. '06] on the growth of hereditary classes of ordered graphs. Second, it gives a fixed-parameter approximation algorithm for twin-width on ordered graphs. Third, it yields a full classification of fixed-parameter tractable first-order model checking on hereditary classes of ordered binary structures. Fourth, it provides a model-theoretic characterization of classes with bounded twin-width.

1 Introduction

The section characterizes bounded twin-width in hereditary ordered graph classes through structural, enumerative, logical, and algorithmic conditions, and presents related results for matrix classes and ordered binary structures. It also addresses growth dichotomies, FO model-checking tractability under FPT≠AW[∗], an FPT approximation algorithm, and model-theoretic consequences.

1 Introduction

  • For C, bounded twin-width, bounded grid rank, growth 2O(n), failure to transduce all graphs, and FPT FO model checking are listed as equivalent conditions.Source: §1 · p. 4
  • For hereditary matrix classes over finite alphabets, growth is at most c^n or at least n!, with six specified matrix classes serving as obstructions in the 0,1 case.The six classes are indexed by equality, inequality, or one-sided row or column propagation; each is an inclusion-minimal superexponential-growth class, and every superexponential 0,1-matrix class contains one.Source: §1 · pp. 4–5
  • A fixed-parameter algorithm given an ordered binary structure of twin-width k outputs a witness of twin-width at most 2^O(k^4).This is an approximation algorithm for totally ordered binary structures.Source: §1 · p. 4
  • For arbitrary structure classes, not transducing all graphs, monadic NIP, not defining large grids, and 1-dimensionality are equivalent and imply being restrained; for hereditary ordered binary classes, all five conditions are equivalent to bounded twin-width.The implication from 1-dimensionality to restrained classes is the paper’s contribution; the equivalence for ordered binary structures is also established here.Source: §1 · pp. 4–5
  • The results identify precisely 25 Stanley-Wilf classes of ordered graphs and settle the ordered-graph growth gap with the optimal lower bound floor(n/2)!.They also resolve the small-class conjecture for ordered graphs: bounded twin-width is equivalent to having growth 2^O(n).Source: §1 · pp. 5–6

Ramsey theory.

  • For every ordered matching H, some cubic graph has the property that every vertex ordering induces an ordered graph containing H as an induced subgraph.The argument uses the ordered-graph characterization to show that the class of ordered subcubic graphs avoiding H cannot have bounded twin-width.Source: Ramsey theory · p. 6
  • Theorem 3 gives a grid theorem: classes that are not restrained define arbitrarily large grids, and hereditary classes of ordered graphs with unbounded twin-width interpret all graphs.For ordered graphs, not transducing all graphs characterizes bounded twin-width; for unordered graph classes, bounded twin-width is equivalent to arising by forgetting the order of a monadically NIP ordered-graph class.Source: Ramsey theory · pp. 6–7
  • Assuming FPT≠AW[∗], hereditary ordered graph classes have FPT FO model checking exactly when they have bounded twin-width; unbounded twin-width is AW[∗]-hard.The bounded-twin-width FPT algorithm and the unbounded-twin-width hardness result are both new; twin-width is the tractability dividing line for ordered graphs.Source: Ramsey theory · p. 7
  • Theorem 2 gives an FPT algorithm that either certifies twin-width at least k or produces a witness bounded by a computable function of k.This removes the requirement in [8] that a bounded-twin-width witness be supplied for ordered graphs.Source: Ramsey theory · p. 7
  • Theorem 3 implies that graph classes of bounded twin-width, even without an order, and transductions of nowhere dense classes are restrained.The authors suggest the result may apply beyond ordered binary structures; it generalizes bounded-grid results for ordered graphs of bounded twin-width.Source: Ramsey theory · pp. 7–8
  • An alternative proof of Theorem 1 can be derived from Theorem 3, illustrating a connection between model-theoretic methods and algorithmic and structural graph theory.The alternative proof is described in unpublished report [40]; the paper's own proof is purely combinatorial.Source: Ramsey theory · p. 8
  • The ordered conjecture holds for every subclass of a hereditary dependent class of finite ordered binary structures.This follows because the ordered conjecture holds on every class with FPT FO model checking [12, Cor. III.2], and Theorem 1 establishes that condition for these subclasses.Source: Ramsey theory · p. 8

2 Roadmap

The roadmap characterizes bounded twin-width through matrix conditions and structural obstructions, then traces how these links yield growth bounds, algorithms, and model-checking results.

2 Roadmap

  • Bounded twin-width, bounded grid rank, excluding six permutation-derived classes, and several interpretation, growth, and model-checking conditions are equivalent for matrix classes.The growth alternatives are at least n! or at most 2^O(n); the FO model-checking implication assumes FPT≠AW[*].Source: §2 · p. 8
  • For hereditary ordered binary structures, bounded twin-width, small subfactorial growth, and tractability of FO model checking are equivalent.The paper also connects bounded twin-width with other characterizations across combinatorics, logic, and graph theory.Source: §2 · pp. 8–9
  • The fixed-parameter algorithm either returns a 2^O(k^4)-sequence certifying tww(G)=2^O(k^4), or a 2k(k+1)-rich division certifying tww(G)>k.The input is an ordered binary structure encoded by a matrix, together with parameter k.Source: §2 · p. 9
  • The natural order can give a checkerboard matrix with large bad divisions, while rank-k divisions characterize bounded twin-width without requiring reordering.The checkerboard example has no rank-k division for k=3; reordering its vertices so odds precede evens makes every 4-division contain a constant zone.Source: §2 · p. 9, Figure 5 · p. 10
  • A greedy search for a bounded-twin-width witness can be stopped only by a large rich division, and large rich divisions contain large rank divisions.The proof then uses Ramsey-like arguments to find structured submatrices encoding universal permutations, ultimately obtaining one of six permutation encodings.Source: §2 · p. 10
  • Classes of unbounded grid rank contain one of six permutation-derived classes and therefore have growth at least n!, while bounded-twin-width matrix classes have growth 2^O(n).The six classes interpret all graphs and have AW[*]-hard model checking.Source: §2 · p. 10
  • Translating permutation encodings to ordered graphs refines their growth gap and shows the obstruction classes prevent NIP; unbounded twin-width also precludes FPT FO model checking.The final model-theoretic characterization uses methods including an analogue of forking independence for monadically NIP classes.Source: §2 · p. 10

3 Preliminaries

This section establishes the representations and terminology for ordered graphs, matrices, permutations, and binary structures, and introduces twin-width, divisions, and concepts used to discuss growth, tractability, and interpretation. It also develops interpretations and transductions for ordered binary structures, including constraints from bounded twin-width, a reduction for first-order model checking on adjacency matrices, and the role of ordered matchings in interpreting graphs.

3.1 Graphs, orders, matrices, permutations

  • Matrices are identified up to order-preserving isomorphism and classes are submatrix-closed; permutations have multiple ordered-graph and matrix representations used in the theory.The paper previews five further matrix classes and twenty-three further ordered-graph classes that represent permutations.Source: §3.1 · pp. 11–13

3.2 Structures

  • An ordered binary structure has unary and binary relations including a total order, while a matrix is encoded using row, column, order, and entry relations.Each alphabet symbol gets a binary relation linking a row to a column exactly when that symbol is the matrix entry.Source: §3.2 · p. 13

3.3 Twin-width

  • Matrix twin-width is defined through contraction sequences whose row and column partitions have bounded overlap and error; ordered binary structures can be encoded by mixed-symmetric matrices.The matrix twin-width is the minimum k + e for a sequence with k-overlapping partitions and error at most e; the simpler (k, k) condition bounds it within a factor of two.Source: §3.3 · pp. 13–14

3.4 Rank division and rich division

  • Grid rank is the largest k for which a matrix admits a rank-k division, while rich divisions preserve row- and column-vector diversity after controlled removal of parts.A rank-k division requires each zone to have at least k distinct rows or at least k distinct columns; richness imposes corresponding diversity conditions after removing up to k opposite-side parts.Source: §3.4 · p. 14

3.5 Enumerative combinatorics

  • Bounded-twin-width classes of ordered binary structures have growth c^n, and this paper confirms the small-class converse for totally ordered binary structures.For ordered graphs, the paper also previews that bounded twin-width implies tractability and that the converse holds for hereditary classes.Source: §3.5 · p. 15, §3.6 · p. 15

3.6 Computational complexity

  • Bounded-twin-width ordered-graph classes are tractable, and for hereditary ordered-graph classes tractability also implies bounded twin-width.Tractability means FO model checking runs in time f(ℓ)(m + n)^c on n × m matrices, with ℓ the sentence’s quantifier depth.Source: §3.6 · p. 15

3.7 Interpretations and transductions

  • Efficient interpretations compose and give FPT reductions for FO model checking; if a class efficiently interprets all graphs, its model checking is AW[∗]-hard.The reduction translates an input structure and sentence into an equivalent model-checking instance on the interpreting class.Source: §3.7 · p. 16
  • The class of all ordered matchings efficiently interprets the class of all graphs.The paper includes a proof of this folklore result in Appendix A.Source: §3.7 · p. 16
  • A class C transduces D when adding unary relations yields an expansion whose Σ-reduct is C and which interprets D.A reduct forgets relations outside Σ.Source: §3.7 · p. 16
  • A class of ordered binary structures with bounded twin-width cannot transduce the class of all graphs.This is stated for ordered structures because the paper’s twin-width definition applies to them; the result also holds for binary structures without an order.Source: §3.7 · p. 16
  • An interpretation from ordered structures to ordered graphs can use an atomic type τ(x, y), joining u < v exactly when τ(u, v) holds.An atomic type is a maximal satisfiable conjunction of atomic or negated atomic formulas; the resulting graph retains the structure’s domain and order.Source: §3.7 · pp. 16–17
  • First-order model checking on adjacency matrices of a class of ordered binary structures FPT-reduces to model checking on the structures themselves.If model checking for the matrix class is AW[*]-hard, then it is AW[*]-hard for the original class.Source: §3.7 · p. 17

3.8 Model theory

These sections define monadic dependence, pattern-avoiding matrix and ordered-graph classes, and a Ramsey lemma for permutations.

3.8 Model theory

  • Monadic dependence is equivalent to not transducing the class of all finite graphs.The theorem characterizes it through dependence of formulas over every monadic lift.Source: §3.8 · p. 17

3.9 Patterns

  • Pattern avoidance for finite-alphabet matrices requires every letter-selection to avoid the six specified 0,1-matrix pattern classes.The corresponding ordered-graph classes are defined from ordered matchings using permutation-based adjacency rules and within-side edge parameters.Source: §3.9 · p. 18
  • The ordered permutation graph class P is hereditary, closed under edge complements, and has growth n!.The strict-inequality pattern classes coincide with their non-strict counterparts.Source: §3.9 · p. 18

3.10 Ramsey theory

  • For any fixed permutation σ and finite color set, a sufficiently large permutation π contains σ on a subset where the coloring depends only on the two order types.The subset size is the size of σ; the conclusion holds for every coloring of pairs of indices.Source: §3.10 · p. 19

4 Effective equivalence of bounded twin-width and no large rich division

The section establishes an effective equivalence between bounded twin-width and the absence of large rich divisions, and derives an FPT approximation algorithm for matrices over a finite alphabet.

4 Effective equivalence of bounded twin-width and no large rich division

  • A 2k(k + 1)-rich division certifies that tww(M) > k.Conversely, the algorithm either finds such a division or returns a contraction sequence certifying tww(M) = |A|O(k4).Source: §4 · pp. 19–20
  • The algorithm runs in 22O(k2 log k)(n + m)O(1) time and returns either a rich-division certificate or a low-twin-width contraction sequence.The sequence has error value |A|O(k4).Source: §4 · p. 20
  • The greedy algorithm maintains row and column conditions by bounding distinct vectors outside a limited set of exceptional parts.It merges consecutive parts while preserving those conditions; checking them is fixed-parameter tractable.Source: §4 · p. 20
  • If the greedy process stops before a full sequence, its terminal division yields a rich-division certificate; a full sequence instead yields a bounded-error contraction sequence.For the full-sequence case, the construction refines the divisions into overlapping partitions and bounds the resulting sequence's error value.Source: §4 · p. 21
  • If no r-rich division exists, then tww(M) = 2O(r2).With alphabet size treated as constant, this follows because the algorithm's only possible outcome is a contraction sequence.Source: §4 · p. 21

5 Large rich divisions imply large rank divisions

A sufficiently large rich division contains a rank-k division: the proof colors high-rank zones red, uses blue witnesses for other zones, and applies the Marcus-Tardos bound.

5 Large rich divisions imply large rank divisions

  • Every A-matrix with a K-rich division, for K = |A|k mt(k2), has a rank-k division.Here mt is the Marcus-Tardos bound.Source: §5 · p. 22
  • Zones with at least k distinct rows or columns are colored red, while blue zones carry row vectors absent from earlier non-red zones.Each column part has at least mt(k2) colored zones, either directly or through blue witnesses.Source: §5 · p. 22
  • The proof coarsens to a k2 × k2 division with a colored zone in every cell, then groups cells into k × k supercells.Each supercell has rank at least k because it contains a red zone or a diagonal of blue-witness zones.Source: §5 · p. 22

6 Rank Latin divisions

The section converts unbounded grid rank into structured Latin divisions, providing a route from large matrix classes to permutation encodings and superexponential growth.

6 Rank Latin divisions

  • A rank-K division over a finite alphabet yields a rank-k division in some single-letter selection of the matrix.The selection replaces one chosen letter by 1 and every other letter by 0.Source: §6 · pp. 22–23
  • For every k, sufficiently large matrices contain one of eight specified k × k patterns as a submatrix.The patterns include diagonal and anti-diagonal forms, which the proof uses to build rank Latin divisions.Source: §6 · p. 24
  • Every 0,1-matrix with a rank-K division has a submatrix with a rank-k Latin division for a suitable K.A Latin division places a contiguous pattern from Nk in each cell, with the associated row and column sets partitioning those of the submatrix and prescribed cross-intersections.Source: §6 · p. 24
  • A rank-T(κ) division can be coarsened to a submatrix with a rank-κ pre-Latin d-division.The construction selects one pattern submatrix in each cell while ensuring the selected row sets and column sets each partition the submatrix.Source: §6 · p. 25
  • Pairwise extractions from the pre-Latin structure enforce the required cross-intersections and produce a rank-k Latin division.The extraction yields the prescribed 1k or 0k intersections between distinct embedded submatrices.Source: §6 · pp. 24–25
  • Every class M with unbounded grid rank satisfies |M_n| ≥ ⌊n/2⌋!, via a simple injection from n-permutations to 2n × 2n submatrices of any rank-2 Latin n-division.The sharper lower bound n! requires more work.Source: §6 · p. 25

7 Matrix classes with unbounded grid rank

This section characterizes matrix classes with unbounded grid rank or twin-width through structural and growth properties, including factorial growth, unavoidable pattern classes, and a reduction from sixteen pattern classes to six minimal classes. It also shows that unbounded-twin-width matrix classes efficiently interpret all graphs and gives a conditional first-order model-checking obstruction.

7.2 Minimal family of six unavoidable classes

  • A matrix class with unbounded grid rank has an a-selection containing one of six classes Fs, and these six classes are pairwise incomparable under containment.The six choices of s are =, ̸=, ⩽R, ⩾R, ⩽C, and ⩾C.Source: §7 · p. 26, §7.2 · pp. 28–29

7.1 Finding k! distinct k × k matrices when the grid rank is unbounded

  • Every 0,1-matrix class with unbounded grid rank contains at least k! distinct k × k matrices for every k, and contains some pattern class Fη.The pattern class is for one of the sixteen encodings η: {−1, 1} × {−1, 1} → {0, 1}.Source: §7.1 · pp. 26, 28

7.2 Minimal family of six unavoidable classes

  • The six classes Fs are precisely the matrix classes with growth 2^ω(n) for which every proper subclass has growth 2^O(n).Source: §7.2 · p. 30

7.3 Matrix classes of unbounded twin-width are independent

  • Every matrix class over a finite alphabet with unbounded twin-width efficiently interprets all graphs, is independent, and has AW[∗]-hard first-order model checking.Source: §7.3 · p. 30

7.4 Proof of Theorem 5

  • Unbounded twin-width is equivalent to unbounded grid rank, failure of pattern avoidance, and admitting r-rich divisions for every r.The proof links these properties in both directions.Source: §7.4 · p. 31
  • Unbounded twin-width is also equivalent to interpreting or transducing the class of all graphs.The proof establishes the interpretation and transduction implications through the non-pattern-avoiding condition.Source: §7.4 · p. 31
  • Unbounded twin-width is equivalent to matrix-class growth of at least n! and at least 2^ω(n).The proof derives factorial growth from failure of pattern avoidance, then derives the 2^ω(n) bound from factorial growth.Source: §7.4 · p. 31
  • If FPT≠AW[∗], unbounded twin-width is equivalent to first-order model checking not being FPT on the matrix class.The proof obtains the model-checking implication from failure of pattern avoidance under this assumption.Source: §7.4 · p. 31

8 Classes of ordered graphs with unbounded twin-width

This section studies hereditary ordered-graph classes with unbounded twin-width, identifying unavoidable subclasses and deriving structural, growth, and model-checking consequences, including for interpreted ordered-graph classes. It also characterizes hereditary ordered-graph classes at a specified growth threshold and states a dichotomy for hereditary classes of finite ordered binary structures.

8.1 Twenty-five unavoidable classes of ordered graphs

  • Every hereditary ordered-graph class with unbounded twin-width contains at least one of 25 specified classes: P or one of the classes Ms,λ,ρ.These subclasses have growth at least ⌊n/2⌋! for Ms,λ,ρ and n! for P.Source: §8.1 · pp. 31, 34
  • Every ordered-graph class with unbounded twin-width efficiently interprets all graphs, making FO model checking AW[∗]-hard and the class independent.The proof reduces this to the efficient interpretation of ordered matchings by the unavoidable subclasses.Source: §8.1 · pp. 32, 34

8.2 Lowerbounding the growth of Ms,λ,ρ

  • For every s, λ, and ρ, the growth of Ms,λ,ρ meets the conjectured Balogh–Bollobás–Morris lower bound for hereditary ordered-graph classes with superexponential growth.The passage states that equality holds when s is ‘=’ and λ = ρ = 0.Source: §8.2 · p. 34

8.3 Proof of Theorem 1

  • If a hereditary class of finite ordered binary structures has bounded twin-width, it also has bounded grid rank, growth 2^O(n), does not transduce all graphs, and has FPT FO model checking.The theorem presents these as equivalent conditions.Source: §8.3 · p. 36
  • If such a class has unbounded twin-width, it interprets all graphs and has growth at least ⌊n/2⌋!, while FO model checking is AW[∗]-hard.Some atomic-type interpretation of the class contains P or one of the 24 classes Ms,λ,ρ.Source: §8.3 · p. 36
  • The interpreted ordered-graph class Iτ(C) has unbounded twin-width and contains one of the 25 classes P or M_{s,λ,ρ}.Source: §8.3 · p. 36
  • Iτ(C), and therefore C, has growth at least P⌊n/2⌋ k!, while Iτ(C) interprets the class of all graphs.Source: §8.3 · p. 36

8.4 Minimality

  • None of the classes P and M_{s,λ,ρ} is included in another.Source: §8.4 · p. 36
  • The 25 classes P and M_{s,λ,ρ} are precisely the hereditary ordered-graph classes with growth 2^ω(n) whose every proper subclass has growth 2^O(n).Source: §8.4 · p. 37

9 Model-theoretic characterizations

This section develops model-theoretic characterizations of bounded twin-width, extending several implications to arbitrary structure classes and giving equivalent conditions for hereditary classes of finite ordered binary structures. It also completes an inductive step whose resulting tuples show that M is not 1-dimensional.

9 Model-theoretic characterizations

  • Restrained classes of finite ordered binary structures have bounded twin-width.The definition of restraint bounds the number of distinct Δ-types between some pair of definable disjoint sets in sufficiently large definable disjoint families.Source: §9 · pp. 37–38
  • For arbitrary structure classes over a fixed signature, not transducing all graphs, monadic dependence, not defining large grids, and 1-dimensionality are equivalent, and each implies restraint.The paper’s contribution to this chain is the implication from 1-dimensionality to restraint.Source: §9 · p. 39
  • For hereditary classes of finite ordered binary structures, seven conditions are equivalent, including not defining large grids, being restrained, having bounded twin-width, and being dependent.The first six conditions are equivalent for arbitrary classes over a fixed signature; there, the result also establishes that not transducing all graphs, monadic dependence, not defining large grids, and 1-dimensionality are equivalent, each implying restraint.Source: §9 · p. 39

9.1 1-dimensionality

  • A model is 1-dimensional when independence of tuples over it is preserved after adjoining a single element to either tuple; models that do not define large grids are 1-dimensional.A class is 1-dimensional when every model in its elementary closure has this property.Source: §9.1 · pp. 40–41

9.2 Proof of Theorem 54

  • The proof that 1-dimensionality implies restraint argues contrapositively: failure of restraint yields witnesses that contradict 1-dimensionality.The witnesses include sets with infinitely many θ-types and lead to tuples that are not independent over the base model.Source: §9.2 · pp. 41–42
  • The proof excludes the second possibility using Claim 66, completing the inductive step and proving Claim 67.Source: §9.2 · p. 42
  • Claim 65 supplies tuples a and b that are not independent over M; Claim 67 then implies M is not 1-dimensional, finishing Theorem 54.Source: §9.2 · p. 42

A Ordered matchings interpret all graphs

The section constructs an ordered matching from an ordered graph and shows that the graph can be reconstructed from that matching by interpretation. The construction is polynomial-time, so ordered matchings efficiently interpret all graphs.

A Ordered matchings interpret all graphs

  • Ordered matchings efficiently interpret all graphs by encoding each graph as a matching and reconstructing it through a simple interpretation.The matching corresponding to an ordered graph is constructed in polynomial time.Source: A Ordered matchings interpret all graphs · p. 43
  • The construction orders graph vertices and auxiliary vertices on the matching’s left and right sides, then matches designated vertex and auxiliary pairs.The passage describes the vertex ordering and matching pairs, though some construction details are split across fragments.Source: A Ordered matchings interpret all graphs · p. 43
  • A graph’s vertices are recovered as matching vertices preceding the definable marker x, in their matching order.The interpretation defines x from x′, then selects the vertices smaller than x.Source: A Ordered matchings interpret all graphs · p. 43
  • Adjacency is recovered by a definable condition involving edge markers and their associated incidence markers.The interpretation tests for an edge marker adjacent to one incidence marker, with an order condition on another incidence marker.Source: A Ordered matchings interpret all graphs · p. 43

B Reducing the model checking problem for matrices to structures

The section reduces first-order model checking on adjacency matrices to model checking on the underlying ordered binary structures. It translates each matrix sentence into a structure sentence that preserves truth.

B Reducing the model checking problem for matrices to structures

  • There is an FPT reduction from FO model checking on adjacency matrices to FO model checking on the underlying ordered binary structures.The lemma applies to adjacency matrices of structures in the class.Source: B Reducing the model checking problem… · p. 44
  • The translation rewrites matrix atoms using the structure’s binary relations and the row-or-column types of their variables.It replaces row and column predicates by true, cross-sort equality by false, and relation atoms by the corresponding structure relation when variables have different sorts.Source: B Reducing the model checking problem… · p. 44
  • A matrix satisfies the original sentence exactly when its underlying structure satisfies the translated sentence.This equivalence establishes the reduction.Source: B Reducing the model checking problem… · p. 44

C.1 Basic notions from model theory

This appendix reviews basic model-theoretic notions used in the paper. It explains how compactness yields larger models and elementary extensions, and how types and parameters are defined.

C.1 Basic notions from model theory

  • A theory is a set of sentences over a signature, and a model satisfies the theory when it satisfies every sentence in that set.A theory has a model if some model satisfies all its sentences.Source: §C.1 · p. 44
  • Compactness says that a theory has a model whenever every finite subset has a model.The appendix also applies compactness to obtain models of arbitrarily large cardinality from classes with arbitrarily large finite structures.Source: §C.1 · p. 44
  • An elementary extension preserves the truth of every formula on tuples from the original model.The text describes constructing such extensions using the elementary diagram, and identifies models of that diagram with elementary extensions.Source: §C.1 · pp. 44–45
  • Compactness extends a model with an infinite definable equivalence relation to one with at least any specified finite number of equivalence classes.The proof adds constants required to be pairwise inequivalent and uses the elementary diagram to preserve the original model.Source: §C.1 · p. 45
  • Parameters are named elements of a model, while a type over those parameters is a set of formulas in specified variables.A complete type is satisfiable and decides each formula or its negation; a type is satisfiable when each finite conjunction is realizable in the model.Source: §C.1 · pp. 45–46

C.2 Finite satisfiability

Finite satisfiability in A can be represented using filters and average types. This representation yields complete extensions for finitely satisfiable partial types.

C.2 Finite satisfiability

  • A type with parameters from M is finitely satisfiable in M exactly when it is satisfiable.Source: §C.2 · p. 46
  • A partial type is finitely satisfiable in A exactly when it is contained in AvF for some filter F on A^x.Source: §C.2 · p. 47
  • A complete type over N is finitely satisfiable in A exactly when it equals AvF for some ultrafilter F on A^x.Source: §C.2 · p. 47
  • Every partial type finitely satisfiable in A extends to a complete type over N that is finitely satisfiable in A.Source: §C.2 · p. 47

C.3 Indiscernible sequences

The section defines indiscernibility and mutual indiscernibility over a parameter set. It shows that sequences built by iterating a finitely satisfiable type are indiscernible over the base.

C.3 Indiscernible sequences

  • A sequence is indiscernible over A when increasing finite subsequences have the same type over A.Source: §C.3 · p. 47
  • Two sequences are mutually indiscernible over A when each remains indiscernible over A together with the other sequence.Source: §C.3 · p. 48
  • If each tuple realizes AvF restricted to B and its predecessors, the resulting sequence is indiscernible over B.The proof establishes equality of types for increasing finite subsequences by induction.Source: §C.3 · p. 48
  • A Morley sequence of a type finitely satisfiable in A over B is indiscernible over B.Source: §C.3 · p. 48

C.4 Building indiscernible sequences

Ramsey’s theorem and compactness provide ways to construct indiscernible sequences, including mutually indiscernible subsequences. The section also represents indiscernible sequences as Morley sequences of average types.

C.4 Building indiscernible sequences

  • Any sequence has a family based on it, indexed by an arbitrary linear order, in an elementary extension.The construction follows from Ramsey’s theorem and compactness.Source: §C.4 · p. 49
  • For finite Δ and m, sufficiently long pairs of sequences of d-tuples contain length-m subsequences that are mutually Δ-indiscernible.Source: §C.4 · p. 49
  • A countable indiscernible sequence can be made a Morley sequence of AvF over a submodel, for an ultrafilter F.The construction uses an elementary extension and an ultrafilter on an extended sequence.Source: §C.4 · p. 49
  • Two mutually indiscernible sequences can each be represented as a Morley sequence of an average type over a submodel and the other sequence.Source: §C.4 · pp. 49–50

D Proof of Lemma 64

The proof turns failure of restraint into indiscernible sequences with pairwise inconsistent definable families and persistently many types between their definable sets. It then extracts one formula witnessing infinitely many such types.

D Proof of Lemma 64

  • Lemma 86 yields two sequences indiscernible over M′, pairwise inconsistent formula families, infinitely many types for each paired definable set, and the stated finite-satisfiability relation.Source: D Proof of Lemma 64 · pp. 50–51
  • Failure of restraint supplies arbitrarily large disjoint definable families whose paired sets realize at least k distinct Δ-types.Source: D Proof of Lemma 64 · p. 50
  • Compactness and finite mutual-indiscernibility extraction produce sequences whose definable families remain pairwise disjoint while every paired set has arbitrarily many Δ-types.Source: D Proof of Lemma 64 · pp. 50–51
  • Because Δ is finite, some θ in Δ has infinitely many types between the selected definable sets.Source: D Proof of Lemma 64 · p. 51

Related papers

Loading 2102.03117v3…