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.
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 [
For example, the following sentence belongs to Quine’s ordered fragment:
∀1( 1 → ∃2(12 ∧ ∀3123)).
Herzig [
Herzig’s translation relies on an intuitive reading of quantifiers as modal operators: ∀ corresponds 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 [
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 .
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 difer 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 . . . if ∈ () • ℳ, ⊨ ¬ if it is not the case that
ℳ, ⊨ • ℳ, ⊨ ∧ if ℳ, ⊨ and ℳ, ⊨ • ℳ, − 1 ⊨ ∀ if 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, ⊨ □ if 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 if (∀ ∈ )(∃ ∈ ).
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, . . . , ) if – = ( + 1), – for 1 ≤ ≤ , = , – +1; • for ∈ , (1, . . . , ) ∈ ′() if ∈ ().
Definition 4 (Bounded morphism). A bounded morphism from an ℒ -model M to an ℒ -model M′ is a function : →− ′ s.t.: • for ∈ and ∈ , ∈ () if () ∈ ′(); • 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, ⊨ if 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 [
This ends the preliminaries. Now we move on to the translation of (ℒ ) into
(ℒ ), which is due to Herzig [
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 ifrst-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 , ∈ , if = 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: ℳ, ⊨ if M, ⊨ ().
Proof. By induction on ordered formulas. We only analyse the case where = ∀+1 : ℳ, ⊨ ∀+1 if ℳ, ⊨ for every ∈ if (by I.H.) M, ⊨ ( ) for every ∈ if 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 if 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 if 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 , ′ ∈ , ′ if ()(′) for any ∈ and any ∈ , ∈ () if () ∈ () Then, set M+1 = ⟨+1, +1, +1⟩ where +1 = ∪ ⋃︀1≤ ≤ +1 = ∪ {(, − 1()) : 1 ≤ ≤ } ∪ ⋃︀1≤ ≤ for any ∈ , +1() = () ∪ ⋃︀1≤ ≤ () ′ = ⋃︀ ; ′ = ⋃︀ ; for any ∈ , ′() = ⋃︀ ().
This procedure yields the desired tree model M′ = ⟨ ′, ′, ′⟩ where: Moreover, we have the function : M′ →−
() = 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 ifrst-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 , ∈ * , if = 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, ℎ( ) ⊨ () if ℳ, ⊨ , where is an ordered formula of level , and is an -tuple from * .
Proposition 4 (Satisfiability invariance under ). Let be an ordered sentence. Then: is satisfiable if () is KD-satisfiable. Therefore, the satisfiability problem for Quine’s ordered fragment is decidable.
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 [
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.
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: 1For instance, consider the following case: ∀11 ↔ □ . Let be a hybrid model and a state in its domain. It holds that , ⊨ ∀11 if , () ⊨ ∀11 if , () ⊨ 1 for every ∈ if , ⊨ for every s.t. if , ⊨ □ . Therefore, , ⊨ ∀11 ↔ □ .
No student admires every professor
∀1(1 → ¬∀2( 2 → 12))
No lecturer introduces any professor to every student
∀1(1 → ¬∃2( 2 ∧ ∀3(3 → 123)))
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. [
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 . . . if ∈ ( ) ( is not unary) • , ⊨ if ( ) ∈ ( ) ( is unary) • , ⊨ ¬ if it is not the case that , ⊨ • , ⊨ ∧ if , ⊨ and , ⊨ • , − 1 ⊨ ∀ if for all ∈ , , − 1 ⊨
The translation function for the grooved fragment is slightly diferent 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 , ∈ , if = for some ∈ • for non-unary , () = () • for unary , () = { ∈ * ∖ { } : ( ) ∈ ()} ( is the empty tuple)
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: ℳ, ⊨ if M, ⊨ ().
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.
∈ () if ∈ ().
∈ * ∖ { }, if ( ) = ( ) then: for any ∈ S(),
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 if 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 if for 1 ≤ ≤ |Srt(M)|, |Q()| = (Q). A well-sorted tree model is fulfilled if 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 tree model M′ = ⟨ ′, ′, ′⟩ over a perfect ︁( ∑︀|S=r1t(M)| (Q))︁ -ary tree with root 0′, and a surjective bounded morphism : M′ →− M s.t. (0′) = 0.
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 Let = (Q) − | let : →−
Q()|. For 1 ≤ ≤ , let be a set of fresh nodes s.t. | | = | |; and be a bijection. Let ⊆ 2 and : →− ( ) be as follows: for any , ′ ∈ , ′ if () (′) for any ∈ and any ∈ , ∈ () if () ∈ () Then, set M+1 = ⟨+1, +1, +1⟩ where +1 = ∪ ⋃︀1≤ ≤ +1 = ∪ {(, − 1()) : 1 ≤ ≤ } ∪ ⋃︀1≤ ≤ for any ∈ , +1() = () ∪ ⋃︀1≤ ≤ ()
As before, we end up with the desired tree model M′ = ⟨ ′, ′, ′⟩ where: ′ = ⋃︀ ; ′ = ⋃︀ ; for any ∈ , ′() = ⋃︀ (). Obviously, each node in M′ has exactly ∑︀|S=r1t(M)| (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 , ∈ * , if = 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, ℎ( ) ⊨ () if ℳ, ⊨ , where is a grooved formula of level , and is an -tuple from * .
Proposition 10 (Satisfiability invariance under ). Let be a grooved sentence. Then: is satisfiable if () is satisfied in a KD-model in which Υ( ) is valid. Therefore, the satisfiability problem for the grooved fragment is decidable.
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.
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 234 ∧ 34 is not a formula of the loosely grooved fragment (even though both 234 and 34 are loosely grooved formulas of level 4), since the two conjuncts have diferent 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 sentence is not grooved but loosely grooved:
∀1( 1 → ∀2(∀3( 3 → 23) → ¬12)) Since the atom 23 is not grooved. Notice that, if we introduce a fresh unary predicate, say , substitute 2 for ∀3( 3 → 23), and conjoin the result with the formula ∀1(1 ↔ ∀2( 2 → 12)), we get
∀1( 1 → ∀2(2 → ¬12)) ∧ ∀1(1 ↔ ∀2( 2 → 12)) which is satisfiability-equivalent to the original formula. Notice also that 2 is a grooved formula of level 2, and 1 and ∀2( 2 → 12) 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 efectively 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.
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. Diferent fragments allow one to capture diferent 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(+11 . . . +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 ∧ +11 . . . +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 → 23) ∧ 12) → ¬ 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 [
Second, the loosely grooved fragment is, from a diferent 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 ∧ ¬12)) Clearly, the subformula ∃2( 2 ∧ ¬12) is not guarded.
The fluted fragment (see [
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.