=Paper=
{{Paper
|id=Vol-3733/paper17
|storemode=property
|title=Decidability of Ordered Fragments of FOL via Modal Translation
|pdfUrl=https://ceur-ws.org/Vol-3733/paper17.pdf
|volume=Vol-3733
|authors=Hongkai Yin,Matteo Pascucci
|dblpUrl=https://dblp.org/rec/conf/cilc/YinP24
}}
==Decidability of Ordered Fragments of FOL via Modal Translation==
<pdf width="1500px">https://ceur-ws.org/Vol-3733/paper17.pdf</pdf>
<pre>
                                Decidability of ordered fragments of 𝐹 𝑂𝐿 via modal
                                translation
                                Hongkai Yin1,*,† , Matteo Pascucci1,†
                                1
                                    Central European University, Quellenstrasse 51, 1100 Wien, Austria


                                               Abstract
                                               We present a simplification and a modification of a method introduced by Herzig to prove the decidability
                                               of Quine’s ordered fragment of first-order logic. The method consists in an interpretation of quantifiers
                                               as modal operators. We show that our modification yields the decidability of two new ordered fragments
                                               of first-order logic, called the grooved fragment and the loosely grooved fragment, whose expressive
                                               power lies between Quine’s ordered fragment and the fluted fragment.

                                               Keywords
                                               Fragments of first-order logic, Decidability, Modal logic, Tree model property




                                1. Introduction
                                The ordered fragments of first-order logic (𝐹 𝑂𝐿) are those fragments in which an ordering
                                associated with the set of variables imposes restrictions on their occurrences in atomic formulas,
                                as well as on scopes of quantifiers [1]. The simplest of such fragments is due to Quine [2] and
                                results from the following ideas:
                                       1. an atomic formula can be formed only by giving variables 𝑥1 , ..., 𝑥𝑛 (in this order) as
                                          arguments to an 𝑛-ary predicate;
                                       2. a complex formula is either obtained by applying sentential connectives to formulas with
                                          the same free variables, or by quantifying over the free variable with the largest index in
                                          a formula.

                                For example, the following sentence belongs to Quine’s ordered fragment:
                                                                            ∀𝑥1 (𝑃 𝑥1 → ∃𝑥2 (𝑅𝑥1 𝑥2 ∧ ∀𝑥3 𝑆𝑥1 𝑥2 𝑥3 )).
                                Herzig [3] provides a translation from this fragment into propositional modal language in such
                                a way that any input formula is satisfied in a first-order model iff its translation is satisfied in
                                a Kripke model over a serial frame. Accordingly, one can employ decision procedures for the
                                modal logic KD (which is semantically characterized by the class of all serial frames) to decide
                                the satisfiability problem for Quine’s ordered fragment.
                                CILC 2024: 39th Italian Conference on Computational Logic, June 26-28, 2024, Rome, Italy
                                *
                                  Corresponding author.
                                †
                                  Hongkai Yin is mainly responsible for the technical proofs in the article. Matteo Pascucci is mainly responsible for
                                  the structure of the contents.
                                $ yin_hongkai@phd.ceu.edu (H. Yin); pascuccim@ceu.edu (M. Pascucci)
                                 0009-0006-0082-6541 (H. Yin); 0000-0003-4867-4082 (M. Pascucci)
                                             © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).




CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
   Herzig’s translation relies on an intuitive reading of quantifiers as modal operators: ∀ cor-
responds to □ and ∃ corresponds to ♢. In other words, the claim that 𝜑 is the case for every
individual amounts to the claim that 𝜑 is necessary, whereas the claim that 𝜑 is the case for some
individual amounts to the claim that 𝜑 is possible. We stress that such a connection between
quantifiers and modalities is simpler than the one employed in the standard translation of modal
logic into (the guarded fragment of) first-order logic.
   In the present article we provide a simplification and a modification of Herzig’s method. By
doing so, we obtain decidability and direct model construction for two other ordered fragments
of 𝐹 𝑂𝐿 called the grooved fragment and the loosely grooved fragment, both of which lie between
Quine’s ordered fragment and the fluted fragment [4, 5]. More precisely, we have the following
chain of (strict) inclusion for the mentioned fragments of 𝐹 𝑂𝐿:

                         Quine’s ⊂ grooved ⊂ loosely grooved ⊂ fluted

   The rest of the article is arranged as follows. In Section 2 we introduce the modal translation
of Quine’s ordered fragment, followed by our simplified proof of satisfiability-invariance under
the translation. In Section 3 we define the grooved fragment and use a modified translation to
address the satisfiability problem. The loosely grooved fragment is defined in Section 4, where
we show that its sentences can be rewritten into satisfiability-equivalent ones in the grooved
fragment. We conclude the article with some remarks on potential applications of the ordered
fragments, and on the relation between the fragments analysed here and some other fragments
of 𝐹 𝑂𝐿.


2. Quine’s ordered fragment
The first-order language we are considering here is denoted by ℒ𝐹 𝑂𝐿 . It consists of a countable
set 𝑃 𝑟𝑒𝑑 of predicates (each with an arity 𝑛 ≥ 1), a countable set 𝑉 𝑎𝑟 of individual variables,
¬, ∧, ∀, and parentheses. (Other logical symbols can be introduced by definition in the usual
way.) Elements of 𝑃 𝑟𝑒𝑑 are denoted by 𝑃1 , 𝑃2 , etc., whereas those of 𝑉 𝑎𝑟 by 𝑥1 , 𝑥2 , etc. The
set of well-formed formulas of ℒ𝐹 𝑂𝐿 , denoted by 𝐹 𝑜𝑟𝑚(ℒ𝐹 𝑂𝐿 ), is constructed in the usual
way.
   Now we start by specifying Quine’s ordered fragment. For the sake of a more concise
exposition, we associate each formula of the fragment with a level (a natural number).

Definition 1 (Ordered formulas). The set of ordered formulas 𝐹 𝑜𝑟𝑚𝑜𝑟𝑑 (ℒ𝐹 𝑂𝐿 ) is the smallest
subset of 𝐹 𝑜𝑟𝑚(ℒ𝐹 𝑂𝐿 ) that satisfies the following conditions:
   1. For any 𝑛-ary predicate 𝑃𝑖 (𝑛 ≥ 1), 𝑃𝑖 𝑥1 . . . 𝑥𝑛 is an ordered formula of level 𝑛.
   2. If 𝜑 and 𝜓 are ordered formulas of level 𝑛, so are ¬𝜑 and (𝜑 ∧ 𝜓).
   3. If 𝜑 is an ordered formula of level 𝑛 (𝑛 > 0), then ∀𝑥𝑛 𝜑 is an ordered formula of level
      𝑛 − 1.
Note that an ordered formula of level 0 is an ordered sentence since it does not contain any free
variables.
   In the analysis of ordered formulas we will employ a simplified definition of the satisfaction
relation. Recall that a model for ℒ𝐹 𝑂𝐿 is an ordered pair ℳ = ⟨𝐷, 𝐼⟩, where 𝐷 is a non-empty
set and 𝐼 is an interpretation function s.t. for any 𝑛-ary predicate 𝑃𝑖 , 𝐼(𝑃𝑖 ) ⊆ 𝐷𝑛 . For an
ordered formula of level 𝑛, since its free variables are exactly 𝑥1 , . . . , 𝑥𝑛 , we do not need to
distinguish assignments which differ only on the value of other variables. Thus, we can use
an 𝑛-tuple ⟨𝑎1 , . . . , 𝑎𝑛 ⟩, where 𝑎𝑖 ∈ 𝐷, to denote any assignment which assigns 𝑎𝑖 to 𝑥𝑖 . In
particular, we can use the empty tuple 𝜖 for any assignment.

Definition 2 (Satisfaction for ordered formulas). Let ℳ = ⟨𝐷, 𝐼⟩ be a model for ℒ𝐹 𝑂𝐿 and
𝐷* be the set of all finite tuples of elements of 𝐷. We write 𝜎𝑛 for an element of 𝐷𝑛 (where
𝐷𝑛 ⊂ 𝐷* ) and 𝜑𝑛 , 𝜓𝑛 for ordered formulas of level 𝑛. The satisfaction relation ⊨ is defined as
follows (where 𝜎𝑛−1 𝑎 ∈ 𝐷𝑛 is the concatenation of 𝜎𝑛−1 ∈ 𝐷𝑛−1 and 𝑎 ∈ 𝐷):

    • ℳ, 𝜎𝑛 ⊨ 𝑃𝑖 𝑥1 . . . 𝑥𝑛 iff 𝜎𝑛 ∈ 𝐼(𝑃𝑖 )
    • ℳ, 𝜎𝑛 ⊨ ¬𝜑𝑛 iff it is not the case that ℳ, 𝜎𝑛 ⊨ 𝜑𝑛
    • ℳ, 𝜎𝑛 ⊨ 𝜑𝑛 ∧ 𝜓𝑛 iff ℳ, 𝜎𝑛 ⊨ 𝜑𝑛 and ℳ, 𝜎𝑛 ⊨ 𝜓𝑛
    • ℳ, 𝜎𝑛−1 ⊨ ∀𝑥𝑛 𝜑𝑛 iff for all 𝑎 ∈ 𝐷, ℳ, 𝜎𝑛−1 𝑎 ⊨ 𝜑𝑛

