Random Models and Guarded Logic

TL;DR

This paper introduces a probabilistic proof for the finite model property of the Guarded Fragment, achieving optimal bounds and extending to the Triguarded Fragment, with a derandomized explicit construction.

Contribution

It provides a simple, probabilistic proof with optimal bounds for the Guarded Fragment and extends the approach to the Triguarded Fragment, including a derandomized explicit model construction.

Findings

Optimal doubly-exponential upper bound on minimal model size

Probabilistic method extends to Triguarded Fragment

Explicit derandomized model construction achieved

Abstract

Building on ideas of Gurevich and Shelah for the G\"odel Class, we present a new probabilistic proof of the finite model property for the Guarded Fragment of First-Order Logic. Our proof is conceptually simple and yields the optimal doubly-exponential upper bound on the size of minimal models. We precisely analyse the obtained bound, up to constant factors in the exponents, and construct sentences that enforce models of tightly matching size. The probabilistic approach adapts naturally to the Triguarded Fragment, an extension of the Guarded Fragment that also subsumes the Two-Variable Fragment. Finally, we derandomise the probabilistic proof by providing an explicit model construction which replaces randomness with deterministic hash functions.