Structural Preservation and the Logical Expressiveness of Graph Neural Networks

# Structural Preservation and the Logical Expressiveness of Graph Neural Networks
Source: [https://arxiv.org/html/2606.17882](https://arxiv.org/html/2606.17882)
\\declaretheorem

\[name=Theorem\]thm

Przemysław Andrzej Wałęga Queen Mary University of London p\.walega@qmul\.ac\.uk &Bernardo Cuenca Grau University of Oxford bernardo\.grau@cs\.ox\.ac\.uk

###### Abstract

Bridges between graph neural networks \(GNNs\) and logical formalisms have been established by fixing architectural choices, such as the types of aggregation, combination, and activation functions\. These choices define restricted classes of GNNs for which tight correspondences with logical formalisms can be obtained, by showing that logical formulae can be translated into equivalent GNNs and, conversely, that GNNs can be translated into equivalent formulae\.

In this paper we take a semantic perspective by establishing the logical expressiveness of classes of GNN classifiers that are preserved under structural properties: embeddings \(extensions\), injective homomorphisms, and homomorphisms\. We show that, for each such property, there exists a fragment of graded modal logic characterising the class of GNNs\. In particular, preservation under embeddings, injective homomorphisms, and homomorphisms corresponds to existential graded modal logic, its existential\-positive fragment, and existential\-positive modal logic, respectively\. These results characterise the expressiveness of broad classes of GNNs independently of specific architectural choices, but we also show that each of these classes admits a GNN architecture of the same expressiveness\.

Technically, our approach uses a new well\-quasi\-order result for trees of bounded height, yielding finite representations of unravelling\-invariant classes\.

## 1Introduction

Graph neural networks \(GNNs\)Gilmeret al\.\([2017](https://arxiv.org/html/2606.17882#bib.bib23)\)are models designed to operate directly on graphs of variable size while ensuring that model predictions are invariant under graph isomorphisms\. In the aggregate\-combine paradigm, each node maintains a vector representation that is iteratively updated by aggregating information from its neighbours\. This design induces a strong structural bias: GNNs withLLlayers are invariant under isomorphisms and inherently local, in the sense that node representations depend only on the node’sLL\-hop neighbourhood\. These two properties bring GNNs close to logical formalisms, in particular modal logics, which are also local and isomorphism\-invariantBarcelóet al\.\([2020](https://arxiv.org/html/2606.17882#bib.bib48)\); Hauke and Wałęga \([2026](https://arxiv.org/html/2606.17882#bib.bib10)\); Cuenca Grauet al\.\([2026](https://arxiv.org/html/2606.17882#bib.bib24)\)\. Establishing such connections is beneficial, as logic provides principled tools for analysing expressiveness and enabling symbolic methods for verification and explanation\.

These connections have been studied extensively\. In particular, bridges between GNNs and logic have been established by fixing architectural choices, such as aggregation, combination, and activation functions\. These choices define restricted families of GNN classifiers for which precise correspondences with logical formalisms can be obtained\. In particular, prior work has identified such families corresponding to extensions of first\-order logic with counting termsGrohe \([2024](https://arxiv.org/html/2606.17882#bib.bib36)\); Nunnet al\.\([2024](https://arxiv.org/html/2606.17882#bib.bib42)\)and Presburger quantifiersBenediktet al\.\([2024](https://arxiv.org/html/2606.17882#bib.bib55)\), as well as to rule\-based knowledge representation formalisms such as DatalogTena Cucalaet al\.\([2025](https://arxiv.org/html/2606.17882#bib.bib21),[2023](https://arxiv.org/html/2606.17882#bib.bib26)\)\.

In this paper, we complement such architecture\-driven characterisations with a semantic framework based on structural properties that impose strictly stronger constraints on classifiers than invariance under graph isomorphisms, namely preservation under embeddings, injective homomorphisms, and homomorphisms\. We show that for each such property, the corresponding class of GNN classifiers has the same expressiveness as a fragment of graded modal logic \([Section˜4\.5](https://arxiv.org/html/2606.17882#S4.SS5),[Section˜4\.5](https://arxiv.org/html/2606.17882#S4.SS5)\):

- •The class of GNN classifiers preserved underembeddingshas the same expressiveness as existential graded modal logic∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\},
- •The class of GNN classifiers preserved underinjective homomorphismshas the same expressiveness as existential\-positive graded modal logic∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}, and
- •The class of GNN classifiers preserved underhomomorphismshas the same expressiveness as existential\-positive modal logic∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\.

Our approach is inspired by finite model theory, where preservation theorems relate structural properties to logical definabilityLibkin \([2004](https://arxiv.org/html/2606.17882#bib.bib52)\); Rosen \([2002](https://arxiv.org/html/2606.17882#bib.bib17)\); Grädelet al\.\([2007](https://arxiv.org/html/2606.17882#bib.bib51)\); Rosen \([1997](https://arxiv.org/html/2606.17882#bib.bib18)\); Abramsky and Reggio \([2024](https://arxiv.org/html/2606.17882#bib.bib14)\)\. Classical results include the van Benthem–Rosen theoremRosen \([1997](https://arxiv.org/html/2606.17882#bib.bib18)\), which characterises modal logic as the bisimulation\-invariant fragment of first\-order logic, and Rossman’s theoremRossman \([2008](https://arxiv.org/html/2606.17882#bib.bib20)\), which characterises existential\-positive first\-order logic as the fragment preserved under homomorphisms\. We adapt this methodology to the setting of GNNs\. Since existing preservation theorems do not directly apply in this setting, we develop new results tailored to graph structures induced by GNN computations\.

The key intuition underlying our approach is that, in addition to being invariant under isomorphisms, GNNs are inherently local: in a GNN withLLlayers, the representation of a node depends only on itsLL\-hop neighbourhoodBarcelóet al\.\([2020](https://arxiv.org/html/2606.17882#bib.bib48)\); Wang and Zhang \([2022](https://arxiv.org/html/2606.17882#bib.bib28)\); Morriset al\.\([2019b](https://arxiv.org/html/2606.17882#bib.bib58)\)\. This locality allows us to reduce the analysis of GNNs to trees obtained via unravellingBarcelóet al\.\([2020](https://arxiv.org/html/2606.17882#bib.bib48)\)\. Combined with preservation under structural relations, it yields the logical characterisations stated above\.

The main technical challenge is to obtain a finite representation of such classes\. To address this, we show a new result on well\-quasi\-orders \([Section˜4\.4](https://arxiv.org/html/2606.17882#S4.SS4)\) which is of independent interest:

- •Every class of trees of bounded height iswell\-quasi\-orderedby the embedding relation\.

SinceLL\-unravellings have bounded height and well\-quasi\-orders admit only finitely many minimal elements, this yields a finite representation of each class via its minimal trees\. At a high level, each minimal tree can be characterised by a logical formula, and the entire class is defined by a finite disjunction of such formulae\. The fragment of modal logic is determined by the preservation relation\.

In addition to the semantic characterisations, we show that each class of GNN classifiers defined via preservation properties can be captured by a specific architecture\. In particular \([Section˜5](https://arxiv.org/html/2606.17882#S5)\):

- •GNNs preserved underinjective homomorphismshave the same expressiveness as monotonic GNNs \(i\.e\., GNNs with non\-decreasing aggregation and combination functions\),
- •GNNs preserved underhomomorphismshave the same expressiveness as monotonic GNNs usingMAX\\mathrm\{MAX\}as aggregation,
- •GNNs preserved underembeddingshave the same expressiveness as monotonic GNNs with an additional layer that transforms node features independently of their neighbours\.

Moreover, our results reveal an interesting property of GNN architectures considered in prior work, which we refer to as positive\-weight GNNs, whose parameter matrices have non\-negative entries\. In particular, it follows that any GNN preserved under injective homomorphisms \(and so, also any monotonic GNN\) can be transformed into an equivalent positive\-weight GNN\. Thus, with respect to expressiveness, the syntactic restriction to non\-negative weights is not restrictive within this class\.

In summary, our contributions are as follows\. We develop a framework for analysing the expressiveness of GNNs based on structural preservation properties\. We establish preservation theorems linking these properties to definability in fragments of graded modal logic, supported by new well\-quasi\-ordering results ensuring finite representations\. Finally, we provide architectural characterisations of the GNN classes defined by preservation properties\.

## 2Related Work

The expressiveness of GNNs has been studied from several perspectives\. Their*discriminative power*measures their ability to distinguish graphs, and it is well known that message\-passing GNNs are bounded by the Weisfeiler–Lehman \(WL\) graph isomorphism test\. Thus, they cannot distinguish graphs that WL fails to separateMorriset al\.\([2019a](https://arxiv.org/html/2606.17882#bib.bib35)\); Xuet al\.\([2019](https://arxiv.org/html/2606.17882#bib.bib37)\)\. Work on the logical expressiveness of GNNs treats them as node classifiers that compute unary queries over graphs and establishes correspondences between GNN architectures and logical formalisms\. In particular, GNN expressiveness is not captured by first\-order logic alone and requires extensions with counting terms, Presburger quantifiers, or related mechanismsGrohe \([2024](https://arxiv.org/html/2606.17882#bib.bib36)\); Benediktet al\.\([2024](https://arxiv.org/html/2606.17882#bib.bib55)\); Nunnet al\.\([2024](https://arxiv.org/html/2606.17882#bib.bib42)\)\. Furthermore, connections to graded modal logic and related fragments have been establishedBarcelóet al\.\([2020](https://arxiv.org/html/2606.17882#bib.bib48)\)\. Recent work on bounded GNNs refines these correspondences by relating aggregation schemes with bounded multiplicities to two\-variable fragments of first\-order logicCuenca Grauet al\.\([2026](https://arxiv.org/html/2606.17882#bib.bib24)\)\.

A complementary line of work studies connections between GNNs and rule\-based knowledge representation formalisms motivated by logical reasoning and explainability\. In particular, monotonic GNNs have been introduced to capture rule\-based inference in DatalogTena Cucalaet al\.\([2025](https://arxiv.org/html/2606.17882#bib.bib21),[2023](https://arxiv.org/html/2606.17882#bib.bib26)\); Tena Cucala and Cuenca Grau \([2024](https://arxiv.org/html/2606.17882#bib.bib27)\); Morris and Horrocks \([2025](https://arxiv.org/html/2606.17882#bib.bib11)\); Morriset al\.\([2024](https://arxiv.org/html/2606.17882#bib.bib13)\)\. These models enforce structural preservation properties, such as preservation under homomorphisms or injective homomorphisms\. These properties are enforced through architectural constraints, including non\-negative weights, monotone activation functions, and restricted aggregation\. While effective in practice, these approaches are inherently syntax\-driven, as the desired preservation properties are enforced indirectly through design choices rather than characterised explicitly in semantic terms\.

Our work is also related to preservation theorems in finite model theory, which characterise logical fragments in terms of structural preservation properties and, in some cases, invariance conditions\. Classical results such as Łoś\-Tarski, Lyndon, and Homomorphism Preservation theorems establish correspondences between fragments of first\-order logic and preservation under embeddings, surjective homomorphisms, and homomorphisms, respectivelyŁoś and Suszko \([1955](https://arxiv.org/html/2606.17882#bib.bib7)\); Lyndon \([1959](https://arxiv.org/html/2606.17882#bib.bib6)\); Hodges \([1997](https://arxiv.org/html/2606.17882#bib.bib12)\)\. While many such results fail over finite structures \(and thus over graphs\), Rossman’s theorem shows that homomorphism preservation continues to hold in the finite settingRossman \([2008](https://arxiv.org/html/2606.17882#bib.bib20)\)\. In modal logic, preservation results are tied to locality and invariance under bisimulation\. Van Benthem’s theorem \(and its finite variant due to Rosen\) characterises bisimulation\-invariant first\-order properties as those definable in modal logicAndrékaet al\.\([1998](https://arxiv.org/html/2606.17882#bib.bib16)\); Rosen \([1997](https://arxiv.org/html/2606.17882#bib.bib18)\)\. More recent work has extended preservation results to graded modal logic and related settingsAbramsky and Reggio \([2024](https://arxiv.org/html/2606.17882#bib.bib14)\)\. Our results on well\-quasi\-orders are related to recent work in a similar directionLopez \([2023](https://arxiv.org/html/2606.17882#bib.bib15)\), however, these techniques rely on additional structural assumptions, such as closure under substructures, that do not hold in our setting\.

## 3Background

#### Graphs and Graph Relations

We consider finite, undirected, simple, node\-labelled graphsG=\(V,E,λ\)G=\(V,E,\\lambda\), whereVVis a finite set of nodes,EEa set of undirected edges without self\-loops, andλ:V→\{0,1\}d\\lambda:V\\to\\\{0,1\\\}^\{d\}assigns to each node a binary vector of fixed dimensiondd\. Intuitively,ddrepresents the number of possible labels \(propositional features\) andλi​\(v\)=1\\lambda\_\{i\}\(v\)=1, for a labeli∈\[d\]i\\in\[d\], indicates that nodevvhas labelii; the set\{1,…,n\}\\\{1,\\dots,n\\\}is represented as\[n\]\[n\]\. We write vectors in bold, e\.g\.,𝐱\\mathbf\{x\},𝐲\\mathbf\{y\},𝐳\\mathbf\{z\}, and usexix\_\{i\}to denote theii\-th component of𝐱\\mathbf\{x\}\. For vectors𝐱,𝐲∈ℝd\\mathbf\{x\},\\mathbf\{y\}\\in\\mathbb\{R\}^\{d\}, we write𝐱≤𝐲\\mathbf\{x\}\\leq\\mathbf\{y\}ifxi≤yix\_\{i\}\\leq y\_\{i\}for alli∈\[d\]i\\in\[d\]\. This discrete labelling enables a direct connection with logical formalismsBarcelóet al\.\([2020](https://arxiv.org/html/2606.17882#bib.bib48)\); Benediktet al\.\([2024](https://arxiv.org/html/2606.17882#bib.bib55)\)\.

A*pointed graph*is a pair\(G,v\)\(G,v\)consisting of a graph and a distinguished node\. A*tree*is a connected acyclic graph\. A*rooted tree*is a pointed graph\(G,v\)\(G,v\)whereGGis a tree andvvis its root\. The*depth*of a nodeuuin a pointed tree is the length of the unique path from the root touu, and the*height*of a treeGGis the maximum depth of any node\.

Let\(G,w\)\(G,w\)and\(H,v\)\(H,v\)be pointed graphs, withG=\(V,E,λ\)G=\(V,E,\\lambda\)andH=\(V′,E′,λ′\)H=\(V^\{\\prime\},E^\{\\prime\},\\lambda^\{\\prime\}\)\. We will consider the following definitions of mappingsf:V→V′f:V\\rightarrow V^\{\\prime\}, withf​\(w\)=vf\(w\)=v\.

- •*Isomorphism:*ffis a bijection,λ​\(u\)=λ′​\(f​\(u\)\)\\lambda\(u\)=\\lambda^\{\\prime\}\(f\(u\)\), and\{u,z\}∈E\\\{u,z\\\}\\in Eiff\{f​\(u\),f​\(z\)\}∈E′\\\{f\(u\),f\(z\)\\\}\\in E^\{\\prime\}\.
- •*Embedding:*ffis an isomorphism from\(G,w\)\(G,w\)onto the subgraph ofHHinduced byf​\(V\)f\(V\)\.
- •*Homomorphism:*ffsatisfiesλ​\(u\)≤λ′​\(f​\(u\)\)\\lambda\(u\)\\leq\\lambda^\{\\prime\}\(f\(u\)\)for allu∈Vu\\in V, and\{u,z\}∈E\\\{u,z\\\}\\in Eimplies\{f​\(u\),f​\(z\)\}∈E′\\\{f\(u\),f\(z\)\\\}\\in E^\{\\prime\}\. Ifffis also injective, we call it an*injective homomorphism*\.

Intuitively, these mappings capture different ways in which one graph can be embedded into another: isomorphisms preserve the entire structure, embeddings preserve a subgraph exactly, while homomorphisms allow labels to be extended and nodes to be merged \(unless the mapping is injective\)\. For examples of these relations see[Figure˜1](https://arxiv.org/html/2606.17882#S3.F1)\. Clearly, every isomorphism is an embedding, every embedding is an injective homomorphism, and every injective homomorphism is a homomorphism\.

\(1,1\)\{\(1,1\)\}\(1,0\)\{\(1,0\)\}\(1,0\)\{\(1,0\)\}\(1,1\)\{\(1,1\)\}\(1,0\)\{\(1,0\)\}\(1,0\)\{\(1,0\)\}\(1,0\)\{\(1,0\)\}\(a\) embedding\(1,1\)\{\(1,1\)\}\(0,0\)\{\(0,0\)\}\(0,0\)\{\(0,0\)\}\(1,1\)\{\(1,1\)\}\(1,0\)\{\(1,0\)\}\(1,0\)\{\(1,0\)\}\(1,0\)\{\(1,0\)\}\(b\) injective homomorphism\(1,1\)\{\(1,1\)\}\(0,0\)\{\(0,0\)\}\(0,0\)\{\(0,0\)\}\(1,1\)\{\(1,1\)\}\(1,0\)\{\(1,0\)\}\(1,0\)\{\(1,0\)\}\(1,0\)\{\(1,0\)\}\(c\) homomorphism

Figure 1:Embedding \(a\), injective homomorphism \(not an embedding\) \(b\), and a homomorphism which is not injective \(c\)Each notion above induces a corresponding binary relation⪯\\preceqon pointed graphs, such that\(G,w\)⪯\(H,v\)\(G,w\)\\preceq\(H,v\)if there exists a mapping of the corresponding type from\(G,w\)\(G,w\)to\(H,v\)\(H,v\)\.

Let𝒞\\mathcal\{C\}be a class of pointed graphs and⪯\\preceqa binary relation as above\. Class𝒞\\mathcal\{C\}is*preserved*under⪯\\preceqif\(G,w\)∈𝒞\(G,w\)\\in\\mathcal\{C\}and\(G,w\)⪯\(H,v\)\(G,w\)\\preceq\(H,v\)implies that\(H,v\)∈𝒞\(H,v\)\\in\\mathcal\{C\}\. Class𝒞\\mathcal\{C\}is*invariant*under⪯\\preceqif𝒞\\mathcal\{C\}is preserved under both⪯\\preceqand its inverse relation⪯−1\\preceq^\{\-1\}\. These preservation properties capture the robustness of classifiers under structural transformations of the input graph\.

#### Graph Neural Networks

We consider node classification with graph neural networks \(GNNs\) based on the standard*aggregate\-combine*paradigmBenediktet al\.\([2024](https://arxiv.org/html/2606.17882#bib.bib55)\); Barcelóet al\.\([2020](https://arxiv.org/html/2606.17882#bib.bib48)\)\. GNNs iteratively update node representations by aggregating information from neighbours and combining it with the current representation\.

Formally, a GNN layer is a pair\(𝖺𝗀𝗀,𝖼𝗈𝗆𝖻\)\(\\mathsf\{agg\},\\mathsf\{comb\}\), where𝖺𝗀𝗀\\mathsf\{agg\}is an*aggregation function*mapping multisets of vectors into vectors and𝖼𝗈𝗆𝖻\\mathsf\{comb\}is a*combination function*mapping pairs of vectors \(or their concatenation\) to vectors\. Applying a layer toG=\(V,E,λ\)G=\(V,E,\\lambda\)produces a graphG′=\(V,E,λ′\)G^\{\\prime\}=\(V,E,\\lambda^\{\\prime\}\)with the same nodes and edges, but with updated node features\.

For each nodev∈Vv\\in V, the updated label is defined by

λ′\(v\)=𝖼𝗈𝗆𝖻\(λ\(v\),𝖺𝗀𝗀\(\{\|λ\(w\)\|\}w∈NG​\(v\)\)\),\\lambda^\{\\prime\}\(v\)=\\mathsf\{comb\}\\Big\(\\lambda\(v\),\\mathsf\{agg\}\(\\mathopen\{\\\{\\mkern\-3\.0mu\|\}\\lambda\(w\)\\mathclose\{\|\\mkern\-3\.0mu\\\}\}\_\{w\\in N\_\{G\}\(v\)\}\)\\Big\),\(1\)whereNG​\(v\)=\{w∣\{v,w\}∈E\}N\_\{G\}\(v\)=\\\{w\\mid\\\{v,w\\\}\\in E\\\}denotes the set of neighbours ofvv, and\{\|⋅\|\}\\mathopen\{\\\{\\mkern\-3\.0mu\|\}\\cdot\\mathclose\{\|\\mkern\-3\.0mu\\\}\}is a multiset\. Aggregation and combination functions have fixed input and output dimensions and must be compatible; if𝖺𝗀𝗀\\mathsf\{agg\}maps vectors of dimensionddto dimensiond′d^\{\\prime\}, then𝖼𝗈𝗆𝖻\\mathsf\{comb\}takes as input the concatenation of vectors of dimensionsddandd′d^\{\\prime\}\.

Often𝖼𝗈𝗆𝖻\\mathsf\{comb\}is a one\-layer MLP with a componentwise activationσ\\sigma\(e\.g\., ReLU or truncated ReLU\):

λ′\(v\)=σ\(𝐛\+λ\(v\)𝐀\+𝖺𝗀𝗀\(\{\|λ\(w\)∣w∈NG\(v\)\|\}\)𝐂\),\\lambda^\{\\prime\}\(v\)=\\sigma\\Big\(\\mathbf\{b\}\+\\lambda\(v\)\\mathbf\{A\}\+\\mathsf\{agg\}\\big\(\\mathopen\{\\\{\\mkern\-3\.0mu\|\}\\lambda\(w\)\\mid w\\in N\_\{G\}\(v\)\\mathclose\{\|\\mkern\-3\.0mu\\\}\}\\big\)\\mathbf\{C\}\\Big\),\(2\)where𝐛\\mathbf\{b\}is a bias vector, and𝐀\\mathbf\{A\}and𝐂\\mathbf\{C\}are real\-valued matrices\. Following previous workBarcelóet al\.\([2020](https://arxiv.org/html/2606.17882#bib.bib48)\), we refer to such layers as*simple*\. Common choices for𝖺𝗀𝗀\\mathsf\{agg\}include position\-wiseSUM\\mathrm\{SUM\},MAX\\mathrm\{MAX\}, andMEAN\\mathrm\{MEAN\}althoughMEAN\\mathrm\{MEAN\}is not monotone with respect to the multiset order used later\. Another aggregation isMAX\\mathrm\{MAX\}\-kk\-SUM\\mathrm\{SUM\}Tena Cucalaet al\.\([2023](https://arxiv.org/html/2606.17882#bib.bib26)\)which sums thekklargest values per component\.

A*GNN classifier*𝒩\\mathcal\{N\}of dimensionddconsists ofLLaggregate\-combine layers followed by a classification function𝖼𝗅𝗌\\mathsf\{cls\}mapping vectors to truth values\. In this paper, we consider only threshold\-based classification functions satisfying𝖼𝗅𝗌​\(x\)=𝗍𝗋𝗎𝖾\\mathsf\{cls\}\(x\)=\\mathsf\{true\}ifx≥tx\\geq tfor some fixed thresholdttand𝖿𝖺𝗅𝗌𝖾\\mathsf\{false\}otherwise\. This restriction is without loss of generality for the expressiveness results proved in this paper\. The output dimension of each layer matches the input dimension of the next\. We writeλ\(ℓ\)​\(v\)\\lambda^\{\(\\ell\)\}\(v\)for the vector associated with nodevvafter applying layerℓ\\ell, withλ\(0\)​\(v\)=λ​\(v\)\\lambda^\{\(0\)\}\(v\)=\\lambda\(v\)andλ\(L\)​\(v\)\\lambda^\{\(L\)\}\(v\)the final representation\. The output of𝒩\\mathcal\{N\}on\(G,v\)\(G,v\)is the truth value𝒩​\(G,v\)=𝖼𝗅𝗌​\(λ\(L\)​\(v\)\)\\mathcal\{N\}\(G,v\)=\\mathsf\{cls\}\\bigl\(\\lambda^\{\(L\)\}\(v\)\\bigr\)\.

#### Logical Expressiveness

A*node classifier*is a function mapping pointed graphs to truth values𝗍𝗋𝗎𝖾\\mathsf\{true\}\(accepted\) or𝖿𝖺𝗅𝗌𝖾\\mathsf\{false\}\(rejected\)\. Two classifiers are*equivalent*if they accept exactly the same pointed graphs\. We compare the expressiveness of families of classifiers arising from GNNs or logical formulae\. We say that two families of classifiers have the same expressiveness if each classifier in one family has an equivalent classifier in the other, and vice versa\.

## 4A Logical Toolkit for Analysing Expressiveness

We introduce logical and combinatorial tools that underpin our analysis\. Our approach is based on relating structural preservation properties to definability in fragments of graded modal logic\.

### 4\.1Locality and Unravelling

GNNs are inherently local: afterLLlayers, a node representation depends only on itsLL\-hop neighbourhood\. This locality can be captured by the notion of*unravelling*, which transforms a pointed graph\(G,v\)\(G,v\)into a rooted tree𝖴𝗇𝗋L​\(G,v\)\\mathsf\{Unr\}^\{L\}\(G,v\)whose nodes correspond to paths inGGstarting atvv, of length at mostLL\. TheLL\-unravelling unfolds all paths of length up toLLinto a tree of height at mostLL\. This construction mirrors the computation of a GNN, where each node aggregates information from its neighbourhood in a tree\-shaped manner\. An example of a pointed graph and its22\-unravelling is shown in[Figure˜2](https://arxiv.org/html/2606.17882#S4.F2)\. Note that the unravelling unfolds cycles into distinct paths, thereby yielding a tree\.

𝐯0\\mathbf\{v\}\_\{0\}𝐯1\\mathbf\{v\}\_\{1\}𝐯2\\mathbf\{v\}\_\{2\}𝐯3\\mathbf\{v\}\_\{3\}\(G,v\)\(G,v\)𝐯0\\mathbf\{v\}\_\{0\}𝐯1\\mathbf\{v\}\_\{1\}𝐯2\\mathbf\{v\}\_\{2\}𝐯3\\mathbf\{v\}\_\{3\}𝐯2\\mathbf\{v\}\_\{2\}𝐯0\\mathbf\{v\}\_\{0\}𝐯0\\mathbf\{v\}\_\{0\}𝐯1\\mathbf\{v\}\_\{1\}𝐯0\\mathbf\{v\}\_\{0\}𝖴𝗇𝗋2​\(G,v\)\\mathsf\{Unr\}^\{2\}\(G,v\)

Figure 2:A pointed graph and its22\-unravellingImportantly, GNNs withLLlayers are invariant under this transformation: evaluating a GNN withLLlayers on a graph yields the same result as evaluating it on itsLL\-unravelling\. This observation will be central to our analysis, as it allows us to reason about GNNs using tree\-shaped structures, and has been exploited in prior work to relate GNNs to logical formalismsBarcelóet al\.\([2020](https://arxiv.org/html/2606.17882#bib.bib48)\)\.

We now give the formal definition of unravelling\.

###### Definition\\thethm\.

Let\(G,v\)\(G,v\)be a pointed graph withG=\(V,E,λ\)G=\(V,E,\\lambda\), and letL∈ℕL\\in\\mathbb\{N\}\. TheLL\-*unravelling*of\(G,v\)\(G,v\), denoted𝖴𝗇𝗋L​\(G,v\)\\mathsf\{Unr\}^\{L\}\(G,v\), is the pointed graph\(\(V′,E′,λ′\),v′\)\(\(V^\{\\prime\},E^\{\\prime\},\\lambda^\{\\prime\}\),v^\{\\prime\}\)defined as follows:

- •V′V^\{\\prime\}contains a node for each sequence\(v,v1,…,vℓ\)\(v,v\_\{1\},\\ldots,v\_\{\\ell\}\)of lengthℓ≤L\\ell\\leq Lsuch that\{vi,vi\+1\}∈E\\\{v\_\{i\},v\_\{i\+1\}\\\}\\in Efor alli<ℓi<\\ell;
- •v′v^\{\\prime\}corresponds to the sequence\(v\)\(v\)of length0;
- •E′E^\{\\prime\}has an edge between\(v,v1,…,vℓ−1\)\(v,v\_\{1\},\\ldots,v\_\{\\ell\-1\}\)and\(v,v1,…,vℓ\)\(v,v\_\{1\},\\ldots,v\_\{\\ell\}\)iff\{vℓ−1,vℓ\}∈E\\\{v\_\{\\ell\-1\},v\_\{\\ell\}\\\}\\in E;
- •λ′\\lambda^\{\\prime\}is defined byλ′​\(\(v,v1,…,vℓ\)\)=λ​\(vℓ\)\\lambda^\{\\prime\}\(\(v,v\_\{1\},\\ldots,v\_\{\\ell\}\)\)=\\lambda\(v\_\{\\ell\}\)\.

Thus,𝖴𝗇𝗋L​\(G,v\)\\mathsf\{Unr\}^\{L\}\(G,v\)is a tree of height at mostLL, whose nodes represent all paths of length at mostLLstarting fromvv\. This construction captures the locality of GNN computations: GNN classifiers are invariant under unravelling, as formalised next \(see also\(Barcelóet al\.,[2020](https://arxiv.org/html/2606.17882#bib.bib48), Proposition C\.4\)\)\.

###### Proposition\\thethm\.

Let𝒩\\mathcal\{N\}be an aggregate\-combine GNN withLLlayers\. Then, for every pointed graph\(G,v\)\(G,v\)and everyK≥LK\\geq L, we have𝒩​\(G,v\)=𝒩​\(𝖴𝗇𝗋K​\(G,v\)\)\.\\mathcal\{N\}\(G,v\)=\\mathcal\{N\}\(\\mathsf\{Unr\}^\{K\}\(G,v\)\)\.

Modal logics exhibit an analogous invariance property: the truth of a modal formula of depthLLat a node depends only on itsLL\-unravelling\.

### 4\.2Modal Logic

Formulae of graded modal logic𝒢​ℳ​ℒ\\mathcal\{GML\}de Rijke \([2000](https://arxiv.org/html/2606.17882#bib.bib3)\); Tobies \([2001](https://arxiv.org/html/2606.17882#bib.bib46)\); Otto \([2019](https://arxiv.org/html/2606.17882#bib.bib54)\)are defined inductively by the grammar

φ:=p​∣¬φ∣​φ∧φ​∣φ∨φ∣​◇≥k​φ,\\varphi:=p\\mid\\neg\\varphi\\mid\\varphi\\land\\varphi\\mid\\varphi\\lor\\varphi\\mid\\Diamond^\{\\geq k\}\\varphi,whereppranges over propositionspip\_\{i\}andk∈ℕk\\in\\mathbb\{N\}\. The*depth*ofφ\\varphiis the maximum nesting depth of its modal operators\. The*existential*fragment∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}restricts negation to occur in front of propositions, while the*existential\-positive*fragment∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}is negation\-free\. The logicℳ​ℒ\\mathcal\{ML\}restricts the graded modal operators tok=1k=1, and the fragments∃ℳ​ℒ\\exists\\mathcal\{ML\}and∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}ofℳ​ℒ\\mathcal\{ML\}are defined analogously\.

We interpret formulae over pointed graphs111Modal formulae are typically interpreted over Kripke structures \(directed graphs\); in our setting, we work with undirected graphs by viewing the edge relation as symmetric\.\(G,v\)\(G,v\)withG=\(V,E,λ\)G=\(V,E,\\lambda\)\. We assume that each propositionpip\_\{i\}corresponds to theii\-th component of the node feature vector\.

The*satisfaction relation*⊧\\modelsis defined inductively as follows:

\(G,v\)⊧pi\\displaystyle\(G,v\)\\models p\_\{i\}iffλ​\(v\)i=1\\displaystyle\\lambda\(v\)\_\{i\}=1\(G,v\)⊧¬φ\\displaystyle\(G,v\)\\models\\neg\\varphiiff\(G,v\)⊧̸φ\\displaystyle\(G,v\)\\not\\models\\varphi\(G,v\)⊧φ∧ψ\\displaystyle\(G,v\)\\models\\varphi\\land\\psiiff\(G,v\)⊧φ​and​\(G,v\)⊧ψ\\displaystyle\(G,v\)\\models\\varphi\\text\{ and \}\(G,v\)\\models\\psi\(G,v\)⊧φ∨ψ\\displaystyle\(G,v\)\\models\\varphi\\lor\\psiiff\(G,v\)⊧φ​or​\(G,v\)⊧ψ\\displaystyle\(G,v\)\\models\\varphi\\text\{ or \}\(G,v\)\\models\\psi\(G,v\)⊧◇≥k​φ\\displaystyle\(G,v\)\\models\\Diamond^\{\\geq k\}\\varphiiffthere exist at leastkneighbours​w​of​v​such that​\(G,w\)⊧φ\\displaystyle\\text\{there exist at least $k$ neighbours \}w\\text\{ of \}v\\text\{ such that \}\(G,w\)\\models\\varphi
For example, the formulap1∧◇≥2​p2p\_\{1\}\\land\\Diamond^\{\\geq 2\}p\_\{2\}holds in a pointed graph\(G,v\)\(G,v\)ifvvsatisfiesp1p\_\{1\}\(i\.e\.,λ​\(v\)1=1\\lambda\(v\)\_\{1\}=1\) and it has at least two neighbours satisfyingp2p\_\{2\}\(i\.e\., their second component is11\)\. This formula belongs to∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\(and even to∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}\), but is not expressible inℳ​ℒ\\mathcal\{ML\}\.

It is well known that for each𝒢​ℳ​ℒ\\mathcal\{GML\}formulaφ\\varphiof depthLLand each pointed graph\(G,v\)\(G,v\), we have

\(G,v\)⊧φiff𝖴𝗇𝗋L​\(G,v\)⊧φ\.\(G,v\)\\models\\varphi\\quad\\text\{iff\}\\quad\\mathsf\{Unr\}^\{L\}\(G,v\)\\models\\varphi\.That is, the class of pointed graphs satisfyingφ\\varphiis invariant underLL\-unravelling\.

Given a modal logicℒ\\mathcal\{L\}, each formulaφ∈ℒ\\varphi\\in\\mathcal\{L\}defines a node classifier by mapping a pointed graph\(G,v\)\(G,v\)to𝗍𝗋𝗎𝖾\\mathsf\{true\}if\(G,v\)⊧φ\(G,v\)\\models\\varphi, and to𝖿𝖺𝗅𝗌𝖾\\mathsf\{false\}otherwise\. We refer to such classifiers as*ℒ\\mathcal\{L\}\-classifiers*\.

A class𝒞\\mathcal\{C\}of pointed graphs is*definable*in a modal logicℒ\\mathcal\{L\}if there exists a formulaφ∈ℒ\\varphi\\in\\mathcal\{L\}such that\(G,v\)⊧φ\(G,v\)\\models\\varphiif and only if\(G,v\)∈𝒞\(G,v\)\\in\\mathcal\{C\}\.

### 4\.3Well\-quasi\-orders

A key step in our approach is to ensure that only finitely many structures need to be considered when characterising a class of graphs\. This finiteness property is guaranteed by well\-quasi\-orders \(wqos\)\.

A*quasi\-order*\(or*preorder*\)\(A,⪯\)\(A,\\preceq\)is a setAAequipped with a binary relation⪯\\preceqthat is reflexive \(a⪯aa\\preceq afor alla∈Aa\\in A\) and transitive \(a⪯ba\\preceq bandb⪯cb\\preceq cimpliesa⪯ca\\preceq c\)\. A quasi\-order\(A,⪯\)\(A,\\preceq\)is a*well\-quasi\-order*if every infinite sequencea1,a2,…a\_\{1\},a\_\{2\},\\ldotsinAAcontains indicesi<ji<jsuch thatai⪯aja\_\{i\}\\preceq a\_\{j\}\. Intuitively, this rules out infinite antichains and ensures that every infinite sequence contains an increasing pair\. In particular, any subset of a wqo has only finitely many⪯\\preceq\-minimal elements \(up to equivalence\), which will be crucial for our results\.

A central tool in our analysis is Higman’s Lemma, which ensures that the wqo property is preserved when extended to sequences\. LetA∗A^\{\*\}be the set of all finite sequences overAA, and let⪯∗\\preceq^\{\*\}be the*subsequence order*, defined by\(a1,…,an\)⪯∗\(b1,…,bm\)\(a\_\{1\},\\ldots,a\_\{n\}\)\\preceq^\{\*\}\(b\_\{1\},\\ldots,b\_\{m\}\)if there exists a strictly increasing mapf:\{1,…,n\}→\{1,…,m\}f:\\\{1,\\ldots,n\\\}\\to\\\{1,\\ldots,m\\\}such thatai⪯bf​\(i\)a\_\{i\}\\preceq b\_\{f\(i\)\}for alli∈\{1,…,n\}i\\in\\\{1,\\ldots,n\\\}\. For example,\(a1,a2\)⪯∗\(b1,b2,b3\)\(a\_\{1\},a\_\{2\}\)\\preceq^\{\*\}\(b\_\{1\},b\_\{2\},b\_\{3\}\)holds ifa1⪯b1a\_\{1\}\\preceq b\_\{1\}anda2⪯b3a\_\{2\}\\preceq b\_\{3\}\.

###### Lemma\\thethm\(Higman’s Lemma\)\.

If\(A,⪯\)\(A,\\preceq\)is a wqo, then\(A∗,⪯∗\)\(A^\{\*\},\\preceq^\{\*\}\)is also a wqo\.

### 4\.4A New Well\-Quasi\-Ordering Result for Trees

We now apply the wqo framework to trees, in particular to those obtained via unravelling, although the results of this section apply more generally\. We show that any \(possibly infinite\) class of trees obtained byLL\-unravelling has finitely many minimal trees with respect to embedding\. This finiteness is crucial, as it allows us to represent an infinite class using only finitely many minimal elements\. To establish this, we prove a stronger result: the embedding relation on any class of trees of bounded height is a wqo\. SinceLL\-unravellings have height at mostLL, and every wqo admits finitely many minimal elements, this result yields the desired finiteness\.

This is the main technical result underlying our framework\. Beyond its role in establishing our preservation theorems, it is of independent interest in the study of well\-quasi\-orders\.

Intuitively, trees of bounded height can be decomposed into their immediate subtrees, which themselves have smaller height\. This recursive structure allows one to reduce embeddings between trees to embeddings between sequences\. Using Higman’s Lemma we can ensure that such sequences form a well\-quasi\-order, yielding the result\.

###### Theorem\\thethm\.

The embedding relation on any class of rooted trees, whose heights are uniformly bounded by a fixed constant, is a well\-quasi\-order\.

As a consequence, the same result holds for injective homomorphisms and homomorphisms, since these relations extend the embedding relation\.

###### Corollary\\thethm\.

The injective homomorphism and homomorphism relations on any class of rooted trees of bounded height are well\-quasi\-orders\.

Any such class admits finitely many minimal trees, which provide a finite representation of the entire \(infinite\) class\. This property underpins the preservation theorems developed in the next section\. The bounded\-height assumption is essential: without it, the wqo property fails\.

###### Theorem\\thethm\.

The embedding, injective homomorphism, and homomorphism relations on classes of rooted trees of unbounded height are not, in general, well\-quasi\-orders\.

For example, consider the case of injective homomorphisms and the class𝒯\\mathcal\{T\}of rooted trees shown in[Figure˜3](https://arxiv.org/html/2606.17882#S4.F3), where nodes are unlabelled\. For anyn≠mn\\neq m, there is neither an injective homomorphism from\(Gn,v1\)\(G\_\{n\},v\_\{1\}\)to\(Gm,v1\)\(G\_\{m\},v\_\{1\}\), nor vice\-versa\. Intuitively, the position of the branching nodes depends on the height of the tree, making these structures incomparable under injective homomorphisms\. Thus,𝒯\\mathcal\{T\}forms an infinite antichain with respect to injective homomorphisms, and so, it is not a wqo\.

v1v\_\{1\}v2v\_\{2\}v3v\_\{3\}uuww\(G1,v1\)\(G\_\{1\},v\_\{1\}\)v1v\_\{1\}v2v\_\{2\}v3v\_\{3\}v4v\_\{4\}uuww\(G2,v1\)\(G\_\{2\},v\_\{1\}\)v1v\_\{1\}v2v\_\{2\}v3v\_\{3\}v4v\_\{4\}v5v\_\{5\}uuww\(G3,v1\)\(G\_\{3\},v\_\{1\}\)⋅⁣⋅⁣⋅\\cdot\\ \\cdot\\ \\cdot

Figure 3:An infinite antichain of rooted trees with respect to the injective homomorphism
### 4\.5Preservation Theorems

We now combine the well\-quasi\-ordering results from the previous section with unravelling invariance to obtain preservation theorems\.

At a high level, the idea is as follows\. Let𝒞\\mathcal\{C\}be a class of pointed graphs invariant underLL\-unravelling and preserved under a structural relation⪯\\preceq\(such as embedding, injective homomorphism, or homomorphism\)\. Then membership of a pointed graph in𝒞\\mathcal\{C\}is determined by itsLL\-unravelling, which is a tree of bounded height\. By the wqo results, such trees admit a finite set of⪯\\preceq\-minimal elements\. This finiteness allows us to represent𝒞\\mathcal\{C\}using a finite logical description: each minimal tree can be characterised by a formula, and the class𝒞\\mathcal\{C\}is defined by a finite disjunction of such formulae\.

Each of the relations⪯\\preceqcorresponds to a fragment of modal logic: embeddings, injective homomorphisms, and homomorphisms correspond to∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\},∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}, and∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}, respectively\. We formalise this in the following theorem\.

###### Theorem\\thethm\.

Let𝒞\\mathcal\{C\}be a class of pointed graphs,L∈ℕL\\in\\mathbb\{N\}, and let⪯\\preceqbe one of the following relations: embedding, injective homomorphism, or homomorphism\. Then the following are equivalent:

- •𝒞\\mathcal\{C\}is invariant underLL\-unravelling and preserved under⪯\\preceq
- •𝒞\\mathcal\{C\}is definable by a formula of depth at mostLLin a corresponding logic:∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}if⪯\\preceqis embedding,∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}if⪯\\preceqis injective homomorphism, and∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}if⪯\\preceqis homomorphism\.

SinceLL\-layer GNN classifiers are invariant underLL\-unravelling, these preservation theorems yield a semantic characterisation of GNN expressiveness\.

###### Corollary\\thethm\.

Let𝒩\\mathcal\{N\}be a GNN withLLlayers, let𝒞\\mathcal\{C\}be the class of pointed graphs accepted by𝒩\\mathcal\{N\}, and let⪯\\preceqbe one of the relations: embedding, injective homomorphism, or homomorphism\. Then the following are equivalent:

- •𝒞\\mathcal\{C\}is preserved under⪯\\preceq
- •𝒞\\mathcal\{C\}is definable by a formula of depth at mostLLin the corresponding fragment of graded modal logic:∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}if⪯\\preceqis embedding,∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}if⪯\\preceqis injective homomorphism, and∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}if⪯\\preceqis homomorphism\.

## 5Syntactic Characterisations of Structural Preservation Classes

We now complement the semantic characterisations with corresponding syntactic ones, showing that each preservation class identified in the previous section can be realised by a suitable class of GNN architectures\. In particular, we show that GNN classifiers preserved under embeddings can be realised as monotonic GNNs preceded by a pointwise feature transformation\. Removing this preprocessing step yields a class of monotonic GNNs corresponding to preservation under injective homomorphisms, which generalises previously proposed monotonic architectures\. Further restricting the aggregation functions yields GNN classes corresponding to preservation under homomorphisms\.

These architectures consist of two types of layers: monotonic layers which involve only non\-decreasing combination and aggregation functions, and augmentation layers which realise pointwise feature transformations independently of the graph structure\. We formalise these notions as follows\.

###### Definition\\thethm\.

For multisetsMMandM′M^\{\\prime\}of vectors of the same dimension, we writeM≤M′M\\leq M^\{\\prime\}if there exists an injective mapping from the elements ofMMto the elements ofM′M^\{\\prime\}such that𝐱≤f​\(𝐱\)\\mathbf\{x\}\\leq f\(\\mathbf\{x\}\), for every𝐱∈M\\mathbf\{x\}\\in M\. A functionffmapping vectors or multisets to vectors is*non\-decreasing*ifx≤yx\\leq yimpliesf​\(x\)≤f​\(y\)f\(x\)\\leq f\(y\)for all inputsx,yx,yof the same type \(e\.g\. vectors or multisets\)\.

Using this notion, we define monotonic and augmentation layers and the relevant GNN architectures\.

###### Definition\\thethm\.

A GNN layer\(𝖺𝗀𝗀,𝖼𝗈𝗆𝖻\)\(\\mathsf\{agg\},\\mathsf\{comb\}\)is*monotonic*if both the aggregation𝖺𝗀𝗀\\mathsf\{agg\}and the combination𝖼𝗈𝗆𝖻\\mathsf\{comb\}functions are non\-decreasing\. An*augmentation layer*is a functionη:ℝd→ℝd′\\eta:\\mathbb\{R\}^\{d\}\\to\\mathbb\{R\}^\{d^\{\\prime\}\}, applied pointwise to node feature vectors\.

###### Definition\\thethm\.

A*monotonic GNN*\(MGNN\) is a GNN whose layers are all monotonic\. AMAX\\mathrm\{MAX\}\-MGNN is an MGNN using onlyMAX\\mathrm\{MAX\}as aggregation\. Then an*augmented \(MAX\\mathrm\{MAX\}\-\)MGNN*is an \(MAX\\mathrm\{MAX\}\-\)MGNN with an additional augmentation layer before monotonic layers\.

Monotonic GNNs have been studied previously in the context of explainability and logical reasoning, where architectural constraints are imposed to enforce structural preservation propertiesTena Cucalaet al\.\([2025](https://arxiv.org/html/2606.17882#bib.bib21),[2023](https://arxiv.org/html/2606.17882#bib.bib26)\)\. These models are designed to satisfy monotonicity conditions that ensure preservation under homomorphisms or injective homomorphisms\. Our definitions subsume these approaches by isolating the underlying semantic property and expressing it in a modular, layer\-wise manner\. In particular, the class of monotonic GNNs defined above generalises the architectures proposed in prior work, which we recapitulate in the following definition\.

###### Definition\\thethm\.

A*positive\-weight GNN*is a GNN consisting of simple layers \(see Equation \([2](https://arxiv.org/html/2606.17882#S3.E2)\)\) in which all weight matrices have non\-negative entries, the activation function is non\-decreasing, and the aggregation functions areSUM\\mathrm\{SUM\},MAX\\mathrm\{MAX\}, orMAX​\-​k​\-​SUM\\mathrm\{MAX\}\\text\{\-\}k\\text\{\-\}\\mathrm\{SUM\}\.

These syntactic constraints ensure that all aggregation and combination functions are non\-decreasing with respect to their inputs\. Thus, the following can be observed\.

###### Proposition\\thethm\.

Every positive\-weight GNN is a monotonic GNN\.

The syntactic classes defined above satisfy the corresponding structural preservation properties\.

###### Theorem\\thethm\.

Augmented MGNNs are preserved under embeddings, MGNNs are preserved under injective homomorphisms, andMAX\\mathrm\{MAX\}\-MGNNs are preserved under homomorphisms\.

These preservation results can be understood intuitively as follows\. Monotonic layers ensure that increasing node features \(with respect to the underlying order\) or neighbourhood information cannot invalidate positive predictions\. Injective homomorphisms preserve the structure of the graph without merging nodes, and therefore preserve such monotonic behaviour\. In contrast, non\-injective homomorphisms may merge nodes and reduce multiplicities, which can invalidate properties that depend on counting\. Restricting aggregation toMAX\\mathrm\{MAX\}eliminates this issue, asMAX\\mathrm\{MAX\}is insensitive to multiplicities: merging nodes does not affect the maximum value\. Thus,MAX\\mathrm\{MAX\}\-MGNN classifiers are preserved even under homomorphisms\. Finally, augmentation layers allow for additional feature transformations applied pointwise, without changing the graph structure, thus preserving embeddings\.

To obtain exact characterisations of GNNs classes, we start by establishing lower bounds\. That is, we show that every formula in a relevant fragment can be realised by a GNN in the corresponding syntactic class\.

###### Theorem\\thethm\.

The following statements hold:

- •For each∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\-classifier there is an equivalent augmented MGNN classifier,
- •For each∃ℳ​ℒ\\exists\\mathcal\{ML\}\-classifier there is an equivalent augmentedMAX\\mathrm\{MAX\}\-MGNN classifier,
- •For each∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}\-classifier there is an equivalent MGNN classifier,
- •For each∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\-classifier there is an equivalentMAX\\mathrm\{MAX\}\-MGNN classifier\.

Furthermore, each GNN above can be assumed to be simple, with truncated ReLUσ​\(𝐱\)=min⁡\(max⁡\(0,𝐱\),1\)\\sigma\(\\mathbf\{x\}\)=\\min\(\\max\(0,\\mathbf\{x\}\),1\)as activation function\.

To derive exact characterisations of the expressiveness of GNN classes we need to show matching upper bounds\. For this, we use our preservation theorems together with the results in[Section˜4\.5](https://arxiv.org/html/2606.17882#S4.SS5)\. Consequently we obtain the following tight bounds\.

###### Theorem\\thethm\.

The following tight expressiveness results hold:

- •Augmented MGNN classifiers have the same expressiveness as∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}classifiers,
- •AugmentedMAX\\mathrm\{MAX\}\-MGNN classifiers have the same expressiveness as∃ℳ​ℒ\\exists\\mathcal\{ML\}classifiers,
- •MGNN classifiers have the same expressiveness as∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}classifiers,
- •MAX\\mathrm\{MAX\}\-MGNN classifiers have the same expressiveness as∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}classifiers\.

These results provide concrete insights into the kinds of properties expressible by GNNs under different structural preservation constraints\. At one end of the spectrum, augmented MGNNs, which correspond to preservation under embeddings, can express a wide range of local properties, including pointwise non\-monotone properties such as “nodevvdoes not have labelAA”\. However, such models cannot express non\-monotone properties that depend on the node’s neighbourhood, such as exact counting \(“exactlykkneighbours ofvvsatisfy propertypp”\), parity conditions \(e\.g\., “the number of neighbours ofvvis even”\), or global properties such as connectivity\.

Restricting to MGNNs, which correspond to preservation under injective homomorphisms, restricts expressiveness to monotone properties\. These include existential and threshold\-based conditions, such as “nodevvhas at leastkkneighbours satisfying propertypp”, or “there exists a path of length at mostkkfromvvto a node satisfyingpp”\.

At the most restrictive level,MAX\\mathrm\{MAX\}\-MGNNs, which correspond to preservation under homomorphisms, can express only purely existential properties, such as “nodevvhas some neighbour satisfying propertypp”\. In particular, they cannot express threshold\-based conditions, asMAX\\mathrm\{MAX\}aggregation is insensitive to multiplicities\.

Overall, these results reveal a fundamental trade\-off: preservation under stronger graph transformations leads to simpler logical characterisations, but at the cost of reduced expressive power\. In particular, preservation properties constrain GNN expressiveness to fragments of modal logic, ruling out global and counting\-based properties that fall outside these fragments\.

## 6Conclusion

We have developed a semantic framework for analysing the expressiveness of GNNs based on structural preservation properties\. By combining preservation theorems with new well\-quasi\-order results for trees, we established exact correspondences between preservation under structural relations, fragments of graded modal logic, and natural classes of GNN architectures\. Our approach highlights a fundamental trade\-off between structural invariance and expressive power: stronger preservation properties lead to simpler logical characterisations, but at the cost of reduced expressiveness\. Our framework also extends naturally to directed graphs as the underlying logical results apply to Kripke models\. The extension requires only minor adaptations to the GNN architecture, such as distinguishing between incoming and outgoing neighbourhoods\.

LimitationsOur framework focuses on node classification tasks; extending it to graph\-level prediction remains an open problem\. Moreover, we study GNNs whose behaviour is determined by local neighbourhoods and structural preservation properties, and thus do not capture architectures that rely on global reasoning or other non\-local mechanisms\. We also restrict attention to threshold\-based classifiers and to graphs without edge features\. Our logical characterisations assume discrete node labels represented as finite\-dimensional binary vectors, and extending the results to richer feature domains is non\-trivial\. Finally, our correspondence with logic captures precisely the locality\-bounded behaviour of GNNs, i\.e\., those invariant under bounded unravelling, and does not account for properties beyond this regime\.

## References

- \[1\]\(2024\)Arboreal categories and equi\-resource homomorphism preservation theorems\.Ann\. Pure Appl\. Log\.175\(6\),pp\. 103423\.External Links:[Link](https://doi.org/10.1016/j.apal.2024.103423),[Document](https://dx.doi.org/10.1016/J.APAL.2024.103423)Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p4.1),[§2](https://arxiv.org/html/2606.17882#S2.p3.1)\.
- \[2\]H\. Andréka, I\. Németi, and J\. van Benthem\(1998\)Modal languages and bounded fragments of predicate logic\.J\. Philos\. Log\.27\(3\),pp\. 217–274\.External Links:[Link](https://doi.org/10.1023/A:1004275029985),[Document](https://dx.doi.org/10.1023/A%3A1004275029985)Cited by:[§2](https://arxiv.org/html/2606.17882#S2.p3.1)\.
- \[3\]F\. Baader, D\. Calvanese, D\. L\. McGuinness, D\. Nardi, and P\. F\. Patel\-Schneider \(Eds\.\)\(2003\)The description logic handbook: theory, implementation, and applications\.Cambridge University Press\.External Links:ISBN 0\-521\-78176\-0Cited by:[§B\.2](https://arxiv.org/html/2606.17882#A2.SS2.p6.6)\.
- \[4\]P\. Barceló, E\. V\. Kostylev, M\. Monet, J\. Pérez, J\. L\. Reutter, and J\. P\. Silva\(2020\)The logical expressiveness of graph neural networks\.InProc\. of ICLR,Cited by:[Appendix C](https://arxiv.org/html/2606.17882#A3.43.p2.10),[§1](https://arxiv.org/html/2606.17882#S1.p1.2),[§1](https://arxiv.org/html/2606.17882#S1.p5.2),[§2](https://arxiv.org/html/2606.17882#S2.p1.1),[§3](https://arxiv.org/html/2606.17882#S3.SS0.SSS0.Px1.p1.22),[§3](https://arxiv.org/html/2606.17882#S3.SS0.SSS0.Px2.p1.1),[§3](https://arxiv.org/html/2606.17882#S3.SS0.SSS0.Px2.p4.14),[§4\.1](https://arxiv.org/html/2606.17882#S4.SS1.p2.3),[§4\.1](https://arxiv.org/html/2606.17882#S4.SS1.p4.4)\.
- \[5\]M\. Benedikt, C\. Lu, B\. Motik, and T\. Tan\(2024\)Decidability of Graph Neural Networks via Logical Characterizations\.InProc\. of ICALP,Vol\.297,pp\. 127:1–127:20\.Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p2.1),[§2](https://arxiv.org/html/2606.17882#S2.p1.1),[§3](https://arxiv.org/html/2606.17882#S3.SS0.SSS0.Px1.p1.22),[§3](https://arxiv.org/html/2606.17882#S3.SS0.SSS0.Px2.p1.1)\.
- \[6\]B\. Cuenca Grau, E\. Feng, and P\. Walega\(2026\)The correspondence between bounded graph neural networks and fragments of first\-order logic\.InProc\. of AAAI,Cited by:[§B\.1](https://arxiv.org/html/2606.17882#A2.SS1.p1.5),[Appendix C](https://arxiv.org/html/2606.17882#A3.44.p3.15),[§1](https://arxiv.org/html/2606.17882#S1.p1.2),[§2](https://arxiv.org/html/2606.17882#S2.p1.1)\.
- \[7\]M\. de Rijke\(2000\)A note on graded modal logic\.Stud Logica64\(2\),pp\. 271–283\.External Links:[Link](https://doi.org/10.1023/A:1005245900406),[Document](https://dx.doi.org/10.1023/A%3A1005245900406)Cited by:[§4\.2](https://arxiv.org/html/2606.17882#S4.SS2.p1.1)\.
- \[8\]J\. Gilmer, S\. S\. Schoenholz, P\. F\. Riley, O\. Vinyals, and G\. E\. Dahl\(2017\)Neural message passing for quantum chemistry\.InProc\. of ICML,Vol\.70,pp\. 1263–1272\.Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p1.2)\.
- \[9\]E\. Grädel, P\. G\. Kolaitis, L\. Libkin, M\. Marx, J\. Spencer, M\. Y\. Vardi, Y\. Venema, and S\. Weinstein\(2007\)Finite model theory and its applications\.Texts in Theoretical Computer Science\. An EATCS Series,Springer\.Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p4.1)\.
- \[10\]M\. Grohe\(2024\)The descriptive complexity of graph neural networks\.TheoretiCS3\.Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p2.1),[§2](https://arxiv.org/html/2606.17882#S2.p1.1)\.
- \[11\]S\. P\. Hauke and P\. A\. Wałęga\(2026\)Aggregate\-combine\-readout GNNs are more expressive than logic C2\.InProc\. of AAAI,Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p1.2)\.
- \[12\]W\. Hodges\(1997\)A shorter model theory\.Cambridge University Press\.External Links:ISBN 978\-0\-521\-58713\-6Cited by:[§2](https://arxiv.org/html/2606.17882#S2.p3.1)\.
- \[13\]L\. Libkin\(2004\)Elements of finite model theory\.Texts in Theoretical Computer Science\. An EATCS Series,Springer\.Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p4.1)\.
- \[14\]A\. Lopez\(2023\)First order preservation theorems in finite model theory : locality, topology, and limit constructions\. \(théorèmes de préservation pour la logique au premier ordre: localité, topologie et constructions limites\)\.Ph\.D\. Thesis,University of Paris\-Saclay, France\.External Links:[Link](https://tel.archives-ouvertes.fr/tel-04534568)Cited by:[§2](https://arxiv.org/html/2606.17882#S2.p3.1)\.
- \[15\]J\. Łoś and R\. Suszko\(1955\)On the extending of models \(ii\)\.Fundamenta Mathematicae42\(2\),pp\. 343–347\.Cited by:[§2](https://arxiv.org/html/2606.17882#S2.p3.1)\.
- \[16\]R\. C\. Lyndon\(1959\)Properties preserved under homomorphism\.\.Cited by:[§2](https://arxiv.org/html/2606.17882#S2.p3.1)\.
- \[17\]C\. Morris, M\. Ritzert, M\. Fey, W\. L\. Hamilton, J\. E\. Lenssen, G\. Rattan, and M\. Grohe\(2019\)Weisfeiler and leman go neural: higher\-order graph neural networks\.InProc\. of AAAI,Vol\.33,pp\. 4602–4609\.Cited by:[§2](https://arxiv.org/html/2606.17882#S2.p1.1)\.
- \[18\]C\. Morris, M\. Ritzert, M\. Fey, W\. L\. Hamilton, J\. E\. Lenssen, G\. Rattan, and M\. Grohe\(2019\)Weisfeiler and leman go neural: higher\-order graph neural networks\.InProc\. of AAAI,pp\. 4602–4609\.Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p5.2)\.
- \[19\]M\. Morris, D\. J\. T\. Cucala, B\. C\. Grau, and I\. Horrocks\(2024\)Relational graph convolutional networks do not learn sound rules\.InProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, KR 2024, Hanoi, Vietnam\. November 2\-8, 2024,P\. Marquis, M\. Ortiz, and M\. Pagnucco \(Eds\.\),External Links:[Link](https://doi.org/10.24963/kr.2024/84),[Document](https://dx.doi.org/10.24963/KR.2024/84)Cited by:[§2](https://arxiv.org/html/2606.17882#S2.p2.1)\.
- \[20\]M\. Morris and I\. Horrocks\(2025\)Sound logical explanations for mean aggregation graph neural networks\.InThe Thirty\-ninth Annual Conference on Neural Information Processing Systems,External Links:[Link](https://openreview.net/forum?id=7TY89cqLfE)Cited by:[§B\.2](https://arxiv.org/html/2606.17882#A2.SS2.p6.6),[§2](https://arxiv.org/html/2606.17882#S2.p2.1)\.
- \[21\]P\. Nunn, M\. Sälzer, F\. Schwarzentruber, and N\. Troquard\(2024\)A logic for reasoning about aggregate\-combine graph neural networks\.InProc\. of IJCAI,pp\. 3532–3540\.Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p2.1),[§2](https://arxiv.org/html/2606.17882#S2.p1.1)\.
- \[22\]M\. Otto\(2019\)Graded modal logic and counting bisimulation\.CoRRabs/1910\.00039\.External Links:[Link](http://arxiv.org/abs/1910.00039),1910\.00039Cited by:[§B\.1](https://arxiv.org/html/2606.17882#A2.SS1.p1.5),[§B\.1](https://arxiv.org/html/2606.17882#A2.SS1.p2.10),[§4\.2](https://arxiv.org/html/2606.17882#S4.SS2.p1.1)\.
- \[23\]E\. Rosen\(1997\)Modal logic over finite structures\.J\. Log\. Lang\. Inf\.6\(4\),pp\. 427–439\.External Links:[Link](https://doi.org/10.1023/A:1008275906015),[Document](https://dx.doi.org/10.1023/A%3A1008275906015)Cited by:[Appendix C](https://arxiv.org/html/2606.17882#A3.44.p3.15),[§1](https://arxiv.org/html/2606.17882#S1.p4.1),[§2](https://arxiv.org/html/2606.17882#S2.p3.1)\.
- \[24\]E\. Rosen\(2002\)Some aspects of model theory and finite structures\.Bull\. Symb\. Log\.8\(3\),pp\. 380–403\.External Links:[Link](https://doi.org/10.2178/bsl/1182353894),[Document](https://dx.doi.org/10.2178/BSL/1182353894)Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p4.1)\.
- \[25\]B\. Rossman\(2008\)Homomorphism preservation theorems\.J\. ACM55\(3\),pp\. 15:1–15:53\.External Links:[Link](https://doi.org/10.1145/1379759.1379763),[Document](https://dx.doi.org/10.1145/1379759.1379763)Cited by:[§B\.3](https://arxiv.org/html/2606.17882#A2.SS3.12.p4.9),[§1](https://arxiv.org/html/2606.17882#S1.p4.1),[§2](https://arxiv.org/html/2606.17882#S2.p3.1)\.
- \[26\]D\. Tena Cucala, B\. Cuenca Grau, B\. Motik, and E\. V\. Kostylev\(2023\)On the correspondence between monotonic max\-sum gnns and datalog\.InProc\. of KR,P\. Marquis, T\. C\. Son, and G\. Kern\-Isberner \(Eds\.\),pp\. 658–667\.Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p2.1),[§2](https://arxiv.org/html/2606.17882#S2.p2.1),[§3](https://arxiv.org/html/2606.17882#S3.SS0.SSS0.Px2.p4.14),[§5](https://arxiv.org/html/2606.17882#S5.p4.1)\.
- \[27\]D\. J\. Tena Cucala, B\. Cuenca Grau, B\. Motik, and E\. V\. Kostylev\(2025\)Expressive power of monotonic graph neural networks via datalog\.InHandbook on Neurosymbolic AI and Knowledge Graphs,pp\. 780–807\.Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p2.1),[§2](https://arxiv.org/html/2606.17882#S2.p2.1),[§5](https://arxiv.org/html/2606.17882#S5.p4.1)\.
- \[28\]D\. J\. Tena Cucala and B\. Cuenca Grau\(2024\)Bridging max graph neural networks and datalog with negation\.InProc\. of KR,P\. Marquis, M\. Ortiz, and M\. Pagnucco \(Eds\.\),Cited by:[§2](https://arxiv.org/html/2606.17882#S2.p2.1)\.
- \[29\]S\. Tobies\(2001\)PSPACE reasoning for graded modal logics\.J\. Log\. Comput\.11\(1\),pp\. 85–106\.External Links:[Link](https://doi.org/10.1093/logcom/11.1.85),[Document](https://dx.doi.org/10.1093/LOGCOM/11.1.85)Cited by:[§4\.2](https://arxiv.org/html/2606.17882#S4.SS2.p1.1)\.
- \[30\]X\. Wang and M\. Zhang\(2022\)How powerful are spectral graph neural networks\.InProc\. of ICML,Cited by:[§1](https://arxiv.org/html/2606.17882#S1.p5.2)\.
- \[31\]K\. Xu, W\. Hu, J\. Leskovec, and S\. Jegelka\(2019\)How powerful are graph neural networks?\.InProc\. of ICLR,Cited by:[§2](https://arxiv.org/html/2606.17882#S2.p1.1)\.

## Technical Appendix

## Appendix AProofs for[Section˜4\.4](https://arxiv.org/html/2606.17882#S4.SS4)

See[4\.4](https://arxiv.org/html/2606.17882#S4.SS4)

###### Proof\.

LetLLbe the uniform bound on the height of the trees under consideration, and let⪯\\preceqbe the embedding relation between pointed trees\. Clearly,⪯\\preceqis a quasi\-order\. We prove by induction onℓ≤L\\ell\\leq Lthe following claim: for every class𝒯\\mathcal\{T\}of pointed trees of height at mostℓ\\ell, the quasi\-order\(𝒯,⪯\)\(\\mathcal\{T\},\\preceq\)is a wqo\.

*Base case \(ℓ=0\\ell=0\)*\. A tree of height0consists of a single root labelled by some vector in\{0,1\}d\\\{0,1\\\}^\{d\}\. Since the dimensionddof trees is finite, there are finitely many non\-isomorphic trees of this form\. Hence, for any class of pointed trees of height0, the quasi\-order induced by⪯\\preceqis a wqo\. Note that the finiteness ofddis essential for this argument\.

*Inductive step*\. Letℓ≥1\\ell\\geq 1and assume that the claim holds forℓ−1\\ell\-1\. Let𝒯\\mathcal\{T\}be an arbitrary class of pointed trees of height at mostℓ\\ell\. We show that\(𝒯,⪯\)\(\\mathcal\{T\},\\preceq\)is a wqo\.

We begin by partitioning𝒯\\mathcal\{T\}into subclasses𝒯S\\mathcal\{T\}^\{S\}indexed byS⊆\{1,…,d\}S\\subseteq\\\{1,\\dots,d\\\}, where𝒯S\\mathcal\{T\}^\{S\}consists of all pointed trees in𝒯\\mathcal\{T\}whose root has exactly the labels inSS\. Since2d2^\{d\}is finite and a finite disjoint union of wqos is also a wqo, it suffices to show that each\(𝒯S,⪯\)\(\\mathcal\{T\}^\{S\},\\preceq\)is a wqo\.

FixS⊆\{1,…,d\}S\\subseteq\\\{1,\\dots,d\\\}\. For each\(𝔐,w\)\(\\mathfrak\{M\},w\)in𝒯S\\mathcal\{T\}^\{S\}, letτ𝔐,w=\(τ1,…,τn\)\\tau\_\{\\mathfrak\{M\},w\}=\(\\tau\_\{1\},\\dots,\\tau\_\{n\}\)be a finite sequence enumerating its immediate subtrees rooted at the children ofww\. As the children are unordered, we fix an arbitrary but canonical ordering on the subtrees to obtain a well\-defined enumeration\. The embedding relation⪯\\preceqon pointed graphs induces the subsequence order relation⪯∗\\preceq^\{\*\}on their finite sequences, defined as in Higman’s Lemma \(see Lemma[4\.3](https://arxiv.org/html/2606.17882#S4.SS3)\)\. To account for the arbitrary ordering of children, we consider the permutation\-closed variant⪯π∗\\preceq^\{\*\}\_\{\\pi\}defined byτ⪯π∗τ′\\tau\\preceq^\{\*\}\_\{\\pi\}\\tau^\{\\prime\}if and only ifτ⪯∗f​\(τ′\)\\tau\\preceq^\{\*\}f\(\\tau^\{\\prime\}\)for some permutationff\. We claim that for any\(𝔐,w\),\(𝔑,v\)∈𝒯S\(\\mathfrak\{M\},w\),\(\\mathfrak\{N\},v\)\\in\\mathcal\{T\}^\{S\}, we have\(𝔐,w\)⪯\(𝔑,v\)\(\\mathfrak\{M\},w\)\\preceq\(\\mathfrak\{N\},v\)if and only ifτ𝔐,w⪯π∗τ𝔑,v\\tau\_\{\\mathfrak\{M\},w\}\\preceq^\{\*\}\_\{\\pi\}\\tau\_\{\\mathfrak\{N\},v\}\. Indeed, an embedding from\(𝔐,w\)\(\\mathfrak\{M\},w\)into\(𝔑,v\)\(\\mathfrak\{N\},v\)must map each child ofwwinjectively to a distinct child ofvv, such that the corresponding subtree embeds recursively\. This yieldsτ𝔐,w⪯π∗τ𝔑,v\\tau\_\{\\mathfrak\{M\},w\}\\preceq^\{\*\}\_\{\\pi\}\\tau\_\{\\mathfrak\{N\},v\}\. Conversely, ifτ𝔐,w⪯π∗τ𝔑,v\\tau\_\{\\mathfrak\{M\},w\}\\preceq^\{\*\}\_\{\\pi\}\\tau\_\{\\mathfrak\{N\},v\}then each subtree inτ𝔐,w\\tau\_\{\\mathfrak\{M\},w\}embeds into a distinct subtree inτ𝔑,v\\tau\_\{\\mathfrak\{N\},v\}, yielding an embedding from\(𝔐,w\)\(\\mathfrak\{M\},w\)into\(𝔑,v\)\(\\mathfrak\{N\},v\)\.

Thus, to show that\(𝒯S,⪯\)\(\\mathcal\{T\}^\{S\},\\preceq\)is a wqo, it suffices to show that\(\{τ𝔐,w∣\(𝔐,w\)∈𝒯S\},⪯π∗\)\\bigl\(\\\{\\tau\_\{\\mathfrak\{M\},w\}\\mid\(\\mathfrak\{M\},w\)\\in\\mathcal\{T\}^\{S\}\\\},\\preceq^\{\*\}\_\{\\pi\}\\bigr\)is a wqo\. To this end, letℐ\\mathcal\{I\}be the set of all rooted trees of height at mostℓ−1\\ell\-1\. By the inductive hypothesis,\(ℐ,⪯\)\(\\mathcal\{I\},\\preceq\)is a wqo\. By Higman’s Lemma \(Lemma[4\.3](https://arxiv.org/html/2606.17882#S4.SS3)\), the set of finite sequencesℐ∗\\mathcal\{I\}^\{\*\}ordered by the subsequence relation⪯∗\\preceq^\{\*\}is also a wqo\. Since wqos are closed under taking subsets, and\(τ𝔐,w∣\(𝔐,w\)∈𝒯S\)\(\\tau\_\{\\mathfrak\{M\},w\}\\mid\(\\mathfrak\{M\},w\)\\in\\mathcal\{T\}^\{S\}\)is a subset ofℐ∗\\mathcal\{I\}^\{\*\}, it follows that\(\(τ𝔐,w∣\(𝔐,w\)∈𝒯S\),⪯∗\)\(\(\\tau\_\{\\mathfrak\{M\},w\}\\mid\(\\mathfrak\{M\},w\)\\in\\mathcal\{T\}^\{S\}\),\\preceq^\{\*\}\)is a wqo\. Moreover, as⪯∗\\preceq^\{\*\}is a subrelation of⪯π∗\\preceq^\{\*\}\_\{\\pi\}and⪯π∗\\preceq^\{\*\}\_\{\\pi\}is a quasi\-order, it follows that⪯π∗\\preceq^\{\*\}\_\{\\pi\}is also a wqo on this set\. This completes the inductive step and the whole proof\. ∎

See[4\.4](https://arxiv.org/html/2606.17882#S4.SS4)

###### Proof\.

We start with the case of injective homomorphisms, which also covers embeddings as a special case\. Consider the class𝒯\\mathcal\{T\}of pointed trees that, for everyn≥1n\\geq 1, contains a rooted tree\(Gn,v1\)\(G\_\{n\},v\_\{1\}\)with nodesv1,…​vn,vn\+1,vn\+2,u,wv\_\{1\},\\ldots v\_\{n\},v\_\{n\+1\},v\_\{n\+2\},u,wwhich has edges\{vi<vi\+1\}\\\{v\_\{i\}<v\_\{i\+1\}\\\}for1≤i≤n\+11\\leq i\\leq n\+1as well as the edges\{v1,u\}\\\{v\_\{1\},u\\\}and\{vn\+1,w\}\\\{v\_\{n\+1\},w\\\}, as depicted in[Figure˜3](https://arxiv.org/html/2606.17882#S4.F3)\. All nodes are unlabelled \(equivalently, they all have the same label\)\.

In each\(Gn,v1\)\(G\_\{n\},v\_\{1\}\)there are exactly two nodes at distancen\+1n\+1from the root, namelyvn\+2v\_\{n\+2\}andww\. By contrast, ifm\>nm\>n, then\(Gm,v1\)\(G\_\{m\},v\_\{1\}\)has a single node at distancen\+1n\+1, namelyvn\+2v\_\{n\+2\}\. Hence, for anyn≠mn\\neq m, there is neither an injective homomorphism from\(Gn,v1\)\(G\_\{n\},v\_\{1\}\)to\(Gm,v1\)\(G\_\{m\},v\_\{1\}\), nor vice\-versa\. Thus,𝒯\\mathcal\{T\}forms an infinite antichain with respect to injective homomorphisms and hence also with respect to embeddings\.

We now turn to the case of homomorphisms\. Consider the modification of𝒯\\mathcal\{T\}where, in each graph\(Gn,v1\)\(G\_\{n\},v\_\{1\}\), nodes are labelled with vectors of length 4, where the labellingλ\\lambdais defined such thatλ​\(v\)1=1\\lambda\(v\)\_\{1\}=1iffv=viv=v\_\{i\}for some evenii,λ​\(v\)2=1\\lambda\(v\)\_\{2\}=1iffv=viv=v\_\{i\}for some oddii,λ​\(v\)3=1\\lambda\(v\)\_\{3\}=1iffv=uv=u, andλ​\(v\)4=1\\lambda\(v\)\_\{4\}=1iffv=wv=w\.

Letn<mn<mand suppose, towards a contradiction, thatffis a homomorphism from\(Gn,v1\)\(G\_\{n\},v\_\{1\}\)to\(Gm,v1\)\(G\_\{m\},v\_\{1\}\)\. We prove by induction oni≤n\+2i\\leq n\+2thatf​\(vi\)=vif\(v\_\{i\}\)=v\_\{i\}\. The base casei=1i=1is immediate\. For the inductive step, assume thatf​\(vi\)=vif\(v\_\{i\}\)=v\_\{i\}\. Then,f​\(vi\+1\)f\(v\_\{i\+1\}\)must be a successor ofviv\_\{i\}inGmG\_\{m\}satisfying the same labels asvi\+1v\_\{i\+1\}inGnG\_\{n\}\. InGmG\_\{m\}the only such successor isvi\+1v\_\{i\+1\}itself, hencef​\(vi\+1\)=vi\+1f\(v\_\{i\+1\}\)=v\_\{i\+1\}\. In particular,f​\(vn\+1\)=vn\+1f\(v\_\{n\+1\}\)=v\_\{n\+1\}\. It follows thatf​\(w\)f\(w\)is a successor ofvn\+1v\_\{n\+1\}inGmG\_\{m\}with label 4\. However, the only node inGmG\_\{m\}with label 4 isww, which is a successor ofvm\+1v\_\{m\+1\}rather thanvn\+1v\_\{n\+1\}\. This yields a contradiction\. A symmetric argument shows that no homomorphism exists from\(Gm,v1\)\(G\_\{m\},v\_\{1\}\)to\(Gn,v1\)\(G\_\{n\},v\_\{1\}\)\. ∎

## Appendix BProofs for[Section˜4\.5](https://arxiv.org/html/2606.17882#S4.SS5)

In what follows we will prove the following theorem\.

See[4\.5](https://arxiv.org/html/2606.17882#S4.SS5)

The above theorem consists of three statements; we will prove them one by one in three subsections\.

Since proofs exploit modal logic machinery, in the following subsections we will use notions and syntax used in this research area\. In particular, instead of pointed graphs we will write about pointed \(Kripke\) models, and represent them as𝔐=\(W,R,V\)\\mathfrak\{M\}=\(W,R,V\), whereWWis a non\-empty finite set of*worlds*\(corresponding to nodes\),R⊆W×WR\\subseteq W\\times Wis the*accessibility relation*\(corresponding to edges\), andVVis a*valuation function*mapping each propositional variablepi∈𝖯𝖱𝖮𝖯p\_\{i\}\\in\\mathsf\{PROP\}to a subset ofWW\(corresponding to the node labelling, where𝖯𝖱𝖮𝖯\\mathsf\{PROP\}has as many labels as the dimensionddof vectors\)\.

### B\.1Preservation Under Embeddings

Our aim is to show that any class of models preserved under embeddings and invariant underLL\-unravelling is definable by a∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\-formula\. Moreover, we show that such a formula can be chosen to have depth at mostLL\. To this end, we introduce characteristic formulae in∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\. These formulae are obtained as a modification of the standard characteristic formulae for graded modal logic from the literature\[[22](https://arxiv.org/html/2606.17882#bib.bib54),[6](https://arxiv.org/html/2606.17882#bib.bib24)\]\. The key difference is that our characteristic formulae in∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}do not contain negated modal operators\.

###### Definition\\thethm\.

Let\(𝔐,w\)\(\\mathfrak\{M\},w\)be a pointed model with𝔐=\(W,R,V\)\\mathfrak\{M\}=\(W,R,V\)\. For eachℓ∈ℕ\\ell\\in\\mathbb\{N\}, we define a*characteristic∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}formula*,φ𝔐,wℓ\\varphi\_\{\\mathfrak\{M\},w\}^\{\\ell\}of depthℓ\\ellinductively as follows\. Forℓ=0\\ell=0, let

φ𝔐,w0:=⋀\{p∣\(𝔐,w\)⊧p\}∧⋀\{¬p∣\(𝔐,w\)⊧̸p\}\.\\varphi\_\{\\mathfrak\{M\},w\}^\{0\}:=\\bigwedge\\\{p\\mid\(\\mathfrak\{M\},w\)\\models p\\\}\\land\\bigwedge\\\{\\neg p\\mid\(\\mathfrak\{M\},w\)\\not\\models p\\\}\.Forℓ\+1\\ell\+1, partition theRR\-successors ofwwinto equivalence classesC1,…,CmC\_\{1\},\\dots,C\_\{m\}according to the relation≡ℓ𝒢​ℳ​ℒ\\equiv^\{\\mathcal\{GML\}\}\_\{\\ell\}\. For eachCjC\_\{j\}, choose an arbitrary representativewj∈Cjw\_\{j\}\\in C\_\{j\}and define

φ𝔐,wℓ\+1:=φ𝔐,w0∧⋀j=1m◇≥\|Cj\|​φ𝔐,wjℓ\.\\varphi\_\{\\mathfrak\{M\},w\}^\{\\ell\+1\}\\ :=\\ \\varphi\_\{\\mathfrak\{M\},w\}^\{0\}\\ \\wedge\\ \\bigwedge\_\{j=1\}^\{m\}\\Diamond^\{\\geq\|C\_\{j\}\|\}\\,\\varphi\_\{\\mathfrak\{M\},w\_\{j\}\}^\{\\ell\}\.

For full𝒢​ℳ​ℒ\\mathcal\{GML\}, a characteristic formula of depthℓ\\ellfor a pointed model\(𝔐,w\)\(\\mathfrak\{M\},w\)holds in\(𝔑,v\)\(\\mathfrak\{N\},v\)if and only if there exists a gradedℓ\\ell\-bisimulation between these two pointed models\. Over finite models, this is equivalent to\(𝔐,w\)≡ℓ𝒢​ℳ​ℒ\(𝔑,v\)\(\\mathfrak\{M\},w\)\\equiv^\{\\mathcal\{GML\}\}\_\{\\ell\}\(\\mathfrak\{N\},v\)\[[22](https://arxiv.org/html/2606.17882#bib.bib54)\]\. The characteristic defined above for∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}are strictly weaker, and these equivalences no longer hold\. Instead, the∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}characteristic ensure a one\-way structural property: theℓ\\ell\-unravelling of the model used to construct the characteristic formula embeds into theℓ\\ell\-unravelling of any model satisfying the formula\. This property is captured by the following lemma, which plays a central role in the preservation theorem for embeddings\.

###### Lemma\\thethm\.

Let\(𝔐,w\)\(\\mathfrak\{M\},w\)and\(𝔑,v\)\(\\mathfrak\{N\},v\)be pointed models and letℓ∈ℕ\\ell\\in\\mathbb\{N\}\. We have\(𝔑,v\)⊧φ𝔐,wℓ\(\\mathfrak\{N\},v\)\\models\\varphi\_\{\\mathfrak\{M\},w\}^\{\\ell\}if and only if𝖴𝗇𝗋ℓ​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\)embeds into𝖴𝗇𝗋ℓ​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\)\.

###### Proof\.

We prove the equivalence by induction onℓ\\ell\. Let⪯\\preceqbe the embedding relation between pointed models\.

*Base case \(ℓ=0\\ell=0\)*\. Formulaφ𝔐,w0\\varphi\_\{\\mathfrak\{M\},w\}^\{0\}is a conjunction of all literals \(propositions and their negations\) satisfied at\(𝔐,w\)\(\\mathfrak\{M\},w\)\. Thus,\(𝔑,v\)⊧φ𝔐,w0\(\\mathfrak\{N\},v\)\\models\\varphi\_\{\\mathfrak\{M\},w\}^\{0\}iff\(𝔐,w\)≡0𝒢​ℳ​ℒ\(𝔑,v\)\(\\mathfrak\{M\},w\)\\equiv^\{\\mathcal\{GML\}\}\_\{0\}\(\\mathfrak\{N\},v\)\. Since𝖴𝗇𝗋0​\(𝔐,w\)\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{M\},w\)and𝖴𝗇𝗋0​\(𝔑,v\)\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{N\},v\)consist single worlds, it holds iff𝖴𝗇𝗋0​\(𝔐,w\)⪯𝖴𝗇𝗋0​\(𝔑,v\)\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{M\},w\)\\preceq\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{N\},v\)\.

*Inductive step\.*Assume that the claim holds forℓ≥0\\ell\\geq 0\. We prove that it also holds forℓ\+1\\ell\+1\. Recall thatφ𝔐,wℓ\+1:=φ𝔐,w0∧⋀j=1m◇≥\|Cj\|​φ𝔐,wjℓ\\varphi\_\{\\mathfrak\{M\},w\}^\{\\ell\+1\}\\ :=\\ \\varphi\_\{\\mathfrak\{M\},w\}^\{0\}\\ \\wedge\\ \\bigwedge\_\{j=1\}^\{m\}\\Diamond^\{\\geq\|C\_\{j\}\|\}\\,\\varphi\_\{\\mathfrak\{M\},w\_\{j\}\}^\{\\ell\}, whereC1,…,CmC\_\{1\},\\dots,C\_\{m\}are the equivalence classes ofRR\-successors ofwwunder≡ℓ𝒢​ℳ​ℒ\\equiv^\{\\mathcal\{GML\}\}\_\{\\ell\}, andwj∈Cjw\_\{j\}\\in C\_\{j\}is an arbitrary representative\. For eachjj, we also fix an enumerationCj=\{wj,1,…,wj,\|Cj\|\}C\_\{j\}=\\\{w\_\{j,1\},\\ldots,w\_\{j,\|C\_\{j\}\|\}\\\}\.

*\(⇒\\Rightarrow\)*Assume that\(𝔑,v\)⊧φ𝔐,wℓ\+1\(\\mathfrak\{N\},v\)\\models\\varphi\_\{\\mathfrak\{M\},w\}^\{\\ell\+1\}\. Then,\(𝔑,v\)⊧φ𝔐,w0\(\\mathfrak\{N\},v\)\\models\\varphi\_\{\\mathfrak\{M\},w\}^\{0\}, and hence\(𝔐,w\)≡0𝒢​ℳ​ℒ\(𝔑,v\)\(\\mathfrak\{M\},w\)\\equiv^\{\\mathcal\{GML\}\}\_\{0\}\(\\mathfrak\{N\},v\)\. Moreover, for eachjj, there exist\|Cj\|\|C\_\{j\}\|distinct successorsvj,1,…,vj,\|Cj\|v\_\{j,1\},\\ldots,v\_\{j,\|C\_\{j\}\|\}ofvvsuch that\(𝔑,vj,k\)⊧φ𝔐,wjℓ\(\\mathfrak\{N\},v\_\{j,k\}\)\\models\\varphi\_\{\\mathfrak\{M\},w\_\{j\}\}^\{\\ell\}\.

By the inductive hypothesis, for each suchjjandkk, there exists an embeddingfj,kf\_\{j,k\}from𝖴𝗇𝗋ℓ​\(𝔐,wj\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\_\{j\}\)into𝖴𝗇𝗋ℓ​\(𝔑,vj,k\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\_\{j,k\}\)\. Sincewj,k≡ℓ𝒢​ℳ​ℒwjw\_\{j,k\}\\equiv^\{\\mathcal\{GML\}\}\_\{\\ell\}w\_\{j\}, the unravellings𝖴𝗇𝗋ℓ​\(𝔐,wj,k\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\_\{j,k\}\)and𝖴𝗇𝗋ℓ​\(𝔐,wj\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\_\{j\}\)are isomorphic\. Composing this isomorphism withfj,kf\_\{j,k\}yields an embedding of𝖴𝗇𝗋ℓ​\(𝔐,wj,k\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\_\{j,k\}\)into𝖴𝗇𝗋ℓ​\(𝔑,vj,k\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\_\{j,k\}\)\.

We now construct a global embeddingfffrom𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)into𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)as follows\. Functionffmaps the root of𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)to the root of𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)\. For eachjjandkk,ffcoincides with the embedding constructed above on the subtree rooted at the node corresponding towj,kw\_\{j,k\}\. Since the successorsvj,kv\_\{j,k\}are pairwise distinct, the images of these embeddings are disjoint\. It follows thatffis an embedding of𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)into𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)\.

*\(⇐\\Leftarrow\)*Conversely, assume thatffis an embedding of𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)into𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)\. Then,ffmaps the root of𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)to the root of𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\), and therefore,\(𝔐,w\)≡0𝒢​ℳ​ℒ\(𝔑,v\)\(\\mathfrak\{M\},w\)\\equiv^\{\\mathcal\{GML\}\}\_\{0\}\(\\mathfrak\{N\},v\)\. Thus,\(𝔑,v\)⊧φ𝔐,w0\(\\mathfrak\{N\},v\)\\models\\varphi\_\{\\mathfrak\{M\},w\}^\{0\}\. Fixj∈\{1,…,m\}j\\in\\\{1,\\ldots,m\\\}\. By the definition of unravelling, the root of𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)has exactly\|Cj\|\|C\_\{j\}\|distinct nodes at depth11corresponding to the successorswj,1,…,wj,\|Cj\|w\_\{j,1\},\\dots,w\_\{j,\|C\_\{j\}\|\}ofww\. Sinceffis injective, it maps these nodes to\|Cj\|\|C\_\{j\}\|distinct nodes at depth11in𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)\. Each such node corresponds to a successorvj,kv\_\{j,k\}ofvvin𝔑\\mathfrak\{N\}, and the subtree below this node is precisely𝖴𝗇𝗋ℓ​\(𝔑,vj,k\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\_\{j,k\}\)\. Restrictingffto the corresponding subtrees yields embeddings, so𝖴𝗇𝗋ℓ​\(𝔐,wj,k\)⪯𝖴𝗇𝗋ℓ​\(𝔑,vj,k\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\_\{j,k\}\)\\preceq\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\_\{j,k\}\)fork=1,…,\|Cj\|k=1,\\dots,\|C\_\{j\}\|\. By the inductive hypothesis, this implies\(𝔑,vj,k\)⊧φ𝔐,wj,kℓ\(\\mathfrak\{N\},v\_\{j,k\}\)\\models\\varphi\_\{\\mathfrak\{M\},w\_\{j,k\}\}^\{\\ell\}\. Since eachwj,k∈Cjw\_\{j,k\}\\in C\_\{j\}, we obtain thatφ𝔐,wj,kℓ\\varphi\_\{\\mathfrak\{M\},w\_\{j,k\}\}^\{\\ell\}is identical toφ𝔐,wjℓ\\varphi\_\{\\mathfrak\{M\},w\_\{j\}\}^\{\\ell\}\. Moreover, the worldsvj,kv\_\{j,k\}are pairwise distinct successors ofvv\. Hence,\(𝔑,v\)⊧◇≥\|Cj\|​φ𝔐,wjℓ\(\\mathfrak\{N\},v\)\\models\\Diamond^\{\\geq\|C\_\{j\}\|\}\\,\\varphi\_\{\\mathfrak\{M\},w\_\{j\}\}^\{\\ell\}, as required\. ∎

Equipped with[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1)and[Section˜4\.4](https://arxiv.org/html/2606.17882#S4.SS4), we are now ready to prove the preservation theorem for classes of models preserved under embeddings and invariant underLL\-unravelling\. As we show below, these are exactly the classes definable by∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\- of modal depth at mostLL\.

###### Theorem\\thethm\.

The following are equivalent for any class𝒞\\mathcal\{C\}of pointed models and anyL∈ℕL\\in\\mathbb\{N\}:

- •𝒞\\mathcal\{C\}is invariant underLL\-unravelling and preserved under embeddings,
- •𝒞\\mathcal\{C\}is definable by an∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}formula of depth at mostLL\.

###### Proof\.

*\(⇒\\Rightarrow\)*Let𝒯=\{𝖴𝗇𝗋L​\(𝔐,w\)∣\(𝔐,w\)∈𝒞\}\\mathcal\{T\}=\\\{\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)\\mid\(\\mathfrak\{M\},w\)\\in\\mathcal\{C\}\\\}and let⪯\\preceqbe the embedding relation\. Since𝒞\\mathcal\{C\}is invariant underLL\-unravelling, we have that𝒯⊆𝒞\\mathcal\{T\}\\subseteq\\mathcal\{C\}\. By[Section˜4\.4](https://arxiv.org/html/2606.17882#S4.SS4),\(𝒯,⪯\)\(\\mathcal\{T\},\\preceq\)is a wqo and therefore admits only finitely many⪯\\preceq\-minimal elements up to isomorphism\. Let𝒯𝗆𝗂𝗇\\mathcal\{T\}\_\{\\mathsf\{min\}\}contain exactly one representative for each such minimal isomorphism type\. For each\(𝔗,v\)∈𝒯𝗆𝗂𝗇\(\\mathfrak\{T\},v\)\\in\\mathcal\{T\}\_\{\\mathsf\{min\}\}, we construct the∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}characteristic formulaφ𝔗,vL\\varphi\_\{\\mathfrak\{T\},v\}^\{L\}and defineφ𝒞=⋁\(𝔗,v\)∈𝒯𝗆𝗂𝗇φ𝔗,vL\\varphi\_\{\\mathcal\{C\}\}=\\bigvee\_\{\(\\mathfrak\{T\},v\)\\in\\mathcal\{T\}\_\{\\mathsf\{min\}\}\}\\varphi\_\{\\mathfrak\{T\},v\}^\{L\}\. Since the disjunction is finite and eachφ𝔗,vL\\varphi\_\{\\mathfrak\{T\},v\}^\{L\}is an∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\-formula,φ𝒞\\varphi\_\{\\mathcal\{C\}\}is a \(finite\)∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\-formula\. We show thatφ𝒞\\varphi\_\{\\mathcal\{C\}\}defines𝒞\\mathcal\{C\}\.

Let\(𝔐,w\)∈𝒞\(\\mathfrak\{M\},w\)\\in\\mathcal\{C\}\. Then𝖴𝗇𝗋L​\(𝔐,w\)∈𝒯\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)\\in\\mathcal\{T\}\. Since\(𝒯,⪯\)\(\\mathcal\{T\},\\preceq\)is a wqo, there exists a⪯\\preceq\-minimal element\(𝔗,v\)∈𝒯𝗆𝗂𝗇\(\\mathfrak\{T\},v\)\\in\\mathcal\{T\}\_\{\\mathsf\{min\}\}such that\(𝔗,v\)⪯𝖴𝗇𝗋L​\(𝔐,w\)\(\\mathfrak\{T\},v\)\\preceq\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)\. Because\(𝔗,v\)\(\\mathfrak\{T\},v\)is tree\-shaped of height at mostLL, we have𝖴𝗇𝗋L​\(𝔗,v\)=\(𝔗,v\)\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{T\},v\)=\(\\mathfrak\{T\},v\)\. Hence,𝖴𝗇𝗋L​\(𝔗,v\)⪯𝖴𝗇𝗋L​\(𝔐,w\)\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{T\},v\)\\preceq\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)and by[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1)we obtain\(𝔐,w\)⊧φ𝔗,vL\(\\mathfrak\{M\},w\)\\models\\varphi\_\{\\mathfrak\{T\},v\}^\{L\}\. It follows that\(𝔐,w\)⊧φ𝒞\(\\mathfrak\{M\},w\)\\models\\varphi\_\{\\mathcal\{C\}\}\.

Conversely, suppose that\(𝔐,w\)⊧φ𝒞\(\\mathfrak\{M\},w\)\\models\\varphi\_\{\\mathcal\{C\}\}\. Then,\(𝔐,w\)⊧φ𝔗,vL\(\\mathfrak\{M\},w\)\\models\\varphi\_\{\\mathfrak\{T\},v\}^\{L\}for some\(𝔗,v\)∈𝒯𝗆𝗂𝗇\(\\mathfrak\{T\},v\)\\in\\mathcal\{T\}\_\{\\mathsf\{min\}\}\. By[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1), this implies𝖴𝗇𝗋L​\(𝔗,v\)⪯𝖴𝗇𝗋L​\(𝔐,w\)\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{T\},v\)\\preceq\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)\. Since\(𝔗,v\)\(\\mathfrak\{T\},v\)is tree\-shaped of height at mostLL, we again have𝖴𝗇𝗋L​\(𝔗,v\)=\(𝔗,v\)\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{T\},v\)=\(\\mathfrak\{T\},v\), and hence\(𝔗,v\)⪯𝖴𝗇𝗋L​\(𝔐,w\)\(\\mathfrak\{T\},v\)\\preceq\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)\. By construction,𝒯𝗆𝗂𝗇⊆𝒯⊆𝒞\\mathcal\{T\}\_\{\\mathsf\{min\}\}\\subseteq\\mathcal\{T\}\\subseteq\\mathcal\{C\}, so\(𝔗,v\)∈𝒞\(\\mathfrak\{T\},v\)\\in\\mathcal\{C\}\. Since𝒞\\mathcal\{C\}is preserved under embeddings, we have𝖴𝗇𝗋L​\(𝔐,w\)∈𝒞\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)\\in\\mathcal\{C\}\. Finally, invariance of𝒞\\mathcal\{C\}underLL\-unravelling yields\(𝔐,w\)∈𝒞\(\\mathfrak\{M\},w\)\\in\\mathcal\{C\}\.

*\(⇐\\Leftarrow\)*Suppose that𝒞\\mathcal\{C\}is definable by an∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\-formulaφ\\varphiof depth at mostLL\. Then𝒞\\mathcal\{C\}is invariant underLL\-unravellings: for every pointed model,\(𝔐,w\)⊧φ\(\\mathfrak\{M\},w\)\\models\\varphiif and only if𝖴𝗇𝗋L​\(𝔐,w\)⊧φ\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)\\models\\varphisince the truth ofφ\\varphidepends only on the unravelling up to depthLL\. We argue that𝒞\\mathcal\{C\}is also preserved under embeddings\. Let\(𝔐,w\)⊧φ\(\\mathfrak\{M\},w\)\\models\\varphiand suppose that there exists an embedding witnessing\(𝔐,w\)⪯\(𝔑,v\)\(\\mathfrak\{M\},w\)\\preceq\(\\mathfrak\{N\},v\)\. Since embeddings preserve propositional labels and map successors injectively, a routine induction on the structure ofφ\\varphishows that\(𝔑,v\)⊧φ\(\\mathfrak\{N\},v\)\\models\\varphi\. In particular, for each subformula of the form◇≥k​ψ\\Diamond^\{\\geq k\}\\psioccurring inφ\\varphi, the existence ofkksuccessors satisfyingψ\\psiin\(𝔐,w\)\(\\mathfrak\{M\},w\)implies the existence ofkksuccessors satisfyingψ\\psiin\(𝔑,v\)\(\\mathfrak\{N\},v\)\. Thus,𝒞\\mathcal\{C\}is preserved under embeddings\. ∎

### B\.2Preservation Under Injective Homomorphisms

We next characterise unravelling\-invariant classes that are preserved under injective homomorphisms\. Recall that every embedding is an injective homomorphism, but not conversely\. This suggests that the logical language defining classes preserved under injective homomorphisms should be strictly weaker than the one required for preservation under embeddings\. By[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1), the latter language is∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\. As we show next, the appropriate language in the case of injective homomorphisms is∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}, the existential\-positive fragment of𝒢​ℳ​ℒ\\mathcal\{GML\}\.

We first define characteristic∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}\-, obtained from the characteristic∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}by deleting all negative literals\.

###### Definition\\thethm\.

Let\(𝔐,w\)\(\\mathfrak\{M\},w\)be a pointed model with𝔐=\(W,R,V\)\\mathfrak\{M\}=\(W,R,V\)\. The*characteristic∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}\-formula*ψ𝔐,wℓ\\psi\_\{\\mathfrak\{M\},w\}^\{\\ell\}of depthℓ\\ellis defined as the formula obtained from the characteristic∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\-formulaφ𝔐,wℓ\\varphi\_\{\\mathfrak\{M\},w\}^\{\\ell\}\(see[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1)\) by removing all negative literals¬p\\neg p\.

Note thatψ𝔐,wℓ\\psi\_\{\\mathfrak\{M\},w\}^\{\\ell\}is defined in the same way asφ𝔐,wℓ\\varphi\_\{\\mathfrak\{M\},w\}^\{\\ell\}, except that the conjunction⋀\{¬p∣\(𝔐,w\)⊧̸p\}\\bigwedge\\\{\\neg p\\mid\(\\mathfrak\{M\},w\)\\not\\models p\\\}is omitted\. As a result,ψ𝔐,wℓ\\psi\_\{\\mathfrak\{M\},w\}^\{\\ell\}contains no negations and is therefore an∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}\-formula\.

Whileφ𝔐,wℓ\\varphi\_\{\\mathfrak\{M\},w\}^\{\\ell\}guarantees the existence of an embedding betweenℓ\\ell\-unravellings of models, the formulaψ𝔐,wℓ\\psi\_\{\\mathfrak\{M\},w\}^\{\\ell\}guarantees the existence of an injective homomorphism between these unravellings\. This is captured by the following lemma\.

###### Lemma\\thethm\.

Let\(𝔐,w\)\(\\mathfrak\{M\},w\)and\(𝔑,v\)\(\\mathfrak\{N\},v\)be pointed models and letℓ∈ℕ\\ell\\in\\mathbb\{N\}\. Then,\(𝔑,v\)⊧ψ𝔐,wℓ\(\\mathfrak\{N\},v\)\\models\\psi\_\{\\mathfrak\{M\},w\}^\{\\ell\}if and only if there exists an injective homomorphism from𝖴𝗇𝗋ℓ​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\)to𝖴𝗇𝗋ℓ​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\)\.

###### Proof\.

The proof is by induction onℓ\\elland closely parallels the proof of Lemma[B\.1](https://arxiv.org/html/2606.17882#A2.SS1); we highlight only the points where injective homomorphisms replace embeddings\. Throughout this proof, let⪯\\preceqbe the injective homomorphism relation\.

*Base case \(ℓ=0\\ell=0\)\.*The formulaψ𝔐,w0\\psi^\{0\}\_\{\\mathfrak\{M\},w\}is the conjunction of all propositional symbols satisfied atww\. Thus,\(𝔑,v\)⊧ψ𝔐,w0\(\\mathfrak\{N\},v\)\\models\\psi^\{0\}\_\{\\mathfrak\{M\},w\}if and only if\(𝔑,v\)\(\\mathfrak\{N\},v\)satisfies at least the same propositions as\(𝔐,w\)\(\\mathfrak\{M\},w\)\. Since𝖴𝗇𝗋0​\(𝔐,w\)\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{M\},w\)and𝖴𝗇𝗋0​\(𝔑,v\)\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{N\},v\)each consist of a single world, this holds if and only if𝖴𝗇𝗋0​\(𝔐,w\)⪯𝖴𝗇𝗋0​\(𝔑,v\)\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{M\},w\)\\preceq\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{N\},v\)\.

*Inductive step\.*Assume that the claim holds for someℓ≥0\\ell\\geq 0, and considerℓ\+1\\ell\+1\. We use the same notation as in the proof of[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1)\.

*\(⇒\\Rightarrow\)*Assume that\(𝔑,v\)⊧ψ𝔐,wℓ\+1\(\\mathfrak\{N\},v\)\\models\\psi^\{\\ell\+1\}\_\{\\mathfrak\{M\},w\}\. Then\(𝔑,v\)⊧ψ𝔐,w0\(\\mathfrak\{N\},v\)\\models\\psi^\{0\}\_\{\\mathfrak\{M\},w\}, and for each equivalence classCjC\_\{j\}, there exist\|Cj\|\|C\_\{j\}\|distinct successorsvj,1,…,vj,\|Cj\|v\_\{j,1\},\\dots,v\_\{j,\|C\_\{j\}\|\}ofvvsuch that\(𝔑,vj,k\)⊧ψ𝔐,wjℓ\(\\mathfrak\{N\},v\_\{j,k\}\)\\models\\psi^\{\\ell\}\_\{\\mathfrak\{M\},w\_\{j\}\}\. By the inductive hypothesis, for eachj,kj,k, there exists an injective homomorphism and hence𝖴𝗇𝗋ℓ​\(𝔐,wj\)⪯𝖴𝗇𝗋ℓ​\(𝔑,vj,k\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\_\{j\}\)\\preceq\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\_\{j,k\}\)\. As in the proof of[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1), these homomorphisms can be combined together into a single injective homomorphism from𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)to𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)by mapping the roots and using the homomorphisms above on the corresponding subtrees\. Since the targets lie in pairwise disjoint subtrees rooted at distinct depth\-11nodes, the resulting homomorphism is injective\. Thus,𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)⪯𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)\\preceq\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)\.

*\(⇐\\Leftarrow\)*Conversely, suppose that there exists an injective homomorphismfffrom𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)to𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)\. Thenffmaps the root to the root, which implies\(𝔑,v\)⊧ψ𝔐,w0\(\\mathfrak\{N\},v\)\\models\\psi^\{0\}\_\{\\mathfrak\{M\},w\}\. Fixj∈\{1,…,m\}j\\in\\\{1,\\ldots,m\\\}\. Injectivity offfforces the\|Cj\|\|C\_\{j\}\|distinct depth\-11nodes below the root of𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)to be mapped to∣Cj∣\\mid C\_\{j\}\\middistinct nodes of depth 1 of𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)\. Each such node corresponds to a successorvj,kv\_\{j,k\}ofvvin𝔑\\mathfrak\{N\}\. Restrictingffto the corresponding subtrees yields injective homomorphisms from𝖴𝗇𝗋ℓ​\(𝔐,wj,k\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\_\{j,k\}\)to𝖴𝗇𝗋ℓ​\(𝔑,vj,k\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\_\{j,k\}\)\. By the induction hypothesis we obtain\(𝔑,vj,k\)⊧ψ𝔐,wjℓ\(\\mathfrak\{N\},v\_\{j,k\}\)\\models\\psi^\{\\ell\}\_\{\\mathfrak\{M\},w\_\{j\}\}for allkk\. Since the worldsvj,kv\_\{j,k\}are pairwise distinct successors ofvv, we conclude that\(𝔑,v\)⊧◇≥\|Cj\|​ψ𝔐,wjℓ\(\\mathfrak\{N\},v\)\\models\\Diamond^\{\\geq\|C\_\{j\}\|\}\\psi^\{\\ell\}\_\{\\mathfrak\{M\},w\_\{j\}\}\. As this holds for eachjj,\(𝔑,v\)⊧ψ𝔐,wℓ\+1\(\\mathfrak\{N\},v\)\\models\\psi^\{\\ell\+1\}\_\{\\mathfrak\{M\},w\}\. ∎

Using the results above on characteristic∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\-, we can now establish the following preservation theorem for unravelling\-invariant classes preserved under injective homomorphisms\.

###### Theorem\\thethm\.

The following are equivalent for any class𝒞\\mathcal\{C\}of pointed models and anyL∈ℕL\\in\\mathbb\{N\}:

- •𝒞\\mathcal\{C\}is preserved under injective homomorphisms and invariant underLL\-unravelling,
- •𝒞\\mathcal\{C\}is definable by an∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}\-formula of depth at mostLL\.