In particular, when an ordered sentence 𝜑 is true in ℳ, we write ℳ ⊨ 𝜑 instead of ℳ, 𝜖 ⊨ 𝜑.

This definition can be trivially generalized to cover also the case where 𝜑𝑛 , a formula of level 𝑛,
is evaluated with a tuple of length 𝑛 + 𝑚 (where 𝑚 ≥ 1). Since the elements of 𝐷 assigned to
variables 𝑥𝑛+1 ...𝑥𝑛+𝑚 are irrelevant to the satisfaction of 𝜑𝑛 .

   The propositional modal language ℒ𝑃 𝑀 𝐿 used to translate Quine’s ordered fragment consists
of a countable set 𝑃 𝑟𝑜𝑝 of propositional variables, ¬, ∧, and the modal operator □. (Other
logical symbols can be introduced by definition in the usual way.) The set 𝑃 𝑟𝑜𝑝 is assumed to
be equinumerous with 𝑃 𝑟𝑒𝑑, and elements of 𝑃 𝑟𝑜𝑝 will be denoted by 𝑝1 , 𝑝2 , etc. We say that
a propositional variable corresponds to a predicate (and vice versa) if they have the same index.
The set of formulas of ℒ𝑃 𝑀 𝐿 is constructed as usual and will be denoted by 𝐹 𝑜𝑟𝑚(ℒ𝑃 𝑀 𝐿 ).
   We employ the standard relational semantics for ℒ𝑃 𝑀 𝐿 . A model for ℒ𝑃 𝑀 𝐿 (henceforth also
ℒ𝑃 𝑀 𝐿 -model or Kripke model) is an ordered triple M = ⟨𝑊, 𝑅, 𝑉 ⟩ where: 𝑊 is a non-empty
set; 𝑅 is a binary relation on 𝑊 ; and 𝑉 : 𝑃 𝑟𝑜𝑝 −→ ℘(𝑊 ) is a function. Formulas of ℒ𝑃 𝑀 𝐿 are
evaluated relative to elements of 𝑊 . In particular, M, 𝑤 ⊨ □𝜑 iff M, 𝑣 ⊨ 𝜑 for all 𝑣 ∈ 𝑊 s.t.
𝑅𝑤𝑣. We will assume that the elements 𝑊 , 𝑅 and 𝑉 define an ℒ𝑃 𝑀 𝐿 -model M, the elements
𝑊 ′ , 𝑅′ and 𝑉 ′ define an ℒ𝑃 𝑀 𝐿 -model M′ , etc. The frame of an ℒ𝑃 𝑀 𝐿 -model M = ⟨𝑊, 𝑅, 𝑉 ⟩
is the pair ⟨𝑊, 𝑅⟩. A frame is said to be serial iff (∀𝑤 ∈ 𝑊 )(∃𝑣 ∈ 𝑊 )𝑅𝑤𝑣.
   Some model-theoretic concepts will become relevant later, so we also mention them here for
reference.

Definition 3 (Tree unravelling). Given an ℒ𝑃 𝑀 𝐿 -model M = ⟨𝑊, 𝑅, 𝑉 ⟩ and 𝑤 ∈ 𝑊 , the tree
unravelling of M at 𝑤 is the model M′ = ⟨𝑊 ′ , 𝑅′ , 𝑉 ′ ⟩ defined as follows:

    • 𝑊 ′ is the set of all sequences (𝑣1 , . . . , 𝑣𝑛 ) ∈ 𝑊 𝑛 (where 𝑛 ≥ 1) s.t.:
         – 𝑣1 = 𝑤,
          – for 1 ≤ 𝑖 < 𝑛, 𝑅𝑣𝑖 𝑣𝑖+1 ;
    • 𝑅′ (𝑣1 , . . . , 𝑣𝑛 )(𝑢1 , . . . , 𝑢𝑚 ) iff
          – 𝑚 = (𝑛 + 1),
          – for 1 ≤ 𝑖 ≤ 𝑛, 𝑣𝑖 = 𝑢𝑖 ,
          – 𝑅𝑣𝑛 𝑢𝑛+1 ;
    • for 𝑝 ∈ 𝑃 𝑟𝑜𝑝, (𝑣1 , . . . , 𝑣𝑛 ) ∈ 𝑉 ′ (𝑝) iff 𝑣𝑛 ∈ 𝑉 (𝑝).

Definition 4 (Bounded morphism). A bounded morphism from an ℒ𝑃 𝑀 𝐿 -model M to an
ℒ𝑃 𝑀 𝐿 -model M′ is a function 𝑓 : 𝑊 −→ 𝑊 ′ s.t.:

    • for 𝑝 ∈ 𝑃 𝑟𝑜𝑝 and 𝑤 ∈ 𝑊 , 𝑤 ∈ 𝑉 (𝑝) iff 𝑓 (𝑤) ∈ 𝑉 ′ (𝑝);
    • if 𝑅𝑤𝑣, then 𝑅′ 𝑓 (𝑤)𝑓 (𝑣);
    • if 𝑅′ 𝑓 (𝑤)𝑣 ′ , then 𝑅𝑤𝑢 for some 𝑢 ∈ 𝑊 s.t. 𝑓 (𝑢) = 𝑣 ′ .

   If 𝑓 is a bounded morphism from M to M′ , then, for each 𝜑 ∈ 𝐹 𝑜𝑟𝑚(ℒ𝑃 𝑀 𝐿 ) and each
𝑤 ∈ 𝑊 , it holds that M, 𝑤 ⊨ 𝜑 iff M′ , 𝑓 (𝑤) ⊨ 𝜑. Also, if M′ is the tree-unraveling of M at 𝑤,
there is a bounded morphism from the former to the latter.
   Moreover, filtration is one of the standard techniques for constructing finite models in modal
logic. (A detailed discussion can be found in [6].) Specifically, it allows one to prove that if
𝜑 ∈ 𝐹 𝑜𝑟𝑚(ℒ𝑃 𝑀 𝐿 ) is satisfiable in a class of ℒ𝑃 𝑀 𝐿 -models 𝒞, then it is satisfiable in a finite
model in 𝒞. In our case 𝒞 will be the class of models over serial frames or a specified subclass of
this.
   This ends the preliminaries. Now we move on to the translation of 𝐹 𝑜𝑟𝑚𝑜𝑟𝑑 (ℒ𝐹 𝑂𝐿 ) into
𝐹 𝑜𝑟𝑚(ℒ𝑃 𝑀 𝐿 ), which is due to Herzig [3].

Definition 5 (Translation). The translation function, 𝑡𝑟 : 𝐹 𝑜𝑟𝑚𝑜𝑟𝑑 (ℒ𝐹 𝑂𝐿 ) −→ 𝐹 𝑜𝑟𝑚(ℒ𝑃 𝑀 𝐿 ),
is defined recursively as follows:

    • 𝑡𝑟(𝑃𝑖 𝑥1 . . . 𝑥𝑛 ) = 𝑝𝑖
    • 𝑡𝑟(¬𝜑) = ¬𝑡𝑟(𝜑)
    • 𝑡𝑟(𝜑 ∧ 𝜓) = 𝑡𝑟(𝜑) ∧ 𝑡𝑟(𝜓)
    • 𝑡𝑟(∀𝑥𝜑) = □𝑡𝑟(𝜑)

   Now we present a way to construct a Kripke model (i.e. a model for ℒ𝑃 𝑀 𝐿 ) based on a
first-order model (i.e. a model for ℒ𝐹 𝑂𝐿 ).
   Let ℳ = ⟨𝐷, 𝐼⟩ be a model for ℒ𝐹 𝑂𝐿 . Then the ℒ𝑃 𝑀 𝐿 -analogue of ℳ, M = ⟨𝑊, 𝑅, 𝑉 ⟩, is
a model for ℒ𝑃 𝑀 𝐿 such that:

    • 𝑊 = 𝐷* (the set of all finite tuples of elements of 𝐷)
    • for any 𝜎, 𝜏 ∈ 𝑊 , 𝑅𝜎𝜏 iff 𝜏 = 𝜎𝑎 for some 𝑎 ∈ 𝐷
    • 𝑉 (𝑝𝑖 ) = 𝐼(𝑃𝑖 )

