Several decidable fragments of rst-order logic have been identi ed in the past as a generalisation of the standard translation of modal logic. These include: the uted fragment, the two-variable fragment, 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 onedimensional fragment). None of the fragments allows one to express transitivity of a binary relation or related properties like being an equivalence, a linear or a partial order, that naturally appear in speci cations or in veri cation. 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 nite satis ability, as presence of transitivity axioms often allows one to express axioms of in nity. Simultaneously, we locate in the picture known description logics, discuss relevant technics, admire a few exotic results and state some open questions.
quanti ers 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 fragments of rst order logic: (i) the uted fragment F L, (ii) the guarded fragment GF , (iii) the unary negation fragment U N F , and (iv) the two-variable fragment F O2. All of the four languages have the nite model property, and hence are decidable. As already mentioned in the abstract, none of them can express transitivity 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 Kieronski, Jakub Michaliszyn, Andreas Pieris, Ian Pratt-Hartmann, and Wieslaw Szwast. In the next section we recall formal de nitions 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
De nitions We assume relational signatures not containing constants or function symbols. De nition 1. The uted fragment [5]: Let x! = x1; x2; : : : be a xed sequence of variables. We de ne the sets of formulas F L[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 F L[k]; (ii) F L[k] is closed under boolean combinations; (iii) if ' is in F L[k+1], then 9xk+1' and 8xk+1' are in F L[k]. The set of uted formulas is de ned as F L = Sk 0 F L[k]. A uted sentence is a uted formula over an empty set of variables, i.e. an element of F L[0]. Thus, when forming Boolean combinations in the uted fragment, all the combined formulas must have as their free variables some su x of some pre x x1; : : : ; xk of x!; and when quantifying, only the last variable in this sequence may be bound. De nition 2. The guarded fragment [1], GF , is de ned as the least set of formulas such that: (i) every atomic formula belongs to GF ; (ii) GF is closed under logical connectives :; _; ^; !; and (iii) quanti ers are appropriately relativised by atoms. More speci cally, 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 8x( ! ') and 9x( ^ ') 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. De nition 3. The unary negation fragment [6], U N F , consists of formulas in which the use of negation is restricted only to subformulas with at most one free variable. More precisely, U N F is de ned as the least set of formulas such that: (i) every atomic formula of the form R(x) or x = y belongs to U N F ; (ii) U N F is closed under logical connectives _, ^ and under existential quanti cation; (iii) if '(x) is a formula of U N F featuring no free variables besides (possibly) x, then :'(x) belongs to U N F .
De nition 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 F Ok denotes the set of all rst-order formulas with at most k variables.
All of the above languages are incomparable in terms of expressive power, have the nite model property and the satis ability problem (= nite satis ability problem) is decidable. 2
Fluted Fragment with Transitive Relations We show two undecidability results for the uted fragment with two variables, F L2, extended with transitive relations. We employ the apparatus of tiling systems (cf. e.g. [3]).
A tiling system is a tuple C = (C; CH ; CV ), where C is a nite 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) 2 S: ( (p; q); (p + 1; q)) 2 CH and ( (p; q); (p; q + 1)) 2 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 ( nite) satis ability 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) (ii)
C is satis able i C tiles N N or Z C is nitely satis able i C tiles Zt
Z, and Zt, for some t 1.
Properties (i) and (ii) above yield undecidability of the satis ability, respectively, nite satis ability, problem for L.
In order to encode tilings using two-variable logics it is useful to de ne structures 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 su ces to require that G j= 8x(9yh(x; y) ^ 9yv(x; y)) (note that this is an F L2-formula) and the following con uence property holds
G j= 8x; x0; y; y0((h(x; y) ^ v(x; x0) ^ v(y; y0) ! h(x0; y0)): (*) The con uence property above uses four variables and is not uted. We will enforce it (or a variation of it) in F L2 using transitive relations.
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 0i3n Fig1u3re 1. 2T3 here,33each e03lemen1t3 with2c3oordi3n3ates (k; l) satis es
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 'g32rid is a conjunction
of the statements (
8x(cij (x) ! 9y(b(x; y) ^ ci+1;j (y))) 8x(ci+1;j (x) ! 9y(b(x; y) ^ ci+1;j+1(y))) 8x(ci+1;j+1(x) ! 9y(b(x; y) ^ ci;j+1(y)))
8x(ci;j+1(x) ! 9y(b(x; y) ^ cij (y)))
(
8x(cij(x) ! 9y(r(x; y) ^ ci+1;j(y))) 8x(ci+1;j(x) ! 9y(r(x; y) ^ ci+1;j+1(y))) 8x(ci+1;j+1(x) ! 9y(r(x; y) ^ ci;j+1(y)))
8x(ci;j+1(x) ! 9y(r(x; y) ^ cij(y)))
(
Let us introduce the following de nitions: h(x; y) :=b(x; y) ^ _ (cij(x) ^ ci+1;j(y)) _ r(x; y) ^ i=0;2 j=0;1;2;3 _ (cij(x) ^ ci+1;j(y)) i=1;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 (6a) (6b) (6d) (7a) (7b) (7d) Let A j= 'grid. We show that every model (A; h; v) of 'grid is grid-like. We rst show that A satis es 8x(9yh(x; y) ^ 9yv(x; y)). One considers several cases depending on the values of the unary predicates.
Let a 2 A and assume A j= c00(a). By (
The same argument works if a has one of the colours c02; c20 or c22 and,
similarly, applying (
Consider now the case A j= c10(a). By (
Remaining cases are shown similarly.
Now, we show the con uence property (*). Let a; a0; b; b0 2 A and A j=
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 j= h(a0; b0). For instance:
{ A j= c00(a). Then A j= c01(a0)^b(a; a0)^b(a; b)^c10(b)^b(b; b0)^c11(b0). By (
Similarly as above, b belongs to a red clique of a, hence A j= r(b; a). By (6a),
A j= b(b; a). Moreover, b0 is in a blue clique of b, and so A j= b(b0; b). By
transitivity of b, A j= b(b0; a0). Now, by (7c), A j= r(b0; a0). By (
_ C0:(C;C0)2CH
C0y)); ; (9a) and similarly for CV .
Formula (8) is uted, formulas in (9) are not, but can be written as uted using rst-order tautologies. E.g. each conjunct in (9a) can be written as follows: ^ i=0;2;j=0;1;2;3
^ 8x(Cx ^ cij (x) ! 8y(b(x; y) ^ ci+1;j (y) ! 8x(Cx ^ cij (x) ! 8y(r(x; y) ^ ci+1;j (y) ! _ Let2 C be the conjunction of 'grid with the properties (8) and (9) written in F L , 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 j= C and G is in nite we obtain a tiling of Z Z; in case G is nite we obtain a tiling of Zt Zt with t divisible by 4. As a result we simultaneously conclude that the satis ability and the nite satis ability problems for F L2 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 ( nite) satis ability problem for the intersection of the uted fragment with equality with the two-variable guarded fragment is undecidable in the presence of two transitive relations.
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 understood modulo 6 in the rst 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 rst 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 de ne a partition of the universe as follows: an element (k; k0) with k0 > k satis es ci;j with i = k mod 6, j = k0 mod 3, and an element (k; k0) with k k0 satis es di;j with i = k mod 3; j = k0 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:
8x colour(x) ^ diag(x) ^ border(x) ! 9y(t(x; y) ^ colour0(y)) ;
(
^ 8x c0;j (x) ^ l(x) ! 8y(c0;j+1(y) ^ (b(x; y) _ g(x; y)) ! l(y)) 0 j 5
^ 8x di;j (x) ^ e(x) ! 8y((b(x; y) _ g(x; y) _ r(x; y)) ^ di+1;j+1(y) ! e(y)) :
0 i 2
0 j 5
(
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 j= 'grid. We de ne 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 de ned
on GN as depicted by the thick path in Figure 3 starting in (0; 0) (ignoring any
colours). Let a 2 A be an element such that A j= d00(a) ^ e(a) ^ l(a) ^ f (a) that
exists by condition (
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 (
We have one more obstacle to overcome. De ning 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 xed order of variables. The idea is to de ne 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 de ned 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 combination 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 diagonal. The de nition of lt(x; y) is written complementing the de nition 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)) (i;j)2f(1;2);(2;2);(3;1);(4;1);(5;0);(0;0)g _ (dij (x) ^ di 1;j (y)) (i;j)2f(0;1);(2;3);(1;5)g _ Analogously one de nes the relations up and dn. Now the counterpart of the formula (9a) from the previous subsection can be written as follows: ^ 8x(Cx ! 8y(rt(x; y) ! C2C ^ 8x(Cx ! 8y(lt(x; y) ! C2C
_ and similarly for CV . As before, the formulas can be further rewritten as uted thanks to the fact that in the de nitions 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 satis ability problem for the intersection of the uted fragment 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 modi ed to de ne embeddings of nite grids. Hence decidability of the corresponding nite satis ability problem remains open. It also is open whether the full uted fragment, F L, 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.