###### Proof\.

The proof follows the same strategy as that of Theorem[B\.1](https://arxiv.org/html/2606.17882#A2.SS1), but now exploits[Section˜B\.2](https://arxiv.org/html/2606.17882#A2.SS2)instead of[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1)\.

*\(⇒\\Rightarrow\)*Let𝒯=\{𝖴𝗇𝗋L​\(𝔐,w\)∣\(𝔐,w\)∈𝒞\}\\mathcal\{T\}=\\\{\\,\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)\\mid\(\\mathfrak\{M\},w\)\\in\\mathcal\{C\}\\,\\\}and let⪯\\preceqbe the injective homomorphism relation\. Since𝒞\\mathcal\{C\}is invariant underLL\-unravellings, we have𝒯⊆𝒞\\mathcal\{T\}\\subseteq\\mathcal\{C\}\. By[Section˜4\.4](https://arxiv.org/html/2606.17882#S4.SS4),\(𝒯,⪯\)\(\\mathcal\{T\},\\preceq\)is a wqo and hence admits only finitely many⪯\\preceq\-minimal elements up to isomorphism\. Let𝒯𝗆𝗂𝗇\\mathcal\{T\}\_\{\\mathsf\{min\}\}contain one representative for each such minimal isomorphism type\. For each\(𝔗,v\)∈𝒯𝗆𝗂𝗇\(\\mathfrak\{T\},v\)\\in\\mathcal\{T\}\_\{\\mathsf\{min\}\}, we construct the∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}characteristic formulaψ𝔗,vL\\psi\_\{\\mathfrak\{T\},v\}^\{L\}and defineψ𝒞=⋁\(𝔗,v\)∈𝒯𝗆𝗂𝗇ψ𝔗,vL\\psi\_\{\\mathcal\{C\}\}=\\bigvee\_\{\(\\mathfrak\{T\},v\)\\in\\mathcal\{T\}\_\{\\mathsf\{min\}\}\}\\psi\_\{\\mathfrak\{T\},v\}^\{L\}\. The argument showing thatψ𝒞\\psi\_\{\\mathcal\{C\}\}defines𝒞\\mathcal\{C\}is identical to the corresponding one in the proof of[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1), with[Section˜B\.2](https://arxiv.org/html/2606.17882#A2.SS2)used in place of[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1)\.

*\(⇐\\Leftarrow\)*Suppose that𝒞\\mathcal\{C\}is definable by an∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}\-formulaφ\\varphiof depth at mostLL\. Then𝒞\\mathcal\{C\}is invariant underLL\-unravellings: for every pointed model\(𝔐,w\)\(\\mathfrak\{M\},w\),\(𝔐,w\)⊧φ\(\\mathfrak\{M\},w\)\\models\\varphiif and only if𝖴𝗇𝗋L​\(𝔐,w\)⊧φ\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)\\models\\varphi\. We now show that𝒞\\mathcal\{C\}is preserved under injective homomorphisms\. Let\(𝔐,w\)⊧φ\(\\mathfrak\{M\},w\)\\models\\varphiand letffbe an injective homomorphism witnessing\(𝔐,w\)⪯\(𝔑,v\)\(\\mathfrak\{M\},w\)\\preceq\(\\mathfrak\{N\},v\)\. Since injective homomorphisms preserve propositional labels monotonically and map successors injectively, a routine induction on the structure ofφ\\varphishows that\(𝔑,v\)⊧φ\(\\mathfrak\{N\},v\)\\models\\varphi, exactly as in the proof of Theorem[B\.1](https://arxiv.org/html/2606.17882#A2.SS1)\. ∎

It is worth noting that logics corresponding to both𝒢​ℳ​ℒ\\mathcal\{GML\}and∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}have been studied extensively in the setting of description logics in knowledge representation and reasoning\. In particular, the description logic corresponding to𝒢​ℳ​ℒ\\mathcal\{GML\}is𝒜​ℒ​𝒞​𝒬\\mathcal\{ALCQ\}\[[3](https://arxiv.org/html/2606.17882#bib.bib62)\], while the logic corresponding to∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}isℰ​ℒ​𝒰​𝒬\\mathcal\{ELUQ\}\[[20](https://arxiv.org/html/2606.17882#bib.bib11)\]\.

### B\.3Preservation Under Homomorphisms

We now turn to classes preserved under homomorphisms\. We show that if such a class is invariant under unravelling, then it is definable by existential\-positive modal logic \(∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\)\. Our proof strategy follows the same general pattern as in the cases of embeddings and injective homomorphisms\. In particular, we define an appropriate form of characteristic∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\-\.

###### Definition\\thethm\.

Let\(𝔐,w\)\(\\mathfrak\{M\},w\)be a pointed model with𝔐=\(W,R,V\)\\mathfrak\{M\}=\(W,R,V\), the*characteristic∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\-formula*χ𝔐,wℓ\\chi\_\{\\mathfrak\{M\},w\}^\{\\ell\}of depthℓ\\ellis defined as the formula obtained from the characteristic∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\-formulaφ𝔐,wℓ\\varphi\_\{\\mathfrak\{M\},w\}^\{\\ell\}\(see[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1)\) by removing all negative literals¬p\\neg pand replacing each graded modal operator◇≥k\\Diamond^\{\\geq k\}with the basic modal operator◇\\Diamond\.

Characteristic∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\- are related to homomorphisms between unravellings by the following lemma\.

###### Lemma\\thethm\.

Let\(𝔐,w\)\(\\mathfrak\{M\},w\)and\(𝔑,v\)\(\\mathfrak\{N\},v\)be pointed models and letℓ∈ℕ\\ell\\in\\mathbb\{N\}\. Then,\(𝔑,v\)⊧χ𝔐,wℓ\(\\mathfrak\{N\},v\)\\models\\chi\_\{\\mathfrak\{M\},w\}^\{\\ell\}if and only if𝖴𝗇𝗋ℓ​\(𝔐,w\)⪯𝖴𝗇𝗋ℓ​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\)\\preceq\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\), where⪯\\preceqdenotes the homomorphism relation\.