Note that the frame ⟨𝑊, 𝑅⟩ specified here is a tree where the root is the empty tuple. Also note
that the frame is serial and M is thus a KD-model.
Proposition 1 (Satisfiability invariance for ℒ𝑃 𝑀 𝐿 -analogues). Let ℳ = ⟨𝐷, 𝐼⟩ be a model for
ℒ𝐹 𝑂𝐿 and M = ⟨𝑊, 𝑅, 𝑉 ⟩ its ℒ𝑃 𝑀 𝐿 -analogue. For 𝑛 ≥ 0, if 𝜑𝑛 is an ordered formula of level 𝑛
and 𝜎𝑛 is an 𝑛-tuple in 𝐷* , then: ℳ, 𝜎𝑛 ⊨ 𝜑𝑛 iff M, 𝜎𝑛 ⊨ 𝑡𝑟(𝜑𝑛 ).
Proof. By induction on ordered formulas. We only analyse the case where 𝜑𝑛 = ∀𝑥𝑛+1 𝜓:
ℳ, 𝜎𝑛 ⊨ ∀𝑥𝑛+1 𝜓 iff ℳ, 𝜎𝑛 𝑎 ⊨ 𝜓 for every 𝑎 ∈ 𝐷 iff (by I.H.) M, 𝜎𝑛 𝑎 ⊨ 𝑡𝑟(𝜓) for every 𝑎 ∈ 𝐷
iff M, 𝜎𝑛 ⊨ □𝑡𝑟(𝜓).

   So far we have shown that, if we have a first-order model which satisfies an ordered sentence
𝜑, we can build a KD-model over a tree in which 𝑡𝑟(𝜑) is satisfied at the root.
   For the other direction, namely to show that when we have a KD-model satisfiying 𝑡𝑟(𝜑) we
can build a first-order model satisfying 𝜑, we begin with the following observations. First, given
a KD-model where 𝑡𝑟(𝜑) is satisfied, a filtration of the model through the set of subformulas of
𝑡𝑟(𝜑) preserves the satisfiability of 𝑡𝑟(𝜑) as well as the seriality of the frame, and therefore we
can restrict our attention to KD-models with a bounded size. Second, for a finite KD-model
with a bounded size, its tree unravelling is a KD-model where each node has a bounded number
of children.
   Let us fix some terminology before moving on. We say that a tree is 𝑚-ary iff each of its
nodes has at most 𝑚 children. A perfect 𝑚-ary tree is one in which each node has exactly 𝑚
children. A tree is serial iff every one of its nodes has at least one child. Clearly, for 𝑚 > 0, a
perfect 𝑚-ary tree is serial. Moreover, each node in a tree is assigned a natural number as its
height, defined as follows:
    • if 𝑣 is the root, ℎ𝑒𝑖𝑔ℎ𝑡(𝑣) = 0;
    • if 𝑣 ′ is a child of 𝑣, ℎ𝑒𝑖𝑔ℎ𝑡(𝑣 ′ ) = ℎ𝑒𝑖𝑔ℎ𝑡(𝑣) + 1.
We say that a node 𝑤 is lower than a node 𝑣 just in case ℎ𝑒𝑖𝑔ℎ𝑡(𝑤) < ℎ𝑒𝑖𝑔ℎ𝑡(𝑣).
   We proceed in two steps. First, we show that each serial 𝑚-ary tree model can be expanded
to a perfect 𝑚-ary tree model which is invariant w.r.t. the satisfiability of modal formulas.
Proposition 2 (From a tree to a perfect tree). Let M = ⟨𝑊, 𝑅, 𝑉 ⟩ be a model over a serial
𝑚-ary tree (𝑚 > 0) with root 𝑤0 . Then there is a model M′ = ⟨𝑊 ′ , 𝑅′ , 𝑉 ′ ⟩ over a perfect 𝑚-ary
tree with root 𝑤0′ and a surjective bounded morphism 𝑓 : M′ −→ M s.t. 𝑓 (𝑤0′ ) = 𝑤0 .
Proof. We describe a systematic procedure for constructing M′ and 𝑓 .

Stage 0 Set M0 = ⟨𝑊0 , 𝑅0 , 𝑉0 ⟩ = M, and 𝑓0 = 𝑖𝑑𝑊 (the identity function on 𝑊 ).

