Random Models and Guarded Logic

In addition to decidability, a central question in the study of logical fragments is the finite model property: namely, whether every satisfiable sentence admits a finite model. For the Guarded Fragment, the finite model property is known to hold, with a doubly exponential upper bound (in the length of the sentence) on the size of minimal models.

The first proof of the finite model property for GF was given by Grädel [18], relying on a deep combinatorial theorem by Herwig [21]. While Grädel’s approach was elegant in its logical formulation – using Herwig’s result as a black box – the underlying construction is technically involved. Moreover, this proof yields only a triply-exponential upper bound on the size of minimal models, which is far from being optimal. A significant improvement came from Bárány, Gottlob, and Otto [4], who established an optimal doubly-exponential bound. Their approach involves analysing finite guarded bisimilar covers of hypergraphs and relational structures, substantially generalising Rosati’s finite chase [28]. In fact, their result extends beyond GF, covering the richer setting where (negations of) conjunctive queries are also allowed. A simplified version tailored specifically to GF appears in Pratt-Hartmann’s book [27], though we believe that even this version remains challenging to follow.

As the existing proofs of the finite model property for GF are unexpectedly difficult, it is natural to ask: Can we find simpler proofs of this fundamental result?

A perspective that connects abstract model theory with applied computer science arises in knowledge representation and reasoning, a subfield of artificial intelligence. In this context, the Guarded Fragment can serve as a logical foundation for decidable reasoning frameworks, subsuming and extending the basic description logics (DLs) of the $𝒜ℒ𝒞$ family (for an introduction to DLs, see, e.g., [3]). Here, objects from applications such as databases, knowledge bases, or computer programs are represented as logical structures, while formulas act as a declarative specification language describing their properties. Algorithms for satisfiability then become reasoning engines: given a formula, they decide whether an object satisfying the imposed logical constraints exists.

Over the years, a variety of algorithms solving satisfiability for the Guarded Fragment have been developed, ranging from purely theoretical decision procedures (e.g., [18]) to practically implementable methods based on resolution, saturation, or tableau (e.g., [9, 23, 22]). A key aspect is that many of these algorithms not only decide satisfiability but also produce a finite combinatorial object: a certificate of formula consistency.

Our interest lies in the subsequent step: How to turn such certificates into explicit finite models? Since smaller models are typically more useful – both for computational efficiency and for practical interpretability – the central challenge is to generate finite models as small as possible: not only close to the theoretical doubly exponential bounds, typically considered up to polynomial slack in the second-level exponent, but actually sharpened to within constant factors and detailed structural parameters of sentences.

In this work, we give a new proof of the finite model property for GF, yielding the optimal doubly exponential bound on the size of minimal models. To the best of our knowledge, no earlier proof exhibits comparable simplicity and self-containment.

We employ a probabilistic approach inspired by Gurevich and Shelah’s proof of the finite model property for the Gödel Class [20]. The central idea is the following: given a formula $\phi$ and a (possibly infinite) model $𝔄$ with $𝔄\vDash \phi$, we define a random procedure that generates a finite structure ${𝔅}_n$ with domain of size $n\in \mathbb{N}$. We then prove that, once $n$ exceeds a certain threshold depending only on $\phi$, the probability that ${𝔅}_n\vDash \phi$ becomes strictly positive. Consequently, some finite ${𝔅}_n$ must be a model of $\phi$, yielding the finite model property with an upper bound on the minimal model size that matches this threshold.

Applying this probabilistic method to the Guarded Fragment, we establish our main result: every satisfiable GF-sentence $\phi$ has a finite model whose domain size is $2^{2^{𝒪(|\phi |\cdot \log |\phi |)}}.$

In this work, we assume that $|\phi |$ measures the uniform length of $\phi$: formulas are viewed as words over an infinite alphabet consisting of parentheses, logical connectives, quantifiers, variables, relation symbols, and constants, with each symbol contributing $1$ to the length.¹¹1The uniform length differs from the bit-length of formulas (finite alphabet), in which $n$ distinct variables or symbols requires $\mathrm{\Theta }(n\cdot \log n)$ bits.

To witness the tightness of our upper bound, we construct a family of sentences ${({\phi }_n)}_{n\in \mathbb{N}}$ whose minimal models have domains of size at least $2^{2^{\mathrm{\Omega }(|{\phi }_n|\cdot \log |{\phi }_n|)}}.$ It is an improvement upon earlier approaches for enforcing large models in GF, as they only achieved domain sizes of $2^{2^{\mathrm{\Omega }(\sqrt{|{\phi }_n|})}}$ (cf. [18]). Consequently, our probabilistic model construction yields an essentially optimal upper bound, up to constant factors in the second-level exponent.

