Order-invariant queries

Definitions and mathematical statement

Shared notation.

$\mathbb N=\{1,2,\ldots\}$, and $\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$ denote the integers, rationals, reals and complex numbers. Any other conventions are specified locally.

Work with finite graphs carrying a fixed finite vocabulary of unary vertex-colour predicates. First-order logic (FO) quantifies over vertices; monadic second-order logic (MSO) also quantifies over vertex subsets. A formula $\varphi$ using an additional linear order $<$ is order-invariant if its truth, including for each assignment to free variables, is independent of the chosen vertex order. Write $\operatorname{InvFO}(<)$ for the resulting queries on unordered graphs. Expressive-power equality or inclusion means equivalence to a formula of the other logic on the specified graph class. A tree decomposition consists of vertex bags on a tree, covering edges and satisfying connectedness of the bags containing each vertex; tree-width is the least maximum bag size minus one.

A query is Gaifman-local if a fixed-radius induced neighborhood of its parameter tuple determines its value within a fixed structure. It is Hanf-local if, for some fixed radius, agreement of the counts of rooted neighborhood isomorphism types (with the parameters distinguished) forces agreement of the query value. A $0$--$1$ law means that each sentence has limiting probability zero or one in the usual uniform random labeled finite-structure model. Effective syntax means a computably recognizable collection of formulas with effective finite-structure semantics.

For addition-invariant FO, label the vertices bijectively by an initial segment of the positive integers and add the induced ternary relation $x+y=z$; require answers to be independent of that bijection. On words, the underlying word order and letter predicates remain part of the input, while the extra numerical labeling is arbitrary. A regular word language is one accepted by a finite automaton.

Statement recorded in the supplied source.

The source asks all of the following. (1) For every fixed tree-width bound $b$, does $\operatorname{InvFO}(<)=\mathrm{FO}$ hold on graphs of tree-width at most $b$? (2) Is $\operatorname{InvFO}(<)\subseteq\mathrm{MSO}$ on all finite graphs? (3) Does order-invariant FO have a $0$--$1$ law? (4) Is every order-invariant FO query Hanf-local? (5) Is there a logic with effective syntax capturing exactly order-invariant FO? Its additional questions are (6) is addition-invariant FO Gaifman-local, and (7) can addition-invariant FO define a nonregular language of finite words? [S2]

Short English statement

The seven questions concern whether order-invariant first-order logic collapses on bounded-tree-width graphs, lies in monadic second-order logic, has a zero-one law or locality, and admits effective syntax, together with locality and word-language expressiveness for addition-invariant logic.

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 3338 (OPG-37429). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Open Problem Garden, Order-invariant queries, node 37429, original problem page. Original question and full discussion. https://www.openproblemgarden.org/op/order_invariant_queries.