Henson Graphs Finite Model Property

Definitions and mathematical statement

In the standard graph-theoretic usage, for an integer $m\geq3$ the Henson graph $H_m$ is the countably infinite homogeneous $K_m$-free graph whose finite induced subgraphs, up to isomorphism, are exactly all finite $K_m$-free graphs. Here $K_m$ is the complete graph on $m$ vertices, $K_m$-free means containing no such clique, and homogeneous means that every isomorphism between finite induced subgraphs extends to an automorphism. The source neither selects $m$ nor states that this standard family, rather than another Henson structure, is the intended one.

A precise finite-model-property question must specify a language $\mathcal L$, a theory $T$, a class of allowed sentences, a class of finite structures, and the convention for finite models. Two distinct possible conventions illustrate the omission. One is finite satisfiability of each sentence true in a fixed structure $H$: \[ \forall\varphi\text{ an }\mathcal L\text{-sentence},\quad H\models\varphi\ \Longrightarrow\ \exists M\text{ finite}:\ M\models\varphi. \] This is the usual pseudofiniteness formulation when $H$ is infinite. One could instead require finite $K_m$-free graph witnesses, which is an additional restriction on $M$. Another theory-relative convention is \[ \forall\varphi\text{ an allowed }\mathcal L\text{-sentence},\quad T\cup\{\varphi\}\text{ satisfiable}\ \Longrightarrow\ \exists M\text{ finite}:\ M\models T\cup\{\varphi\}. \] These formulations impose different requirements; in particular requiring a finite model of an entire theory containing infinitude axioms is different from requiring separate finite models of individual sentences of that theory. A fragment of logic or a different associated theory could yield still another question. None is selected here as the intended meaning of the unqualified phrase "Henson graphs have the finite model property".

The supplied background describes Henson graphs as universal homogeneous graphs omitting finite subgraphs and connects the proposed finite-model question to infinite graph theory, model theory, combinatorics and decidability. The literature triage, checked 2026-08-17, explicitly says the question is inadequately specified and reports only that Evans's notes retain a closely related associated-theory finite-model-property problem as open. It does not give that theory or its exact convention. The same assessment reports recent finite big Ramsey degrees for Henson graphs, emphasizing that this is a different property and does not answer the stored finite-model question. It says no theorem answering the dataset's unqualified wording was verified and calls for recovery of the intended structure and definition before a status audit.

Short English statement

Specify which Henson structure and which finite-model convention are intended, then ask whether the relevant satisfiable or true sentences have the required finite witnesses. The supplied record does not fix these choices, and its cited recent big-Ramsey result concerns a different property.

Sources

• UnsolvedMath local registry, permanent ID 1464, source code catalogue entry, "Henson Graphs Finite Model Property". Dataset attribution: Ulam AI and the UnsolvedMath Contributors; curation and metadata under CC BY 4.0.
• D. Evans, lecture notes, title supplied only as Model-theoretic constructions for..., https://www.ma.imperial.ac.uk/~dmevans/hattingen.pdf. The supplied triage says these notes pose an associated theory's finite model property as open, but gives no section or exact formulation.
• The finite big Ramsey degrees of Henson graphs are provable in $\mathrm{ACA}_0$, arXiv:2606.30885 (2026), https://arxiv.org/abs/2606.30885. The supplied record gives no authors and cites this only for a distinct recent Henson-graph property.
• The local literature triage records checks on 2026-08-17; no external sources were independently visited.