The upper bound of Theorem 1 is clean and elegant, but it is stated solely in terms of the length of $\phi$ and an unspecified constant in the second-level exponent. We complement this result by deriving a more precise bound on the size of minimal models. For a concise formulation, we express it in terms of the number of (atomic) $k$-types – that is, maximal consistent configurations of literals over $k$ variables (see Section 2 for a formal definition).

Given a sentence $\phi$, its induced signature $\sigma$ is the set of all relation and constant symbols occurring in $\phi$. The width of $\sigma$, denoted $\mathrm{wd}(\sigma )$, is the maximum arity of any relation symbol in $\sigma$. We define the expanded normal-form signature ${\sigma }_{\mathrm{nf}}$ from $\sigma$ as follows: for every subformula $\chi$ of $\phi$ that begins with a maximal block of quantifiers and which is not a sentence (i.e., $\chi$ has free variables), we introduce a fresh relation symbol $R_{\chi }$ whose arity equals the number of free variables of $\chi$ (which is at most $\mathrm{wd}(\sigma )$, since $\chi$ is required to be guarded).

Note that the construction of ${\sigma }_{\mathrm{nf}}$ preserves width, i.e., $\mathrm{wd}({\sigma }_{\mathrm{nf}})=\mathrm{wd}(\sigma )$, does not introduce new constants, and keeps the overall size of ${\sigma }_{\mathrm{nf}}$ linear in $|\phi |$.

The exponent in Theorem 2 converges to $1-1/e\approx 0.63$ as $t\to \mathrm{\infty }$. Informally, Theorem 2 can thus be read as stating that every satisfiable GF-sentence admits a finite model of domain size proportional to ${\left|{𝝉}_k^{{\sigma }_{\mathrm{nf}}}\right|}^{\mathrm{\hspace{0.17em}0.63}},$ provided that the width $k=\mathrm{wd}({\sigma }_{\mathrm{nf}})$ is sufficiently large.

At first sight, working with the expanded normal-form signature rather than the induced one may seem unintuitive. However, this choice is in fact a consequence of the semantics of guarded sentences: a quantified subformula $\chi (\overline{y})$ with free variables $\overline{y}$ naturally defines a relation in a structure $𝔄$, namely $R_{\chi }^{𝔄}=\{\overline{a}\mid 𝔄\vDash \chi (\overline{a})\}.$ To simplify the quantifier structure of a sentence, a standard technique is to transform it into a suitable normal form (see Section 3 for a definition). The normal-form reduction makes such implicitly defined relations explicit by introducing corresponding relation symbols. As a result, it distinguishes elements that are locally – i.e., at the level of atomic types – indistinguishable in the induced signature, but differ in their satisfaction of quantified subformulas.

The Guarded Fragment (GF) and the Two-Variable Fragment (${\text{FO}}^2$) are among the most prominent fragments of First-Order Logic. Both capture a wide range of modal and description logics and are decidable, yet they differ substantially and are incomparable in expressive power. In particular, GF cannot express certain basic properties, expressible in ${\text{FO}}^2$, such as $\forall s,d\left(\left(\mathrm{𝗌𝗍𝗎𝖽𝖾𝗇𝗍}(s)\wedge \mathrm{𝖽𝖾𝖺𝗇}(d)\right)\to \mathrm{𝗄𝗇𝗈𝗐𝗌}(s,d)\right).$

To unify these two perspectives, Rudolph and Šimkus [29] introduced the Triguarded Fragment (TGF), building on related ideas developed earlier in [23, 8].

The key idea of TGF is to relax the quantification restrictions of GF: formulas with at most two free variables may be quantified freely, while the guardedness requirement is retained for formulas with three or more free variables (hence the name “tri-guarded”). This way, TGF subsumes both ${\text{FO}}^2$ and GF, while also capturing properties beyond their reach. For instance, in formula (2), the quantifier $\forall p,s$ is admissible in TGF because the quantified subformula has only two free variables, $p$ and $s$, whereas the quantifier $\exists t$ is required to be guarded, and indeed is by the atom $\mathrm{𝖻𝖾𝗍𝗍𝖾𝗋}\text{-}\mathrm{𝗍𝗁𝖺𝗇}\text{-}\mathrm{𝗂𝗇}(p,s,t)$. Hence (2) belongs to TGF.