Stage n+1 If the frame in M𝑛 = ⟨𝑊𝑛 , 𝑅𝑛 , 𝑉𝑛 ⟩ is not a perfect tree, choose the lowest node
     𝑤 ∈ 𝑊𝑛 having less than 𝑚 children; if there are multiple such nodes, choose one of
     them. Then pick a 𝑣 ∈ 𝑊𝑛 s.t. 𝑅𝑛 𝑤𝑣, and let

            𝑈 = {𝑢 ∈ 𝑊𝑛 : 𝑅𝑛* 𝑣𝑢} (𝑅𝑛* is the reflexive and transitive closure of 𝑅𝑛 )

      Suppose 𝑤 has 𝑚 − 𝑘 children (0 < 𝑘 < 𝑚). For 1 ≤ 𝑖 ≤ 𝑘, let 𝑈𝑖 be a set of fresh nodes
      (i.e. 𝑈𝑖 ∩ 𝑊𝑛 = ∅ and for 1 ≤ 𝑗 < 𝑖, 𝑈𝑖 ∩ 𝑈𝑗 = ∅) s.t. |𝑈𝑖 | = |𝑈 |, and 𝑔𝑖 : 𝑈𝑖 −→ 𝑈 be a
      bijection. Let 𝑆𝑖 ⊆ 𝑈𝑖2 and 𝑇𝑖 : 𝑃 𝑟𝑜𝑝 −→ 𝒫(𝑈𝑖 ) be as follows:
            for any 𝑢, 𝑢′ ∈ 𝑈𝑖 , 𝑆𝑖 𝑢𝑢′ iff 𝑅𝑛 𝑔𝑖 (𝑢)𝑔𝑖 (𝑢′ )
            for any 𝑢 ∈ 𝑈𝑖 and any 𝑝 ∈ 𝑃 𝑟𝑜𝑝, 𝑢 ∈ 𝑇𝑖 (𝑝) iff 𝑔𝑖 (𝑢) ∈ 𝑉𝑛 (𝑝)

      Then, set M𝑛+1 = ⟨𝑊𝑛+1 , 𝑅𝑛+1 , 𝑉𝑛+1 ⟩ where
                              ⋃︀
            𝑊𝑛+1 = 𝑊𝑛 ∪   1≤𝑖≤𝑘 𝑈𝑖
            𝑅𝑛+1 = 𝑅𝑛 ∪ {(𝑤, 𝑔𝑖−1 (𝑣)) : 1 ≤ 𝑖 ≤ 𝑘} ∪ 1≤𝑖≤𝑘 𝑆𝑖
                                                     ⋃︀

            for any 𝑝 ∈ 𝑃 𝑟𝑜𝑝, 𝑉𝑛+1 (𝑝) = 𝑉𝑛 (𝑝) ∪
                                                         ⋃︀
                                                              1≤𝑖≤𝑘 𝑇𝑖 (𝑝)

      Also, let 𝑓𝑛+1 : M𝑛+1 −→ M𝑛 be the function such that
                        {︃
                          𝑤      𝑤 ∈ 𝑊𝑛
            𝑓𝑛+1 (𝑤) =
                          𝑔𝑖 (𝑤) 𝑤 ∈ 𝑈𝑖

This procedure yields the desired tree model M′ = ⟨𝑊 ′ , 𝑅′ , 𝑉 ′ ⟩ where:
      𝑊 ′ = 𝑊𝑛 ;
             ⋃︀

      𝑅′ = 𝑅𝑛 ;
            ⋃︀

      for any 𝑝 ∈ 𝑃 𝑟𝑜𝑝, 𝑉 ′ (𝑝) = 𝑉𝑛 (𝑝).
                                  ⋃︀

Moreover, we have the function 𝑓 : M′ −→ M such that
      𝑓 (𝑤) = 𝑓0 ∘ 𝑓1 ∘ · · · ∘ 𝑓𝑛 (𝑤), if 𝑤 first appears in stage 𝑛.
This is a surjective bounded morphism, and, obviously, 𝑓 (𝑤0′ ) = 𝑤0 .

   Now we can proceed to the second step of our construction, which consists in deriving a
first-order model from a Kripke model over a perfect 𝑚-ary tree.
   Let M = ⟨𝑊, 𝑅, 𝑉 ⟩ be a model for ℒ𝑃 𝑀 𝐿 in which ⟨𝑊, 𝑅⟩ is a perfect 𝑚-ary tree (𝑚 > 0).
Let 𝐷 be a set with |𝐷| = 𝑚, 𝐸 ⊆ 𝐷* ×𝐷* be a relation such that: for 𝜎, 𝜏 ∈ 𝐷* , 𝐸𝜎𝜏 iff 𝜎 = 𝜏 𝑎
for some 𝑎 ∈ 𝐷; accordingly, ⟨𝐷* , 𝐸⟩ is isomorphic to ⟨𝑊, 𝑅⟩. Let ℎ : ⟨𝐷* , 𝐸⟩ −→ ⟨𝑊, 𝑅⟩
be an isomorphism, and 𝐼 be the interpretation function on ℒ𝐹 𝑂𝐿 such that: for any 𝑛-ary
predicate 𝑃𝑖 , 𝐼(𝑃𝑖 ) = {𝜎 ∈ 𝐷𝑛 : ℎ(𝜎) ∈ 𝑉 (𝑝𝑖 )}. Then ℳ = ⟨𝐷, 𝐼⟩ is a model for ℒ𝐹 𝑂𝐿 ,
and we call it an ℒ𝐹 𝑂𝐿 -analogue of M. Notice that there is a unique ℒ𝐹 𝑂𝐿 -analogue for each
ℒ𝑃 𝑀 𝐿 -model, up to isomorphism.
Proposition 3 (Satisfiability invariance for ℒ𝐹 𝑂𝐿 -analogues). Let M = ⟨𝑊, 𝑅, 𝑉 ⟩ be a perfect
𝑚-ary (𝑚 > 0) tree model for ℒ𝑃 𝑀 𝐿 , and ℳ = ⟨𝐷, 𝐼⟩ be an ℒ𝐹 𝑂𝐿 -analogue of M. Then: for
𝑛 ≥ 0, M, ℎ(𝜎𝑛 ) ⊨ 𝑡𝑟(𝜑𝑛 ) iff ℳ, 𝜎𝑛 ⊨ 𝜑𝑛 , where 𝜑𝑛 is an ordered formula of level 𝑛, and 𝜎𝑛 is
an 𝑛-tuple from 𝐷* .
Proof. By induction on ordered formulas.

Proposition 4 (Satisfiability invariance under 𝑡𝑟). Let 𝜑 be an ordered sentence. Then: 𝜑 is
satisfiable iff 𝑡𝑟(𝜑) is KD-satisfiable. Therefore, the satisfiability problem for Quine’s ordered
fragment is decidable.
Proof. By Propositions 1, 2, and 3.

   We also stress that the construction provided above indicates that one can build a conservative
extension of both Quine’s fragment of 𝐹 𝑂𝐿 and KD thanks to function 𝑡𝑟, as discussed in [7].
We can define a conservative extension of Quine’s fragment of 𝐹 𝑂𝐿 and KD as a system 𝑆
of first-order modal logic (hence, whose language results from the combination of ℒ𝐹 𝑂𝐿 and
ℒ𝑃 𝑀 𝐿 ) such that (i) 𝑆 contains all theorems of each of the two systems at issue, and (ii) the
schema ∀𝑥𝜑 ↔ 𝜓 is derivable in 𝑆 for some formula 𝜓 ∈ ℒ𝑃 𝑀 𝐿 . In order to see this point,
consider the semantic procedure described below.
   Combine any ℒ𝑃 𝑀 𝐿 -model M = ⟨𝑊, 𝑅, 𝑉 ⟩ over a perfect 𝑚-ary tree (𝑚 > 0) and an
ℒ𝐹 𝑂𝐿 -analogue ℳ = ⟨𝐷, 𝐼⟩ of M thanks to the bijective function ℎ used in the construction
of ℳ (see Proposition 2). The result is a hybrid structure 𝑀 = ⟨𝑊, 𝑅, 𝑉, 𝐷, 𝐼, ℎ⟩ where ℒ𝑃 𝑀 𝐿
and ℒ𝐹 𝑂𝐿 are simultaneously interpreted. Use the bijective function ℎ to assign a label to each
element of 𝑊 , i.e. for 𝜎 ∈ 𝐷* , if ℎ(𝜎) = 𝑤 ∈ 𝑊 , then 𝜎 = 𝑙𝑎𝑏𝑒𝑙(𝑤). Moreover, put together
the definition of the satisfaction relation ⊨ in Kripke models and in first-order models and let
𝑀, 𝑤 ⊨ 𝜑 become interchangeable with 𝑀, 𝑙𝑎𝑏𝑒𝑙(𝑤) ⊨ 𝜑. Once this is done, it is immediate
to see that 𝜑 ↔ 𝑡𝑟(𝜑) is valid in 𝑀 . A fortiori, ∀𝑥𝜑 ↔ □𝑡𝑟(𝜑) is valid in 𝑀 .1 Furthermore,
notice that □𝑡𝑟(𝜑) ∈ ℒ𝑃 𝑀 𝐿 . Finally, let 𝒞 be the class of all hybrid models defined as above and
𝑇 ℎ(𝒞) the set of first-order modal formulas that are valid in 𝒞. Then, any system of first-order
modal logic 𝑆 whose set of theorems contains 𝑇 ℎ(𝒞) is a conservative extension of both Quine’s
fragment of 𝐹 𝑂𝐿 and KD.


3. The grooved fragment
In this section we present a modification of the method used above. We consider an ordered
fragment which is larger than Quine’s. We name it the grooved fragment. The additional
expressiveness of this new fragment results from allowing unary predicates to take a variable
𝑥𝑛 , for any 𝑛 > 0.

Definition 6 (Grooved formulas). The set of grooved formulas 𝐹 𝑜𝑟𝑚𝑔𝑟𝑜 (ℒ𝐹 𝑂𝐿 ) is the smallest
subset of 𝐹 𝑜𝑟𝑚(ℒ𝐹 𝑂𝐿 ) that satisfies the following conditions:
       1. If 𝑃 is an 𝑛-ary predicate (𝑛 > 1), 𝑃 𝑥1 . . . 𝑥𝑛 is a grooved formula of level 𝑛.
       2. If 𝑃 is a unary predicate, 𝑃 𝑥𝑛 is a grooved formula of level 𝑛 (𝑛 > 0).
       3. If 𝜑 and 𝜓 are grooved formulas of level 𝑛, so are ¬𝜑 and (𝜑 ∧ 𝜓).
       4. If 𝜑 is a grooved formula of level 𝑛 (𝑛 > 0), then ∀𝑥𝑛 𝜑 is a grooved formula of level 𝑛 − 1.

   The identification of the grooved fragment is inspired by works on the relational syllogistic,
the extension of the classical syllogistic with relational terms. Logical systems in that context
feature, for example, the following sentences:


1
    For instance, consider the following case: ∀𝑥1 𝑃𝑖 𝑥1 ↔ □𝑝𝑖 . Let 𝑀 be a hybrid model and 𝑤 a state in its domain.
    It holds that 𝑀, 𝑤 ⊨ ∀𝑥1 𝑃𝑖 𝑥1 iff 𝑀, 𝑙𝑎𝑏𝑒𝑙(𝑤) ⊨ ∀𝑥1 𝑃𝑖 𝑥1 iff 𝑀, 𝑙𝑎𝑏𝑒𝑙(𝑤)𝑎 ⊨ 𝑃𝑖 𝑥1 for every 𝑎 ∈ 𝐷 iff 𝑀, 𝑣 ⊨ 𝑝𝑖
    for every 𝑣 s.t. 𝑅𝑤𝑣 iff 𝑀, 𝑤 ⊨ □𝑝𝑖 . Therefore, 𝑀, 𝑤 ⊨ ∀𝑥1 𝑃𝑖 𝑥1 ↔ □𝑝𝑖 .
      No student admires every professor
      ∀𝑥1 (𝑆𝑥1 → ¬∀𝑥2 (𝑃 𝑥2 → 𝐴𝑥1 𝑥2 ))
      No lecturer introduces any professor to every student
      ∀𝑥1 (𝐿𝑥1 → ¬∃𝑥2 (𝑃 𝑥2 ∧ ∀𝑥3 (𝑆𝑥3 → 𝐼𝑥1 𝑥2 𝑥3 )))
Clearly, such sentences are not in the ordered fragment defined in the previous section, since
they typically contain atoms of the form 𝑃 𝑥𝑛 , where 𝑛 > 1, whereas this is now accommodated
by the grooved fragment. In fact, the grooved fragment is more expressive than many systems
for the relational syllogistic. See e.g. [8] and [9] for a detailed comparison.
   Given the existence of formulas of the form 𝑃 𝑥𝑛 , we modify the satisfaction relation as
follows.
Definition 7 (Satisfaction for grooved formulas). Let ℳ = ⟨𝐷, 𝐼⟩ be a model for ℒ𝐹 𝑂𝐿 , 𝜎𝑛
be an 𝑛-tuple from 𝐷* , 𝑙𝑎𝑠𝑡(𝜎𝑛 ) be the last element of 𝜎𝑛 , and 𝜑𝑛 , 𝜓𝑛 be grooved formulas of
level 𝑛. Then:
    • 𝑀, 𝜎𝑛 ⊨ 𝑃 𝑥1 . . . 𝑥𝑛 iff 𝜎𝑛 ∈ 𝐼(𝑃 ) (𝑃 is not unary)
    • 𝑀, 𝜎𝑛 ⊨ 𝑃 𝑥𝑛 iff 𝑙𝑎𝑠𝑡(𝜎𝑛 ) ∈ 𝐼(𝑃 ) (𝑃 is unary)
    • 𝑀, 𝜎𝑛 ⊨ ¬𝜑𝑛 iff it is not the case that 𝑀, 𝜎𝑛 ⊨ 𝜑𝑛
    • 𝑀, 𝜎𝑛 ⊨ 𝜑𝑛 ∧ 𝜓𝑛 iff 𝑀, 𝜎𝑛 ⊨ 𝜑𝑛 and 𝑀, 𝜎𝑛 ⊨ 𝜓𝑛
    • 𝑀, 𝜎𝑛−1 ⊨ ∀𝑥𝑛 𝜑𝑛 iff for all 𝑎 ∈ 𝐷, 𝑀, 𝜎𝑛−1 𝑎 ⊨ 𝜑𝑛
  The translation function for the grooved fragment is slightly different from the one in
Definition 5. We will call the new function 𝑡𝑟 as well since no ambiguity will arise.
Definition 8 (Translation). The translation function, 𝑡𝑟 : 𝐹 𝑜𝑟𝑚𝑔𝑟𝑜 (ℒ𝐹 𝑂𝐿 ) −→ 𝐹 𝑜𝑟𝑚(ℒ𝑃 𝑀 𝐿 ),
is defined recursively as follows:
    • 𝑡𝑟(𝑃𝑖 𝑥1 . . . 𝑥𝑛 ) = 𝑝𝑖 (𝑃𝑖 is not unary)
    • 𝑡𝑟(𝑃𝑖 𝑥𝑛 ) = 𝑝𝑖 (𝑃𝑖 is unary)
    • 𝑡𝑟(¬𝜑) = ¬𝑡𝑟(𝜑)
    • 𝑡𝑟(𝜑 ∧ 𝜓) = 𝑡𝑟(𝜑) ∧ 𝑡𝑟(𝜓)
    • 𝑡𝑟(∀𝑥𝜑) = □𝑡𝑟(𝜑)
 Now we present a modified way to construct a Kripke model from a first-order one. Let
ℳ = ⟨𝐷, 𝐼⟩ be a model for ℒ𝐹 𝑂𝐿 . Then the ℒ𝑃 𝑀 𝐿 -analogue of ℳ, M = ⟨𝑊, 𝑅, 𝑉 ⟩, is a
model for ℒ𝑃 𝑀 𝐿 defined as below:
    • 𝑊 = 𝐷*
    • for any 𝜎, 𝜏 ∈ 𝑊 , 𝑅𝜎𝜏 iff 𝜏 = 𝜎𝑎 for some 𝑎 ∈ 𝐷
    • for non-unary 𝑃𝑖 , 𝑉 (𝑝𝑖 ) = 𝐼(𝑃𝑖 )
    • for unary 𝑃𝑖 , 𝑉 (𝑝𝑖 ) = {𝜎 ∈ 𝐷* ∖ {𝜖} : 𝑙𝑎𝑠𝑡(𝜎) ∈ 𝐼(𝑃𝑖 )} (𝜖 is the empty tuple)
M is obviously a KD-model over a tree.
Proposition 5 (Satisfiability invariance for ℒ𝑃 𝑀 𝐿 -analogues). Let ℳ be a model for ℒ𝐹 𝑂𝐿
and M its ℒ𝑃 𝑀 𝐿 -analogue. For 𝑛 ≥ 0, if 𝜑𝑛 is a grooved formula of level 𝑛 and 𝜎𝑛 is an 𝑛-tuple
in 𝐷* , then: ℳ, 𝜎𝑛 ⊨ 𝜑𝑛 iff M, 𝜎𝑛 ⊨ 𝑡𝑟(𝜑𝑛 ).
Proof. As in Proposition 1.

   Thus, in particular, a grooved sentence 𝜑 is true in ℳ exactly when 𝑡𝑟(𝜑) is true at the root
of M.
   Given a grooved sentence 𝜑, let S(𝜑) be the set of propositional variables corresponding
to the unary predicates in 𝜑. Let Γ(𝜑) be the set of maximal consistent sets of literals (i.e.
propositional variables or their negation) formed by elements of S(𝜑), and let
                                           {︁⋀︁              }︁
                                  Ψ(𝜑) =         Σ : Σ ∈ Γ(𝜑)
                        ⎛                        ⎞    ⎛                           ⎞
                              ⋀︁                             ⋀︁
               Υ(𝜑) = ⎝             (♢𝜓 → □♢𝜓)⎠ ∧ ⎝               (¬♢𝜓 → □¬♢𝜓)⎠
                          𝜓∈Ψ(𝜑)                          𝜓∈Ψ(𝜑)



Proposition 6. Let ℳ = ⟨𝐷, 𝐼⟩ be a model for ℒ𝐹 𝑂𝐿 , M = ⟨𝑊, 𝑅, 𝑉 ⟩ be the ℒ𝑃 𝑀 𝐿 -analogue
of ℳ. Then Υ(𝜑) is valid (globally true) in M.

Proof. We observe that for any 𝜎, 𝜏 ∈ 𝐷* ∖ {𝜖}, if 𝑙𝑎𝑠𝑡(𝜎) = 𝑙𝑎𝑠𝑡(𝜏 ) then: for any 𝑠 ∈ S(𝜑),
𝜎 ∈ 𝑉 (𝑠) iff 𝜏 ∈ 𝑉 (𝑠).

   So far, we have seen that if a grooved sentence 𝜑 is satisfiable, then its translation 𝑡𝑟(𝜑)
is satisfied in a KD-model where Υ(𝜑) is valid. For the opposite direction we start from the
following observations.
   Given a KD-model where Υ(𝜑) is valid and 𝑡𝑟(𝜑) is satisfied, a filtration of the model through
the set of subformulas of Υ(𝜑) or 𝑡𝑟(𝜑) preserves the satisfiability of 𝑡𝑟(𝜑) as well as the validity
(global truth) of Υ(𝜑). Also, since the filtration remains a KD-model and has a bounded size, its
tree unravelling at the node satisfying 𝑡𝑟(𝜑) is a KD-model in which each node has a bounded
number of children.
   For simplicity, from now on we always assume the restriction of ℒ𝐹 𝑂𝐿 to the predicates
occurring in 𝜑, and, correspondingly, the restriction of ℒ𝑃 𝑀 𝐿 to the propositional variables
occurring in 𝑡𝑟(𝜑).
   Given a Kripke model M = ⟨𝑊, 𝑅, 𝑉 ⟩, let the sort of each 𝑤 ∈ 𝑊 , written 𝑠𝑟𝑡(𝑤), be as
follows:

                                   𝑠𝑟𝑡(𝑤) = {𝑠 ∈ S(𝜑) : 𝑤 ∈ 𝑉 (𝑠)}

Proposition 7. Let M = ⟨𝑊, 𝑅, 𝑉 ⟩ be a tree model for ℒ𝑃 𝑀 𝐿 , with 𝑤0 ∈ 𝑊 its root, such
that Υ(𝜑) is valid in M. For any 𝑤, 𝑢, 𝑣 ∈ 𝑊 , if 𝑅𝑤𝑢 then there is 𝑢′ ∈ 𝑊 s.t. 𝑅𝑣𝑢′ and
𝑠𝑟𝑡(𝑢) = 𝑠𝑟𝑡(𝑢′ ).

Proof. Suppose 𝑠1 , . . . , 𝑠𝑛⋀︀are all the members of S(𝜑). Let 𝑛𝑖=1 ±𝑠𝑖 be the conjunction of
                                                                ⋀︀
literals true at 𝑢. Then ♢ 𝑛𝑖=1 ±𝑠𝑖 is true at 𝑤. Since Υ(𝜑) is valid in the model, in particular
we have that
                                            𝑛
                                           ⋀︁            𝑛
                                                        ⋀︁
                                         ♢    ±𝑠𝑖 → □♢     ±𝑠𝑖
                                         𝑖=1           𝑖=1
and
                                          𝑛
                                         ⋀︁                 𝑛
                                                           ⋀︁
                                    ¬♢         ±𝑠𝑖 → □¬♢         ±𝑠𝑖
                                         𝑖=1               𝑖=1
                                           ⋀︀𝑛
are valid, from which  we
                     ⋀︀𝑛  can show  that ♢     𝑖=1 ±𝑠𝑖 is true (false) at the root 𝑤0 iff it is globally
true (false). Since ♢ 𝑖=1 ±𝑠𝑖 is true at 𝑤, it must also⋀︀be true at 𝑤0 , and therefore globally true.
Thus, for any 𝑣 ∈ 𝑊 , there is 𝑢′ ∈ 𝑊 s.t. 𝑅𝑣𝑢′ and 𝑛𝑖=1 ±𝑠𝑖 is true there.

  Given a Kripke model M = ⟨𝑊, 𝑅, 𝑉 ⟩ and 𝑤 ∈ 𝑊 , let

                              Srt(𝑤) = {𝑠𝑟𝑡(𝑢) : 𝑢 ∈ 𝑊 and 𝑅𝑤𝑢}

Then, if M is a tree model and Υ(𝜑) is valid in M, by Proposition 7 we have that, for any
𝑤, 𝑣 ∈ 𝑊 , Srt(𝑤) = Srt(𝑣). We thus call M a well-sorted tree model, and let

                                  Srt(M) = {𝑠𝑟𝑡(𝑤) : 𝑤 ∈ 𝑊 }

Also, if ⟨𝑊, 𝑅⟩ is an 𝑚-ary tree, we have |Srt(M)| ≤ 𝑚.
  For a well-sorted tree model M = ⟨𝑊, 𝑅, 𝑉 ⟩, we denote the members of Srt(M) by
Q1 , . . . , Q|Srt(M)| , and then, for each 𝑤 ∈ 𝑊 , let

                           Q𝑖 (𝑤) = {𝑢 ∈ 𝑊 : 𝑅𝑤𝑢 and 𝑠𝑟𝑡(𝑢) = Q𝑖 }

Let 𝜇(Q𝑖 ) be the maximum number of children of sort Q𝑖 that a node of the tree can have, i.e.

                                𝜇(Q𝑖 ) = 𝑚𝑎𝑥{|Q𝑖 (𝑤)| : 𝑤 ∈ 𝑊 }

Obviously, if ⟨𝑊, 𝑅⟩ is an 𝑚-ary tree, then 𝜇(Q𝑖 ) ≤ 𝑚.
  In a well-sorted tree model M = ⟨𝑊, 𝑅, 𝑉 ⟩, a node 𝑤 ∈ 𝑊 is fulfilled iff for 1 ≤ 𝑖 ≤
|Srt(M)|, |Q𝑖 (𝑤)| = 𝜇(Q𝑖 ). A well-sorted tree model is fulfilled iff all of its nodes are fulfilled.
Clearly, the frame of a fulfilled tree model is a perfect tree.
  We next proceed, as in Section 2, by showing how to expand a serial tree to a perfect tree.
This time, though, the number of children of each node in the resulting tree may be higher than
the maximum number of children of a node in the original tree.
Proposition 8 (From a well-sorted tree model to a fulfilled tree model). Let M = ⟨𝑊, 𝑅, 𝑉 ⟩ be
a well-sorted tree model over a serial 𝑚-ary tree
                                               (︁∑︀(𝑚 > 0) with root
                                                                   )︁ 𝑤0 . Then there is a fulfilled
              ′       ′   ′   ′                     |Srt(M)|
tree model M = ⟨𝑊 , 𝑅 , 𝑉 ⟩ over a perfect          𝑖=1      𝜇(Q𝑖 ) -ary tree with root 𝑤0′ , and a
surjective bounded morphism 𝑓 : M′ −→ M s.t. 𝑓 (𝑤0′ ) = 𝑤0 .
Proof. The following procedure constructs M′ and 𝑓 .

Stage 0 Set M0 = ⟨𝑊0 , 𝑅0 , 𝑉0 ⟩ = M, and 𝑓0 = 𝑖𝑑𝑊 .

Stage n+1 If M𝑛 = ⟨𝑊𝑛 , 𝑅𝑛 , 𝑉𝑛 ⟩ is not fulfilled, choose the lowest node 𝑤 ∈ 𝑊𝑛 which is not
     fulfilled; if there are multiple such nodes, choose one. For the least 𝑖 s.t. |Q𝑖 (𝑤)| < 𝜇(Q𝑖 ):

      Pick up a 𝑣 ∈ 𝑊𝑛 s.t. 𝑅𝑛 𝑤𝑣 and 𝑠𝑟𝑡(𝑣) = Q𝑖 , and let
            𝑈 = {𝑢 ∈ 𝑊𝑛 : 𝑅𝑛* 𝑣𝑢} (𝑅𝑛* is the reflexive and transitive closure of 𝑅𝑛 )

      Let 𝑙 = 𝜇(Q𝑖 ) − |Q𝑖 (𝑤)|. For 1 ≤ 𝑗 ≤ 𝑙, let 𝑈𝑗 be a set of fresh nodes s.t. |𝑈𝑗 | = |𝑈 |; and
      let 𝑔𝑗 : 𝑈𝑗 −→ 𝑈 be a bijection. Let 𝑆𝑗 ⊆ 𝑈𝑗2 and 𝑇𝑗 : 𝑃 𝑟𝑜𝑝 −→ 𝒫(𝑈𝑗 ) be as follows:

            for any 𝑢, 𝑢′ ∈ 𝑈𝑗 , 𝑆𝑗 𝑢𝑢′ iff 𝑅𝑛 𝑔𝑗 (𝑢)𝑔𝑗 (𝑢′ )
            for any 𝑢 ∈ 𝑈𝑗 and any 𝑝 ∈ 𝑃 𝑟𝑜𝑝, 𝑢 ∈ 𝑇𝑗 (𝑝) iff 𝑔𝑗 (𝑢) ∈ 𝑉𝑛 (𝑝)

      Then, set M𝑛+1 = ⟨𝑊𝑛+1 , 𝑅𝑛+1 , 𝑉𝑛+1 ⟩ where
                             ⋃︀
            𝑊𝑛+1 = 𝑊𝑛 ∪   1≤𝑗≤𝑙 𝑈𝑗

            𝑅𝑛+1 = 𝑅𝑛 ∪ {(𝑤, 𝑔𝑗−1 (𝑣)) : 1 ≤ 𝑗 ≤ 𝑙} ∪ 1≤𝑗≤𝑙 𝑆𝑗
                                                     ⋃︀

            for any 𝑝 ∈ 𝑃 𝑟𝑜𝑝, 𝑉𝑛+1 (𝑝) = 𝑉𝑛 (𝑝) ∪
                                                        ⋃︀
                                                          1≤𝑗≤𝑙 𝑇𝑗 (𝑝)

      Also, let 𝑓𝑛+1 : M𝑛+1 −→ M𝑛 be the function such that
                       {︃
                         𝑤      𝑤 ∈ 𝑊𝑛
            𝑓𝑛+1 (𝑤) =
                         𝑔𝑗 (𝑤) 𝑤 ∈ 𝑈𝑗

    As before, we end up with the desired  tree model     ′ = ⟨𝑊 ′ , 𝑅′ , 𝑉 ′ ⟩ where: 𝑊 ′ =    𝑊𝑛 ;
                                                                                             ⋃︀
                                                       M
𝑅 = 𝑅𝑛 ; for any 𝑝 ∈ 𝑃 𝑟𝑜𝑝, 𝑉 (𝑝) = 𝑉𝑛 (𝑝). Obviously, each node in M has exactly
  ′                                 ′                                                  ′
        ⋃︀                                  ⋃︀
∑︀|Srt(M)|
    𝑖=1    𝜇(Q𝑖 ) children. We can also define the surjective bounded morphism 𝑓 : M′ −→ M
in the same way as in the proof of Proposition 2.

   Now, with a fulfilled tree model we can build a first-order model. Let M = ⟨𝑊, 𝑅, 𝑉 ⟩ be
a fulfilled tree model for ℒ𝑃 𝑀 𝐿 , where ⟨𝑊, 𝑅⟩ is a perfect 𝑚-ary tree (𝑚 > 0). Let 𝐷 be an
arbitrary set s.t. |𝐷| = 𝑚, and 𝐸 ⊆ 𝐷* × 𝐷* be a relation s.t., for 𝜎, 𝜏 ∈ 𝐷* , 𝐸𝜎𝜏 iff 𝜎 = 𝜏 𝑎
for some 𝑎 ∈ 𝐷; accordingly, ⟨𝐷* , 𝐸⟩ is isomorphic to ⟨𝑊, 𝑅⟩. Let ℎ : ⟨𝐷* , 𝐸⟩ −→ ⟨𝑊, 𝑅⟩ be
an isomorphism such that

      for 𝜎, 𝜎 ′ ∈ 𝐷* ∖ {𝜖}, if 𝑙𝑎𝑠𝑡(𝜎) = 𝑙𝑎𝑠𝑡(𝜎 ′ ) then 𝑠𝑟𝑡(ℎ(𝜎)) = 𝑠𝑟𝑡(ℎ(𝜎 ′ )).

Let 𝐼 be an interpretation function on ℒ𝐹 𝑂𝐿 such that: for any 𝑛-ary predicate 𝑃𝑖 , 𝐼(𝑃𝑖 ) = {𝜎 ∈
𝐷𝑛 : ℎ(𝜎) ∈ 𝑉 (𝑝𝑖 )}. Then ℳ = ⟨𝐷, 𝐼⟩ is a model for ℒ𝐹 𝑂𝐿 , and we call it an ℒ𝐹 𝑂𝐿 -analogue
of M.

Proposition 9 (Satisfiability invariance for ℒ𝐹 𝑂𝐿 -analogues). Let M be a fulfilled tree model
for ℒ𝑃 𝑀 𝐿 and ℳ its ℒ𝐹 𝑂𝐿 -analogue. Then: for 𝑛 ≥ 0, M, ℎ(𝜎𝑛 ) ⊨ 𝑡𝑟(𝜑𝑛 ) iff ℳ, 𝜎𝑛 ⊨ 𝜑𝑛 ,
where 𝜑𝑛 is a grooved formula of level 𝑛, and 𝜎𝑛 is an 𝑛-tuple from 𝐷* .

Proof. By induction on grooved formulas.

Proposition 10 (Satisfiability invariance under 𝑡𝑟). Let 𝜑 be a grooved sentence. Then: 𝜑 is
satisfiable iff 𝑡𝑟(𝜑) is satisfied in a KD-model in which Υ(𝜑) is valid. Therefore, the satisfiability
problem for the grooved fragment is decidable.
Proof. By Propositions 5, 6,7, 8, and 9.

  Let KD+Υ(𝜑) be the system obtained by adding Υ(𝜑) to an axiomatic basis for KD. The
construction provided in this section indicates that we can build a conservative extension of both
the grooved fragment and KD+Υ(𝜑). To see this, one can proceed as at the end of Section 2.


4. The loosely grooved fragment
In this section we define an ordered fragment more expressive than the grooved fragment. We
call it the loosely grooved fragment. We will show that each sentence in this fragment can be
rewritten into a satisfiability-equivalent grooved sentence.
Definition 9 (Loosely grooved formulas). The set of loosely grooved formulas 𝐹 𝑜𝑟𝑚𝑔𝑟𝑜′ (ℒ𝐹 𝑂𝐿 )
is the smallest subset of 𝐹 𝑜𝑟𝑚(ℒ𝐹 𝑂𝐿 ) that satisfies the following conditions:
   1. For each (𝑛 − 𝑚 + 1)-ary predicate 𝑃 (𝑚 ≤ 𝑛), 𝑃 𝑥𝑚 . . . 𝑥𝑛 is a loosely grooved formula
      of level 𝑛.
   2. If 𝜑 is a loosely grooved formulas of level 𝑛, then so is ¬𝜑.
   3. If 𝜑(𝑥𝑙 , . . . , 𝑥𝑛 ) and 𝜓(𝑥𝑚 , . . . , 𝑥𝑛 ) are loosely grooved formulas of level 𝑛, whose free
      variables are exactly those in the parentheses respectively, and one of the following
      conditions holds, then so is (𝜑 ∧ 𝜓):
          • 𝑙 = 𝑚, i.e. 𝜑 and 𝜓 have the same free variables
          • 𝑙 = 𝑛 or 𝑚 = 𝑛, i.e. one of 𝜑 and 𝜓 has exactly 𝑥𝑛 free
          • 𝑙 > 𝑛 or 𝑚 > 𝑛, i.e. one of them has no free variable
   4. If 𝜑 is a loosely grooved formula of level 𝑛 (𝑛 > 0), then ∀𝑥𝑛 𝜑 is a grooved formula of
      level 𝑛 − 1.
  Note that if, for example, 𝑃 is a ternary predicate and 𝑄 is a binary predicate, then 𝑃 𝑥2 𝑥3 𝑥4 ∧
𝑄𝑥3 𝑥4 is not a formula of the loosely grooved fragment (even though both 𝑃 𝑥2 𝑥3 𝑥4 and 𝑄𝑥3 𝑥4
are loosely grooved formulas of level 4), since the two conjuncts have different numbers of free
variables and both of them have more than one free variable.
  Before describing a general procedure for rewriting a loosely grooved sentence into a
satisfiability-equivalent grooved one, let us take a look at an example. The following sen-
tence is not grooved but loosely grooved:

                      ∀𝑥1 (𝑃 𝑥1 → ∀𝑥2 (∀𝑥3 (𝑃 𝑥3 → 𝑅𝑥2 𝑥3 ) → ¬𝑅𝑥1 𝑥2 ))

Since the atom 𝑅𝑥2 𝑥3 is not grooved. Notice that, if we introduce a fresh unary predicate, say 𝑄,
substitute 𝑄𝑥2 for ∀𝑥3 (𝑃 𝑥3 → 𝑅𝑥2 𝑥3 ), and conjoin the result with the formula ∀𝑥1 (𝑄𝑥1 ↔
∀𝑥2 (𝑃 𝑥2 → 𝑅𝑥1 𝑥2 )), we get

          ∀𝑥1 (𝑃 𝑥1 → ∀𝑥2 (𝑄𝑥2 → ¬𝑅𝑥1 𝑥2 )) ∧ ∀𝑥1 (𝑄𝑥1 ↔ ∀𝑥2 (𝑃 𝑥2 → 𝑅𝑥1 𝑥2 ))

which is satisfiability-equivalent to the original formula. Notice also that 𝑄𝑥2 is a grooved
formula of level 2, and 𝑄𝑥1 and ∀𝑥2 (𝑃 𝑥2 → 𝑅𝑥1 𝑥2 ) are grooved formulas of level 1, so the
whole formula is indeed a grooved sentence.
   In the following we write ∀𝑥𝑖+1 𝜑(𝑥𝑖 , 𝑥𝑖+1 ) for a formula in that form where 𝜑 has exactly
𝑥𝑖 and 𝑥𝑖+1 free (so the whole formula has only 𝑥𝑖 free). We say a loosely grooved formula is
bad if it is not grooved and is of the form ∀𝑥𝑖+1 𝜑(𝑥𝑖 , 𝑥𝑖+1 ), where 𝑖 > 1.

Proposition 11. Let 𝜙 be a loosely grooved sentence. We can effectively construct a loosely grooved
sentence 𝜙′ which is (i) satisfiability-equivalent to 𝜙 and (ii) free of bad subformulas.

Proof. The following procedure constructs the sentence we desire. It starts by setting 𝜙0 := 𝜙.
Then, for each loosely grooved sentence 𝜙𝑘 , if 𝜙𝑘 contains a bad subformula ∀𝑥𝑖+1 𝜑(𝑥𝑖 , 𝑥𝑖+1 )
of which no proper-subformula is bad, choose a unary predicate 𝑄 not occurring in 𝜙𝑘 , and let

                              𝜙𝑘+1 := 𝜙𝑛 [∀𝑥𝑖+1 𝜑(𝑥𝑖 , 𝑥𝑖+1 )/𝑄𝑥𝑖 ]

                              𝜓𝑘+1 := ∀𝑥1 (𝑄𝑥1 ↔ ∀𝑥1 𝜑(𝑥1 , 𝑥2 ))
where ∀𝑥1 𝜑(𝑥1 , 𝑥2 ) is the result of decreasing all indices of variables in ∀𝑥𝑖+1 𝜑(𝑥𝑖 , 𝑥𝑖+1 ) by
𝑖 − 1.
   Observe that 𝑄𝑥𝑖 is a loosely grooved formula of level 𝑖, and 𝑄𝑥1 , ∀𝑥1 𝜑(𝑥1 , 𝑥2 ) are loosely
grooved formulas of level 1, so 𝜙𝑛+1 and 𝜓𝑛+1 are both loosely grooved sentences. Also,
since ∀𝑥𝑖+1 𝜑(𝑥𝑖 , 𝑥𝑖+1 ) contains no non-grooved subformula of the form ∀𝑥𝑗+1 𝜓(𝑥𝑗 , 𝑥𝑗+1 )
(𝑗 > 𝑖), we observe that ∀𝑥1 𝜑(𝑥1 , 𝑥2 ) contains no bad subformulas. Therefore, the procedure
will terminate on a loosely grooved sentence 𝜙𝑛 free from bad subformulas, together with a
sequence of formulas 𝜓1 , . . . , 𝜓𝑛 , all of which are free from bad subformulas, too. Finally, let

                                    𝜙′ := 𝜙𝑛 ∧ 𝜓1 ∧ · · · ∧ 𝜓𝑛

Clearly, 𝜙′ is a loosely grooved sentence satisfiability-equivalent to 𝜙.

  The following result shows that the procedure indeed gives us a grooved sentence.

Proposition 12. A loosely grooved sentence 𝜙 free from bad subformulas is a grooved sentence.

Proof. Looking at Definition 9, we observe that the definition of grooved formulas is the special
case where in clause 1 we only allow that 𝑚 = 1 or 𝑚 = 𝑛. (Since in that case the conditions
on forming conjunctions are automatically satisfied.) In other words, a loosely grooved formula
is grooved if all of its atomic subformulas are of the form 𝑃 𝑥1 . . . 𝑥𝑛 or 𝑃 𝑥𝑛 .
   Thus, we only need to show that 𝜙 contains no atomic formulas of the form 𝑃 𝑥𝑚 . . . 𝑥𝑛
(1 < 𝑚 < 𝑛). Suppose to the contrary that 𝜙 contains 𝑃 𝑥𝑚 . . . 𝑥𝑛 (1 < 𝑚 < 𝑛). Given the
constraints on forming conjunctions, we observe that a superformula of 𝑃 𝑥𝑚 . . . 𝑥𝑛 having at
least 𝑥𝑚 and 𝑥𝑚+1 free cannot form a conjunction with any formula having also 𝑥𝑙 free, where
𝑙 < 𝑚. Let 𝜑(𝑥𝑚 , 𝑥𝑚+1 ) be the largest superformula of 𝑃 𝑥𝑚 . . . 𝑥𝑛 which has exactly 𝑥𝑚 and
𝑥𝑚+1 free. Since 𝜑 is the largest such subformula of 𝜙, we know that neither ¬𝜑(𝑥𝑚 , 𝑥𝑚+1 )
nor 𝜑(𝑥𝑚 , 𝑥𝑚+1 ) ∧ 𝜓 (where 𝜓 has at most 𝑥𝑚 and 𝑥𝑚+1 free) are subformulas of 𝜑. Thus,
∀𝑥𝑚+1 𝜑(𝑥𝑚 , 𝑥𝑚+1 ) is a subformula of 𝜙. Since ∀𝑥𝑚+1 𝜑(𝑥𝑚 , 𝑥𝑚+1 ) is a superformula of
𝑃 𝑥𝑚 . . . 𝑥𝑛 , it is not grooved and hence bad, contradicting the assumption that 𝜙 has no such
subformula.
5. Final remarks
Ordered fragments of 𝐹 𝑂𝐿 can be used to describe properties of data structures like lists, stacks
or queues, given that information is stored in a sequential way in these structures. Different
fragments allow one to capture different properties of data structures. We mention two simple
examples of this use in the case of the grooved fragment.
   Suppose that we read the predicate 𝑆 𝑛 (for 𝑛 ≥ 1) as “form(s) a stack with 𝑛 elements” and
the predicate 𝑅 as “is removed”. Then, consider the following grooved formula:

                      ∃𝑥𝑛+1 (𝑆 𝑛+1 𝑥1 . . . 𝑥𝑛+1 ∧ 𝑅𝑥𝑛+1 ) → 𝑆 𝑛 𝑥1 . . . 𝑥𝑛
    This may be used to say that if an object is at the top of a stack and it is removed, we get
a smaller stack. In other words, if we have a stack of 𝑛 objects where 𝑥𝑛 is the latest object
(i.e. the one at the top) and we perform the operation of removing 𝑥𝑛 , then we get a stack with
𝑛 − 1 elements (i.e. 𝑥1 , . . . , 𝑥𝑛−1 ).
    Moreover, suppose that we read the predicate 𝐴 as “is added”. Then, consider the following
grooved formula:

                      𝑆 𝑛 𝑥1 . . . 𝑥𝑛 → ∃𝑥𝑛+1 (𝐴𝑥𝑛+1 ∧ 𝑆 𝑛+1 𝑥1 . . . 𝑥𝑛+1 )

This may be used to say that an object can always be added on top of a stack,. In other words, if
𝑥1 , . . . , 𝑥𝑛 form a stack with 𝑛 elements, then there is some object 𝑥𝑛+1 s.t. if one performs
the action of adding 𝑥𝑛+1 , one gets a stack with 𝑛 + 1 elements (i.e. 𝑥1 , . . . , 𝑥𝑛 , 𝑥𝑛+1 ).
   From a theoretical point of view, the motivation for introducing the loosely grooved fragment,
the strongest of the fragments analysed in this article, has two main sources. First, some
extended systems of the relational syllogistic feature sentences that are not accommodated by
the grooved fragment. For example,

      Everything which is 𝑅elated to something which is 𝑅elated to every 𝑄 is not 𝑃 .
      ∀𝑥1 (∃𝑥2 (∀𝑥3 (𝑄𝑥3 → 𝑅𝑥2 𝑥3 ) ∧ 𝑅𝑥1 𝑥2 ) → ¬𝑃 𝑥1 )

So, for a generalization to such systems of the relational syllogistic, we need an expansion
in more or less the same spirit as the loosely grooved fragment. In fact, the formulation of
the loosely grooved fragment allows for much more sentences than the relational syllogistic,
as most languages in that context only allow for unary and binary predicates, and Boolean
operations are highly restricted. (Again, see [8] and [9] for a detailed comparison.)
   Second, the loosely grooved fragment is, from a different aspect, a generalization of what we
can call the ‘modal fragment’ of first-order logic, i.e. the fragment in which all formulas are the
standard translation of some modal formula. Note that the standard translation of basic modal
formulas are all loosely grooved formulas, provided that variables are suitably chosen. Given a
modal formula 𝜒, we can define the standard translation 𝑠𝑡 for its subformulas as follows:

    • 𝑠𝑡(𝑝) = 𝑃 𝑥𝑛+1 , if 𝑝 is in the scope of exactly 𝑛 □’s
    • 𝑠𝑡(¬𝜑) = ¬𝑠𝑡(𝜑)
    • 𝑠𝑡(𝜑 ∧ 𝜓) = 𝑠𝑡(𝜑) ∧ 𝑠𝑡(𝜓)
    • 𝑠𝑡(□𝜑) = ∀𝑥𝑛+1 (𝑅𝑥𝑛 𝑥𝑛+1 → 𝑠𝑡(𝜑)), where 𝑥𝑛+1 is the free variable in 𝑠𝑡(𝜑)
Observe that if a subformula is in the scope of exactly 𝑛 □’s, its translation has exactly 𝑥𝑛+1
free, so 𝑠𝑡 always outputs a loosely grooved formula of level 1.
   Meanwhile, the loosely grooved fragment, and, indeed, all ordered fragments mentioned in
this paper, are not comparable with the guarded fragment of 𝐹 𝑂𝐿. Recall the example,

      No student admires every professor
      ∀𝑥1 (𝑆𝑥1 → ∃𝑥2 (𝑃 𝑥2 ∧ ¬𝐴𝑥1 𝑥2 ))

Clearly, the subformula ∃𝑥2 (𝑃 𝑥2 ∧ ¬𝐴𝑥1 𝑥2 ) is not guarded.
  The fluted fragment (see [4, 5]) can be seen as a generalization of the loosely grooved fragment
by allowing conjunction between any two formulas of the same level in clause 3 of Definition 9.
One direction of our future work is to investigate the modal translation of the fluted fragment.


Acknowledgments
The following statement applies to Matteo Pascucci: This research was funded in whole or in
part by the Austrian Science Fund (FWF) 10.55776/I6499. For open access purposes, the author
has applied a CC BY public copyright license to any author-accepted manuscript version arising
from this submission.


References
[1] R. Jaakkola, Ordered fragments of first-order logic, in: Proceedings of MCFS2021, 2021, pp.
    1–14.
[2] W. V. O. Quine, Variables explained away, Proceedings of the American Philosophical
    Society 104 (1960) 343–347.
[3] A. Herzig, A new decidable fragment of first-order logic, Abstracts of the 3rd Logical
    Biennial Summer School and Conference in Honour of S. C. Kleene (1990).
[4] I. Pratt-Hartmann, W. Szwast, L. Tendera, The fluted fragment revisited, The Journal of
    Symbolic Logic 84 (2019) 1020–1048. doi:10.1017/jsl.2019.33.
[5] W. C. Purdy, Fluted formulas and the limits of decidability, Journal of Symbolic Logic 61
    (1996) 608–620. doi:10.2307/2275678.
[6] P. Blackburn, M. d. Rijke, Y. Venema, Modal Logic, Cambridge Tracts in Theoretical Com-
    puter Science, Cambridge University Press, 2001.
[7] F. Pelletier, A. Urquhart, Synonymous logics, Journal of Philosophical Logic 32 (2003)
    259–285. doi:10.1023/A:1024248828122.
[8] A. Kruckman, L. S. Moss, Exploring the landscape of relational syllogistic logics, The
    Review of Symbolic Logic 14 (2021) 728–765. doi:10.1017/S1755020320000386.
[9] I. Pratt-Hartmann, L. S. Moss, Logics for the relational syllogistic, The Review of Symbolic
    Logic 2 (2009) 647–683. doi:10.1017/S1755020309990086.

</pre>