Building on ideas of Gurevich and Shelah for the Gödel 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.

翻译：基于Gurevich和Shelah针对哥德尔类的研究思想，我们提出了一种新的概率证明方法，用于验证一阶逻辑守卫片段的有穷模型性质。该证明在概念上简洁明了，并能推导出最小模型尺寸的最优双指数上界。我们精确分析了所得界限（直至指数中的常数因子），并构造了能强制生成严格匹配尺寸模型的语句。这种概率方法可自然适配于三守卫片段——该片段不仅是守卫逻辑的扩展，同时也包含双变量片段。最后，我们通过提供显式模型构造实现了证明的去随机化，该构造采用确定性哈希函数替代了随机性过程。