An important distinction concerns the role of equality. While both ${\text{FO}}^2$ and GF remain decidable in the presence of equality, the satisfiability problem for TGF with equality is undecidable. The reason is that TGF is expressive enough to encode the Gödel Class (i.e., the prefix class $\forall \forall {\exists }^{\ast }$), which was shown to be undecidable in the presence of equality by Goldfarb [13]. Excluding equality suffices to restore decidability of satisfiability, with complexity $2$-ExpTime without constants and $2$-NExpTime when constants are allowed [29].

Returning to the finite model property, Kieroński and Rudolph [24] proved that the equality-free fragment of TGF has the finite model property, with an optimal doubly exponential bound on minimal model size. Their proof, however, is technically intricate: it uses the finite model property for GF as a black box and adds a further combinatorial construction that carefully glues several structures into a single model.

In contrast, our probabilistic approach to GF extends seamlessly to TGF, yielding a considerably simpler proof of the finite model property for this broader fragment. Moreover, it also achieves the optimal doubly-exponential upper bound on minimal model size.

As mentioned earlier, the satisfiability problem for the Guarded Fragment is $2$-ExpTime-complete [18]. Yet, although the probabilistic construction shows that every satisfiable sentence has a model of doubly exponential size, this alone does not imply that such a model can be constructed in time matching the decision complexity. Indeed, the number of structures of doubly exponential size is triply exponential.

From a practical point of view, this gap is minor: our randomised construction succeeds with probability at least $1/2$ while sampling structures over a domain of doubly exponential size. Nevertheless, from a theoretical standpoint it leaves a conceptual separation between reasoning and model building: deterministic vs. randomised time complexity.

We close this gap by providing a constructive, fully deterministic version of Theorem 1. The central idea is to replace the random choices by carefully selected deterministic ones, using families of hash functions that mimic the statistical properties of true randomness. We then prove that these deterministic choices always produce a valid model.

In our formulation, we rely on the notion of a witness of satisfiability: a finite combinatorial object – namely, a set of $k$-types satisfying specific closure and consistency properties – that certifies the satisfiability of a sentence. Its definition is deferred to Section 3; for the present discussion it suffices to know that such a witness can be computed from a satisfiable sentence in $2$-ExpTime [18, 27]. On this basis we obtain the following constructive guarantee:

Beyond Gurevich and Shelah’s approach for the Gödel class [20], the probabilistic method has been employed in several other proofs of the finite model property.

One of the earliest and most influential applications of probabilistic techniques in logic is Fagin’s proof of the $0$–$1$ law for First-Order Logic [10]. A notable consequence of Fagin’s argument is that any finite subset of the theory of the Rado graph admits a finite model.

Goldfarb, Gurevich, and Shelah subsequently extended the approach of the latter two authors to the so-called subminimal Gödel class with identity [16]. Goldfarb later developed probabilistic proofs for additional decidable fragments, namely a solvable Skolem class [15] and the Maslov class [14]. For recent applications of the probabilistic method, see [11, 12].

We begin in Section 2 by introducing the basic notation and conventions used throughout the paper. Section 3 provides the necessary background on GF, including its syntax, the normal form, and a satisfiability criterion. Building on this, Section 4 develops probabilistic constructions of finite models for GF. In Section 5, we construct sentences enforcing models that tightly match the upper bound established in Section 4. Section 6 demonstrates that our methods extend naturally to TGF. In Section 7, we give a deterministic procedure for constructing finite models. Finally, Section 8 concludes the paper and discusses directions for future research.

The missing material is provided in the full version of the paper. Beyond the technical details omitted here, the full version also contains additional results, remarks, and examples.

We assume general familiarity with First-Order Logic (FO). The logical symbols are $=,\perp ,\top ,\vee ,\wedge ,\neg ,\to ,\leftrightarrow$, and the quantifiers $\forall ,\exists$. Formulas may also use non-logical symbols: relation symbols of arbitrary arity (from a countably infinite set), constant symbols (also from a countably infinite set), and variables (again countably many). We do not allow function symbols. The length of a formula $\phi$, denoted $|\phi |$, is defined as the total number of symbols it contains, where each occurrence of a symbol – be it a variable, relation symbol, or constant – contributes $1$. We use $\mathrm{fv}(\phi )$ to denote the set of free variables of $\phi$.

A signature $\sigma$ is a finite set of symbols, partitioned as $\sigma =\mathrm{Rels}\uplus \mathrm{Cons}$, where $\mathrm{Rels}$ is the set of relation symbols and $\mathrm{Cons}$ is the set of constant symbols. We require $\mathrm{Rels}\ne \mathrm{\varnothing }$. Every relation symbol $R\in \mathrm{Rels}$ comes with associated arity, denoted $\mathrm{ar}(R)$. We require $\mathrm{ar}(R)\ge 1$. The width of $\sigma$, denoted $\mathrm{wd}(\sigma )$, is the maximum arity of any symbol in $\mathrm{Rels}$. The signature of a formula is the finite set of relation and constant symbols that appear in the formula.

