Finite Model Theory of the Triguarded Fragment and Related Logics (Extended Abstract)? Emanuel Kieroński1 and Sebastian Rudolph2 1 Institute of Computer Science, University of Wroclaw 2 Computational Logic Group, Technische Universität Dresden Ever since first-order logic (FOL) was found to have an undecidable satisfi- ability problem, researchers have attempted to identify expressive yet decidable fragments of FOL and pinpoint their complexity. In many cases, such fragments embed propositional modal logic as well as many description logics. Two of the most prominent examples in this regard are FO2 (the two-variable fragment) and GF (the guarded fragment). For FO2 , decidability is retained through re- ducing the number of available variables to 2, essentially restricting expressivity to independent pairwise interactions between domain elements. Its satisfiability problem is NExpTime-complete [5]. For GF, which owes its decidability to the restricted “guarded” use of quantifiers, the problem is 2ExpTime-complete [4]. Both FO2 and GF possess the finite model property (FMP), meaning that any satisfiable sentence has a finite model. For satisfiable FO2 sentences, models of at most exponential size in the sentence exist [5]; for GF, the tight bound on the size of minimal models is doubly exponential [1]. In an attempt to unify FO2 and GF toward an even more expressive decid- able FOL fragment, the triguarded fragment (TGF) was introduced [9], extending prior results [6]. TGF brings a new quality, as it allows one to express properties expressible in neither FO2 nor GF. In particular it embeds Gödel’s class, consist- ing of prenex sentences of the shape ∃x̄∀y1 y2 ∃z̄ϕ (formally we need to replace the variables from x̄ by constants and add a dummy guard for ∃z̄). Thus, the price to pay for retaining decidability is that equality needs to be disallowed, as Gödel’s class with equality is undecidable [2]. Checking satisfiability of TGF is N2ExpTime-complete, dropping to 2ExpTime when disallowing constants – as opposed to FO2 and GF, where presence or absence of constants does not make a difference, complexity-wise – and to NExpTime if the arity of predicates is bounded. One central question left wide open in the original work on TGF [9] is if TGF has the FMP. In that paper, it is noted that neither technique used for establishing the FMP for FO2 and GF seems to directly lend itself for solving the question for TGF, yet it is conjectured that the FMP holds. Indeed, one of our core contributions is to answer this open question in the positive. Let us briefly outline our approach. ? This abstract presents work accepted at LICS 2021. E.K. is supported by Polish Na- tional Science Centre grant No 2016/21/B/ST6/01444. S.R. is supported by the Eu- ropean Research Council through the ERC Consolidator Grant 771779 (DeciGUT). Copyright c 2021 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). 2 E. Kieroński, S. Rudolph. For convenience, we work with the equivalent logic GFU, the guarded frag- ment with universal role. We assume that signatures for GFU always contain the distinguished binary relation symbol U. GFU sentences are then defined precisely like GF sentences, but the set of admissible models is restricted to those which interpret U as the universally true relation. Structures interpreting U in this way will be called U-biquitous structures. It is not difficult to see that TGF and GFU have the same expressive power modulo the extra predicate U. As typical for decidable fragments of first-order logic we introduce a normal form for TGF formulas, similar to those used, e.g., for GF [4] and FO2 [5]. Given a satisfiable GFU normal form sentence ϕ, we take its (possibly infi- nite) U-biquitous model A and construct a finite U-biquitous model A0 of ϕ as follows (for simplicity, we consider here the case without constants; adding them is routine): 1. Extend ϕ by conjuncts saying that: exactly the 1-types from A are realized; for any two 1-types from A, there are U-connected representatives; U holds between any pair of elements co-occurring in any relation. The resulting normal form sentence ϕ∗ is still guarded and still satisfies A |= ϕ∗ . 2. Use the FMP for GF to obtain a finite (yet non-ubiquitous) model C of ϕ∗ . 3. Obtain A0 |= ϕ∗ as 125 · |C|2 -fold disjoint union of C with itself. View A0 as a 5|C| × 5|C| table whose each cell contains a copy of the 5-fold disjoint union of C with itself. The elements in each cell are numbered from 1 to 5|C|. 4. U-saturation: Obtain A1 , A2 , . . . by iteratively picking a pair a, b of yet non- U-connected elements, connecting them, and adjoining them to one of the copies of C. This is done using an appropriate pair of connected elements as template (hence maintaining ϕ∗ -modelhood). Designing a strategy allowing one to perform this step without conflicts is quite challenging. In our solution, the numbers of a and b in their cells B0 , B00 determine a cell B, and the coordinates of B0 and B00 in the table are used to choose a particular copy of C in B to which a and b are adjoined. 5. As the number of elements remains constant, the procedure terminates and yields a U-biquitous An = A0 . We also consider a scenario where some distinguished binary symbols have to be interpreted as transitive relations, capturing this way, e.g., some description logics from the family S. One needs to be careful here, since both FO2 and GF become undecidable under this scenario [3,4]. However, the decidability of GF can be regained if the transitive symbols are allowed to occur only as guards [10] (note that this is sufficient to encode the logic S). The same holds for the corresponding extension of TGF [7]. Results for the finite model case are less extensive: so far, only finite satis- fiability of the two-variable variant GF2 +TG of GF with transitive guards was shown to be decidable and 2ExpTime-complete [8]. We note that already this logic does not have the FMP: indeed, a typical infinity axiom saying that, for a transitive relation T , every element has a T -successor but is not related by T to itself is naturally expressible in GF2 +TG. We remark that all the results concerning logics with transitive guards assume the absence of constants. It is Finite Model Theory of the Triguarded Fragment and Related Logics 3 conjectured that adding constants to the picture is technically challenging but generally possible without hazarding decidability. In the current paper we are able to show that (at least in the absence of constants) the finite satisfiability problems for GF and TGF with transitive guards are decidable. Our approach incorporates some ideas from the above- described finite model construction for satisfiable TGF sentences and some other concepts, in particular calling as a subprocedure the small-model construction for GF2 +TG from [8]. All our results come with tight complexity bounds and tight bounds on the size of minimal models. Summarising: Theorem 1. TGF has the finite model property; every satisfiable TGF sentence has a finite model of size bounded doubly exponentially in its length. Hence, satisfiability and finite satisfiability for TGF coincide and are N2ExpTime- complete if constants are admitted and 2 ExpTime-complete otherwise. Theorem 2. Every finitely satisfiable sentence in (constant-free) GF or TGF with transitive guards has a model of size bounded doubly exponentially in its length. The finite satisfiability problems for (constant-free) GF and TGF with transitive guards are 2 ExpTime-complete. Decidability and complexity of finite satisfiability of GF and TGF with tran- sitive guards with constant is left open. References 1. Vince Bárány, Georg Gottlob, and Martin Otto. Querying the guarded fragment. Logical Methods in Computer Science, 10(2), 2014. 2. W. D. Goldfarb. The unsolvability of the Gödel class with identity. J. Symb. Logic, 49:1237–1252, 1984. 3. E. Grädel, M. Otto, and E. Rosen. Undecidability results on two-variable logics. Archiv für Mathematische Logik und Grundlagenforschung, 38(4-5):313–354, 1999. 4. Erich Grädel. On the restraining power of guards. J. Symb. Log., 64(4):1719–1742, 1999. 5. Erich Grädel, Phokion Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53–69, 1997. 6. Yevgeny Kazakov. Saturation-Based Decision Procedures for Extensions of the Guarded Fragment. PhD thesis, Universität des Saarlandes, Saarbrücken, Germany, March 2006. 7. Emanuel Kieronski and Adam Malinowski. The triguarded fragment with tran- sitivity. In Logic for Programming, Artificial Intelligence and Reasoning 2020, volume 73 of EPiC, pages 334–353. EasyChair, 2020. 8. Emanuel Kieroński and Lidia Tendera. Finite satisfiability of the two-variable guarded fragment with transitive guards and related variants. ACM Trans. Com- put. Logic, 19(2):8:1–8:34, 2018. 9. Sebastian Rudolph and Mantas Šimkus. The triguarded fragment of first-order logic. In LPAR, volume 57 of EPiC Series in Computing, pages 604–619, 2018. 10. Wieslaw Szwast and Lidia Tendera. The guarded fragment with transitive guards. Annals of Pure and Applied Logic, 128:227–276, 2004.