###### Proof\.

The proof is by induction onℓ\\ell\.

*Base case \(ℓ=0\\ell=0\)\.*The formulaχ𝔐,w0\\chi^\{0\}\_\{\\mathfrak\{M\},w\}is a conjunction of propositional symbols satisfied atww\. Thus,\(𝔑,v\)⊧χ𝔐,w0\(\\mathfrak\{N\},v\)\\models\\chi^\{0\}\_\{\\mathfrak\{M\},w\}if and only if\(𝔑,v\)\(\\mathfrak\{N\},v\)satisfies at least the same propositional symbols as\(𝔐,w\)\(\\mathfrak\{M\},w\)\. Since𝖴𝗇𝗋0​\(𝔐,w\)\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{M\},w\)and𝖴𝗇𝗋0​\(𝔑,v\)\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{N\},v\)each consist of a single world, this holds if and only if𝖴𝗇𝗋0​\(𝔐,w\)⪯𝖴𝗇𝗋0​\(𝔑,v\)\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{M\},w\)\\preceq\\mathsf\{Unr\}^\{0\}\(\\mathfrak\{N\},v\)\.

*Inductive step\.*Assume that the claim holds for someℓ≥0\\ell\\geq 0, and considerℓ\+1\\ell\+1\. We use the same notation as in the proof of[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1)\.