We use Fraktur letters such as $𝔄,𝔅,\mathrm{\dots }$ to denote structures, and the corresponding Roman letters $A,B,\mathrm{\dots }$ for their domains. A $\sigma$-structure $𝔄$ is a structure that interprets the symbols in $\sigma$: a relation symbol $R$ as a relation $R^{𝔄}\subseteq A^k$ with $k$ denoting the arity of $R$; and a constant symbol $c$ as an element $c^{𝔄}\in A$. If $B\subseteq A$, we write $𝔄\upharpoonright B$ for the restriction of $𝔄$ to the subdomain $B$. Note that $B$ must include all interpretations of constant symbols to remain a $\sigma$-structure. The structure $𝔄$ is empty if it contains no facts, i.e., $R^{𝔄}=\mathrm{\varnothing }$ for all relation symbols $R$; however, we do not insist (and even forbid) that the domain is the empty set $\mathrm{\varnothing }$. The size of a structure is the cardinality of its domain.

With respect to satisfiability, equality between constants can be eliminated by a straightforward reduction: if a formula has a model $𝔄$ satisfying $c_1^{𝔄}=c_2^{𝔄}$, then $c_2$ can be replaced by $c_1$ throughout the formula, without affecting satisfiability. Thus we work under the standard name assumption requiring that constants are interpreted in structures by themselves. Given a $\sigma$-structure $𝔄$, we partition its domain $A$ as $A_0\uplus \mathrm{Cons}$, where $A_0$ and $\mathrm{Cons}$ are disjoint sets of unnamed and, respectively, named elements.

Fix a signature $\sigma =\mathrm{Rels}\uplus \mathrm{Cons}$. For $k\in \mathbb{N}$, let ${\mathrm{Lit}}_k(\sigma )$ denote the set of all non-equality literals over relation and constant symbols from $\sigma$ and variables $x_1,\mathrm{\dots },x_k$.

For $k\in \mathbb{N}$, a $k$-type over $\sigma$ is a maximal consistent subset of ${\mathrm{Lit}}_k(\sigma )$. A type is simply a $k$-type for some $k\in \mathbb{N}$. We write ${𝝉}_k^{\sigma }$ for the set of all $k$-types over $\sigma$, and ${𝝉}^{\sigma }:={\bigcup }_{k\in \mathbb{N}}{𝝉}_k^{\sigma }$.

We denote by ${\tau }_{\mathrm{all}\text{-}\mathrm{neg}}$ the type consisting exclusively of negative literals (the value of $k$ will be clear from the context).

If $k\le \mathrm{\ell }$, we write ${\tau }_2\vDash {\tau }_1$ to indicate that a $k$-type ${\tau }_1$ is contained in an $\mathrm{\ell }$-type ${\tau }_2$.

For $\tau \in {𝝉}_k^{\sigma }$, we define: $\partial \tau :=\{\gamma \in \tau \mid \mathrm{fv}(\gamma )=\{x_1,\mathrm{\dots },x_k\}\},$ and $\mathrm{int}(\tau ):=\tau \setminus \partial \tau$, that is, the boundary and interior of $\tau$. The set of all boundary $k$-types is $\partial {𝝉}_k^{\sigma }:=\{\partial \tau \mid \tau \in {𝝉}_k^{\sigma }\}$.

A $k$-type $\tau$ is called guarded if either $k\le 1$ or $\tau$ contains a positive literal $\gamma$ with $\mathrm{fv}(\gamma )=\{x_1,\mathrm{\dots },x_k\},$ i.e., $\gamma \in \partial \tau$. Note that necessarily $k\le \mathrm{wd}(\sigma )$.

Given a $k$-tuple of distinct unnamed elements $⟨a_1,\mathrm{\dots },a_k⟩$ of a $\sigma$-structure $𝔄$, we write ${\mathrm{tp}}^{𝔄}[a_1,\mathrm{\dots },a_k]$ for the unique $k$-type realised by $⟨a_1,\mathrm{\dots },a_k⟩$ in $𝔄$. Formally, ${\mathrm{tp}}^{𝔄}[a_1,\mathrm{\dots },a_k]$ is the set of literals $\gamma \in {\mathrm{Lit}}_k(\sigma )$ such that $𝔄,f\vDash \gamma$, where $f$ is the assignment that sends $x_i\mapsto a_i$ for every $i\in [k]$. The collection of all $k$-types realised in $𝔄$ is denoted

