=Paper=
{{Paper
|id=Vol-2211/paper-02
|storemode=property
|title=Decidability Frontier for Fragments of First-Order Logic with Transitivity
|pdfUrl=https://ceur-ws.org/Vol-2211/paper-02.pdf
|volume=Vol-2211
|authors=Lidia Tendera
|dblpUrl=https://dblp.org/rec/conf/dlog/Tendera18
}}
==Decidability Frontier for Fragments of First-Order Logic with Transitivity==
https://ceur-ws.org/Vol-2211/paper-02.pdf
Decidability frontier for fragments of first-order
logic with transitivity?
Lidia Tendera[0000−0003−0681−4040]
University of Opole, Poland
tendera@math.uni.opole.pl
Abstract. Several decidable fragments of first-order logic have been
identified in the past as a generalisation of the standard translation of
modal logic. These include: the fluted fragment, the two-variable frag-
ment, the guarded fragment and the unary negation fragment; some of
them have been recently generalised or combined to yield even more
expressive decidable logics (guarded negation fragment or uniform one-
dimensional fragment). None of the fragments allows one to express tran-
sitivity of a binary relation or related properties like being an equivalence,
a linear or a partial order, that naturally appear in specifications or in
verification. The question therefore arises what is the impact of adding
transitivity to these fragments and, where the cost is too high, how can
these languages be tamed.
In this talk we survey results concerning the decidability frontier of the
above-mentioned fragments extended with transitivity. We discuss both,
general and finite satisfiability, as presence of transitivity axioms often
allows one to express axioms of infinity. Simultaneously, we locate in the
picture known description logics, discuss relevant technics, admire a few
exotic results and state some open questions.
Keywords: First-Order logic · Decidability · (Finite) Satisfiability ·
Transitivity · Complexity.
Introduction and Preliminaries
It is well-known that formulas of propositional modal logics under Kripke se-
mantics can be naturally encoded in first-order logic, using the so-called stan-
dard translation (cf. [2]); the same applies to the basic description logic ALC and
many of its variations. Since first-order logic is not so well-behaved as modal or
description logics, in particular the (finite) satisfiability problems are undecid-
able, it was natural to ask what the right image of the standard translation is
and ’Why is modal logic so robustly decidable?’. This question opened an in-
teresting and fruitful research path in theoretical computer science, and in this
talk we explore part of the path.
The formulas obtained under the standard translation evince some patterns:
(i) variables appear in some fixed order and no rescoping of variables occurs, (ii)
?
The talk is supported by the European Association for Artificial Intelligence.
quantifiers are relativized by atomic formulas, (iii) negation is applied only to
subformulas with a single free variable. Moreover, by properly reusing variables:
(iv) the number of variables can be restricted to two.
The four syntactic restrictions considered separately give rise to four frag-
ments of first order logic: (i) the fluted fragment FL, (ii) the guarded fragment
GF, (iii) the unary negation fragment UN F, and (iv) the two-variable fragment
FO2 . All of the four languages have the finite model property, and hence are
decidable. As already mentioned in the abstract, none of them can express tran-
sitivity of a binary relation or related properties like being a partial order or an
equivalence relation. Hence, their extensions are studied when it is assumed that
some of the binary symbols from the signature are interpreted in a special way
(as transitive relations, orderings, equivalences etc.).
In the talk we review main properties of the above mentioned fragments
and describe the decidability frontier for their extensions with various transitive
relations. The presentation includes joint work with Georg Gottlob, Emanuel
Kieroński, Jakub Michaliszyn, Andreas Pieris, Ian Pratt-Hartmann, and Wieslaw
Szwast. In the next section we recall formal definitions of the four fragments
mentioned above; more surveying material with several references can be found
e.g. in [7, 4]. In Section 2 we present supplementary material that is featured in
the talk but has not yet been published elsewhere.
1 Definitions
We assume relational signatures not containing constants or function symbols.
Definition 1. The fluted fragment [5]: Let x̄ω = x1 , x2 , . . . be a fixed sequence
of variables. We define the sets of formulas FL[k] (for k ≥ 0) by structural
induction as follows: (i) any atom α(x` , . . . , xk ), where x` , . . . , xk is a contiguous
subsequence of x̄ω , is in FL[k] ; (ii) FL[k] is closed under boolean combinations;
(iii) if ϕ is in FL[k+1] , then ∃x
Sk+1 ϕ and ∀xk+1 ϕ are in FL[k] . The set of fluted
[k]
formulas is defined as FL = k≥0 FL . A fluted sentence is a fluted formula
over an empty set of variables, i.e. an element of FL[0] . Thus, when forming
Boolean combinations in the fluted fragment, all the combined formulas must
have as their free variables some suffix of some prefix x1 , . . . , xk of x̄ω ; and
when quantifying, only the last variable in this sequence may be bound.
Definition 2. The guarded fragment [1], GF, is defined as the least set of for-
mulas such that: (i) every atomic formula belongs to GF; (ii) GF is closed under
logical connectives ¬, ∨, ∧, →; and (iii) quantifiers are appropriately relativised
by atoms. More specifically, in GF, condition (iii) is understood as follows: if
ϕ is a formula of GF, α is an atomic formula featuring all the free variables
of ϕ, and x̄ is any sequence of variables in α, then the formulas ∀x̄(α → ϕ)
and ∃x̄(α ∧ ϕ) belong to GF. In this context, the atom α is called a guard. The
equality symbol when present in the signature is also allowed in guards.
Definition 3. The unary negation fragment [6], UN F, consists of formulas in
which the use of negation is restricted only to subformulas with at most one free
variable. More precisely, UN F is defined as the least set of formulas such that:
(i) every atomic formula of the form R(x̄) or x = y belongs to UN F; (ii) UN F
is closed under logical connectives ∨, ∧ and under existential quantification; (iii)
if ϕ(x) is a formula of UN F featuring no free variables besides (possibly) x, then
¬ϕ(x) belongs to UN F.
Definition 4. The two variable fragment: By the k-variable fragment of a logic
L, denoted Lk , we mean the set of formulas of L featuring at most k distinct
variables. In particular FOk denotes the set of all first-order formulas with at
most k variables.
All of the above languages are incomparable in terms of expressive power,
have the finite model property and the satisfiability problem (=finite satisfiabil-
ity problem) is decidable.
2 Fluted Fragment with Transitive Relations
We show two undecidability results for the fluted fragment with two variables,
FL2 , extended with transitive relations. We employ the apparatus of tiling sys-
tems (cf. e.g. [3]).
A tiling system is a tuple C = (C, CH , CV ), where C is a finite set of tiles,
and CH , CV ⊆ C × C are the horizontal and vertical constraints. Let S be any of
the spaces N × N, Z × Z or Zt × Zt . A tiling system C tiles S, if there exists a
function ρ : S → C such that for all (p, q) ∈ S: (ρ(p, q), ρ(p + 1, q)) ∈ CH and
(ρ(p, q), ρ(p, q + 1)) ∈ CV . It is known that the problem whether a given tiling
system tiles any of the spaces N × N, Z × Z, Zt × Zt is undecidable. To reduce one
of the problems to the (finite) satisfiability problem for some logic L we proceed
as follows.
Let C = (C, CH , CV ) be a tiling system. We write an L-formula ηC such that
the following reduction properties hold
(i) ηC is satisfiable iff C tiles N × N or Z × Z, and
(ii) ηC is finitely satisfiable iff C tiles Zt × Zt , for some t ≥ 1.
Properties (i) and (ii) above yield undecidability of the satisfiability, respectively,
finite satisfiability, problem for L.
In order to encode tilings using two-variable logics it is useful to define struc-
tures that are grid-like. A structure G = (G, h, v) with two binary relation h
and v is grid-like, if one of the standard grids N × N, Z × Z or Zt × Zt can
be homomorphically embedded into G. To show that a structure G is grid-like
it suffices to require that G |= ∀x(∃yh(x, y) ∧ ∃yv(x, y)) (note that this is an
FL2 -formula) and the following confluence property holds
G |= ∀x, x0 , y, y 0 ((h(x, y) ∧ v(x, x0 ) ∧ v(y, y 0 ) → h(x0 , y 0 )). (*)
The confluence property above uses four variables and is not fluted. We will
enforce it (or a variation of it) in FL2 using transitive relations.
2.1 Undecidability of F L2 with two transitive relations and equality
Suppose the signature contains two transitive relations b (blue) and r (red), and
additional unary predictes ci,j (0 ≤ i ≤ 3, 0 ≤ j ≤ 3) called colours. We write a
formula ϕgrid capturing several properties of the intended expansion of the Z×Z
grid as shown 03in Figure
13 1. 23
There,33each element
03 13 with 23
coordinates
33 (k, l) satisfies
ci,j , where i = k mod 4 and j = l mod 4 and the transitive relations connect
only some elements that are close in the grid. The formula ϕgrid is a conjunction
02 12 22 32 02 12 22 32
of the statements (1)-(7) described below; in the formulas in this subsection we
assume that addition in subscripts of the cij s is always understood modulo 4.
01 11 21 31 01 11 21 31
00 10 20 30 00 10 20 30
03 13 23 33 03 13 23 33
02 12 22 32 02 12 22 32
01 11 21 31 01 11 21 31
00 10 20 30 00 10 20 30
Fig. 1. Intended expansion of the Z × Z grid with transitive relations b and r. Edges
without arrows represent connections in both direction. Nodes are marked by the in-
dices of the cij s they satisfy.
(1) there is an initial element: ∃xc00 (x).
(2) the cij s enforce a partition of the universe: ∀x ˙ 0≤i≤3 ˙ 0≤j≤3 ci,j (x).
W W
(3) transitive paths do not connect distinct elements of the same colour:
^
∀x(cij (x) → ∀y((b(x, y) ∨ r(x, y)) ∧ cij (y) → x = y))
0≤i,j≤3
(4) each element belongs to a 4-element blue clique; we write the following con-
juncts for each i, j ∈ {0, 2}:
∀x(cij (x) → ∃y(b(x, y) ∧ ci+1,j (y)))
∀x(ci+1,j (x) → ∃y(b(x, y) ∧ ci+1,j+1 (y)))
∀x(ci+1,j+1 (x) → ∃y(b(x, y) ∧ ci,j+1 (y)))
∀x(ci,j+1 (x) → ∃y(b(x, y) ∧ cij (y)))
(5) each element belongs to a 4-element red clique; we write the following con-
juncts for each i, j ∈ {1, 3}:
∀x(cij (x) → ∃y(r(x, y) ∧ ci+1,j (y)))
∀x(ci+1,j (x) → ∃y(r(x, y) ∧ ci+1,j+1 (y)))
∀x(ci+1,j+1 (x) → ∃y(r(x, y) ∧ ci,j+1 (y)))
∀x(ci,j+1 (x) → ∃y(r(x, y) ∧ cij (y)))
(6) A group of formulas saying that some pairs of elements connected by r are
also connected by b:
^
∀x(cii (x) →∀y(r(x, y) ∧ (ci,i−1 (y) ∨ ci−1,i (y)) → b(x, y))) (6a)
i=0,2
^
∀x(cii (x) →∀y(r(x, y) ∧ (ci,i+1 (y) ∨ ci+1,i (y)) → b(x, y))) (6b)
i=1,3
^
∀x(ci,i+1 (x) →∀y(r(x, y) ∧ (ci,i+2 (y) ∨ ci−1,i+1 (y)) → b(x, y))) (6c)
i=0,2
^
∀x(ci,i−1 (x) →∀y(r(x, y) ∧ (cii (y) ∨ ci,i−2 (y)) → b(x, y))) (6d)
i=1,3
(7) A group of formulas saying that some pairs of elements connected by b are
also connected by r:
^
∀x(cii (x) →∀y(b(x, y) ∧ (ci,i−1 (y) ∨ ci−1,i (y)) → r(x, y))) (7a)
i=0,2
^
∀x(cii (x) →∀y(b(x, y) ∧ (ci,i+1 (y) ∨ ci+1,i (y)) → r(x, y))) (7b)
i=1,3
^
∀x(ci,i+1 (x) →∀y(b(x, y) ∧ (ci,i+2 (y) ∨ ci−1,i+1 (y)) → r(x, y))) (7c)
i=0,2
^
∀x(ci,i−1 (x) →∀y(b(x, y) ∧ (cii (y) ∨ ci,i−2 (y)) → r(x, y))) (7d)
i=1,3
It should be clear that the structure shown in Figure 1 is a model of ϕgrid . One
can note that ϕgrid has also finite models expanding a toroidal grid structure
Z4m × Z4m (m > 0) obtained by identifying elements from columns 0 and 4m
and from rows 0 and 4m.
Let us introduce the following definitions:
_ _
h(x, y) :=b(x, y) ∧ (cij (x) ∧ ci+1,j (y)) ∨ r(x, y) ∧ (cij (x) ∧ ci+1,j (y))
i=0,2 i=1,3
j=0,1,2,3 j=0,1,2,3
_ _
v(x, y) :=b(x, y) ∧ (cij (x) ∧ ci,j+1 (y)) ∨ r(x, y) ∧ (cij (x) ∧ ci,j+1 (y))
i=0,1,2,3 i=0,1,2,3
j=0,2 j=1,3
Let A |= ϕgrid . We show that every model (A, h, v) of ϕgrid is grid-like. We
first show that A satisfies ∀x(∃yh(x, y) ∧ ∃yv(x, y)). One considers several cases
depending on the values of the unary predicates.
Let a ∈ A and assume A |= c00 (a). By (4) there are a1 , a2 , a3 , a4 ∈ A such
that A |= b(a, a1 ) ∧ c10 (a1 ) ∧ b(a1 , a2 ) ∧ c11 (a2 ) ∧ b(a2 , a3 ) ∧ c01 (a3 ) ∧ b(a3 , a4 ) ∧
c00 (a4 ). By (3) a = a4 and by transitivity of b the elements a, a1 , a2 , a3 form a
blue clique in A. Hence, A |= h(a, a1 ) ∧ v(a, a3 ).
The same argument works if a has one of the colours c02 , c20 or c22 and,
similarly, applying (5) instead of (4) when a has the colours c11 , c31 , c13 or c33 .
Consider now the case A |= c10 (a). By (4) there is a0 ∈ A such that A |=
b(a, a0 ) ∧ c11 (a0 ), hence A |= v(a, a0 ). Moreover, by (5) there are a1 , a2 , a3 , a4 ∈ A
such that A |= r(a, a1 )∧c13 (a1 )∧r(a1 , a2 )∧c23 (a2 )∧r(a2 , a3 )∧c20 (a3 )∧r(a3 , a4 )∧
c10 (a4 ). By (3) a = a4 and by transitivity of r the elements a, a1 , a2 , a3 form a
red clique in A. By (6d) A |= b(a, a1 ), hence A |= h(a, a1 ).
Remaining cases are shown similarly.
Now, we show the confluence property (*). Let a, a0 , b, b0 ∈ A and A |=
h(a, b) ∧ v(a, a0 ) ∧ h(b, b0 ). One needs to consider several cases depending on the
colour of a, in each of them showing that A |= h(a0 , b0 ). For instance:
– A |= c00 (a). Then A |= c01 (a0 )∧b(a, a0 )∧b(a, b)∧c10 (b)∧b(b, b0 )∧c11 (b0 ). By (4)
b0 is a member of a blue clique containing elements of colours c11 , c01 , c00 , c10 .
Since by (3) the relation b does not connect distinct elements of the same
colour, a0 belongs to the blue clique of b0 and A |= b(a0 , a). Now, by transi-
tivity of b, A |= h(a0 , b0 ).
– A |= c30 (a). Then A |= c31 (a0 ) ∧ b(a, a0 ) ∧ r(a, b) ∧ c00 (b) ∧ b(b, b0 ) ∧ c01 (b0 ).
Similarly as above, b belongs to a red clique of a, hence A |= r(b, a). By (6a),
A |= b(b, a). Moreover, b0 is in a blue clique of b, and so A |= b(b0 , b). By
transitivity of b, A |= b(b0 , a0 ). Now, by (7c), A |= r(b0 , a0 ). By (5), a0 is a
member of a red clique that, by (3), must contain b0 . Hence h(a0 , b0 ) holds.
Remaining cases can be shown in a similar way. Hence, every model of ϕgrid is
grid-like. Now we ensure that we also can assign tiles to elements of the grid-like
models using fluted formulas. The task in FO2 is easy, it suffices to require that
(8) each node encodes precisely one tile: ∀x( ˙ C∈C Cx),
W
(9) adjacent tiles respect CH and CV ; the first condition can be written as follows:
^ _
∀x(Cx → ∀y(h(x, y) → C 0 y)), , (9a)
C∈C C 0 :(C,C 0 )∈CH
and similarly for CV .
Formula (8) is fluted, formulas in (9) are not, but can be written as fluted using
first-order tautologies. E.g. each conjunct in (9a) can be written as follows:
^ _
∀x(Cx ∧ cij (x) → ∀y(b(x, y) ∧ ci+1,j (y) → C 0 y)) ∧
i=0,2,j=0,1,2,3 C 0 :(C,C 0 )∈CH
^ _
∀x(Cx ∧ cij (x) → ∀y(r(x, y) ∧ ci+1,j (y) → C 0 y)).
i=1,3,j=0,1,2,3 C 0 :(C,C 0 )∈C H
Let ηC be the conjunction of ϕgrid with the properties (8) and (9) written in
FL2 , as explained. Now it is routine to show that the reduction properties (i)
and (ii) hold. If C tiles any of the spaces Z × Z or Zt × Zt , for some t, we expand
the grids to our intended models. In the opposite direction, when G |= ηC and
G is infinite we obtain a tiling of Z × Z; in case G is finite we obtain a tiling of
Zt × Zt with t divisible by 4. As a result we simultaneously conclude that the
satisfiability and the finite satisfiability problems for FL2 with two transitive
relations are undecidable.
One can also observe that the above formulas are guarded or can easily be
rewritten as guarded. Hence we also get the following
Corollary 1. The (finite) satisfiability problem for the intersection of the fluted
fragment with equality with the two-variable guarded fragment is undecidable in
the presence of two transitive relations.
2.2 Undecidability of F L2 without equality and with three
transitive relations
Suppose the signature contains transitive relations b (black), g (green) and r
(red), and additional unary predicates e, e0 , f , l, ci,j (0 ≤ i ≤ 5, 0 ≤ j ≤ 2)
and di,j (0 ≤ i ≤ 2, 0 ≤ j ≤ 5); we refer to the ci,j ’s and to the di,j ’s as
colours. In this section addition in subscripts of the ci,j ’s, it is always under-
stood modulo 6 in the first position, and modulo 3 in the second position, i.e.
ci+a,j+b denotes c(i+a)mod 6,(j+b)mod 3 ; and, addition in subscripts of the di,j ’s is
understood modulo 3 in the first position, and modulo 6 in the second position.
As before we write a formula ϕgrid that captures several properties of the
intended expansion of the N × N grid as shown in Figure 2. There the unary
predicates l and f mark the elements in the left column, respectively, bottom
row of the grid. The predicate e marks elements on the main diagonal and the
predicate e0 marks elements with coordinates (k, k + 1). The predicates ci,j and
di,j together define a partition of the universe as follows: an element (k, k 0 ) with
k 0 > k satisfies ci,j with i = k mod 6, j = k 0 mod 3, and an element (k, k 0 )
with k ≥ k 0 satisfies di,j with i = k mod 3, j = k 0 mod 6. Transitive relations
connect elements that are ’close’ in the grid; more precisely, paths of the same
transitive relation have length at most 7 and they follow one of four designed
patterns.
The formula ϕgrid comprises several conjuncts. The most complex group of
conjuncts describes the requirement that each element of a certain colour has
a successor of an appropriate colour as shown in Figure 3. Conjuncts from this
group have the following form:
∀x colour(x) ∧ diag(x) ∧ border(x) → ∃y(t(x, y) ∧ colour0 (y)) ,
(1)
where colour and colour0 stands for one of the predicates letters ci,j or di,j ,
diag(x) means one of the literals e0 (x), ¬e0 (x), e(x), ¬e(x) or > (i.e. the logical
constant true), border(x) means one of the literals l(x), ¬l(x), f (x), ¬f (x) or
>, and t stands for one of the transitive predicate letters b, r or g. The precise
17
16
15
14
13
12
11
10
9
8
7
6
5
4
3
2
1
0
0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
Fig. 2. Intended expansion of the N × N grid with transitive relations b, g and r. Filled
nodes depict beginning of a transitive path of the same colour; dotted lines connect the
first element with the last element on such path. Paths of length 7 have four distinct
patterns; for instance the same pattern is followed by: the red path starting at node
(5,3), the green path starting at node (3,1) and the black path starting at node (7,5).
Paths starting at nodes (4,2), (8,6) and (6,4) follow another pattern; and similarly,
paths starting at nodes (1,1), (5,5) and (3,3); and paths starting at nodes (6,6), (4,4)
and (2,2). Two shorter path patterns appear on the border.
combinations of the literals and predicate letters in these conjuncts can be read
from Figure 3 and they are defined in Table 1. The remaining conjuncts to ϕgrid
express the following properties:
(2) there is an initial element: ∃x(d00 (x) ∧ e(x) ∧ l(x) ∧ f (x)).
(3) the predicates ci,j together with di,j enforce a partition of the universe.
(4) the predicates l, f , e and e0 propagate as intended; e.g.
^
∀x c0,j (x) ∧ l(x) → ∀y(c0,j+1 (y) ∧ (b(x, y) ∨ g(x, y)) → l(y))
0≤j≤5
^
∀x di,j (x) ∧ e(x) → ∀y((b(x, y) ∨ g(x, y) ∨ r(x, y)) ∧ di+1,j+1 (y) → e(y)) .
0≤i≤2
0≤j≤5
17
16
15
14
13
12
11
10
9
8
7
6
5
4
3
2
1
0
0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
Fig. 3. Construction of the embedding of the N × N grid in a model of ϕgrid . Nodes
on the main diagonal (i.e. satisfying e) are marked orange and nodes satisfying e0 are
marked yellow. Arrows indicate nodes where the successor relation crosses the diagonal
or where its definition switches from one transitive relation to another one.
(5) some pairs of elements connected by one transitive relation are also connected
by another one as intended in Figure 2; for instance:
∀x(c11 (x) →∀y(b(x, y) ∧ c10 (y) → r(x, y)))
∀x(c20 (x) →∀y(g(x, y) ∧ c30 (y) → r(x, y)))
The structure depicted in Figure 2 is a model of ϕgrid . We show the following
Claim. Every model of ϕgrid is grid-like.
Proof. Let A |= ϕgrid . We define an embedding h of the standard grid GN on
N×N into A as follows. Let next : N×N 7→ N×N be a successor function defined
on GN as depicted by the thick path in Figure 3 starting in (0, 0) (ignoring any
colours). Let a ∈ A be an element such that A |= d00 (a) ∧ e(a) ∧ l(a) ∧ f (a) that
exists by condition (2). Define h(0, 0) = a. Now, we proceed inductively: suppose
colour diag(x) border(x) t(x, y) colour0 colour diag(x) border(x) t(x, y) colour0
d00 e l b c01
d00 e ¬l g c50 c01 e0 b d11
d14 e b c31 c20 e0 g d03
d22 e r c12 c42 e0 r d25
d00 ¬e r d01 c01 ¬e0 b c11
d01 r d21 c11 b c10
d21 r d22 c10 b c20
d22 ¬e b d23 c20 ¬e0 g c30
d23 b d13 c30 g c32
d13 b d14 c32 g c42
d14 ¬e g d15 c42 ¬e0 r c52
d15 g d05 c52 r c51
d05 g d00 c51 r c01
d11 b d10 c12 g c02
d10 ¬f b d20 c02 ¬l g c00
d20 ¬f b d25 c00 ¬l g c50
d25 r d24 c50 b c40
d24 r d04 c40 b c41
d04 r d03 c41 b c31
d03 g d02 c31 r c21
d02 g d12 c21 r c22
d12 g d11 c22 r c12
d20 f r d00 c02 l b c00
d10 f r d20 c00 l b c01
Table 1. Various combinations of the literals in conjuncts of the form (1); empty
entries in columns diag(x) or border(x) mean >.
h(k, k 0 ) has already be defined and h(k, k 0 ) = a. Let a0 be the witness of a for
the appropriate conjunct from the group (1), i.e. where the monadic literals for
x agree with the monadic literals satisfied by a in A. Define h(next(k, k 0 )) = a0 .
Correctness of the embedding can be shown by induction considering various
cases depending on the colours of the elements. Interested readers are invited
to do the proof by drawing: print Figure 3 on a sheet of paper, use appropriate
colours to draw the edges induced by transitivity of b, g and r, apply universal
conjuncts from the group (5) and compare the resulting picture with Figure 2
(when they agree the proof is finished!).
We have one more obstacle to overcome. Defining the embedding we moved
through the grid in four directions, so in order to appropriately assign tiles to
nodes in models of ϕgrid we need to respect the four directions as we have fixed
order of variables. The idea is to define four binary relations rt(x, y), lt(x, y),
up(x, y) and dn(x, y) with the intention that rt and the inverse of lt together give
the expected horizontal grid successor, and up and the inverse of dn together give
the expected vertical grid successor. For instance, the relation rt(x, y) is defined
as follows:
rt(x, y) :=(b(x, y) ∨ g(x, y) ∨ r(x, y)) ∧
(c50 (x) ∧ d00 (y)) ∨ (c31 (x) ∧ d14 (y)) ∨ (c12 (x) ∧ d22 (y)) ∨
_ _
(cij (x) ∧ ci+1,j (y)) ∨ (dij (x) ∧ di+1,j (y))
(i,j)∈{(0,2),(1,2),(2,1),(3,1),(4,0),(5,0)}
/ (i,j)∈{(2,1),(1,3),(0,5)}
/
The formula above says that the relation rt connects elements that are connected
by (at least) one of the transitive relation and satisfy one of the possible combi-
nation of colours: in the second line the combinations for crossing the diagonal
from left to right are listed, in the third line the left big disjunction describes
combinations when both elements are located above the diagonal, and in the
right big disjunction—when both elements are located on and below the diago-
nal. The definition of lt(x, y) is written complementing the definition of rt:
lt(x, y) :=(b(x, y) ∨ g(x, y) ∨ r(x, y)) ∧
(d00 (x) ∧ c50 (y)) ∨ (d14 (x) ∧ c31 (y)) ∨ (d22 (x) ∧ c12 (y)) ∨
_ _
(cij (x) ∧ ci−1,j (y)) ∨ (dij (x) ∧ di−1,j (y))
(i,j)∈{(1,2),(2,2),(3,1),(4,1),(5,0),(0,0)} (i,j)∈{(0,1),(2,3),(1,5)}
Analogously one defines the relations up and dn. Now the counterpart of the
formula (9a) from the previous subsection can be written as follows:
^ _
∀x(Cx → ∀y(rt(x, y) → C 0 y))
C∈C C 0 :(C,C 0 )∈CH
^ _
∀x(Cx → ∀y(lt(x, y) → C 0 y))
C∈C C 0 :(C 0 ,C)∈C H
and similarly for CV . As before, the formulas can be further rewritten as fluted
thanks to the fact that in the definitions of rt(x, y), lt(x, y), up(x, y) and dn(x, y)
the binary literals have the form t(x, y) (and not t(y, x)).
As in the previous section all formulas used for the reduction are either
guarded or can easily be rewritten as guarded. Hence we also get the following
Corollary 2. The satisfiability problem for the intersection of the fluted frag-
ment without equality with the two-variable guarded fragment is undecidable in
the presence of three transitive relations.
It is not obvious if the formula ϕgrid can be modified to define embeddings of
finite grids. Hence decidability of the corresponding finite satisfiability problem
remains open. It also is open whether the full fluted fragment, FL, with one or
two transitive relations (without equality) is decidable.
Acknowledgements The research presented in Section 2 is supported by the
Polish National Science Centre grant No 2016/21/B/ST6/01444.
References
1. Andréka, H., van Benthem, J., Németi, I.: Modal languages and bounded frag-
ments of predicate logic. Journal of Philosophical Logic 27, 217–274 (1998).
https://doi.org/10.1023/A:1004275029985
2. Blackburn, P., van Benthem, J., Wolter, F. (eds.): Handbook of Modal Logic. Else-
vier Science Inc., New York (2006)
3. Börger, E., Grädel, E., Gurevich, Y.: The classical decision problem. Perspectives
in Mathematical Logic, Springer (1997)
4. Kieroński, E., Pratt-Hartmann, I., Tendera, L.: Two-variable logics with
counting and semantic constraints. SIGLOG News 5(3), 22–43 (2018).
https://doi.org/10.1145/3242953.3242958
5. Quine, W.V.: The variable. In: The Ways of Paradox, pp. 272–282. Harvard Uni-
versity Press, revised and enlarged edn. (1976)
6. Segoufin, L., ten Cate, B.: Unary negation. Logical Methods in Computer Science
9(3) (2013). https://doi.org/10.2168/LMCS-9(3:25)2013
7. Tendera, L.: Finite model reasoning in expressive fragments of first-order logic.
In: Ghosh, S., Ramanujam, R. (eds.) Proceedings of the Ninth Workshop on
Methods for Modalities, M4M@ICLA 2017, Indian Institute of Technology, Kan-
pur, India, 8th to 10th January 2017. EPTCS, vol. 243, pp. 43–57 (2017).
https://doi.org/10.4204/EPTCS.243.4