Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

First-order logic axiomatization of metric graph theory

Jérémie Chalopin, Manoj Changat, Victor Chepoi, Jeny Jacob

TL;DR

This work develops First Order Logic with Betweenness ($FOLB$) as a unifying framework to axiomatize and study metric graph theory classes. By encoding metric notions via a betweenness predicate, it shows that a wide array of central classes such as weakly modular, median, modular, Helly, dual polar, and partial cubes are definable in $FOLB$, while natural classes like chordal, planar, Eulerian, and dismantlable graphs are not. The authors also derive polynomial time recognition results for $FOLB$-definable classes and discuss the limitations and possible extensions to stronger logics. Overall, the paper provides a Tarski style first order theory for metric graph theory that clarifies expressiveness, paves the way for algorithmic meta-results, and highlights open definability boundaries. The framework promises a principled approach to analyze and classify metric graph phenomena through logic and finite model theory lens.

Abstract

The main goal of this note is to provide a First-Order Logic with Betweenness (FOLB) axiomatization of the main classes of graphs occurring in Metric Graph Theory, in analogy to Tarski's axiomatization of Euclidean geometry. We provide such an axiomatization for weakly modular graphs and their principal subclasses (median and modular graphs, bridged graphs, Helly graphs, dual polar graphs, etc), basis graphs of matroids and even $Δ$-matroids, partial cubes and their subclasses (ample partial cubes, tope graphs of oriented matroids and complexes of oriented matroids, bipartite Pasch and Peano graphs, cellular and hypercellular partial cubes, almost-median graphs, netlike partial cubes), and Gromov hyperbolic graphs. On the other hand, we show that some classes of graphs (including chordal, planar, Eulerian, and dismantlable graphs), closely related with Metric Graph Theory, but defined in a combinatorial or topological way, do not allow such an axiomatization.

First-order logic axiomatization of metric graph theory

TL;DR

This work develops First Order Logic with Betweenness () as a unifying framework to axiomatize and study metric graph theory classes. By encoding metric notions via a betweenness predicate, it shows that a wide array of central classes such as weakly modular, median, modular, Helly, dual polar, and partial cubes are definable in , while natural classes like chordal, planar, Eulerian, and dismantlable graphs are not. The authors also derive polynomial time recognition results for -definable classes and discuss the limitations and possible extensions to stronger logics. Overall, the paper provides a Tarski style first order theory for metric graph theory that clarifies expressiveness, paves the way for algorithmic meta-results, and highlights open definability boundaries. The framework promises a principled approach to analyze and classify metric graph phenomena through logic and finite model theory lens.

Abstract

The main goal of this note is to provide a First-Order Logic with Betweenness (FOLB) axiomatization of the main classes of graphs occurring in Metric Graph Theory, in analogy to Tarski's axiomatization of Euclidean geometry. We provide such an axiomatization for weakly modular graphs and their principal subclasses (median and modular graphs, bridged graphs, Helly graphs, dual polar graphs, etc), basis graphs of matroids and even -matroids, partial cubes and their subclasses (ample partial cubes, tope graphs of oriented matroids and complexes of oriented matroids, bipartite Pasch and Peano graphs, cellular and hypercellular partial cubes, almost-median graphs, netlike partial cubes), and Gromov hyperbolic graphs. On the other hand, we show that some classes of graphs (including chordal, planar, Eulerian, and dismantlable graphs), closely related with Metric Graph Theory, but defined in a combinatorial or topological way, do not allow such an axiomatization.
Paper Structure (27 sections, 13 theorems, 43 equations, 5 figures)

This paper contains 27 sections, 13 theorems, 43 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Graphs
  4. First-Order Logic (FOL)
  5. Ehrenfeucht-Fraïssé games
  6. What can be expressed and what cannot be expressed in FOL for graphs
  7. First Order Logic with Betweenness (FOLB)
  8. Betweenness and interval spaces
  9. FOLB for graphs
  10. What can be expressed in FOLB for graphs: first results
  11. Weakly modular graphs, their subclasses and superclasses
  12. Weakly modular graphs
  13. Median graphs
  14. Bridged graphs and graphs with convex balls
  15. Helly graphs
  16. ...and 12 more sections

Key Result

Theorem 2

Let $r$ be a positive integer and let $\mathbf{A}$ and $\mathbf{B}$ be two $\sigma$-structures. Then the following two conditions are equivalent: Moreover, $\equiv_r$ has finitely many equivalence classes and each $\equiv_r$-equivalence class is definable by a first-order sentence of quantified rank $r$.

Figures (5)

  • Figure 1: Forbidden subgraphs
  • Figure 2: The graphs $A^*$ and $B^*$ for the query Chordal
  • Figure 3: The graphs $A^*$ and $B^*$ for the query Dismantlable
  • Figure 4: The graphs $A^*$ and $B^*$ for the query Partial Johnson
  • Figure 5: The graphs $A^*$ and $B^*$ for the query $\textsf{DPO}\xspace$

Theorems & Definitions (20)

  • Example 1
  • Theorem 2: EhrFra
  • Theorem 3
  • Example 4
  • Lemma 1
  • Lemma 2: BaCh_helly
  • Theorem 5: BaCh_helly
  • Theorem 6: MuNe
  • Lemma 3
  • proof
  • ...and 10 more