One-dimensional guarded fragments

TL;DR

This paper introduces one-dimensional restrictions of the guarded fragment and tri-guarded fragment, analyzing their model properties and computational complexity, showing that these restrictions lead to more tractable decision problems.

Contribution

It defines and studies GF1 and TGF1, new fragments with restricted quantification, establishing their decidability, model properties, and complexity results, extending the understanding of guarded fragments.

Findings

GF1 has an exponential model property.

Satisfiability for GF1 is NExpTime-complete.

TGF1 is decidable with TwoExpTime-complete satisfiability.

Abstract

We call a first-order formula one-dimensional if its every maximal block of existential (universal) quantifiers leaves at most one variable free. We consider the one-dimensional restrictions of the guarded fragment, GF, and the tri-guarded fragment, TGF, the latter being a recent extension of GF in which quantification for subformulas with at most two free variables need not be guarded, and which thus may be seen as a unification of GF and the two-variable fragment, FO2. We denote the resulting formalisms, resp., GF1, and TGF1. We show that GF1 has an exponential model property and NExpTime-complete satisfiability problem (that is, it is easier than full GF). For TGF1 we show that it is decidable, has the finite model property, and its satisfiability problem is TwoExpTime-complete (NExpTime-complete in the absence of equality). All the above-mentioned results are obtained for signatures with no constants. We finally discuss the impact of their addition, observing that constants do not spoil the decidability but increase the complexity of the satisfiability problem.

Tables

Table 1. Table 1 : Complexities of the guarded fragments. If the presence of constants makes a difference, the complexity of the variant with constants is given in the brackets. All logics have the finite model property. Results of this paper are distinguished in bold.

logic	with $=$	without =
GF	2-ExpTime.	2-ExpTime
TGF	undecidable	2-ExpTime (2-NExpTime)
${\text{GF}}_1$	NExpTime (2-ExpTime)	NExpTime (2-ExpTime)
${\text{TGF}}_1$	2-ExpTime (2-NExpTime)	NExpTime (2-NExpTime)

Equations

$$\underset{i\in I}{\bigwedge }\forall \bar{x}({\gamma }_i(\bar{x})\to {\psi }_i(\bar{x}))\wedge \underset{i\in I^{\prime }}{\bigwedge }\forall x\exists \bar{y}{\psi }_i^{\prime }(x,\bar{y})\wedge \forall xy{\psi }^{\prime \prime }(x,y)$$

$$\exists x(Z(x)\wedge \neg O(x))\wedge \forall xy(Z(x)\wedge Z(y)\to x=y)$$

$$\exists x(O(x)\wedge \neg Z(x))\wedge \forall xy(O(x)\wedge O(y)\to x=y)$$

$$\forall x\exists t_1{t}_0(O(t_1)\wedge Z(t_0)\wedge$$

$$C(x,t_1,t_0,t_0\dots ,t_0)\wedge$$

$$C(x,t_1,t_1,t_0,\dots ,t_0)\wedge \dots \wedge$$

$$C(x,t_1,t_1,t_1,\dots ,t_1))$$