*\(⇒\\Rightarrow\)*Let\(𝔑,v\)⊧χ𝔐,wℓ\+1\(\\mathfrak\{N\},v\)\\models\\chi^\{\\ell\+1\}\_\{\\mathfrak\{M\},w\}\. Then, for each equivalence classCjC\_\{j\}of successors ofwwin𝔐\\mathfrak\{M\}, there exists at least one successorvjv\_\{j\}ofvvin𝔑\\mathfrak\{N\}such that\(𝔑,vj\)⊧χ𝔐,wjℓ\(\\mathfrak\{N\},v\_\{j\}\)\\models\\chi^\{\\ell\}\_\{\\mathfrak\{M\},w\_\{j\}\}\. By the inductive hypothesis, for eachjj,𝖴𝗇𝗋ℓ​\(𝔐,wj\)⪯𝖴𝗇𝗋ℓ​\(𝔑,vj\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\_\{j\}\)\\preceq\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\_\{j\}\)\. The unravelling𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)consists of the root together with subtrees rooted at depth\-11nodes corresponding to the successors ofww\. Since homomorphisms need not be injective, all depth\-11nodes corresponding to successors in the same classCjC\_\{j\}may be mapped to the same depth\-11node corresponding tovjv\_\{j\}\. Mapping the root to the root and using the homomorphisms above on the corresponding subtrees yields a homomorphism from𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)to𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)\.