It is convenient to view $k$-types themselves as $\sigma$-structures over the canonical domain $\{x_1,\mathrm{\dots },x_k\}\cup \mathrm{Cons}$. This allows us to use structure-like notation; for instance, if $\tau \in {𝝉}_3^{\sigma }$, we may write ${\mathrm{tp}}^{\tau }[x_1,x_3]$ for the $2$-type induced by $\tau$ on the variables $x_1$ and $x_3$.

We formalise the syntax of the Guarded Fragment in Definition 7.

Note that equality may serve as a guard: the formula $\forall x(x=x\to \psi )$ is in GF whenever $\psi \in \text{GF}$ and $\mathrm{fv}(\psi )\subseteq \{x\}$. This allows for free quantification over individual elements.

Let $\phi$ be a sentence in GF. Then $\phi$ is in normal form if it is a conjunction of a finite number of guarded existential, guarded universal, and guarded Skolem sentences:

where $\overline{x}$ and $\overline{y}$ are disjoint tuples of distinct variables, ${\alpha }_t(\overline{x})$ and ${\beta }_t(\overline{x},\overline{y})$ are guards, and ${\psi }_t$ are quantifier-free formulas. The notation $\psi (\overline{x})$ only highlights that the set of free variables of $\psi$ is contained in the tuple $\overline{x}$. However, it does not imply that all of them are actually used by $\psi$. In particular, when $\psi$ is an atom, the variables can occur in any order and with repetitions. Also the actual sets of free variables of ${\alpha }_t$, ${\beta }_t$, and ${\psi }_t$ can vary with $t$. Nevertheless, we require that each conjunct is properly guarded. For every relevant index $t$, the following must hold: if $t$ corresponds to an existential or universal conjunct, then $\mathrm{fv}({\psi }_t)\subseteq \mathrm{fv}({\alpha }_t)=\overline{x}$; if $t$ corresponds to a Skolem conjunct, then $\mathrm{fv}({\alpha }_t)=\overline{x}$ and $\mathrm{fv}({\psi }_t)\cup \overline{y}\subseteq \mathrm{fv}({\beta }_t)\subseteq \overline{x}\cup \overline{y}$, where in both cases the tuples $\overline{x}$ and $\overline{y}$ may depend on $t$.

Lemma 8 reduces the finite model property for GF to the normal-form case. Moreover, any upper bound on minimal model size that depends only on the length and signature, and is proved for normal-form sentences, naturally carries over to arbitrary GF-sentences.

We now formulate a sufficient criterion for the satisfiability of sentences in GF. This allows us to modularise the argument and clearly separate the general properties of guarded logic from the new components of our proof.

Let $\sigma =\mathrm{Rels}\uplus \mathrm{Cons}$ be a signature. A set of types $𝝉\subseteq {𝝉}^{\sigma }$ is said to be closed (under reductions) if the following holds: for every $\tau \in 𝝉$ which is a $k$-type for some $k$, and for every $\mathrm{\ell }\in [0,k]$ and choice of distinct indices $i_1,\mathrm{\dots },i_{\mathrm{\ell }}\in [k]$, the type ${\mathrm{tp}}^{\tau }[x_{i_1},\mathrm{\dots },x_{i_{\mathrm{\ell }}}]$ also belongs to $𝝉$. Further, the set $𝝉$ is said to be consistent if it contains a unique $0$-type.

Let $\phi$ be a GF-sentence in normal form. If a family of sets of $k$-types ${𝝉}^{\ast }={\bigcup }_{k=0}^{\mathrm{wd}(\sigma )}{𝝉}_k^{\ast }$ satisfies the conditions of Lemma 10, then we call it a satisfiability witness for $\phi$. Assuming that $\phi$ is satisfiable, one may obtain a satisfiability witness for $\phi$ by taking the collection of all $k$-types, with $k\le \mathrm{wd}(\sigma )$, that are realised in some (possibly infinite) model of $\phi$. This argument is inherently non-constructive; see [27] for a procedure that decides satisfiability and, if so, computes a corresponding satisfiability witness in $2$-ExpTime.

W.l.o.g. we will always assume ${𝝉}_k^{\ast }\ne \mathrm{\varnothing }$ for all $k\in [0,\mathrm{wd}(\sigma )]$. By Claim 6, we have that

provided that $\sigma =\mathrm{Rels}\uplus \mathrm{Cons}$ is the induced signature of $\phi$.