$$\forall x\bar{z}(C($$

$$\underset{0\le i<n}{\bigvee }$$

$$\forall x\exists \bar{u}(H(x,\bar{u})\wedge \underset{i}{\bigwedge }(O(u_i)\vee Z(u_i))$$

$$\forall x\bar{u}\bar{v}(C(x,\bar{u},\bar{v})\to H(x,\bar{u})\wedge {\lambda }^{\ne }(\bar{u},\bar{v})\to \neg H(x,\bar{v}))$$

$$\forall x\bar{u}(H(x,\bar{u})\to {\dot{\bigvee }}_i{S}_i(x,\bar{u}))$$

$$\forall x\bar{u}(C(x,\bar{u},\bar{u})\to {\dot{\bigvee }}_i{A}_i(x,\bar{u}))$$

$$\forall x\exists y{t}_1{t}_0(O(t_1)\wedge Z(t_0)\wedge$$

$$Suc{c}_i(x,y,t_1,t_0,t_0\dots ,t_0)\wedge$$

$$Suc{c}_i(x,y,t_1,t_1,t_0,\dots ,t_0)\wedge \dots \wedge$$

$$Suc{c}_i(x,y,t_1,t_1,t_1,\dots ,t_1))$$

$$\forall xy\bar{t}$$

$$Suc{c}_i(x,y,t_{3n-2},t_{3n-1},t_{3n-3},\dots ,t_0)\wedge Suc{c}_i(x,y,t_{3n-2},t_{3n-3},\dots ,t_0,t_{3n-1}))$$

$$\forall xy\bar{u}((Suc{c}_i(x,y,$$

$$\forall$$

$$(H(y,\bar{v})\wedge S_{i^{\prime }}(y,\bar{v})\wedge A_{j^{\prime }}(y,\bar{u}))\vee (H(y,\bar{w})\wedge S_{i^{\prime \prime }}(y,\bar{w})\wedge A_{j^{\prime \prime }}(y,\bar{u})))$$

$$\forall xy$$

$$H(x,\bar{u})\wedge S_i(x,\bar{u})\wedge A_j(x,\bar{u})\wedge {\lambda }^{+1}(\bar{u},\bar{v})\to H(y,\bar{v})\wedge S_{i^{\prime }}(y,\bar{v})\wedge A_{j^{\prime }}(y,\bar{u}))$$

$$\forall xy$$

$$H(x,\bar{u})\wedge S_i(x,\bar{u})\wedge A_j(x,\bar{u})\wedge {\lambda }^{+1}(\bar{w},\bar{u})\to H(y,\bar{w})\wedge S_{i^{\prime }}(y,\bar{w})\wedge A_{j^{\prime }}(y,\bar{u}))$$

$$\neg \exists x{S}_k(x)\wedge \exists xInit(x)$$

$$\forall x\bar{u}(C(x,\bar{u})\to Init(x)\to ($$

$$({\lambda }^{=1}(\bar{u})\to A_{i_1}(x,\bar{u}))\wedge \dots \wedge$$

$$({\lambda }^{=n-1}(\bar{u})\to A_{i_{n-1}}(x,\bar{u}))\wedge$$

$$({\lambda }^{\ge n}(\bar{u})\to A_0(x,\bar{u})))$$

$$\exists xy$$

$$N(x,x,x,\dots ,x)\wedge$$

$$N(y,x,x,\dots ,x)\wedge$$

$$N(y,y,x,\dots ,x)\wedge$$

$$\dots \wedge$$

$$N(y,y,y,\dots ,y)$$

$$\forall \bar{u}$$

$$\forall \bar{u}(N(\bar{u})\to \stackrel{\cdot }{\underset{t\in C}{\bigvee }}{D}_t(\bar{u}))$$

$$\underset{t\in C}{\bigwedge }$$

Full text

One-dimensional guarded fragments

Emanuel Kieroński

1 Introduction

The guarded fragment of first-order logic, GF, is obtained by requiring all quantifiers to be appropriately relativised by atoms. It was introduced by Andréka, van Benthem and Németi [1] as a generalization of propositional modal logic and may be also seen as an extension of some standard description logics. GF has good algorithmic and model-theoretic properties. In particular, Grädel proved that its satisfiability problem is decidable, it has a tree-like model property and the finite model property [7]. The idea of GF turned out to be very fruitful and found numerous applications. In this paper we consider some modifications of the syntax of GF. Our aim is to check if in this way we can obtain interesting fragments with better complexity and/or attractive expressiveness.

The satisfiability problem for GF is 2-ExpTime-complete. This relatively high complexity can be lowered to ExpTime either by bounding the number of variables, or the arity of relation symbols [7]. We propose another way of decreasing the complexity without sacrificing either the number of variables or the arity of relations. The idea is to restrict formulas to be one-dimensional. We say that a formula is one-dimensional if every maximal block of existential (or universal) quantifiers in it leaves at most one variable free. We remark that the one-dimensional restriction of full first-order logic, $\mbox{\rm F}_{1}$, is undecidable, as observed by Hella and Kuusisto [9]. We denote the intersection of $\mbox{\rm F}_{1}$ and GF by $\mbox{\rm GF}_{1}$ and call it the one-dimensional guarded fragment. While this variation decreases the expressive power of the logic, we believe that it is still quite interesting, as, in particular, it still embeds propositional modal logic, and most standard description logics embeddable in full GF. Thus, as GF, it may serve as an extension of modal/description logics to contexts with relations of arbitrary arity. We show that the satisfiability problem for $\mbox{\rm GF}_{1}$ is NExpTime-complete and that it has an exponential model property, that is, its every satisfiable formula has a model of size bounded exponentially in its length. This is in contrast to full GF in which one can enforce doubly exponentially large models. Moreover, proving the finite model property for $\mbox{\rm GF}_{1}$ is much easier than for full GF, in particular it does not need complicated combinatorial constructions used in the case of GF (in [7], and in Bárány, Gottlob and Otto [2]). We obtain a corresponding NExpTime-lower bound even for a weaker logic, uniform $\mbox{\rm GF}_{1}$, that is the intersection of $\mbox{\rm GF}_{1}$ and uniform $\mbox{\rm F}_{1}$, $\mbox{\rm UF}_{1}$, the latter being a decidable restriction of $\mbox{\rm F}_{1}$ introduced in [9] as a canonical generalization of the two-variable fragment $\mbox{\rm FO}^{2}$ (with equality) to scenarios involving relations of arity greater than two (see Kieroński, Kuusisto [13] where NExpTime-completeness of $\mbox{\rm UF}_{1}$ is shown). This is slightly surprising, since in many aspects $\mbox{\rm UF}_{1}$ behaves similarly to the two-variable fragment, $\mbox{\rm FO}^{2}$, and the guarded version of the latter is ExpTime-complete [7].

We also consider an extension of GF called the tri-guarded fragment, TGF. In TGF quantification for subformulas with at most two free variables may be used freely, without guards. Hence, TGF unifies GF and the already-mentioned $\mbox{\rm FO}^{2}$. We borrowed the term tri-guarded fragment from a recent work by Rudolph and Šimkus [15], but, actually, the idea behind TGF is not new and can be traced back already in Kazakov’s PhD thesis [11] where the fragment GF|$\mbox{\rm FO}^{2}$, essentially identical with TGF, was defined. A similar logic, GF with binary cross product, GF${}^{\times_{2}}$, is also considered by Bourhis, Morak and Pieris [4]. Both GF|$\mbox{\rm FO}^{2}$ and GF${}^{\times_{2}}$ do not allow constant symbols. We remark that in our initial scenario we also assume that constants are not present in signature; however, we will discuss their addition later.

Similarly to GF, $\mbox{\rm FO}^{2}$ is a seminal fragment of first-order logic, and its importance is justified, inter alia, by its close relationships to modal and description logics. Mortimer [14] demonstrated that it has the finite model property and Grädel, Kolaitis and Vardi [8] proved that its satisfiability problem is NExpTime-complete. Each of the logics GF, $\mbox{\rm FO}^{2}$ has some advantages and drawbacks with respect to the other. We mention here the fact that GF allows only to express properties of a local character, e.g., it cannot express $\forall xy(Px\wedge Qy\rightarrow Rxy)$, while $\mbox{\rm FO}^{2}$ does not allow for a non-trivial use of relations of arity greater than two. TGF offers a substantial improvement in these aspects. Moreover, in TGF we can embed the Gödel class, that is the class of all prenex formulas of the form $\forall xy\exists\bar{z}\psi(x,y,\bar{z})$. Indeed, any such formula has an equisatisfiable TGF formula obtained just by an addition of a dummy guard, as follows, $\forall xy\exists\bar{z}(G(x,y,\bar{z})\wedge\psi(x,y,\bar{z}))$, where $G$ is a fresh relation symbol of the appropriate arity. Such embedding implies, however, that the satisfiability problem for TGF with equality is undecidable, since the Gödel class with equality is undecidable, as proved by Goldfarb [6]. The undecidability of TGF with equality is also shown in [15] by a direct grid encoding. On the positive side, it turns out that the satisfiability problem for TGF without equality is decidable and 2-ExpTime-complete. It was proved in [11] by a resolution method, and follows also from the decidability of GF${}^{\times}_{2}$, shown in [4] by a use of the database-theoretic concept of chase.111A footnote in [4] suggests that the decidability of GF with binary cross-product is retained in the presence of equality. This has however been later later refuted by the authors (private communication). GF with binary cross product with equality is undecidable by the same arguments we gave for TGF.

In this paper we consider a natural combination of $\mbox{\rm GF}_{1}$ and TGF, the one-dimensional tri-guarded fragment, $\mbox{\rm TGF}_{1}$, which, on the one hand, allows us to use unguarded quantification for subformulas with at most two free variables, but, on the other hand, requires to obey the one-dimensionality restriction. We show that this variant is decidable even in the presence of equality. The complexity, however, depends on the presence/absence of equality: The satisfiability problem is 2-ExpTime-complete with equality and NExpTime-complete without it. The logic has the finite model property (we remark that whether full TGF has the finite model property is an open question), and, again, a bound on the size of minimal models is doubly- or singly exponential, depending on whether equality is allowed or not. $\mbox{\rm TGF}_{1}$ may be seen as a decidable generalization of $\mbox{\rm FO}^{2}$ (with equality) to scenarios with relations of arity greater than two, alternative and orthogonal in the expressive power to the above-mentioned $\mbox{\rm UF}_{1}$. We also remark that $\mbox{\rm TGF}_{1}$ can express the concept of nominals from description logics, since the combination of equality and unguarded quantification for subformulas with two free variables allows us to say that some unary predicates hold for unique elements of a model. Thus we can embed in $\mbox{\rm TGF}_{1}$, e.g., the description logic $\mathcal{ALC}$ plus inverse roles ($\mathcal{I}$), nominals ($\mathcal{O}$), role hierarchies ($\mathcal{H}$), and any Boolean combination of roles (including their negations).

We then briefly consider applications of the ideas of one-dimensionality and tri-guardedness to two decidable extensions of GF, namely, the loosely guarded fragment, LGF, introduced by van Benthem [17], and the guarded negation fragment, GNFO, proposed by Bárány, ten Cate and Segoufin [3]. Regarding one-dimensionality, it helps in the case of LGF: one-dimensional LGF has an exponential model property and NExpTime-complete satisfiability problem (exactly as $\mbox{\rm GF}_{1}$), but does not help in the case of GNFO, where the one-dimensional variant remains 2-ExpTime-hard. Regarding the tri-guardedness, the results are negative: both LGF and GNFO, even in their one-dimensional variants, become undecidable when unguarded quantification for subformulas with two free variables is allowed.

As remarked, all the results discussed above are obtained under the assumption that constants are not present in signatures. It turns out that all the decidability results are preserved in the presence of constants. However, interestingly, the computational complexity may change (we recall that for GF constants make no difference [7]). This is also the case for TGF with constants, without equality, which is shown in [15] to be 2-NExpTime-complete. Here we show that a 2-NExpTime-lower bound can be obtained even for $\mbox{\rm TGF}_{1}$ with constants, without equality. We also observe that the presence of constants lifts the complexity of $\mbox{\rm GF}_{1}$ to 2-ExpTime.

In Table 1 we summarize the above-discussed complexity results for the variations of GF. We point out an interesting status of $\mbox{\rm TGF}_{1}$: it is NExpTime-complete without equality and constants, 2-ExpTime-complete with equality and without constants, and 2-NExpTime-complete with constants (with or without equality).

We finally remark that further pushing the concepts of one-dimensionality and tri-guardedness to, resp., two-dimensionality and tetra-guardedness does not lead to attractive results. Indeed, a 2-ExpTime lower bound for two-dimensional GF can be shown by a slight adaptation of the bound for full GF from [7]; allowing for unguarded quantification for subformulas with three free variables gives undecidability, as the resulting logic contains the undecidable three-variable fragment of FO (see, e.g., Kahr, Moore and Wang [10]). Undecidability of the three-variable fragment can be easily shown even using only one-dimensional formulas.

2 Preliminaries

We mostly work with purely relational signatures with no constants and function symbols (only in Section 6 we consider signatures with constants). For convenience we also assume that there are no relation symbols of arity [math]. We refer to structures using Fraktur capital letters, and to their domains using the corresponding Roman capitals. Given a structure ${\mathfrak{A}}$ and some $B\subseteq A$ we denote by ${\mathfrak{A}}\!\!\restriction\!\!B$ or just by ${\mathfrak{B}}$ the restriction of ${\mathfrak{A}}$ to its subdomain $B$.

We usually use $a,b,\ldots$ to denote elements from domains of structures, $\bar{a}$, $\bar{b}$, $\ldots$ for tuples of elements, $x$, $y$, $\ldots$ for variables and $\bar{x}$, $\bar{y}$, $\ldots$ for tuples of variables; all of these possibly with some decorations. For a tuple of variables $\bar{x}$ we use $\psi(\bar{x})$ to denote a formula (or subformula) $\psi$, whose all free variables are in $\bar{x}$.

An atomic $l$-type $\beta$ over a signature $\sigma$ is a maximal consistent set of atomic or negated atomic formulas (including equalities/inequalities) over $\sigma$ in $l$ variables $x_{1},\ldots,x_{l}$. We often identify a type with the conjunction of its elements, $\beta(x_{1},\ldots,x_{l})$. For an $l$-type $\beta$ we denote by $\beta\!\!\restriction\!\!x_{i}$ ($i=1,\ldots,l$) the $1$-type obtained by removing from $\beta$ all the literals that use some $x_{j}$, with $j\not=i$, and then replacing all occurrences of $x_{i}$ by $x_{1}$. We will be particularly interested in $1$-types and $2$-types over signatures $\sigma$ consisting of the relation symbols used in some given formula. Observe that the number of $1$-types is bounded by a function which is exponential in $|\sigma|$, and hence also in the length of the formula. This is because a $1$-type just corresponds to a subset of $\sigma$. On the other hand, the number of $2$-types may be doubly exponentially large. Indeed, using an $n$-ary predicate and two fixed variables one can build $2^{n}$ atoms which then can be used to form $2^{2^{n}}$ different $2$-types.

Let ${\mathfrak{A}}$ be a structure, and let $a,b\in A$ be such that $a\neq b$. We denote by ${\rm tp}^{{{\mathfrak{A}}}}({a})$ the unique atomic 1-type realized in ${\mathfrak{A}}$ by the element $a$, i.e., the $1$-type $\alpha(x)$ such that ${\mathfrak{A}}\models\alpha(a)$; similarly by ${\rm tp}^{{{\mathfrak{A}}}}({a,b})$ we denote the unique atomic 2-type realized in ${\mathfrak{A}}$ by pair $(a,b)$, i.e., the $2$-type $\beta(x,y)$ such that ${\mathfrak{A}}\models\beta(a,b)$. For $B\subseteq A$ we denote by \mbox{\large\boldmath\alpha}[B] the set of all $1$-types realized in ${\mathfrak{A}}$ by elements of $B$.

Below we define several fragments of first-order logic, FO, including two new fragments, $\mbox{\rm GF}_{1}$ and $\mbox{\rm TGF}_{1}$. Each of the fragments is defined as the least set of formulas (i) containing all atomic formulas (including equalities), (ii) closed under Boolean connectives, and (iii) satisfying appropriate (depending on the fragment) rules of using quantifiers, specified below ($\bar{x}$, $\bar{y}$ represent here any tuples of variables and $x$, $y$ represent any variables):

• •

Guarded fragment of first-order logic, GF:

• –

if $\psi(\bar{x},\bar{y})\in$ GF then $\forall\bar{x}(\gamma(\bar{x},\bar{y})\rightarrow\psi(\bar{x},\bar{y}))$ and $\exists\bar{x}(\gamma(\bar{x},\bar{y})\wedge\psi(\bar{x},\bar{y}))$ belong to GF, where $\gamma(\bar{x},\bar{y})$ is an atomic formula containing all the free variables of $\psi$, called a guard for $\psi$.

• •

One-dimensional fragment of first-order logic, $\mbox{\rm F}_{1}$:

• –

if $\psi(\bar{x},y)\in$ $\mbox{\rm F}_{1}$ then $\exists\bar{x}\psi(\bar{x},y)$ and $\forall\bar{x}\psi(\bar{x},y)$ belong to $\mbox{\rm F}_{1}$.

• •

One-dimensional guarded fragment, $\mbox{\rm GF}_{1}$:

• –

if $\psi(\bar{x},y)\in$ $\mbox{\rm GF}_{1}$ then $\forall\bar{x}(\gamma(\bar{x},{y})\rightarrow\psi(\bar{x},{y}))$ and $\exists\bar{x}(\gamma(\bar{x},{y})\wedge\psi(\bar{x},{y}))$ belong to $\mbox{\rm GF}_{1}$, where $\gamma(\bar{x},{y})$ is a guard for $\psi$.

• •

Tri-guarded fragment, TGF:

• –

if $\psi(\bar{x},\bar{y})\in$ TGF then $\forall\bar{x}(\gamma(\bar{x},\bar{y})\rightarrow\psi(\bar{x},\bar{y}))$ and $\exists\bar{x}(\gamma(\bar{x},\bar{y})\wedge\psi(\bar{x},\bar{y}))$ belong to TGF, where $\gamma(\bar{x},\bar{y})$ is a guard for $\psi$,

• –

if $\psi(x,y)$ is in TGF, then $\exists x\psi(x,y)$ and $\forall x\psi(x,y)$ belong to TGF.

• •

One-dimensional tri-guarded fragment, $\mbox{\rm TGF}_{1}$:

• –

if $\psi(\bar{x},y)\in$ $\mbox{\rm TGF}_{1}$ then $\forall\bar{x}(\gamma(\bar{x},{y})\rightarrow\psi(\bar{x},{y}))$ and $\exists\bar{x}(\gamma(\bar{x},{y})\wedge\psi(\bar{x},{y}))$ belong to $\mbox{\rm TGF}_{1}$, where $\gamma(\bar{x},{y})$ is a guard for $\psi$,

• –

if $\psi(x,y)$ is in $\mbox{\rm TGF}_{1}$, then $\exists x\psi(x,y)$ and $\forall x\psi(x,y)$ belong to $\mbox{\rm TGF}_{1}$.

Note that $\mbox{\rm GF}_{1}$ is just the intersection of GF and $\mbox{\rm F}_{1}$, TGF contains both GF and $\mbox{\rm FO}^{2}$, and $\mbox{\rm TGF}_{1}$ is the intersection of TGF and $\mbox{\rm F}_{1}$, containing full $\mbox{\rm FO}^{2}$.

We recall that the satisfiability problem for $\mbox{\rm F}_{1}$ is undecidable [9]. To regain decidability its uniform restriction, $\mbox{\rm UF}_{1}$, was introduced in [9]. Roughly speaking, a boolean combination of atoms is allowed in $\mbox{\rm UF}_{1}$ if all of them use precisely the same set of variables; the exceptions are atoms with one free variable and equalities, which may be used freely. See [9] or [13] for a formal definition and more details on $\mbox{\rm UF}_{1}$.

We will also be interested in the loosely guarded fragment, LGF, the guarded negation fragment, GNFO, and their one-dimensional and tri-guarded variations. They will be introduced in Section 5.

3 Finite model property

In this section we prove the finite model property for $\mbox{\rm TGF}_{1}$ and obtain (essentially optimal) upper bounds on the size of minimal models of its satisfiable formulas, as well as of formulas of its interesting subfragments.

We introduce a Scott-type normal form for $\mbox{\rm TGF}_{1}$. Given a $\mbox{\rm TGF}_{1}$ formula $\varphi$ we say that it is in normal form if it has the following shape

[TABLE]

where $I,I^{\prime}$ are some sets of indices, the $\psi_{i}$, $\psi_{i}^{\prime}$, and $\psi^{\prime\prime}$ represent arbitrary quantifier-free formulas, and for every $i$, $\gamma_{i}$ is a proper guard for $\psi_{i}$. We remark that we do not require guards in formulas of the form $\forall\bar{\exists}$, even if they contain more than two variables, as their presence there is inessential (cf. Remark in [7], p. 1725). In a rather standard fashion one can show the following lemma.

Lemma 3.1**.**

There is a polynomial nondeterministic procedure, taking as its input a $\mbox{\rm TGF}_{1}$ formula $\varphi$ and producing a normal form formula $\varphi^{\prime}$ (over an extended signature), such that

1. (i)

if ${\mathfrak{A}}\models\varphi$ for some structure ${\mathfrak{A}}$ then there is a run of the procedure producing a normal form $\varphi^{\prime}$ such that ${\mathfrak{A}}^{\prime}\models\varphi^{\prime}$ for some expansion ${\mathfrak{A}}^{\prime}$ of ${\mathfrak{A}}$, 2. (ii)

if the procedure has a run producing $\varphi^{\prime}$ and ${\mathfrak{A}}^{\prime}\models\varphi^{\prime}$, for some ${\mathfrak{A}}^{\prime}$, then ${\mathfrak{A}}^{\prime}\models\varphi$.

Moreover, if $\varphi$ is without equality then the procedure produces $\varphi^{\prime}$ without equality; if $\varphi$ is in $\mbox{\rm GF}_{1}$ then the last conjunct $\forall xy\psi^{\prime\prime}(x,y)$ is not present in $\varphi^{\prime}$.

Lemma 3.1 allows us, when dealing with decidability or complexity issues and when considering the size of minimal models of formulas in $\mbox{\rm TGF}_{1}$, to restrict attention to normal form sentences. The part of this lemma starting with ‘moreover’ will allow us to use it effectively for $\mbox{\rm TGF}_{1}$ without equality and for $\mbox{\rm GF}_{1}$.

Our normal form is similar to normal form for GF [7]. It adapts the latter to the one-dimensional setting and extends it by the last type of conjuncts. The conversion to normal form in [7] is deterministic, it however cannot be used directly in our case as it adds one free variable to every subformula, which spoils one-dimensionality and may lead to unguarded subformulas with three variables.

Let $\varphi$ be a normal form formula and ${\mathfrak{A}}$ its model. Take $a\in A$ and a conjunct $\psi=\forall x\exists\bar{y}\psi^{\prime}_{i}(x,\bar{y})$ of $\varphi$. Let $\bar{b}$ be a tuple of elements of ${\mathfrak{A}}$ such that ${\mathfrak{A}}\models\psi^{\prime}_{i}(a,\bar{b})$. Then ${\mathfrak{A}}\!\!\restriction\!\!(\{a\}\cup\bar{b})$ is called a witness structure for $a$ and $\psi$.

Theorem 3.2**.**

Every satisfiable formula $\varphi$ in

1. (i)

$\mbox{\rm TGF}_{1}$* (with equality) has a finite model of size bounded doubly exponentially in $|\varphi|$.* 2. (ii)

$\mbox{\rm TGF}_{1}$* without equality has a finite model of size bounded exponentially in $|\varphi|$.* 3. (iii)

$\mbox{\rm GF}_{1}$* (with or without equality) has a finite model of size bounded exponentially in $|\varphi|$.*

We concentrate on showing (i) and then obtain (ii) and (iii) as a corollary from the finite model construction presented. Let $\varphi$ be a normal form $\mbox{\rm TGF}_{1}$ formula as in (1), and denote $n=|\varphi|$. Let us fix an arbitrary model ${\mathfrak{A}}$ of $\varphi$. We construct a bounded model ${\mathfrak{B}}\models\varphi$. We mimic the scheme of the classical construction from [8] showing an exponential model property for $\mbox{\rm FO}^{2}$, in particular we adapt the notions of kings and court. The details, however, are more complicated.

Court. We say that an element $a\in A$ is a king if ${\rm tp}^{{{\mathfrak{A}}}}({a})$ is realized in ${\mathfrak{A}}$ only by $a$; ${\rm tp}^{{{\mathfrak{A}}}}({a})$ is then called royal. As in the case of $\mbox{\rm FO}^{2}$ kings are important as their duplication may be forbidden by formulas like $\forall xy(Px\wedge Py\rightarrow x=y)$. Let $K\subseteq A$ be the set of kings of ${\mathfrak{A}}$. For each $a\in K$ and each $i\in I^{\prime}$ choose a witness structure ${\mathfrak{W}}_{a,i}$ for $a$ and $\psi^{\prime}_{i}$ in ${\mathfrak{A}}$. Let $C=K\cup\bigcup_{a,i}W_{a,i}$. We call ${\mathfrak{C}}$ the court of ${\mathfrak{A}}$. The court will be retained in ${\mathfrak{B}}$. Note that the number of elements in $C$ is bounded exponentially in $n$, and it that the structure ${\mathfrak{C}}$ can be described using exponentially many bits (the latter is true since the arity of all relation symbols is bounded by $n$). Note that $K$, and thus also $C$ may be empty.

Pattern witness structures. For each non-royal element $a\in A\setminus K$ we say that the isomorphism type of the structure ${\mathfrak{A}}\!\!\restriction\!\!(K\cup\{a\})$ is the ${\mathfrak{K}}$-type of $a$. Note that from a ${\mathfrak{K}}$-type of an element one can infer its $1$-type, and that the number of the ${\mathfrak{K}}$-types realized in ${\mathfrak{A}}$ is bounded doubly exponentially in $n$. Denote by \mbox{\large\boldmath\alpha}^{\mathfrak{K}} the set of ${\mathfrak{K}}$-types realized in ${\mathfrak{A}}$ by the elements of $A\setminus K$. Later, we will allow ourselves to use the notion of a ${\mathfrak{K}}$-type in a natural way also for other structures with a distinguished substructure ${\mathfrak{K}}$. For each \pi\in\mbox{\large\boldmath\alpha}^{{\mathfrak{K}}} choose an element $a$ having ${\mathfrak{K}}$-type $\pi$ in ${\mathfrak{A}}$ and for each $i\in I^{\prime}$ choose a witness structure ${\mathfrak{W}}_{\pi,i}$ for $a$ and $\psi^{\prime}_{i}$. Let ${\mathfrak{W}}^{*}_{\pi,i}={\mathfrak{W}}_{\pi,i}\!\!\restriction\!\!(W_{\pi,i}\setminus(K\cup\{a\})$). For each \pi\in\mbox{\large\boldmath\alpha}^{{\mathfrak{K}}}, $i\in I^{\prime}$ and $j=0,1,2$ let ${\mathfrak{W}}^{*}_{\pi,i,j}$ be a fresh isomorphic copy of ${\mathfrak{W}}^{*}_{\pi,i}$.

Universe. We define the universe of ${\mathfrak{B}}$ as follows $B:=C\cup\bigcup_{\pi,i,j}W^{*}_{\pi,i,j}$, where $\pi$ ranges over \mbox{\large\boldmath\alpha}^{{\mathfrak{K}}}, $i$ over $I^{\prime}$ and $j$ over $\{0,1,2\}$. We emphasise that the sets $W^{*}_{\pi,i,j}$ are disjoint from $C$ and from each other. We retain in ${\mathfrak{B}}$ the structure on $C$ from ${\mathfrak{A}}$ and for each $\pi,i,j$ we make ${\mathfrak{B}}\!\!\restriction\!\!(K\cup W^{*}_{\pi,i,j})$ isomorphic to ${\mathfrak{A}}\!\!\restriction\!\!(K\cup W^{*}_{\pi,i})$. This, in particular, makes the ${\mathfrak{K}}$-type in ${\mathfrak{B}}$ of each element $b$ belonging to some $W^{*}_{\pi,i,j}$ identical with the ${\mathfrak{K}}$-type in ${\mathfrak{A}}$ of the counterpart of $b$ from the original substructure ${\mathfrak{W}}_{\pi,i}$.

Witness structures for the court. Let us consider an element $c\in C\setminus K$, and denote by $\pi$ its ${\mathfrak{K}}$-type in ${\mathfrak{A}}$. For every $i\in I^{\prime}$ make ${\mathfrak{B}}\!\!\restriction\!\!(\{c\}\cup({W}_{\pi,i}\cap K)\cup{W}^{*}_{\pi,i,0})$ isomorphic to ${\mathfrak{W}}_{\pi,i}$. This provides a witness structure for $c$ and $\psi^{\prime}_{i}$ in ${\mathfrak{B}}$. Note that a single such step (for fixed $c$ and $i$) consists in defining relations on tuples containing $c$, at least one element of ${W}^{*}_{\pi,i,0}$ and possibly some elements of $K$, since relations on other relevant tuples were defined in the desired way in step Universe. Note that no conflicts (attempts to set the same atom to both true and false) can arise, when we perform this step for some $c$ and $i$ and then for the same $c$ and some $i^{\prime}\not=i$, because in the first case we define truth-values of relations only on tuples containing some element from $W^{*}_{\pi,i,0}$, and in the second—only on tuples containing some element from $W^{*}_{\pi,i^{\prime},0}$, and $W^{*}_{\pi,i,0}$ is disjoint from $W^{*}_{\pi,i^{\prime},0}$. Finally, when we perform this step for some $c$, and then for some $c^{\prime}\not=c$ no conflicts arise since in the first case we define relations only on tuples containing $c$ but not $c^{\prime}$ and in the second—only on tuples containing $c^{\prime}$ but not $c$.

Witness structures for the other elements. Consider now any element $b\in B\setminus C$. Assume it belongs to ${W}^{*}_{\pi^{\prime},i^{\prime},j^{\prime}}$ and that $\pi$ is the ${\mathfrak{K}}$-type of $b$ in ${\mathfrak{B}}\!\!\restriction\!\!(K\cup\{b\})$. For each $i\in I^{\prime}$ make the structure on $\{b\}\cup(W_{\pi,i}\cap K)\cup W^{*}_{\pi,i,(j^{\prime}+1\mod{3})}$ isomorphic to ${\mathfrak{W}}_{\pi,i}$. This provides a witness structure for $b$ and $\psi^{\prime}_{i}$ in ${\mathfrak{B}}$. Again, to do it we need to define relations on some tuples containing $b$ and some element of $W^{*}_{\pi,i,(j^{\prime}+1\mod{3})}$, and, due to our strategy, this can be done without conflicts.

Completing the structure. For any pair of distinct elements $b,b^{\prime}\in B$ whose $2$-type has not yet been defined in ${\mathfrak{B}}$ choose a pair of distinct elements $a,a^{\prime}$ with ${\rm tp}^{{{\mathfrak{A}}}}({a})={\rm tp}^{{{\mathfrak{B}}}}({b})$ and ${\rm tp}^{{{\mathfrak{A}}}}({a^{\prime}})={\rm tp}^{{{\mathfrak{B}}}}({b^{\prime}})$, and set ${\rm tp}^{{{\mathfrak{B}}}}({b,b^{\prime}}):={\rm tp}^{{{\mathfrak{A}}}}({a,a^{\prime}})$. An appropriate pair $a,a^{\prime}$ exists even if ${\rm tp}^{{{\mathfrak{B}}}}({b})={\rm tp}^{{{\mathfrak{B}}}}({b^{\prime}})$ since at least one of $b,b^{\prime}$ has a non-royal type. For any tuple $\bar{b}$ of elements of $B$ containing at least three distinct elements, and any relation symbol $R$ of arity $|\bar{b}|$, if the truth-value of $R(\bar{b})$ in ${\mathfrak{B}}$ has not yet been defined then set it to false.

This finishes the definition of ${\mathfrak{B}}$. Let us now estimate its size. We can bound the number and the arity of relation symbols by $n=|\varphi|$. Then the size of $K$ is bounded by the number of possible $1$-types, $2^{n}$. The size of $C$ is bounded by $2^{n}\cdot n(n-1)$, as each element $a$ of $K$ may need at most $n$ witness structures each of them containing (besides $a$) at most $n-1$ elements. The number of possible relations of arity at most $n$ on a a set of $2^{n}+1$ elements is bounded by $2^{{(2^{n}+1)}^{n}}\leq 2^{2^{n^{2}+n}}$, thus the number of ${\mathfrak{K}}$-types is bounded by $(2^{2^{n^{2}+n}})^{n}=2^{n\cdot 2^{n^{2}+n}}\leq 2^{2^{n^{2}+2n}}\leq 2^{2^{2n^{2}}}$ (for $n>1$). Finally, we can bound the size of $B$ by $2^{n}+2^{n}\cdot n(n-1)+3n(n-1)\cdot 2^{2^{2n^{2}}}$, doubly exponentially in $n$.

Presently, we explain that ${\mathfrak{B}}\models\varphi$. First note that for each $b\in B$ and each $i\in I^{\prime}$ there is an appropriate witness structure: if $b\in K$ then this witness structure is provided in ${\mathfrak{C}}$ which is a substructure of ${\mathfrak{B}}$. If $b\in C\setminus K$ or $b\in B\setminus C$ then a proper witness structure is provided explicitly either in step Witness structure for the court or, resp., Witness structures for the other elements. Thus ${\mathfrak{B}}$ satisfies all conjuncts of $\varphi$ of the form $\forall x\exists\bar{y}\psi^{\prime}_{i}(x,\bar{y})$.

Consider any conjunct $\forall\bar{x}(\gamma_{i}(\bar{x})\rightarrow\psi_{i}(\bar{x}))$ of $\varphi$ and a tuple of elements $\bar{b}$ such that ${\mathfrak{B}}\models\gamma_{i}(\bar{b})$. If $\bar{b}\subseteq C$ or $\bar{b}\subseteq K\cup W^{*}_{\pi,i,j}$ for some $\pi,i,j$ then the structure on $\bar{b}$ was made an isomorphic copy of some substructure of ${\mathfrak{A}}$ in step Universe. Otherwise $\bar{b}$ contains at least two distinct elements. In this case the structure on $\bar{b}$ was made an isomorphic copy of some substructure of ${\mathfrak{A}}$ either in one of the steps Witness structures for the court, Witness structures for the other elements or in step Completing the structure (in this last subcase $\bar{b}$ contains precisely two distinct elements). Thus ${\mathfrak{B}}\models\psi_{i}(\bar{b})$. Finally, consider the conjunct $\forall xy\psi^{\prime\prime}(x,y)$ and take any pair $b,b^{\prime}\in B$. Again, the structure on $\{b,b^{\prime}\}$ is an isomorphic copy of a substructure of ${\mathfrak{A}}$ defined (at the latests) in step Completing the structure.

This finishes the proof of (i). To see (ii) and (iii) we first observe that in both cases every satisfiable formula $\varphi$ has a model without kings. Given a structure ${\mathfrak{A}}$ we define two new structures $2{\mathfrak{A}}$ and $2{\mathfrak{A}}^{+}$, each of them with universe $A\times\{0,1\}$ and the substructures on $A\times\{0\}$ and $A\times\{1\}$ isomorphic to ${\mathfrak{A}}$. In $2{\mathfrak{A}}$ we make these two copies of ${\mathfrak{A}}$ completely disjoint by setting the truth-value of $R(\bar{a})$ to false for any $R$ and any tuple $\bar{a}$ (of the appropriate length) contained neither in $A\times\{0\}$ nor $A\times\{1\}$. In $2{\mathfrak{A}}^{+}$, for any tuple $\bar{a}$ contained neither in $A\times\{0\}$ nor $A\times\{1\}$ and for any relation symbol $R$ of arity $|\bar{a}|$, if this tuple contains at least three distinct elements then we also define $R(\bar{a})$ to be false. If $\bar{a}$ contains just two distinct elements, say $(a,0)$ and $(a^{\prime},1)$, then for any relation symbol $R$ or arity $|\bar{a}|$ set $R(\bar{a})$ true iff ${\mathfrak{A}}\models R(\bar{a}\!\!\restriction\!\!1)$ where $\bar{a}\!\!\restriction\!\!1$ is the projection of the elements of $\bar{a}$ on their first position.

Observations that if $\varphi$ is without equality and ${\mathfrak{A}}\models\varphi$ then $2{\mathfrak{A}}^{+}\models\varphi$, and that if $\varphi$ is in $\mbox{\rm GF}_{1}$ (even with equality) and ${\mathfrak{A}}\models\varphi$ then $2{\mathfrak{A}}\models\varphi$ are routine. Of course our new models are without kings. Starting our small model construction from a model without kings we get $K=\emptyset$ and thus ${\mathfrak{K}}$-types trivialize to $1$-types, which means that their number is bounded singly exponentially. Also $C=\emptyset$ and thus we construct ${\mathfrak{B}}$ out of the $W^{*}_{\pi,i,j}$ where $\pi$ ranges over the set of $1$-types, the number of possible $i$ is linear in $n$ and there are just three possible values of $j$. The size of each ${\mathfrak{W}}^{*}_{\pi,i,j}$ is linear in $n$. The size of the constructed models can be thus estimated by $3n(n-1)\cdot 2^{n}$. Hence part (ii) and (iii) of Thm. 3.2 hold.

4 Complexity

In this section we establish the complexity of the considered logics.

Theorem 4.1**.**

The satisfiability problem (= finite satisfiability problem)

1. (i)

for $\mbox{\rm TGF}_{1}$ with equality is 2-ExpTime*-complete.* 2. (ii)

for $\mbox{\rm TGF}_{1}$ without equality is NExpTime-complete. 3. (iii)

for $\mbox{\rm GF}_{1}$ is NExpTime-complete.

Upper bound in (i). We design an alternating satisfiability test for $\mbox{\rm TGF}_{1}$ using only exponential space. A 2-ExpTime-upper bound follows then from the fact that AExpSpace$=$2-ExpTime (Chandra, Kozen, Stockmeyer [5]). The procedure takes as its input a $\mbox{\rm TGF}_{1}$ formula $\varphi$ and works as described below. For simplicity our description is slightly informal. In particular, we do not precisely specify how structures constructed during its execution are represented. We also allow ourselves to write “guess an object $X$ such that $Y$” instead of more accurate “guess an object $X$; verify if $X$ meets property $Y$; if it does not then reject”.

Nondeterministically compute a normal form $\varphi^{\prime}$ as in Lemma 3.1. Let $n:=|\varphi^{\prime}|$. 2. 2.

Guess a set of $1$-types \mbox{\large\boldmath\alpha}=\mbox{\large\boldmath\alpha}_{r}\;\dot{\cup}\;\mbox{\large\boldmath\alpha}_{nr} over the signature of $\varphi^{\prime}$ (royal and non-royal types), such that for any $\alpha_{1}$, $\alpha_{2}$ (possibly $\alpha_{1}=\alpha_{2}$) such that \alpha_{1}\in\mbox{\large\boldmath\alpha} and \alpha_{2}\in\mbox{\large\boldmath\alpha}_{nr} there is a $2$-type $\beta$ such that $\beta\!\!\restriction\!\!x_{1}=\alpha_{1}$ and $\beta\!\!\restriction\!\!x_{2}=\alpha_{2}$, and $\beta$ does not violate the universal conjuncts of $\varphi^{\prime}$. 3. 3.

Guess structures ${\mathfrak{K}}$, ${\mathfrak{C}}$ of size at most $2^{n}$ and $2^{n}\cdot n^{2}$, resp., with ${\mathfrak{K}}$ being a substructure of ${\mathfrak{C}}$, such that (i) \mbox{\large\boldmath\alpha}[K]=\mbox{\large\boldmath\alpha}_{r}, (ii) \mbox{\large\boldmath\alpha}[C\setminus K]\subseteq\mbox{\large\boldmath\alpha}_{nr}, (iii) each element of $K$ has all the required witness structures for $\forall\bar{\exists}$ conjuncts of $\varphi^{\prime}$ in ${\mathfrak{C}}$, and (iv) universal conjuncts of $\varphi^{\prime}$ are not violated in ${\mathfrak{C}}$. 4. 4.

Universally choose an element $c\in C\setminus K$ and a conjunct $\psi$ of $\varphi^{\prime}$ of type $\forall\bar{\exists}$. Set ${\mathfrak{F}}:={\mathfrak{C}}\!\!\restriction\!\!(K\cup\{c\})$. 5. 5.

Set $Counter:=0$. 6. 6.

Guess an extension ${\mathfrak{D}}$ of ${\mathfrak{F}}$, with universe $D=K\cup\{c\}\cup\{a_{1},\ldots,a_{t}\}$, such that (i) {\rm tp}^{{{\mathfrak{D}}}}({a_{i}})\in\mbox{\large\boldmath\alpha}_{nr} for all $i$, (ii) for some $k_{1},\ldots,k_{s}\in K$ the structure ${\mathfrak{W}}={\mathfrak{D}}\!\!\restriction\!\!\{c,k_{1},\ldots,k_{s},a_{1},\ldots,a_{t}\}$ is a witness structure for $c$ and $\psi$, (iii) universal conjuncts of $\varphi^{\prime}$ are not violated in ${\mathfrak{D}}$. If $t=0$ then accept. 7. 7.

Universally choose a new value for $c$ from $\{a_{1},\ldots,a_{t}\}$ and a conjunct $\psi$ of $\varphi^{\prime}$ of the form $\forall\bar{\exists}$. Set ${\mathfrak{F}}:={\mathfrak{F}}\!\!\restriction\!\!(K\cup\{c\})$. 8. 8.

$Counter:=Counter+1$ 9. 9.

If $Counter<2^{2^{2n^{2}}}$ then goto 6 else accept.

Let us first note that exponential space is sufficient to perform the above algorithm. By Lemma 3.1 we have that $n$ is bounded polynomially in $|\varphi|$. The number of $1$-types in $\alpha$ is also bounded by $2^{n}$, as a $1$-type is determined by a subset of the signature. For some pairs of $1$-types we need to guess a $2$-type whose description is exponential (there are at most $2^{n}$ tuples of length not greater than $n$ consisting of a pair of elements, and at most $n$ relation symbols). The size of the structure ${\mathfrak{C}}$ guessed in Step 4 is explicitly required to be exponential in $n$. Also its description requires only exponentially many bits (recall that the arity of all relations is bounded by $n$). Analogously we can bound the size of structures ${\mathfrak{D}}$ guessed in Step 6. Finally, the value of $Counter$ is bounded doubly exponentially, so it also can be written using exponentially many bits.

Now we argue that the procedure accepts its input $\varphi$ iff $\varphi$ is satisfiable. Assume first that the procedure accepts $\varphi$. We show that then $\varphi^{\prime}$ (and thus, by Lemma 3.1, also $\varphi$) has a model. Consider an accepting run of the procedure. We may assume w.l.o.g. that this run is uniform, that is, when entering step 6, in configurations differing only in the values of $Counter$ (but with isomorphic ${\mathfrak{F}}$s) it makes the same (isomorphic) guesses of ${\mathfrak{D}}$. Then the modification of this procedure in which Step 9 is replaced just by ’Goto 6’ can run infinitely (if necessary) without clashes. Indeed if the value $Counter=2^{2^{2n^{2}}}$ is reached we have a guarantee that the ${\mathfrak{K}}$-type of the current $c$ appeared before in the computation (cf. our estimations on the size of the small model constructed in the proof of Thm. 3.2, in particular on the number of ${\mathfrak{K}}$-types). We can construct a model for $\varphi^{\prime}$ starting from the substructure ${\mathfrak{C}}$ guessed in Step 4, and then providing witness structures for all conjuncts of the form $\forall\bar{\exists}$ of $\varphi^{\prime}$ and elements $c$ in accordance with guesses of ${\mathfrak{D}}$ is Step 6 (we add fresh copies of elements $a_{1},\ldots,a_{t}$ and make the structure on the union of $K$, $\{c\}$ and the set of the newly added elements isomorphic to ${\mathfrak{D}}$). We complete the (usually infinite) structure as in Step Completing the structure of the small model construction from the proof of Thm. 3.2 using the $2$-types guaranteed in Step 1. As in that proof we can also show that the constructed structure is a model of $\varphi^{\prime}$.

Conversely, assume that $\varphi$ has a model ${\mathfrak{A}}^{*}$. Nondeterministically compute its normal form $\varphi^{\prime}$ and let ${\mathfrak{A}}\models\varphi^{\prime}$ be an expansion of ${\mathfrak{A}}^{*}$ guaranteed by Lemma 3.1. Let ${\mathfrak{B}}$ be a model of $\varphi^{\prime}$ constructed as in the proof of Thm. 3.2, starting from ${\mathfrak{A}}$. W can now make all the guesses of our procedure in accordance with ${\mathfrak{B}}$: denoting $K_{\mathfrak{B}}$ and $C_{\mathfrak{B}}$ the set of kings and a court of ${\mathfrak{B}}$, resp., we set \mbox{\large\boldmath\alpha}_{r}:=\mbox{\large\boldmath\alpha}[K_{\mathfrak{B}}], \mbox{\large\boldmath\alpha}_{nr}:=\mbox{\large\boldmath\alpha}[B\setminus K_{\mathfrak{B}}], ${\mathfrak{K}}:={\mathfrak{K}}_{\mathfrak{B}}$, ${\mathfrak{C}}:={\mathfrak{C}}_{\mathfrak{B}}$. Then in the loop 6-9, when a structure ${\mathfrak{D}}$ containing a witness structure for $c$ and $\psi$ is going to be guessed we choose an element $c^{\prime}\in{\mathfrak{B}}$ such that the ${\mathfrak{K}}$-types of $c^{\prime}$ in ${\mathfrak{B}}$ and $c$ in ${\mathfrak{F}}$ are identical and find a witness structure for $c^{\prime}$ and $\psi$ in ${\mathfrak{B}}$. We set ${\mathfrak{D}}$ to be isomorphic to the restriction of ${\mathfrak{B}}$ to the union of $K_{\mathfrak{B}}$ and this witness structure. This strategy naturally leads to acceptance.

Lower bound in (i). We encode computations of an alternating Turing machine $M$ working in exponential space on its input $\bar{a}=a_{i_{0}}\ldots a_{i_{n-1}}$.

The general idea of the proof is not far from the ideas used in the proofs of the 2-ExpTime-lower bound for GF [7] and 2-NExpTime-lower bound for TGF with constants [15]. We must, however, be careful to avoid quantification leaving more than one variable free, which happens in both the above-mentioned proofs. E.g., in [7] configurations of a Turing machine are encoded by pairs of elements $a_{1},a_{2}$; concretely, by the truth-values of some relations of arity $O(n)$ on tuples consisting of $a_{1},a_{2}$. To enforce existence of successor configurations quantification leaving two free variables is needed there.

We assume that $M$ has states $s_{0},s_{1},\ldots,s_{k}$, where $s_{0}$ is the initial state, $s_{k-1}$ is the only accepting state, and $s_{k}$ is the only rejecting state. The alphabet of $M$ consists of letters $a_{0},\ldots,a_{l}$ where $a_{0}$ represents blank. Without loss of generality we assume that $M$ has precisely two possible moves in every configuration, that on its every computation path it enters the accepting or rejecting state no later than in $2^{2^{n}}$-th step, and then, after reaching such final state, does not stop but works infinitely in a trivial way, without changing its configuration.

For $i=0,\ldots,k$ we use a predicate $S_{i}$, for $i=0,\ldots,l$ we use a predicate $A_{i}$ and to describe the head position we use a predicate $H$. Each of the $S_{i}$, $A_{i}$ and $H$ is of arity $1+n$.

We enforce the existence of two kings, called zero and one, marked, resp., by unary predicates $Z$ and $O$. They will also be called bits, serve as binary digits and will be used to encode the numbers of tape cells.

[TABLE]

The idea is that every element of a model encodes a configuration of $M$ in its relation to tuples of bits of size $n$. Such a tuple of bits $\bar{b}$ can be naturally read as a number in the range $[0,\ldots,2^{n}-1]$. Let us think that $A_{i}(c,\bar{b})$ means that in the configuration encoded by $c$, tape cell $\bar{b}$ contains $a_{i}$, $H(c,\bar{b})$ denotes that this tape cell is scanned by the head and, for a cell observed by the head, $S_{i}(c,\bar{b})$ means that $M$ is in state $s_{i}$.

To be able to speak about properties of configurations of $M$ in $\mbox{\rm TGF}_{1}$ we introduce a predicate $C$ of arity $1+2n$, which will be made true at least for all tuples consisting of an arbitrary element of a model followed by $2n$ bits. We first say that, for any $0\leq i<2n$, ${C}$ holds for some tuple consisting of $i$ ones and $2n-i$ zeros, and then propagate $C$ to all relevant tuples, using the fact that the pair of permutations $(2,1,3,\ldots,2n)$ and $(2,3,\ldots,2n,1)$ generates the whole permutation group $S_{2n}$. Below $\bar{z}=z_{2n-1},z_{2n-2},\ldots,z_{1},z_{0}$.

[TABLE]

[TABLE]

We use a convention that $\bar{u},\bar{v},\bar{w}$ are tuples of variables of size $n$, $\bar{u}=u_{n-1},\ldots,u_{0}$ and analogously for $\bar{v}$ and $\bar{w}$. We introduce abbreviations, $\lambda^{\scriptscriptstyle\not=}(\bar{u},\bar{v})$ and $\lambda^{\scriptscriptstyle+1}(\bar{u},\bar{v})$ for quantifier-free formulas of size polynomial in $n$. The former is intended to say that the numbers encoded by $\bar{u}$ and $\bar{v}$ differ, the latter—that the number encoded by $\bar{v}$ is greater by one than the number encoded by $\bar{u}$. E.g., $\lambda^{\scriptscriptstyle+1}(\bar{u},\bar{v})$ can be defined as

[TABLE]

Analogously, we use $\lambda^{i}(\bar{u})$ and $\lambda^{\geq i}(\bar{u})$ for formulas saying that the number encoded by $\bar{u}$ is, resp., equal to $i$ and greater or equal $i$. Again, they can be defined in a standard way by quantifier-free, polynomially bounded formulas.

Now we ensure that every element properly encodes a configuration. The following formulas say that, resp., there is a tape cell scanned by the head, there is at most one such cell, this cell carries also information about the state, and every tape cell contains precisely a single letter. Below $\dot{\bigvee}_{i}\psi_{i}$ is an easily definable shorthand for ‘exactly one of the $\psi_{i}$ holds’.

[TABLE]

We then say that every element has two successors, and, using the trick with permutations prepare appropriate guards. Predicates $Succ_{i}$ are of arity $2+3n$. For $i=1,2$ we write:

[TABLE]

[TABLE]

We next describe the computations of $M$ on $\bar{a}$. First we say that the letter at a tape cell not scanned by the head does not change in the successor configurations. For $i=1,2$:

[TABLE]

Consider now existential moves. Assume that in an existential state $s_{i}$, reading a letter $a_{j}$ the machine has two possible transitions: $(s_{i^{\prime}},a_{j^{\prime}},\rightarrow)$ and $(s_{i^{\prime\prime}},a_{j^{\prime\prime}},\leftarrow)$. Then we write:

[TABLE]

Similarly, assume that $M$ has moves as above in a universal state $s_{i}$. We write:

[TABLE]

[TABLE]

We finally say that a model does not contain a configuration with the rejecting state and impose the existence of an element encoding the initial configuration.

[TABLE]

[TABLE]

Showing that $M$ accepts $\bar{a}$ iff the constructed formula has a model is routine.

Upper bounds in (ii) and (iii). In both cases we have proved an exponential model property. Thus, to test satisfiability it suffices to guess an exponentially bounded structure and verify that it indeed is a model. More precisely, given a formula $\varphi$ we nondeterministically convert it into normal form $\varphi^{\prime}$. We guess an exponentially bounded model ${\mathfrak{B}}$ of $\varphi^{\prime}$ (again we remark that not only the universe of ${\mathfrak{B}}$ is bounded exponentially, but also the description of ${\mathfrak{B}}$, since we are dealing only with at most $|\varphi^{\prime}|$ relations of arity at most $|\varphi^{\prime}|$), and verify that it is indeed a model. The last task can be carried out in an exhaustive way: for each $b\in B$ and each conjunct of $\varphi^{\prime}$ of the form $\forall x\exists\bar{y}\psi^{\prime}_{i}(x,\bar{y})$ guess which elements form a witness structure for $b$ and this conjunct and check that they indeed form a required witness structure; for each conjunct $\forall\bar{x}(\gamma_{i}(\bar{x})\rightarrow\psi_{i}(\bar{x}))$ enumerate all tuples $\bar{b}$ of elements of $B$ such that $|\bar{b}|=|\bar{x}|$ and check that ${\mathfrak{B}}\models\gamma_{i}(\bar{b})\rightarrow\psi_{i}(\bar{b})$. Proceed analogously with the conjunct $\forall xy\psi^{\prime\prime}(x,y)$.

Lower bounds in (ii) and (iii). It suffices to show NExpTime-lower bound for $\mbox{\rm GF}_{1}$ without equality. As advertised in the Introduction, we even strengthen this result using only uniform formulas, that is we show NExpTime-hardness of the uniform one-dimensional guarded fragment being the intersection of GF and $\mbox{\rm UF}_{1}$. For our current purposes it is sufficient to say that conjunctions of sentences $\exists\bar{x}\psi(\bar{x})$ and $\forall\bar{x}\psi(\bar{x})$ with quantifier-free $\psi$ are uniform if all atoms of $\varphi$ use either all variables of $\bar{x}$ or just one of them. We use only formulas of such kind. For a general definition of $\mbox{\rm UF}_{1}$ see [9] or [13]. Our proof goes by an encoding of an exponential tiling problem and is given in the Appendix.

5 Variations on extensions of the guarded fragment

Let us see what happens when the ideas of one-dimensionality, tri-guardedness and their combination are applied to two extensions of the guarded fragment: the loosely guarded fragment, LGF, introduced by van Benthem [17], and the guarded negation fragment, GNFO, introduced by Bárány, ten Cate and Segoufin [3]. LGF is defined similarly to GF, but the notion of the guard is more liberal: in subformulas of the form $\exists\bar{y}(\gamma(\bar{x},\bar{y})\wedge\varphi(\bar{x},\bar{y}))$ and $\forall\bar{y}(\gamma(\bar{x},\bar{y})\rightarrow\varphi(\bar{x},\bar{y}))$ we do not require that $\gamma$ is atomic but allow it to be a conjunction of atoms such that for every variable from $\bar{y}$ and every variable from $\bar{y}\cup\bar{x}$ there is an atom in $\gamma$ containing both of them. In GNFO (atomic) guards are required not for quantifiers but for negated subformulas. For a more detailed definition of GNFO see [3].

One-dimensionality. First, let us see that the one-dimensionality decreases the complexity of LGF, similarly as in the case of GF, but does not affect the complexity of GNFO.

Theorem 5.1**.**

1. (i)

The satisfiability (= finite satisfiability) problem for the one-dimensional LGF, $\mbox{\rm LGF}_{1}$, is NExpTime-complete. $\mbox{\rm LGF}_{1}$ has an exponential model property. 2. (ii)

The satisfiability (= finite satisfiability) problem for the one-dimensional GNFO is 2-ExpTime*-complete.*

To prove (i) we adjust the small model construction from the proof of Thm. 3.2, by using more copies of witness structures and refining the strategy of providing witnesses. The construction from the proof of Thm. 3.2 cannot be applied without any changes to the current scenario, as it may accidentally form some cliques of cardinality greater than $2$ in the Gaifmann graph of the constructed model which then could work as loose guards and lead to a violation of some universal conjuncts of the input formula. Details are given in the Appendix.

To see (ii) note that GNFO contains the unary negation fragment, UNFO, whose satisfiability problem is already 2-ExpTime-hard. UNFO is not one-dimensional but can be polynomially translated to its equivalent UN-normal form (ten Cate, Segoufin [16]), which is one-dimensional. The upper bound is inherited from the upper bound for full GNFO [3].

Tri-guardedness. Unfortunately, allowing for unguarded binary subformulas leads to undecidability already in the case of one-dimensional variants of LGF and GNFO.

Theorem 5.2**.**

The (finite) satisfiability problems for the one-dimensional LGF or GNFO, with unguarded subformulas with two variables, even without equality, are undecidable.

In the case of $\mbox{\rm LGF}_{1}$, unguarded binary subformulas give the power of full one-dimensional fragment $\mbox{\rm F}_{1}$. Indeed by adding a conjunct $\forall xyG^{*}(x,y)$ we would be able to guard any tuple of variables $x_{1},\ldots,x_{k}$ by the conjunction $\bigwedge_{i\not=j}G^{*}(x_{i},x_{j})$. (A similar observation is present also in [15].) As the satisfiability problem for $\mbox{\rm F}_{1}$ is undecidable [9] this gives the undecidability of the considered variation of LGF. For the one-dimensional GNFO, using unguarded negations of binary atoms one can express transitivity of binary relations: $\neg\exists xyz(Rxy\wedge Ryz\wedge\neg Rxz)$. One-dimensional GNFO contains the two-variable guarded fragment which becomes undecidable when extended by transitive relations (Kieroński [12], Kazakov [11]). Thus the claim follows.

6 Adding constants

Finally, we study the satisfiability problem for $\mbox{\rm GF}_{1}$ and $\mbox{\rm TGF}_{1}$ with constants. It turns out that in the presence of constants we lose neither the decidability nor the finite model property, however, the complexity increases. The following theorem completes Table 1.

Theorem 6.1**.**

1. (i)

Every satisfiable formula in $\mbox{\rm TGF}_{1}$ with constants has a finite model of size bounded doubly exponentially in its length. 2. (ii)

The satisfiability (= finite satisfiability) problem for $\mbox{\rm GF}_{1}$ with constants (with or without equality) is 2-ExpTime*-complete.* 3. (iii)

The satisfiability (= finite satisfiability) problem for $\mbox{\rm TGF}_{1}$ with constants (with or without equality) is 2-NExpTime*-complete.*

It is not difficult to see that Lemma 3.1 holds for formulas with constants. Thus, to show (i) we can use a minor adaptation of our small model construction from the proof of Thm. 3.2. Indeed, interpretations of constants may be treated as kings. The number of ${\mathfrak{K}}$-types remains doubly exponential. The construction works then essentially without changes, we only remark that in step Completing the structure, when a $2$-type for a pair of elements is chosen, we need to define the truth-values of all relations on tuples built out of these elements and constants. This way we get a doubly exponential bound on the size of models.

The upper bound in (ii) follows from the fact that full GF with constants is in 2-ExpTime [7].

The upper bound in (iii) follows from the fact that full TGF with constants is in 2-NExpTime [15]. We remark, however, that this upper bound for TGF is obtained without proving the finite model property, thus to justify the upper bound for finite satisfiability of $\mbox{\rm TGF}_{1}$ we must refer to part (i) of Thm. 6.1.

The corresponding lower bounds in (ii) and (iii) are proved in the Appendix.

Acknowledgements. The author would like to thank Sebastian Rudolph and the anonymous reviewers for their helpful comments.

Appendix A Normal form (Lemma 3.1)

We sketch a proof of Lemma 3.1.

Proof A.1**.**

Take a $\mbox{\rm TGF}_{1}$ formula $\varphi$. W.l.o.g. assume that all its quantifiers are existential. We begin with an innermost subformula $\psi$ of $\varphi$ starting with a block of quantifiers. If $\psi$ contains a free variable and a quantifier guard, i.e., it is of the form $\exists\bar{y}(\eta(x,\bar{y})\wedge\psi^{\prime}(x,\bar{y}))$, for some guard $\eta$, then we replace it by $P_{\psi}(x)$ and add two normal form conjuncts $\forall x\exists\bar{y}(P_{\psi}(x)\rightarrow(\eta(x,\bar{y})\wedge\psi^{\prime}(x,\bar{y})))$ and $\forall x\bar{y}(\eta(x,\bar{y})\rightarrow\neg\psi^{\prime}(x,\bar{y})\vee P_{\psi}(x))$ axiomatising $P_{\psi}$. If $\psi$ has a free variable but not a quantifier guard, i.e., it is of the form $\exists{y}\psi^{\prime}(x,{y})$ we similarly replace it by $P_{\psi}(x)$ and add normal form conjuncts $\forall x\exists y(P_{\psi}(x)\rightarrow\psi^{\prime}(x,y))$ and $\forall xy(\psi^{\prime}(x,y)\rightarrow P_{\psi}(x))$. If $\psi$ is a subsentence, i.e., it is of the form $\exists\bar{y}\psi^{\prime}(\bar{y})$ then we nondeterministically guess its truth value, replace it by $\top$ or $\bot$ according to this guess and add $\psi$ or, resp., $\neg\psi$ as a conjunct of our new formula. Moving up the original formula $\varphi$ we repeat this procedure for subformulas that are now innermost, and so forth. The formula obtained in this process has, up to trivial logical transformations, the desired shape.

Appendix B NExpTime-lower bound for (uniform) GF1 (Thm. 4.1)

We proceed by a reduction from a variant of the tiling problem. Let ${\mathfrak{G}}_{m}$ denote the standard grid on a finite $m\times m$ torus: ${\mathfrak{G}}_{m}=([0,m-1]^{2},H,V)$, $H=\{((p,q),(p^{\prime},q)):p^{\prime}-p\equiv 1\mod m\}$, $V=\{((p,q),(p,q^{\prime})):q^{\prime}-q\equiv 1\mod m\}$. A tiling system is a quadruple $\mathcal{T}=\langle C,c_{0},Hor,Ver\rangle$, where $C$ is a non-empty, finite set of colours, $c_{0}$ is an element of $C$, and $Hor$, $Ver$ are binary relations on $C$ called the horizontal and vertical constraints, respectively. A tiling for $\mathcal{T}$ of a grid ${\mathfrak{G}}_{m}$ is a function $f:[0,m-1]^{2}\rightarrow C$ such that $f(0,0)=c_{0}$ and, for all $d\in[0,m-1]^{2}$, the pair $\langle f(d),f(h(d))\rangle$ is in $Hor$ and the pair $\langle f(d),f(v(d))\rangle$ is in $Ver$. The exponential tiling problem is defined as follows. Given a number $n\in{\mathbb{N}}$ written in unary, and a tiling system $\mathcal{T}$, verify if $\mathcal{T}$ has a tiling of the grid ${\mathfrak{G}}_{m}$, where $m={2^{n}}$. It is well known that the exponential tiling problem is NExpTime-complete.

Given $n\in{\mathbb{N}}$ and a titling system $\cal T$ we now construct a formula satisfiable iff there is a tiling for $\cal T$ of the grid ${\mathfrak{G}}_{m}$ for $m=2^{n}$. As in the proof of the lower bound in Thm. 4.1 (i), we mark two elements with predicates $Z$ and $O$. This time, however, we cannot make them kings (formulas enforcing kings use both equality and unguarded subformulas with two variables). As we will see this will not be harmful. Let $N$ be a predicate of arity $4n$. We say that two different elements exist, one in $Z$ and one in $O$. We call them, resp., $zero$ and $one$. We enforce that $N$ holds for any tuple built out of zeros and ones. We use the trick we already know: we first say that, for any $0\leq i<4n$, $N$ holds for some tuple consisting of $i$ ones and $4n-i$ zeros, and then propagate $N$ to all relevant tuples. Below $\bar{u}$ denotes the tuple of variables $u_{1},\ldots,u_{4n}$.

[TABLE]

[TABLE]

For every colour $t\in C$ we introduce a predicate $D_{t}$ of arity $4n$. A tuple of $zero$s and $one$s of length $n$ can be naturally interpreted as a number from the range $[0,\ldots,2^{n}-1]$. When $\bar{a}$, $\bar{b}$, $\bar{c}$, $\bar{d}$ are such tuples we want to interpret the fact that $D_{t}(\bar{a},\bar{b},\bar{c},\bar{d})$ for some $\bar{c}$, $\bar{d}$ holds as that the tile of colour $t$ is placed at coordinates $\bar{a}$, $\bar{b}$. To this end we say that for every tuple of length $4n$ precisely one of $D_{t}$ holds, and then we dummify the second half of variables using the trick with permutations. Below $\bar{w}$ represents the tuple $w_{1},\ldots,w_{2n}$.

[TABLE]

[TABLE]

Now we can easily encode horizontal and vertical constraints on tiles. Below we present an encoding of horizontal constraints. Vertical constraints can be encoded analogously.

[TABLE]

Recall that $\lambda^{\scriptscriptstyle+1}(\bar{x},\bar{z})$ is a quantifier-free, formula saying that $\bar{z}$ encodes the number greater by $1$ (we assume that $\lambda^{\scriptscriptstyle+1}$ counts modulo $2^{n}$) than the one encoded by $\bar{x}$.

This finishes the reduction. Observing that the conjunction of (19)–(23) (plus a formula for vertical constraints) is satisfiable iff $\mathcal{T}$ tiles ${\mathfrak{G}}_{m}$ is, again, routine.

As remarked we used only uniform formulas, so we have the following corollary.

Corollary B.1**.**

The satisfiability problem for uniform one-dimensional guarded fragment is NExpTime-complete.

Appendix C NExpTime-upper bound for LGF1 (Thm. 5.1)

For $\mbox{\rm LGF}_{1}$ we can again use a Scott-like normal form, which now looks as follows:

[TABLE]

where the $\gamma_{i}(\bar{x})$ are loose guards, in this case being conjunctions of atoms such that every pair of variables from $\bar{x}$ coincides in at least one atom. A natural counterpart of Lemma 3.1, with a similar proof, holds for $\mbox{\rm LGF}_{1}$. Thus in the sequel we can restrict attention to normal form formulas of the shape as in (24).

To prove (i) we adjust the small model construction from the proof of Thm. 3.2. We assume that $K=\emptyset$ (this can be done w.l.o.g. since, as for GF, if ${\mathfrak{A}}\models\varphi$ then $2{\mathfrak{A}}\models\varphi$, for any LGF formula $\varphi$). Thus, there are no kings, ${\mathfrak{K}}$-types in ${\mathfrak{A}}$ become just $1$-types and there are exponentially many of them.

The construction from the proof of Thm. 3.2 cannot be applied without any changes to the current scenario, as it may accidentally form some cliques of cardinality greater than $2$ in the Gaifmann graph of the constructed model which then could work as loose guards and lead to a violation of some universal conjuncts of (24). There are three sources from which such cliques may arise.

First potential such source is the step Completing the structure which in the proof of Thm. 3.2 allows us to define the $2$-types not specified in the previous steps as any $2$-types from the original model ${\mathfrak{A}}$ which agree with the $1$-types of the given elements. In particular these $2$-types can contain some binary atoms. The potential danger here can be easily avoided by removing from the $2$-types which are going to be used in this step any non-unary atoms (which is a standard strategy in constructions of models for guarded formulas; such a stragety was not used in the proof of Thm. 3.2 since in that proof we needed to cover the case of tri-guarded formulas).

Two other kinds of dangerous cliques could appear in our original construction for $\mbox{\rm GF}_{1}$. Cliques of the first kind are those created by three elements belonging to three different subsets $W^{*}_{\pi,i,j}$ with three different values of $j$. Consider, e.g., a normal form $\mbox{\rm LGF}_{1}$ formula $\forall xyz(Rxy\wedge Ryz\wedge Rzx\rightarrow\bot)\wedge\forall x\exists yRxy$ and its model ${\mathfrak{A}}$ consisting of four elements joined by $R$ in a cyclic fashion. Starting from ${\mathfrak{A}}$, the construction from the proof of Thm. 3.2 would construct a structure ${\mathfrak{B}}$ with three elements forming eventually a triangle forbidden by the universal conjunct.

Cliques of the second kind could appear when two (or more) elements connected by some binary relation, say $R$, having the same type $\pi^{\prime}$ and belonging to the same $W^{*}_{\pi,i,j}$ look for their witnesses for the $i^{\prime}$-th conjunct $\forall\bar{\exists}$, since in such case the original strategy requires them to use the same $W^{*}_{\pi^{\prime},i^{\prime},j+1\mod 3^{\prime}}$, and, e.g., they both could connect by $R$ to the same element forming a triangle, which may again be forbidden by some universal conjunct.

To avoid forming such problematic cliques we need to use more copies of each witness structure this time. For clarity let us describe the whole construction in details. Let $\varphi$ be a normal form $\mbox{\rm LGF}_{1}$ formula as in (24) and ${\mathfrak{A}}$ its model without kings.

Pattern witness structures. For each $1$-type (=${\mathfrak{K}}$-type) $\pi$ realized in ${\mathfrak{A}}$ choose an element $a\in A$ of $1$-type $\pi$ and for each $i\in I^{\prime}$ choose a witness structure ${\mathfrak{W}}_{\pi,i}$ for $a$ and $\psi^{\prime}_{i}$. Let ${\mathfrak{W}}^{*}_{\pi,i}={\mathfrak{W}}_{\pi,i}\!\!\restriction\!\!(W_{\pi,i}\setminus\{a\}$). Let $n$ be the maximum size of $W^{*}_{\pi,i}$ across all the $\pi$ and $i$.

Universe. We define the universe of ${\mathfrak{B}}$ as follows $B:=\bigcup_{\pi,i,j,s}W^{*}_{\pi,i,j,s}$, where $\pi$ ranges over all $1$-types realized in ${\mathfrak{A}}$, $i$ over $I^{\prime}$, $j$ over $\{0,1,2,3\}$, and $s$ over $\{1,\ldots,n\}$. The sets $W^{*}_{\pi,i,j,s}$ are disjoint from each other. For all $\pi$, $i$, $j$, $s$ we make ${\mathfrak{B}}\!\!\restriction\!\!W^{*}_{\pi,i,j,s}$ isomorphic to ${\mathfrak{A}}\!\!\restriction\!\!W^{*}_{\pi,i}$. Note that in comparison to the case of $\mbox{\rm GF}_{1}$ we have four possible values for the index $j$ instead of three and an additional index $s$.

Providing witnesses. Let us number the elements in each $W^{*}_{\pi,i,j,s}$ from $1$ up to, at most, $n$. Consider now any element $b\in B$. Assume it belongs to ${W}^{*}_{\pi^{\prime},i^{\prime},j^{\prime},s^{\prime}}$, is numbered $s$, and has $1$-type $\pi$. For each $i\in I^{\prime}$ make the structure on $\{b\}\cup W^{*}_{\pi,i,(j^{\prime}+1\mod{4}),s}$ isomorphic to ${\mathfrak{W}}_{\pi,i}$. This provides a witness structure for $b$ and $\psi^{\prime}_{i}$ in ${\mathfrak{B}}$. Note that there are no conflicts with the previously defined substructure on $W^{*}_{\pi,i,(j^{\prime}+1\mod{4}),s}$.

Completing the structure. For any tuple $\bar{b}$ of elements of $B$ containing at least two distinct elements, and any relation symbol $R$ of arity $|\bar{b}|$, if the truth-value of $R(\bar{b})$ in ${\mathfrak{B}}$ has not yet been defined then set it to false. Note that this step differs from the corresponding step in the proof of Thm. 3.2, as announced.

This finishes the definition of ${\mathfrak{B}}$. We remark that using four values for $j$ instead of three guarantees that dangerous cliques of the first kind will not appear. On the other hand, introducing the extra index $s$ for witness structures, and the described strategy of providing wintesses guarantee that cliques of the second kind are avoided.

Actually, it is readily verified that the only cliques that can appear in the Gaifmann graph of ${\mathfrak{B}}$ are those consisting of elements from the same witness structure for some element. As the structure on them is copied from the original structure ${\mathfrak{A}}$ it follows that they cannot lead to a violation of the universal conjuncts of $\varphi$. As we explicitly take care of providing witness structures for all elements we get that ${\mathfrak{B}}$ is the desired exponential model of $\varphi$.

NExpTime-upper complexity bound then easily follows: we can just guess an exponentially bounded structure and verify that it is indeed a model of $\varphi$, similarly as described in the case of $\mbox{\rm GF}_{1}$ in the proof of Thm. 4.1 (iii).

Appendix D Complexity in the presence of constants (Thm. 6.1)

In this section we prove Thm. 6.1.

It is not difficult to see that Lemma 3.1 holds for formulas with constants.

Thus, to show (i) we can use a minor adaptation of our small model construction from the proof of Thm. 3.2. Indeed, interpretations of constants may be treated as kings. The number of ${\mathfrak{K}}$-types remains doubly exponential. The construction works then essentially without changes, we only remark that in step Completing the structure, when a $2$-type for a pair of elements is chosen, we need to define the truth-values of all relations on tuples built out of these elements and constants. This way we get a doubly exponential bound on the size of models.

The upper bound in (ii) follows from the fact that full GF with constants is in 2-ExpTime [7].

For the upper bound in (iii) we design a simple algorithm which just converts a given formula into its normal form, guesses its doubly exponentially bounded model guaranteed by part (i) of this lemma and verifies it. Alternatively, the upper bound for the general satisfiability problem follows from the fact that full TGF with constants is in 2-NExpTime [15]. We remark, however, that this upper bound for TGF is obtained without proving the finite model property, thus it does not give automatically the upper bound for finite satisfiability of $\mbox{\rm TGF}_{1}$ with constants.

The rest of this section is devoted for lower bounds.

D.1 2-ExpTime-lower bound for GF1 with constants

Our 2-ExpTime-lower bound proof for $\mbox{\rm TGF}_{1}$ with equality can be easily adapted to the case of $\mbox{\rm GF}_{1}$ with constants and without equality.

In the former, equality is needed only to enforce the existence of two kings (called bits). Here their role will be played by two constants.

Moreover, a simple inspection of the formulas we used shows that the formulas enforcing kings are the only formulas in which quantification in some subformulas with two variables is not guarded.

Thus, in the current scenario, we can use the proof for $\mbox{\rm TGF}_{1}$ with only some minor changes: define bits using constants, replace existentially quantified variables of (4) and (11) by constants, and remove formula (7). This formula is not necessary, since the existence of a tape cell scanned by the head in every configuration will be enforced by requiring this explicitly in the initial configuration and then appropriately defining moves of the head as in formulas (14)–(16).

For the reader’s convenience we reproduce all the formulas with all the required modifications below.

Formulas (2)–(3) are replaced by:

[TABLE]

Formula (4) is replaced by:

[TABLE]

Formula (5) is retained:

[TABLE]

Formula (7) is completely removed. Formulas (8)–(10) are retained:

[TABLE]

Formula (11) is replaced by:

[TABLE]

Formula (12) is retained;

[TABLE]

Formulas (13)–(18) are retained:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

D.2 2-NExpTime-lower bound for TGF1 with constants

Our aim is now to define a doubly exponential toroidal grid, which can then serve to encode a doubly exponential tiling problem defined similarly as in Appendix B. This time, given a number $n\in{\mathbb{N}}$ written in unary, and a tiling system $\mathcal{T}$, the problem is to verify if $\mathcal{T}$ has a tiling of the grid ${\mathfrak{G}}_{m}$, where $m=2^{2^{n}}$. It is well known that the doubly exponential tiling problem is $2\textsc{-NExpTime}$-complete.

As in the previous proof we use two constants $c_{0}$ and $c_{1}$, whose interpretations will be, as usually, called bits, or just zero and one. For unary predicates $O$ and $Z$ we say:

[TABLE]

We introduce a predicate $G$ of arity $2+2n$, which will be made true for all tuples consisting of two arbitrary elements of a model followed by $2n$ bits. Once more we use the trick similar to the one used to create the relation $C$ in the proof of Thm. 4.1 (i). We first say that, for any $0\leq i<2n$, $G$ holds for some tuple consisting of $i$ ones and $2n-i$ zeros and then propagate $G$ to all relevant tuples.

[TABLE]

[TABLE]

The predicate $G$ can be used as a guard for any formula using two variables intended to be interpreted as two arbitrary elements and up to $2n$ variables intended to be interpreted as bits. This turns out to be sufficient for our purposes.

It is probably worth commenting that this kind of a ‘universal guard’ cannot be enforced with in $\mbox{\rm TGF}_{1}$ with equality (and thus with the ability of enforcing kings) but without constants. The reason is that kings would need to be quantified in (40) which would lead to a two-dimensional formula.

All the forthcoming formulas can be guarded by $G(x,y,\bar{u},\bar{v})$, $G(x,x,\bar{u},\bar{u})$, $G(x,x,\bar{u},\bar{v})$ or $(x,y,\bar{u},\bar{u})$, if necessary. For brevity, we omit such guards in our exposition.

We endow each element with a pair of coordinates in the range $[0,2^{2^{n}}-1]$, treating tuples of length $n$ consisting of bits as indices of binary digits. We use predicate $B_{H}$ of arity $n+1$ to encode the horizontal coordinate of element $a$. For a sequence of constants $\bar{c}$ of length $n$ we interpret the value of $B_{H}(a,\bar{c})$ as the value of the $c$-th bit of the horizontal coordinate.

Recall our $\lambda^{\scriptscriptstyle+1}$ abbreviation. We use it to prepare ourselves for defining addition of $1$ to horizontal and vertical coordinates (addition in the range $[0,\ldots,2^{2^{n}}-1]$). To this end we divide positions of coordinates into $Pivot$ (the least significant [math]), $Tail$ (positions to the right from the $Pivot$) and $Head$ (positions to the left from the $Pivot$).

[TABLE]

We proceed analogously for vertical coordinates, using predicates $Tail_{V}$, $Pivot_{V}$, $Head_{V}$, and $B_{V}$.

We enforce the existence of the origo, and a horizontal and a vertical neighbour of each element.

[TABLE]

We now take care of the coordinates of the neighbouring elements. We say that the horizontal coordinates of elements connected by $H$ differs by one.

[TABLE]

We proceed analogously with vertical coordinates of elements connected by $V$.

We next connect any pair of elements with the same vertical and horizontal coordinates by binary predicate $Equal$. To this end we introduce an auxiliary predicate $EqUpTo_{H}$.

[TABLE]

[TABLE]

Analogously we introduce $EqUpTo_{V}$, and write the advertised formula defining equality of the coordinates.

[TABLE]

Having such formulas we can now easily encode an instance of the doubly exponential tiling problem. In particular, the predicate $Equal$ may be used to say that two elements having the same horizontal and vertical coordinates are tiled identically. We omit the routine details.