*\(⇐\\Leftarrow\)*Letffbe a homomorphism from𝖴𝗇𝗋ℓ\+1​\(𝔐,w\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{M\},w\)to𝖴𝗇𝗋ℓ\+1​\(𝔑,v\)\\mathsf\{Unr\}^\{\\ell\+1\}\(\\mathfrak\{N\},v\)\. Then,ffmaps the root to the root, implying\(𝔑,v\)⊧χ𝔐,w0\(\\mathfrak\{N\},v\)\\models\\chi\_\{\\mathfrak\{M\},w\}^\{0\}\. Fix an equivalence classCjC\_\{j\}\. Every depth\-11node corresponding to a successorwjw\_\{j\}ofwwmust be mapped byffto some depth\-11node corresponding to a successorvjv\_\{j\}ofvv\. Restrictingffto the corresponding subtree yields a homomorphism𝖴𝗇𝗋ℓ​\(𝔐,wj\)→𝖴𝗇𝗋ℓ​\(𝔑,vj\)\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{M\},w\_\{j\}\)\\to\\mathsf\{Unr\}^\{\\ell\}\(\\mathfrak\{N\},v\_\{j\}\)and by the inductive hypothesis we obtain\(𝔑,vj\)⊧χ𝔐,wjℓ\(\\mathfrak\{N\},v\_\{j\}\)\\models\\chi^\{\\ell\}\_\{\\mathfrak\{M\},w\_\{j\}\}\. Hence,\(𝔑,v\)⊧◇​χ𝔐,wjℓ\(\\mathfrak\{N\},v\)\\models\\Diamond\\chi^\{\\ell\}\_\{\\mathfrak\{M\},w\_\{j\}\}for eachjjand therefore\(𝔑,v\)⊧χ𝔐,wℓ\+1\(\\mathfrak\{N\},v\)\\models\\chi^\{\\ell\+1\}\_\{\\mathfrak\{M\},w\}\. ∎

The preceding result allows us to establish the homomorphism preservation theorem for unravelling\-invariant classes\.

###### Theorem\\thethm\.

The following are equivalent for any class𝒞\\mathcal\{C\}of pointed models and anyL∈ℕL\\in\\mathbb\{N\}:

- •𝒞\\mathcal\{C\}is preserved under homomorphisms and invariant underLL\-unravelling,
- •𝒞\\mathcal\{C\}is definable by an∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\-formula of depth at mostLL\.

###### Proof\.

The proof follows the same general strategy as that of[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1), but now uses[Section˜B\.3](https://arxiv.org/html/2606.17882#A2.SS3)in place of[Section˜B\.1](https://arxiv.org/html/2606.17882#A2.SS1)\.

*\(⇒\\Rightarrow\)*Let𝒯=\{𝖴𝗇𝗋L​\(𝔐,w\)∣\(𝔐,w\)∈𝒞\}\\mathcal\{T\}=\\\{\\,\\mathsf\{Unr\}^\{L\}\(\\mathfrak\{M\},w\)\\mid\(\\mathfrak\{M\},w\)\\in\\mathcal\{C\}\\,\\\}\. Since𝒞\\mathcal\{C\}is invariant underLL\-unravelling, we have𝒯⊆𝒞\\mathcal\{T\}\\subseteq\\mathcal\{C\}\. Let𝒯𝗆𝗂𝗇⊆𝒯\\mathcal\{T\}\_\{\\mathsf\{min\}\}\\subseteq\\mathcal\{T\}be a set of representatives of the homomorphism\-minimal elements of𝒯\\mathcal\{T\}\. By[Section˜4\.4](https://arxiv.org/html/2606.17882#S4.SS4),𝒯𝗆𝗂𝗇\\mathcal\{T\}\_\{\\mathsf\{min\}\}is finite \(alternatively, finiteness also follows from the fact that there are only finitely manyℳ​ℒ\\mathcal\{ML\}\-inequivalent of depth at mostLL\)\. For each\(𝔗,v\)∈𝒯𝗆𝗂𝗇\(\\mathfrak\{T\},v\)\\in\\mathcal\{T\}\_\{\\mathsf\{min\}\}, letχ𝔗,vL\\chi^\{L\}\_\{\\mathfrak\{T\},v\}be its characteristic∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\-formula and defineχ𝒞=⋁\(𝔗,v\)∈𝒯𝗆𝗂𝗇χ𝔗,vL\\chi\_\{\\mathcal\{C\}\}=\\bigvee\_\{\(\\mathfrak\{T\},v\)\\in\\mathcal\{T\}\_\{\\mathsf\{min\}\}\}\\chi^\{L\}\_\{\\mathfrak\{T\},v\}, which is a finite∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\-formula of depth at mostLL\.

By construction,χ𝒞\\chi\_\{\\mathcal\{C\}\}holds in every model in𝒯𝗆𝗂𝗇\\mathcal\{T\}\_\{\\mathsf\{min\}\}and by[Section˜B\.3](https://arxiv.org/html/2606.17882#A2.SS3)it therefore holds in all models in𝒯\\mathcal\{T\}\. Since𝒞\\mathcal\{C\}is invariant underLL\-unravelling, it follows thatχ𝒞\\chi\_\{\\mathcal\{C\}\}defines𝒞\\mathcal\{C\}\.

*\(⇐\\Leftarrow\)*Suppose that𝒞\\mathcal\{C\}is definable by an∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\-formulaφ\\varphiof depth at mostLL\. Sinceφ\\varphiis positive, the standard translation yields an existential\-positive first\-order logic formula\. Such are preserved under homomorphisms\[[25](https://arxiv.org/html/2606.17882#bib.bib20)\]\. Moreover, sinceφ\\varphihas depth at mostLL, it is invariant underLL\-unravelling\. ∎

## Appendix CProofs for[Section˜5](https://arxiv.org/html/2606.17882#S5)

See[5](https://arxiv.org/html/2606.17882#S5)

###### Proof\.

We will show each of the three claims separately\. We start from MGNNs, then considerMAX\\mathrm\{MAX\}\-MGNNs, and finally show the result for augmented MGNNs\.

Claim 1\.MGNNs are preserved under injective homomorphisms\.

Leth:\(G,v\)→\(G′,v′\)h\\colon\(G,v\)\\to\(G^\{\\prime\},v^\{\\prime\}\)be an injective homomorphism between pointed graphs, and let𝒩\\mathcal\{N\}be anLLlayer MGNN such that𝒩​\(G,v\)=1\\mathcal\{N\}\(G,v\)=1\. We will show that𝒩​\(G′,v′\)=1\\mathcal\{N\}\(G^\{\\prime\},v^\{\\prime\}\)=1\.

Since𝒩\\mathcal\{N\}is monotonic, its classification function is non\-decreasing, so it suffices to show thatλ\(L\)​\(v\)≤λ\(L\)​\(v′\)\\lambda^\{\(L\)\}\(v\)\\leq\\lambda^\{\(L\)\}\(v^\{\\prime\}\)\. To this end, we prove by induction onℓ≤L\\ell\\leq Lthatλ\(ℓ\)​\(w\)≤λ\(ℓ\)​\(h​\(w\)\)\\lambda^\{\(\\ell\)\}\(w\)\\leq\\lambda^\{\(\\ell\)\}\(h\(w\)\), for every nodewwinGG\.

Forℓ=0\\ell=0, we observe thathhpreserves node labels, soλ\(0\)​\(w\)≤λ\(0\)​\(h​\(w\)\)\\lambda^\{\(0\)\}\(w\)\\leq\\lambda^\{\(0\)\}\(h\(w\)\)\. For the inductive step, assume the claim holds forℓ<L\\ell<L\. Sincehhis an injective homomorphism, it induces an injection from the multiset of neighbours ofwwinGGto the multiset of neighbours ofh​\(w\)h\(w\)inG′G^\{\\prime\}\. By the induction hypothesis, this yields\{\|λ\(ℓ\)\(u\)∣u∈NG\(w\)\|\}≤\{\|λ\(ℓ\)\(u′\)∣u′∈NG′\(h\(w\)\)\|\}\\mathopen\{\\\{\\mkern\-3\.0mu\|\}\\lambda^\{\(\\ell\)\}\(u\)\\mid u\\in N\_\{G\}\(w\)\\mathclose\{\|\\mkern\-3\.0mu\\\}\}\\leq\\mathopen\{\\\{\\mkern\-3\.0mu\|\}\\lambda^\{\(\\ell\)\}\(u^\{\\prime\}\)\\mid u^\{\\prime\}\\in N\_\{G^\{\\prime\}\}\(h\(w\)\)\\mathclose\{\|\\mkern\-3\.0mu\\\}\}\. By monotonicity of the aggregation and combination functions, we conclude thatλ\(ℓ\+1\)​\(w\)≤λ\(ℓ\+1\)​\(h​\(w\)\)\\lambda^\{\(\\ell\+1\)\}\(w\)\\leq\\lambda^\{\(\\ell\+1\)\}\(h\(w\)\)\.

Claim 2\.MAX\\mathrm\{MAX\}\-MGNNs are preserved under homomorphisms\.

The proof follows the same general structure as in the case of MGNNs\. Leth:\(G,v\)→\(G′,v′\)h\\colon\(G,v\)\\to\(G^\{\\prime\},v^\{\\prime\}\)be a homomorphism between pointed graphs, and let𝒩\\mathcal\{N\}be anLLlayerMAX\\mathrm\{MAX\}\-MGNN with𝒩​\(G,v\)=1\\mathcal\{N\}\(G,v\)=1\. We need to show that𝒩​\(G′,v′\)=1\\mathcal\{N\}\(G^\{\\prime\},v^\{\\prime\}\)=1\. As before it suffices to prove by induction onℓ≤L\\ell\\leq Lthatλ\(ℓ\)​\(w\)≤λ\(ℓ\)​\(h​\(w\)\)\\lambda^\{\(\\ell\)\}\(w\)\\leq\\lambda^\{\(\\ell\)\}\(h\(w\)\), for each nodewwinGG\.

Forℓ=0\\ell=0the inequality holdshh, as a homomorphism, preserves node labels\. For the inductive step, assume the claim holds forℓ<L\\ell<L\. Sincehhis a homomorphism, each neighbouruuofwwinGGis mapped to a neighbourh​\(u\)h\(u\)ofh​\(w\)h\(w\)inG′G^\{\\prime\}\. By the induction hypothesis,λ\(ℓ\)​\(u\)≤λ\(ℓ\)​\(h​\(u\)\)\\lambda^\{\(\\ell\)\}\(u\)\\leq\\lambda^\{\(\\ell\)\}\(h\(u\)\)and henceMAX\(\{\|λ\(ℓ\)\(u\)∣u∈NG\(w\)\|\}\)≤MAX\(\{\|λ\(ℓ\)\(u′\)∣u′∈NG′\(h\(w\)\)\|\}\)\\mathrm\{MAX\}\(\\mathopen\{\\\{\\mkern\-3\.0mu\|\}\\lambda^\{\(\\ell\)\}\(u\)\\mid u\\in N\_\{G\}\(w\)\\mathclose\{\|\\mkern\-3\.0mu\\\}\}\)\\leq\\mathrm\{MAX\}\(\\mathopen\{\\\{\\mkern\-3\.0mu\|\}\\lambda^\{\(\\ell\)\}\(u^\{\\prime\}\)\\mid u^\{\\prime\}\\in N\_\{G^\{\\prime\}\}\(h\(w\)\)\\mathclose\{\|\\mkern\-3\.0mu\\\}\}\)\. By monotonicity of the combination function, we conclude thatλ\(ℓ\+1\)​\(w\)≤λ\(ℓ\+1\)​\(h​\(w\)\)\\lambda^\{\(\\ell\+1\)\}\(w\)\\leq\\lambda^\{\(\\ell\+1\)\}\(h\(w\)\)\.

Claim 3\.Augmented MGNNs are preserved under embeddings\.

Leth:\(G,v\)→\(G′,v′\)h\\colon\(G,v\)\\to\(G^\{\\prime\},v^\{\\prime\}\)be an embedding between pointed graphs, and let𝒩\\mathcal\{N\}be anLL\-layer augmented MGNN such that𝒩​\(G,v\)=1\\mathcal\{N\}\(G,v\)=1\. We will show that𝒩​\(G′,v′\)=1\\mathcal\{N\}\(G^\{\\prime\},v^\{\\prime\}\)=1\. To this end, it again suffices to prove by induction onℓ≤L\\ell\\leq Lthatλ\(ℓ\)​\(w\)≤λ′⁣\(ℓ\)​\(h​\(w\)\)\\lambda^\{\(\\ell\)\}\(w\)\\leq\\lambda^\{\\prime\(\\ell\)\}\(h\(w\)\), for every nodewwinGG\.

This time, however, layer 1 is different from later layers, so we will consider it separately\. Forℓ=0\\ell=0, sincehhis an embedding, it preserves node labels, and so,λ\(0\)​\(w\)=λ′⁣\(0\)​\(h​\(w\)\)\.\\lambda^\{\(0\)\}\(w\)=\\lambda^\{\\prime\(0\)\}\(h\(w\)\)\.Forℓ=1\\ell=1, we have that the first layer is the augmented layer\. Since it is applied pointwise, it follows thatλ\(1\)​\(w\)=λ′⁣\(1\)​\(h​\(w\)\)\.\\lambda^\{\(1\)\}\(w\)=\\lambda^\{\\prime\(1\)\}\(h\(w\)\)\.

Forℓ≥1\\ell\\geq 1, theℓ\\ellth layer is monotonic\. Hence, the argument is the same as we used to show that MGNNs are preserved under injective homomorphisms\. Thus,λ\(ℓ\)​\(w\)≤λ′⁣\(ℓ\)​\(h​\(w\)\)\\lambda^\{\(\\ell\)\}\(w\)\\leq\\lambda^\{\\prime\(\\ell\)\}\(h\(w\)\)\. ∎

Moreover, we can observe that MGNNs are not preserved under homomorphisms\. To this end, letG=\(V,E,λ\)G=\(V,E,\\lambda\)withV=\{v,u,w\}V=\\\{v,u,w\\\},E=\{\{v,u\},\{v,w\}\}E=\\\{\\\{v,u\\\},\\\{v,w\\\}\\\},λ​\(v\)=λ​\(u\)=λ​\(w\)=1\\lambda\(v\)=\\lambda\(u\)=\\lambda\(w\)=1, and letG′=\(V′,E′,λ′\)G^\{\\prime\}=\(V^\{\\prime\},E^\{\\prime\},\\lambda^\{\\prime\}\)withV′=\{v′,u′\}V^\{\\prime\}=\\\{v^\{\\prime\},u^\{\\prime\}\\\},E=\{\{v′,u′\}\}E=\\\{\\\{v^\{\\prime\},u^\{\\prime\}\\\}\\\}, andλ′​\(v\)=λ′​\(u\)=1\\lambda^\{\\prime\}\(v\)=\\lambda^\{\\prime\}\(u\)=1\. Define𝒩\\mathcal\{N\}with a single layer, aggregation functionSUM\\mathrm\{SUM\}, parameters𝐛=0\\mathbf\{b\}=0and𝐀=𝐂=1\\mathbf\{A\}=\\mathbf\{C\}=1, and classification function𝖼𝗅𝗌​\(x\)=1\\mathsf\{cls\}\(x\)=1iffx≥3x\\geq 3\. Then,𝒩​\(G,v\)=1\\mathcal\{N\}\(G,v\)=1, but𝒩​\(G′,v′\)=0\\mathcal\{N\}\(G^\{\\prime\},v^\{\\prime\}\)=0\. However, the functionffdefined byf​\(v\)=v′f\(v\)=v^\{\\prime\},f​\(u\)=u′f\(u\)=u^\{\\prime\}andf​\(w\)=u′f\(w\)=u^\{\\prime\}is a \(non\-injective\) homomorphism from\(G,v\)\(G,v\)to\(G′,v′\)\(G^\{\\prime\},v^\{\\prime\}\)\.

See[5](https://arxiv.org/html/2606.17882#S5)

###### Proof\.

The statement consists of four claims, that we will prove one by one\.

Claim 1\.For each∃𝒢​ℳ​ℒ\\exists\\mathcal\{GML\}\-classifier there is an equivalent augmented MGNN\.

Fixφ∈∃𝒢​ℳ​ℒ\\varphi\\in\\exists\\mathcal\{GML\}over propositions𝖯𝖱𝖮𝖯​\(φ\)\\mathsf\{PROP\}\(\\varphi\)whose subformulae are𝗌𝗎𝖻​\(φ\)=\(φ1,…,φL\)\\mathsf\{sub\}\(\\varphi\)=\(\\varphi\_\{1\},\\ldots,\\varphi\_\{L\}\), wherek≤ℓk\\leq\\ellwheneverφk\\varphi\_\{k\}is a subformula ofφℓ\\varphi\_\{\\ell\}\. We construct an equivalent augmented MGNN𝒩φ\\mathcal\{N\}\_\{\\varphi\}with layers0,…,L\+10,\\ldots,L\+1\.

The first layer \(ℓ=0\)\\ell=0\)is an augmentation layer which extends node features so that, for each propositionp∈𝖯𝖱𝖮𝖯​\(φ\)p\\in\\mathsf\{PROP\}\(\\varphi\), bothppand its negation¬p\\neg pare explicitly represented\. Concretely, if the original node labels are vectors in\{0,1\}d\\\{0,1\\\}^\{d\}, then the preprocessing layer maps each nodevvto a vectorλ\(0\)​\(v\)\\lambda^\{\(0\)\}\(v\)that contains, for eachp∈𝖯𝖱𝖮𝖯​\(φ\)p\\in\\mathsf\{PROP\}\(\\varphi\), a coordinate forppand a coordinate for¬p\\neg p, where the latter is computed as1−p​\(v\)1\-p\(v\)\. Thus, the augmentation layer doubles the dimension of the input vector\. Note that the augmentation layer can be implemented as a pointwise affine transformation\.

The remainingLLlayers correspond to the subformulae ofφ\\varphiand are specified below\. The classification function𝖼𝗅𝗌\\mathsf\{cls\}is defined by𝖼𝗅𝗌​\(𝐱\)=𝗍𝗋𝗎𝖾\\mathsf\{cls\}\(\\mathbf\{x\}\)=\\mathsf\{true\}iff the last component of𝐱\\mathbf\{x\}is11\.

Each layer1,…,L\+11,\\ldots,L\+1is simple \(as Equation \([2](https://arxiv.org/html/2606.17882#S3.E2)\)\):

λ′\(v\)=σ\(𝐛\+λ\(v\)𝐀\+𝖺𝗀𝗀\(\{\|λ\(w\)∣w∈NG\(v\)\|\}\)𝐂\),\\lambda^\{\\prime\}\(v\)=\\sigma\\Big\(\\mathbf\{b\}\+\\lambda\(v\)\\mathbf\{A\}\+\\mathsf\{agg\}\\big\(\\mathopen\{\\\{\\mkern\-3\.0mu\|\}\\lambda\(w\)\\mid w\\in N\_\{G\}\(v\)\\mathclose\{\|\\mkern\-3\.0mu\\\}\}\\big\)\\mathbf\{C\}\\Big\),\(3\)with activation functionσ\\sigmabeing the componentwise truncated ReLUσ​\(𝐱\)=min⁡\(max⁡\(0,𝐱\),1\)\\sigma\(\\mathbf\{x\}\)=\\min\(\\max\(0,\\mathbf\{x\}\),1\)and the aggregation function𝖺𝗀𝗀\\mathsf\{agg\}beingMAX\\mathrm\{MAX\}\-nn\-SUM\\mathrm\{SUM\}, wherennis the largest integer occurring in a graded modalities ofφ\\varphi\.

The entries of𝐀,𝐂∈ℝL×L\\mathbf\{A\},\\mathbf\{C\}\\in\\mathbb\{R\}^\{L\\times L\}and𝐛∈ℝL\\mathbf\{b\}\\in\\mathbb\{R\}^\{L\}are defined as follows:

1\. ifφℓ\\varphi\_\{\\ell\}is a proposition or the negation of a proposition, thenCℓ​ℓ=1C\_\{\\ell\\ell\}=1;2\. ifφℓ=φj∧φk\\varphi\_\{\\ell\}=\\varphi\_\{j\}\\wedge\\varphi\_\{k\}, thenCj​ℓ=Ck​ℓ=1C\_\{j\\ell\}=C\_\{k\\ell\}=1andbℓ=−1b\_\{\\ell\}=\-1;3\. ifφℓ=φj∨φk\\varphi\_\{\\ell\}=\\varphi\_\{j\}\\vee\\varphi\_\{k\}, thenCj​ℓ=Ck​ℓ=1C\_\{j\\ell\}=C\_\{k\\ell\}=1andbℓ=0b\_\{\\ell\}=0;4\. ifφℓ=◇≥c​φk\\varphi\_\{\\ell\}=\\Diamond^\{\\geq c\}\\varphi\_\{k\}, thenAk​ℓ=1A\_\{k\\ell\}=1andbℓ=−c\+1b\_\{\\ell\}=\-c\+1\.
All other entries are set to0\.

Observe that all entries of𝐀\\mathbf\{A\}and𝐂\\mathbf\{C\}are non\-negative, so𝒩φ\\mathcal\{N\}\_\{\\varphi\}is a positive\-weight GNN with additional augmented layer\. Hence, by[Section˜5](https://arxiv.org/html/2606.17882#S5),𝒩φ\\mathcal\{N\}\_\{\\varphi\}is an augmented MGNN, as required\.

We now show correctness of the construction\. Consider the application of𝒩φ\\mathcal\{N\}\_\{\\varphi\}to a graphG=\(V,E,λ\)G=\(V,E,\\lambda\)\. We show that for each subformulaφℓ\\varphi\_\{\\ell\}, eachi∈\{ℓ,…,L\}i\\in\\\{\\ell,\\ldots,L\\\}, and each nodev∈Vv\\in V,

\(G,v\)⊧φℓiffλ\(i\)​\(v\)ℓ=1\.\(G,v\)\\models\\varphi\_\{\\ell\}\\quad\\text\{iff\}\\quad\\lambda^\{\(i\)\}\(v\)\_\{\\ell\}=1\.
This implies that𝒩φ​\(G,v\)=𝗍𝗋𝗎𝖾\\mathcal\{N\}\_\{\\varphi\}\(G,v\)=\\mathsf\{true\}iff\(G,v\)⊧φ\(G,v\)\\models\\varphi\. The proof is by induction on the structure ofφℓ\\varphi\_\{\\ell\}\.

- •Ifφℓ\\varphi\_\{\\ell\}is a proposition then,λ​\(v\)ℓ\(0\)=1\\lambda\(v\)^\{\(0\)\}\_\{\\ell\}=1if\(G,v\)⊧φℓ\(G,v\)\\models\\varphi\_\{\\ell\}, and otherwiseλ​\(v\)ℓ\(0\)=0\\lambda\(v\)^\{\(0\)\}\_\{\\ell\}=0\. Moreover, sinceφℓ\\varphi\_\{\\ell\}is a proposition, all aggregate\-combine layers haveCℓ​ℓ=1C\_\{\\ell\\ell\}=1,bℓ=0b\_\{\\ell\}=0, andAk​ℓ=0A\_\{k\\ell\}=0for eachkk, so𝖼𝗈𝗆𝖻​\(𝐱,𝐲\)ℓ=𝐱ℓ\\mathsf\{comb\}\(\\mathbf\{x\},\\mathbf\{y\}\)\_\{\\ell\}=\\mathbf\{x\}\_\{\\ell\}\. Thusλ​\(v\)ℓ\(0\)=λ​\(v\)ℓ\(i\)\\lambda\(v\)^\{\(0\)\}\_\{\\ell\}=\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}for anyii\.
- •Ifφℓ\\varphi\_\{\\ell\}is the negation of a proposition, then its value is computed by the augmented layer\. In particular,λ​\(v\)ℓ\(0\)=1\\lambda\(v\)^\{\(0\)\}\_\{\\ell\}=1if\(G,v\)⊧φℓ\(G,v\)\\models\\varphi\_\{\\ell\}, and otherwiseλ​\(v\)ℓ\(0\)=0\\lambda\(v\)^\{\(0\)\}\_\{\\ell\}=0\. As in the propositional case, the construction ensures that this value is preserved across layers, soλ​\(v\)ℓ\(0\)=λ​\(v\)ℓ\(i\)\\lambda\(v\)^\{\(0\)\}\_\{\\ell\}=\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}for alli≥ℓi\\geq\\ell\.
- •Ifφℓ=φj∧φk\\varphi\_\{\\ell\}=\\varphi\_\{j\}\\wedge\\varphi\_\{k\}, then by construction, we haveCj​ℓ=Ck​ℓ=1C\_\{j\\ell\}=C\_\{k\\ell\}=1,bℓ=−1b\_\{\\ell\}=\-1, andAm​ℓ=0A\_\{m\\ell\}=0for eachmm\. Then by Equation \([2](https://arxiv.org/html/2606.17882#S3.E2)\), we have λ​\(v\)ℓ\(i\)=σ​\(λ​\(v\)j\(i−1\)\+λ​\(v\)k\(i−1\)−1\)\.\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}=\\sigma\(\\lambda\(v\)^\{\(i\-1\)\}\_\{j\}\+\\lambda\(v\)^\{\(i\-1\)\}\_\{k\}\-1\)\.By the inductive hypothesis,λ​\(v\)j\(i−1\)=1\\lambda\(v\)^\{\(i\-1\)\}\_\{j\}=1iff\(G,v\)⊧φj\(G,v\)\\models\\varphi\_\{j\}, and similarly forφk\\varphi\_\{k\}\. Hence,λ​\(v\)ℓ\(i\)=1\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}=1iff\(G,v\)⊧φj∧φk\(G,v\)\\models\\varphi\_\{j\}\\wedge\\varphi\_\{k\}, and otherwiseλ​\(v\)ℓ\(i\)=0\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}=0for alli≥ℓi\\geq\\ell\.
- •Ifφℓ=φj∨φk\\varphi\_\{\\ell\}=\\varphi\_\{j\}\\vee\\varphi\_\{k\}, then by construction, we haveCj​ℓ=Ck​ℓ=1C\_\{j\\ell\}=C\_\{k\\ell\}=1,bℓ=0b\_\{\\ell\}=0, andAm​ℓ=0A\_\{m\\ell\}=0for eachmm\. Then by Equation \([2](https://arxiv.org/html/2606.17882#S3.E2)\), we have λ​\(v\)ℓ\(i\)=σ​\(λ​\(v\)j\(i−1\)\+λ​\(v\)k\(i−1\)\)\.\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}=\\sigma\(\\lambda\(v\)^\{\(i\-1\)\}\_\{j\}\+\\lambda\(v\)^\{\(i\-1\)\}\_\{k\}\)\.By the inductive hypothesis,λ​\(v\)j\(i−1\)=1\\lambda\(v\)^\{\(i\-1\)\}\_\{j\}=1iff\(G,v\)⊧φj\(G,v\)\\models\\varphi\_\{j\}, and similarly forφk\\varphi\_\{k\}\. Hence,λ​\(v\)ℓ\(i\)=1\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}=1iff\(G,v\)⊧φj∨φk\(G,v\)\\models\\varphi\_\{j\}\\vee\\varphi\_\{k\}, and otherwiseλ​\(v\)ℓ\(i\)=0\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}=0for alli≥ℓi\\geq\\ell\.
- •Ifφℓ=◇≥c​φk\\varphi\_\{\\ell\}=\\Diamond^\{\\geq c\}\\varphi\_\{k\}, then by construction, we haveAk​ℓ=1A\_\{k\\ell\}=1,bℓ=−c\+1b\_\{\\ell\}=\-c\+1, andCm​ℓ=0C\_\{m\\ell\}=0for eachmm\. Since𝖺𝗀𝗀\\mathsf\{agg\}is theMAX\\mathrm\{MAX\}\-nn\-SUM\\mathrm\{SUM\}, by Equation \([2](https://arxiv.org/html/2606.17882#S3.E2)\), we have λ​\(v\)ℓ\(i\)=σ​\(min⁡\(n,∑w∈NG​\(v\)λ​\(w\)k\(i−1\)\)−c\+1\)\.\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}=\\sigma\\\!\\left\(\\min\\\!\\bigl\(n,\\sum\_\{w\\in N\_\{G\}\(v\)\}\\lambda\(w\)^\{\(i\-1\)\}\_\{k\}\\bigr\)\-c\+1\\right\)\.By the inductive hypothesis,λ​\(w\)k\(i−1\)=1\\lambda\(w\)^\{\(i\-1\)\}\_\{k\}=1iff\(G,w\)⊧φk\(G,w\)\\models\\varphi\_\{k\}\. Hence,λ​\(v\)ℓ\(i\)=1\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}=1iff\(G,v\)⊧◇≥c​φk\(G,v\)\\models\\Diamond^\{\\geq c\}\\varphi\_\{k\}, and otherwiseλ​\(v\)ℓ\(i\)=0\\lambda\(v\)^\{\(i\)\}\_\{\\ell\}=0\.

Claim 2\.For each∃ℳ​ℒ\\exists\\mathcal\{ML\}\-classifier there is an equivalent augmentedMAX\\mathrm\{MAX\}\-MGNN\.

Recall thatℳ​ℒ\\mathcal\{ML\}is a fragment of𝒢​ℳ​ℒ\\mathcal\{GML\}where all graded modalities have index11\. Then, theMAX\\mathrm\{MAX\}\-nn\-SUM\\mathrm\{SUM\}function in our construction isMAX\\mathrm\{MAX\}\-11\-SUM\\mathrm\{SUM\}, which is simply the component\-wiseMAX\\mathrm\{MAX\}function\. Hence𝒩φ\\mathcal\{N\}\_\{\\varphi\}becomes an augmentedMAX\\mathrm\{MAX\}\-MGNN, as required\.

Finally we consider two last claims together:

Claim 3\.For each∃\+𝒢​ℳ​ℒ\\exists^\{\+\}\\mathcal\{GML\}\-classifier there is an equivalent MGNN\.

Claim 4\.For each∃\+ℳ​ℒ\\exists^\{\+\}\\mathcal\{ML\}\-classifier there is an equivalentMAX\\mathrm\{MAX\}\-MGNN\.

In both cases formulae are negation\-free, so the augmented layer in the construction of𝒩φ\\mathcal\{N\}\_\{\\varphi\}can be omitted\. Hence our construction gives rise to an MGNN orMAX\\mathrm\{MAX\}\-MGNN, depending on the case\. ∎

See[5](https://arxiv.org/html/2606.17882#S5)

###### Proof\.

Construction of a required type GNN from formulae from a given modal logic follows directly from[Section˜5](https://arxiv.org/html/2606.17882#S5)\.

For the opposite direction we need to show that for a GNN𝒩\\mathcal\{N\}of a given type there exists an equivalent formulaφ\\varphifrom a particular modal logic\. Let𝒞\\mathcal\{C\}be the class of pointed graphs accepted by𝒩\\mathcal\{N\}\. By Theorem[5](https://arxiv.org/html/2606.17882#S5),𝒞\\mathcal\{C\}is preserved under: embeddings if𝒩\\mathcal\{N\}is an augmented MGNN, injective homomorphisms if𝒩\\mathcal\{N\}is an MGNN, and under homomorphisms if𝒩\\mathcal\{N\}is aMAX\\mathrm\{MAX\}\-MGNN\. Thus, by\[[4](https://arxiv.org/html/2606.17882#bib.bib48)\]there exists a formulaφ\\varphiin the required fragment of modal logic\.

It remains to consider the case when𝒩\\mathcal\{N\}is an augmentedMAX\\mathrm\{MAX\}\-MGNN, and show that it is equivalent to some∃ℳ​ℒ\\exists\\mathcal\{ML\}formula\. We observe that everyMAX\\mathrm\{MAX\}\-MGNN can be seen as a bounded AC\-GNN with set\-based aggregation, denoted asGNN𝗌𝖠𝖢\\text\{GNN\}\_\{\\mathsf\{s\}\}^\{\\mathsf\{AC\}\}, as defined in\[[6](https://arxiv.org/html/2606.17882#bib.bib24)\]\. It has been shown thatGNN𝗌𝖠𝖢\\text\{GNN\}\_\{\\mathsf\{s\}\}^\{\\mathsf\{AC\}\}s have the same expressive power asℳ​ℒ\\mathcal\{ML\}\[[6](https://arxiv.org/html/2606.17882#bib.bib24)\], so we obtain that𝒩\\mathcal\{N\}is equivalent to someℳ​ℒ\\mathcal\{ML\}formula\. Furthermore, recall that augmented MGNNs are preserved under embeddings \([Section˜5](https://arxiv.org/html/2606.17882#S5)\) so𝒩\\mathcal\{N\}, as a special case of an augmented MGNN is also preserved under embeddings\. Consequently, it allows us to apply a well\-known Rosen’s preservation theorem forℳ​ℒ\\mathcal\{ML\}, stating that anℳ​ℒ\\mathcal\{ML\}formula is preserved under embeddings if and only if it is equivalent to an∃ℳ​ℒ\\exists\\mathcal\{ML\}formula\[[23](https://arxiv.org/html/2606.17882#bib.bib18), Proposition 6\]\. As a result we obtain that𝒩\\mathcal\{N\}is equivalent to an∃ℳ​ℒ\\exists\\mathcal\{ML\}formula\. ∎