# A Sequent Calculus for a Modal Logic on Finite Data Trees

David Baelde, Simon Lunel, Sylvain Schmitz

► To cite this version:

David Baelde, Simon Lunel, Sylvain Schmitz. A Sequent Calculus for a Modal Logic on Finite Data Trees. CSL 2016, Sep 2016, Marseille, France. pp.1–16, 10.4230/LIPIcs.CSL.2016.32. hal-01191172v2

HAL Id: hal-01191172

https://inria.hal.science/hal-01191172v2

Submitted on 7 Sep 2015

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License
# A Sequent Calculus for a Modal Logic on Finite Data Trees*

David Baelde, Simon Lunel, and Sylvain Schmitz

LSV, ENS Cachan & CNRS & Inria, France

## Abstract

We investigate the proof theory of a modal fragment of XPath equipped with data (in)equality tests over finite data trees, i.e. over finite unranked trees where nodes are labelled with both a symbol from a finite alphabet and a single data value from an infinite domain. We present a sound and complete sequent calculus for this logic, which yields the optimal PSPACE complexity bound for its validity problem.

**1998 ACM Subject Classification** F.2.2 Nonnumerical Algorithms and Problems (*Complexity of proof procedures*), F.4.1 Mathematical Logic (*Modal logic*), H.2.3 Languages (*Query languages*)

**Keywords and phrases** XPath, proof systems, modal logic, complexity

## 1 Introduction

Arguably the most widespread language for querying XML documents, XPath allows to select and extract elements and values from XML documents. It is embedded in the XSLT and XQuery languages and implemented through libraries in many general-purpose programming languages. The language in its successive revisions has evolved into a full-fledged programming language [18], but its distinguishing feature remains a navigational core (known as **CoreXPath** [2]) supplemented with the ability to perform data joins—this is captured in the fragment dubbed **CoreDataXPath** in [6].

Static analysis of XPath queries, typically inclusion or equivalence checks between queries, can be performed formally through the *validity problem*—or equivalently, for those XPath fragments with negation, through the satisfiability problem. In the data-oblivious case, satisfiability is decidable for **CoreXPath** even in the presence of DTDs [4]. The data-aware version **CoreDataXPath** however turns out to be undecidable [3], which has initiated a quest for decidable fragments and variants [6, 14, 13, 10, 11, 12]—often with prohibitively high complexities. This line of work relies on model-theoretic reasoning, and quite often on the development of ad-hoc models of data automata tailored to capture the fragment at hand.

In this paper, we explore a different avenue, namely the usage of proof systems to reason about XPath queries. In the case of the data-oblivious **CoreXPath**, there is already an extensive literature on Hilbert-style axiomatisations of fragments [3, 21] and extensions with XPath 2.0 features [19]. By contrast, in this work we do not focus on the navigational aspects of XPath, but rather on understanding how to handle data tests through proof systems. Furthermore, while Hilbert-style axiomatisations provide purely syntactic rules to check the validity of formulæ, decidability and complexity results are rather derived from Gentzen-style sequent calculi or from tableaux systems, and we choose to work with the former.

<figure><img src="image_2.png" /></figure>

<footnote>* Work partially funded by the Leverhulme Trust visiting professorship VP1-2014-041 and the ANR grant ANR-14-CE28-0005 PRODAQ. Part of this research was conducted while the second and third authors were visiting the University of Warwick, UK.</footnote>
More precisely, we present a sound and complete cut-free sequent calculus for a fragment of **CoreDataXPath**. For this first attempt at a proof system for a data-aware logic, we work in a somewhat simplified setting:

- our models are finite *data trees* rather than XML trees: these are ordered, unranked trees where each node carries exactly one datum from some infinite data domain $\mathbb{D}$ in addition to a label from some finite alphabet, and

- we strip **CoreDataXPath**'s navigational capabilities down to a simple *modal data logic DataGL* where the usual `□` modality is refined into two data-aware modalities: $□=$ relates the current position to strict descendants labelled with the same data value, while $□ \ne$ relates it to positions with a different data value (see Section 2).

Our logic **DataGL** is a fragment of **CoreDataXPath**($\downarrow^+$), where navigation is restricted to the strict descendant axis $\downarrow^+$ [see 11]. As already noted by ten Cate, Fontaine, and Litak [20], the similarly defined data-oblivious **CoreXPath**($\downarrow^+$) corresponds naturally to the *provability logic GL* (named after Gödel and Löb). Although **GL** was originally intended to model provability in arithmetic, it is best understood for our purpose as the modal logic of finite trees: its set of axioms is sound and weakly complete for well-founded transitive frames [e.g. 5, Chapter 4, where the logic is called **KL**]. By the same token, **DataGL** can be seen as the data-aware extension of **GL**.

Our calculus, defined and shown sound and complete with respect to finite data trees in Section 3, builds upon an existing sequent calculus for **GL** defined by Avron [1]. We found nonetheless that dealing with $□ \ne$ modalities brought significant new challenges—both when enforcing well-foundedness and when dealing with the non-transitivity of the associated ‘descendant with different data’ relation—, which we tackle by introducing so-called *histories* in the calculus.

Among the benefits of our calculus, we exhibit a complete proof search strategy in Section 4, and we show that this strategy works in PSPACE in Section 4.3. This is an improvement over the much more general upper bound shown by Figueira [11, Theorem 6.4] for the EXP-complete **CoreDataXPath**($\downarrow^+$), and matches the PSPACE-hardness of **GL** in the data-oblivious case [e.g. 8, Theorem 7]—thus in **GL**, data can be added for free! Although there might be simpler ways to prove the PSPACE-completeness of **DataGL**, this shows that proof-theoretic methods do not necessarily come at the expense of algorithmic efficiency.

## 2 Modal Logic on Finite Data Trees

We introduce in this section **DataGL**, a bimodal logic (see Section 2.2) defined over *finite data trees* (recalled first in Section 2.1). The logic **DataGL** has however a natural, equivalent formulation in terms of finite transitive irreflexive *data Kripke structures*, as shown in Section 2.2.3, allowing to reuse the tool set of modal logic.

### 2.1 Data Trees

A finite (ordered and unranked) *tree* $t$ over an alphabet $A$ is a partial function from *positions* $w$ in $N^*$ (i.e. finite sequences of non-negative integers) to $A$, with a finite non-empty domain $dom t$, which is furthermore

**prefix-closed:** if $wv \in dom t$ for some $w, v \in N^*$, then $w \in dom t$, and

**predecessor-closed:** if $w(i+1) \in dom t$ for some $w \in N^*$ and $i \in N$, then $wi \in dom t$.
<figure><img src="image_3.png" /><figcaption>Figure 1 A finite data tree over $\Sigma \stackrel{\text{def}}{=} \{a, b\}$ and $\mathbb{D} \stackrel{\text{def}}{=} \mathbb{N}$. The $R_=$ relation is indicated through dashed orange arcs, and the $R_\neq$ relation through dotted red arcs.</figcaption></figure>

Call the length $|w|$ the height of position $w$. The maximal such height $h(t) \stackrel{\text{def}}{=} \max_{w \in \text{dom } t} |w|$ is called the height of $t$; this is well-defined since $\text{dom } t$ is finite. The root of a tree $t$ is then denoted by the empty sequence $\varepsilon$, with height 0.

Let $\Sigma$ be a finite set of tags and $\mathbb{D}$ an infinite countable set of data values. A finite data tree is a finite tree over the Cartesian product $\Sigma \times \mathbb{D}$; see Figure 1 for an example. For a position $w$ in $\text{dom } t$, we write $\ell(w)$ for its tag in $\Sigma$ and $d(w)$ for its datum in $\mathbb{D}$; then $t(w) = (\ell(w), d(w))$. Given a data tree $t$, its strict descendant relation $R \stackrel{\text{def}}{=} \{(w, wv) \in \text{dom } t \times \text{dom } t \mid v \in \mathbb{N}^+\}$ between its positions can be partitioned into $R = R_= \uplus R_\neq$ by defining

$$R_\text{=} \stackrel{\text{def}}{=} \{(w, w') \in R \mid d(w) = d(w')\}, \quad R_\neq \stackrel{\text{def}}{=} \{(w, w') \in R \mid d(w) \neq d(w')\}. \quad (1)$$

It is worth noting that $R_=$ is transitive, but $R_\neq$ is not—as seen for instance on the leftmost branch of the tree in Figure 1—; however, $w R_\neq w' R_=$ $w''$ or $w R_=$ $w' R_\neq w''$ implies $w R_\neq w''$, a fact we dub cross transitivity—see for instance the rightmost branch of the tree in Figure 1.

## 2.2 Modal Data Logic

### 2.2.1 Syntax

Our modal data logic **DataGL** is syntactically a modal logic with two modal operators, namely $\Box_=$ and $\Box_\neq$. Given a countable set $A$ of atomic propositions, its set of formulæ is defined by the abstract syntax

$$\varphi ::= \bot | p | \varphi \supset \varphi | \Box_=\varphi | \Box_\neq\varphi$$

where $p$ ranges over $A$. The usual Boolean connectives can be defined by $\neg\varphi \stackrel{\text{def}}{=} \varphi \supset \bot$, $\top \stackrel{\text{def}}{=} \neg\bot$, $\varphi \vee\psi \stackrel{\text{def}}{=} (\neg\varphi) \supset \psi$, $\varphi \wedge\psi \stackrel{\text{def}}{=} \neg(\neg\varphi \vee\neg\psi)$, and the diamonds by $\Diamond_=\varphi \stackrel{\text{def}}{=} \neg\Box_=\neg\varphi$ and $\Diamond_\neq\varphi \stackrel{\text{def}}{=} \neg\Box_\neq\neg\varphi$; finally the usual box and diamond are defined through $\Box\varphi \stackrel{\text{def}}{=} \Box_=\varphi \wedge \Box_\neq\varphi$ and $\Diamond\varphi \stackrel{\text{def}}{=} \neg\Box\neg\varphi$. Importantly, $\Diamond_=$ and $\Box_\neq$ are not dual, nor are $\Diamond_\neq$ and $\Box_=$.

### 2.2.2 Semantics

Given a finite data tree $t$ and a position $w \in \text{dom } t$, we inductively define a **DataGL** formula $\varphi$ to be satisfied in $t$ at $w$, denoted $t, w \models \varphi$, as usual:

<table><tr><td>t, w</td><td>$\models \bot$</td><td>never</td></tr><tr><td>t, w</td><td>$\models p$</td><td>iff $p \in \ell(w)$</td></tr><tr><td>t, w</td><td>$\models \varphi \supset \psi$</td><td>iff $t, w \models \varphi$ implies $t, w \models \psi$</td></tr><tr><td>t, w</td><td>$\models \Box_=\varphi$</td><td>iff $\forall w' . w R_=$ $w'$ implies $t, w' \models \varphi$</td></tr><tr><td>t, w</td><td>$\models \Box_\neq\varphi$</td><td>iff $\forall w' . w R_\neq w'$ implies $t, w' \models \varphi$</td></tr></table>

The logic **DataGL** is a fragment of **XPath**: when naming `@d` the unique data attribute of data trees, in concrete **XPath** syntax, $\Diamond_\neq\varphi$ could for instance be expressed as the node
<figure><img src="image_4.png" /><figcaption>(a) A counter-model to (2).</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>(b) An infinite counter-model to (3).</figcaption></figure>

Figure 2 Counter-models to formulæ (2) and (3), where $\varphi \stackrel{\text{def}}{=} p$, $\Sigma \stackrel{\text{def}}{=} \{\emptyset, \{p\}\}$, and $\mathbb{D} \stackrel{\text{def}}{=} \mathbb{N}$.

test [./@d != ./descendant::*[χ]/@d] assuming χ is the XPath translation of ϕ. More precisely, we only need the union-free fragment of CoreDataXPath$^{ε}(↓^+)$ as defined by Figueira [11]. See Appendix B for a succinct comparison between DataGL and XPath.

A formula $\varphi$ is satisfiable if there exists a finite data tree $t$ and a position $w$ in dom $t$ such that $t, w \models \varphi$. It is valid if for all finite data trees $t$ and positions $w$ in dom $t$, $t, w \models \varphi$; observe that $\varphi$ is valid if and only if $\neg \varphi$ is not satisfiable, and that we can assume $w = \varepsilon$ without loss of generality by extracting the subtree of $t$ rooted by $w$. Note that for validity or satisfiability questions, we can assume $A$ to be the finite set of atomic propositions appearing in $\varphi$, and work with the tag set $\Sigma \stackrel{\text{def}}{=} 2^A$.

**Example 1 (Löb's Axiom).** Consider the following formula, known as Löb's axiom:

$$ \Box(\Box\varphi \supset \varphi) \supset \Box\varphi, \qquad (\mathbf{L}) $$

which can be viewed as an induction scheme over the depth of a node: to prove that $\varphi$ holds at any node, it suffices to establish that it holds at every node assuming that it holds at deeper nodes. Since we are working on finite data trees, $\mathbf{L}$ is valid: for any finite data tree $t$ and any position $w$ in dom $t$, we can show that $t, w \models \mathbf{L}$. Indeed, if we assume $t, w \models \Box(\Box\varphi \supset \varphi)$, then by induction over $h(t) - |w'|$, if $w R w'$ then $t, w' \models \varphi$: this holds for any leaf $w'$, since then $t, w' \models \Box\varphi$ vacuously, and thus $t, w' \models \varphi$; and for an inner node $w'$, by transitivity of $\mathbf{R}$ all its strict descendants are also strict descendants of $w$, thus by induction hypothesis they satisfy $\varphi$, hence $t, w' \models \Box\varphi$ and therefore $t, w' \models \varphi$ as desired.

**Example 2.** Due to the non-transitivity of $R_\neq$, the following variant of $\mathbf{L}$ is not valid:

$$ \Box_{\neq}(\Box_{\neq}\varphi \supset \varphi) \supset \Box_{\neq}\varphi. \qquad (2) $$

A counter-model is depicted in Figure 2a in the case $\varphi \stackrel{\text{def}}{=} p$. Observe that $t, \varepsilon \not\models \Box_{\neq} p$ due to the middle node. Furthermore, $t, \varepsilon \models \Box_{\neq}(\Box_{\neq} p \supset p)$: the only node related to the root through $R_\neq$ is the middle node, and it satisfies $\Box_{\neq} p \supset p$ because it does not satisfy $\Box_{\neq} p$: indeed, the bottom node does not satisfy $p$.

**Example 3.** The following, more involved formula is also valid over finite data trees:

$$ \Box_{\neq}(\varphi \vee \Diamond_{=\top}) \supset \Diamond_{\neq}\varphi \vee \Box_{\neq}\bot. \qquad (3) $$

Its validity relies on the finiteness assumption, and on the interplay between $\Box_{=}$ and $\Box_{\neq}$. Indeed, assume for the sake of contradiction that $t, w \models \Box_{\neq}(\varphi \vee \Diamond_{=\top})$ but $t, w \not\models \Diamond_{\neq}\varphi$ and $t, w \not\models \Box_{\neq}\bot$, for some finite data tree $t$ and position $w$. Then there exists some $w_0$ in dom $t$ with $w R_\neq w_0$, and $t, w_0 \not\models \varphi$. Necessarily, $t, w_0 \models \Diamond_{=\top}$: there exists $w_1$ in dom $t$ such that $w_0 R_\neq w_1$. By cross transitivity, $w R_\neq w_1$, and we can apply the same reasoning to $w_1$: there
exists $w_2$ in dom $t$ such that $w_1 R_= w_2$, thus by transitivity of $R_=$ and cross transitivity, $w R_\neq w_2$, and so on and so forth. Hence there exists an infinite chain $w_0 R_= w_1 R_=$ \dots of positions in $t$, which contradicts its finiteness.

Note that the previous argument describes a counter-model to (3) if we were to allow infinite data trees as models instead of only finite ones; see a counter-model in Figure 2b.

### 2.2.3 Data Kripke Structures

The data tree semantics of **DataGL** are actually a particular case of its semantics in terms of data Kripke structures. Such a structure is a tuple $\mathfrak{M} = (W, R, d, \ell)$ where $W$ is a set of worlds, $R$ is a binary relation over $W$, $d: W \to \mathbb{D}$ is a data labelling, and $\ell: W \to 2^A$ is a labelling using atomic propositions. Observe that a data tree $t$ defines such a structure with $W \stackrel{\text{def}}{=} \text{dom } t$.

Given a data Kripke structure $\mathfrak{M}$, the relation $R$ can be partitioned as $R = R_\= \uplus R_\neq$ as in Equation (1), allowing to define the satisfaction relation $\mathfrak{M}, w \models \varphi$ exactly as in the case of data trees. Working with Kripke structures and the modal similarity type $\{\Diamond_=, \Diamond_\neq\}$ allows to readily apply the basic model-theoretic constructions of modal logic: satisfaction is invariant under e.g. *generated submodels* [5, Definition 2.5 and Proposition 2.6], *bounded morphisms* [5, Definition 2.12 and Proposition 2.14], and *bisimulations* [5, Definition 2.18 and Theorem 2.20].

We call a data Kripke structure a **DataGL model** if $R$ is transitive irreflexive and $W$ is finite. Given a root world $w_0$, the *height* of a world $w$ is the length $n$ of the maximal chain $w_0 R w_1 R \cdots R w_n = w$ from $w_0$ to $w$, and the *height* of $\mathfrak{M}$ the maximal height of its worlds. The semantics in terms of **DataGL** models is equivalent to that in terms of finite data trees: this is essentially due to the *tree-model property* of modal logic [see e.g. 5, Proposition 2.15], and proven via unfolding (see Appendix A for details):

**Proposition 4 (Tree-Model Property).** For any **DataGL** model $\mathfrak{M}$ and world $w_0$, there exists a finite data tree $t_{\mathfrak{M}}$ of the same height and a surjective bounded morphism $f$ from $t_{\mathfrak{M}}$ to $\mathfrak{M}$ with $f(\varepsilon) = w_0$. Hence, for all **DataGL** formulæ $\varphi$ and positions $w$ in dom $t_{\mathfrak{M}}$, $t_{\mathfrak{M}}, w \models \varphi$ if and only if $\mathfrak{M}, f(w) \models \varphi$.

Since a finite data tree is a particular case of a **DataGL** model, Proposition 4 means that finite data trees and **DataGL** models can be used indifferently.

## 3 Sequent Calculus

Developing sequent calculi for modal logics is often arduous. In order to obtain modular proof systems enjoying both cut elimination and a form of subformula property—which are desirable in order to show decidability—, advanced techniques are typically required: display logic [22], labelled calculi [16], nested sequents [7], or tree-hypersequents [17] to name a few. All these are motivated by the need to maintain additional information throughout proofs, using extra-logical means. As we are going to see, we also introduce a form of enriched sequents for **DataGL**, in the form of *histories*. We define our calculus in Section 3.2, and prove it sound and complete in Sections 3.3 and 3.4. But first we present our main source of inspiration: Avron's sequent calculus for **GL** [1].

### 3.1 Avron's Sequent Calculus for GL

Our sequent calculus for **DataGL** is inspired by the work of Avron [1] who gave a sound and complete sequent calculus for **GL**, which does not require any extra-logical apparatus.
In addition to the usual rules for Boolean connectives, Avron proposed the following sequent calculus rule (□) to deal with modalities in GL (the principal formula is coloured in orange):

$$ \frac{\Box\Gamma, \Gamma, \Box\varphi \vdash \varphi}{\Box\Gamma \vdash \Box\varphi} \Box $$

As usual in classical sequent calculus, a sequent $\Gamma \vdash \Delta$ is made of two sets of formulæ $\Gamma$ (the antecedents) and $\Delta$ (the consequents) and should be interpreted as $\bigwedge_{\varphi \in \Gamma} \varphi \supset \bigvee_{\psi \in \Delta} \psi$. We simply use commas to denote set union. The notation $\Box\Gamma$ stands for the set of all $\Box\varphi$ formulæ for $\varphi \in \Gamma$, and later $\Box=\Gamma$ will denote the set $\{\Box=\varphi | \varphi \in \Gamma\}$, and similarly for $\Box\neq$. A rule consists of a set of premises (the top sequents) along with a single conclusion (the bottom sequent). A sequent $S$ is derivable from a set of sequents $X$ if there exists a derivation with $S$ as root and $X$ as set of open leaves; a sequent is provable if it is derivable from the empty set, or equivalently if has a proof, i.e. a derivation with no open leaves.

When $\Gamma$ is empty, Avron's rule follows immediately from the L axiom: if we can prove $\Box\varphi \supset \varphi$, then we also have $\Box(\Box\varphi \supset \varphi)$ by necessitation, and $\Box\varphi$ follows by L. When $\Gamma$ is not empty, the rule exploits the properties of $\Box$ in order to extract information from the antecedents in the conclusion sequent. Reading the rule bottom-up, the idea is that since we are assuming $\Box\Gamma$, then surely we can assume $\Gamma$ for any strict descendant where $\varphi$ holds, but also $\Box\Gamma$ since our relation $R$ is transitive.

**► Example 5 (Proof of L in Avron's Calculus).** The L axiom can be proven valid using (□) and the classical rules (see Figure 3 for the variants we will use later; we colour again principal formulæ in orange):

$$ \frac{\frac{\Box(\Box\varphi \supset \varphi), \Box\varphi \vdash \Box\varphi, \varphi}{\Box(\Box\varphi \supset \varphi), \Box\varphi, \varphi \vdash \varphi} \quad \text{ax} \quad \Box\varphi \supset \varphi}{\Box(\Box\varphi \supset \varphi), \Box\varphi, \Box\varphi \supset \varphi \vdash \varphi} \quad \text{ax} \quad \Box \supset \Box\varphi \supset \varphi} \supset L \quad \Box \supset \Box\varphi \supset \varphi \supset \Box \supset R $$

Note that the left branch of the proof could not be closed without the addition of $\Box\varphi$ among the antecedents of the premise of (□).

The idea behind the rule (□) applies immediately to our $\Box=\text{modality}$ since $R=\text{is also transitive and well-founded.}$ However, the $\Box\neq\text{modality}$ cannot be handled in the same way because $R\neq\text{is not transitive.}$ A sound rule for $\Box\neq\text{would be:}$

$$ \frac{\Box=\Gamma\neq, \Gamma\neq \vdash \varphi}{\Box=\Gamma=, \Box\neq\Gamma\neq \vdash \Box\neq\varphi} $$

There is however no hope for this rule to yield a complete calculus. First, it fails to use in a significant way the assumptions $\Box=\Gamma=$. When we consider a strict descendant in the premise, we have forgotten about the position from which we came, and so we will never be able to tell when we reach a further descendant with the same datum, whether $\Gamma=$ should hold. Second, it does not enforce tree finiteness. In that respect, note that adding an assumption $\Box\neq\varphi$ to the antecedents of the top sequent (naively mimicking the (□) rule) would yield an unsound rule. Both issues are solved in the following by enriching the structure of our sequents.

## 3.2 Sequent Calculus for DataGL

Our calculus employs sequents enriched with a history: those are sequences $\mathcal{H} = H_1; \dots; H_n$ of sets of modal formulæ $H_i = \Box=H_i^=, \Box\neq H_i^{\neq}$ called its cells. The length of a history $\mathcal{H}$ is
$$ \frac{\overline{\mathcal{H}; \Gamma, \perp \vdash \Delta} \perp_L}{\mathcal{H}; \Gamma, \varphi \supset \psi \vdash \varphi, \Delta} \quad \overline{\mathcal{H}; \Gamma, \varphi \vdash \varphi, \Delta}^{\text{ax}} \quad \frac{\mathcal{H}; \Gamma, \varphi \supset \psi, \Delta}{\mathcal{H}; \Gamma, \varphi \supset \psi \vdash \Delta} \supset_L \quad \frac{\mathcal{H}; \Gamma, \varphi \vdash \varphi \supset \psi, \Delta}{\mathcal{H}; \Gamma \vdash \varphi \supset \psi, \Delta} \supset_R $$

■ **Figure 3** Sequent calculus for **DataGL**: classical sequent calculus rules. The principal formulæ are coloured in orange in the conclusions of the rules. The greyed formulæ $\varphi \supset \psi$ in the premises of $(\supset_L)$ and $(\supset_R)$ can be omitted; we do not use them in examples to reduce clutter.

denoted by $|\mathcal{H}|$. Given an history $\mathcal{H}$ and $1 \le i \le |\mathcal{H}|$, we always write $H_i$ for its $i$th cell and $H_i^=, H_i^{\ne}$ for the sets such that $H_i = \square_=H_i^=, \square_{\ne}H_i^{\ne}$. If $\mathcal{H}$ is a history and $H_i$ one of its cells, we write $\mathcal{H} \setminus H_i$ for the history obtained by removing $H_i$, i.e. for $H_1; \dots; H_{i-1}; H_{i+1}; \dots; H_{|\mathcal{H}|}$. The sequent calculus for **DataGL** deals with sequents of the form $\mathcal{H}; \Gamma \vdash \Delta$ where $\Gamma$ and $\Delta$ are sets of formulæ and $\mathcal{H}$ is a history. Its rules are given in Figures 3 and 4. The calculus enjoys several desirable properties, namely that it does not contain a 'cut' rule, and that it has the subformula property: in any rule, the formulæ found in the premises are subformulæ of those found in the conclusion.

### 3.2.1 Boolean Formulæ

The rules of Figure 3 for the Boolean connectives are not surprising: the history plays no role in these rules, and when we ignore it we recover the usual sequent calculus rules for propositional classical logic. These rules are formulated in a way that avoids explicitly considering the structural rules of contraction and weakening. Note that in rules $(\supset_L)$ and $(\supset_R)$ we have chosen to keep the principal formula $\varphi \supset \psi$ in the premises of the rule (in grey in Figure 3)—this is an inessential choice that simplifies the completeness argument later, in particular Lemma 11. In fact, weakening is admissible in the calculus (meaning that adding the weakening rules does not change the set of provable sequents; see Appendix C), which means that the rules without the greyed formulæ are also admissible:

► **Lemma 6** (Admissibility of Weakening). The following rules are admissible:

$$ \frac{\mathcal{H}; \Gamma \vdash \Delta}{\mathcal{H}; \Gamma, \varphi \vdash \Delta} W_L \qquad \frac{\mathcal{H}; \Gamma \vdash \Delta}{\mathcal{H}; \Gamma \vdash \Delta, \varphi} W_R $$

### 3.2.2 Modal Formulæ

$$ \frac{\mathcal{H}; \Gamma^=, \Box_=\Gamma^=, \Box_{\ne}\Gamma^{\ne}, \{H_i^{\ne}\}_{1\le i \le |\mathcal{H}|}, \Box_=\varphi \vdash \varphi}{\mathcal{H}; \Gamma, \Box_=\Gamma^=, \Box_{\ne}\Gamma^{\ne} \vdash \Box_=\varphi, \Delta} \Box_= \\ \frac{\mathcal{H}; (\Box_=\Gamma^=, \Box_{\ne}\Gamma^{\ne}, \Box_{\ne}\varphi); (\Gamma^{\ne}, \{H_i^{\ne}\}_{1\le i \le |\mathcal{H}|}) \vdash \varphi}{\{ \mathcal{H} \setminus H_j; (\Box_=\Gamma^=, \Box_{\ne}\Gamma^{\ne}, \Box_{\ne}\varphi); (\Gamma^{\ne}, \{H_i^{\ne}\}_{1\le i \le |\mathcal{H}|, i \ne j}, H_j^=, H_j) \vdash \varphi \}_{1\le j \le |\mathcal{H}|}} \Box_{\ne} \\ \frac{\mathcal{H}; \Gamma, \Box_=\Gamma^=, \Box_{\ne}\Gamma^{\ne} \vdash \Box_{\ne}\varphi, \Delta}{\mathcal{H}; \Gamma, \Box_=\Gamma^=, \Box_{\ne}\Gamma^{\ne} \vdash \Box_{\ne}\varphi, \Delta} \Box_{\ne} $$

■ **Figure 4** Sequent calculus for **DataGL**: modal rules. The principal formulæ are coloured in orange in the conclusions of the rules.
Before defining formally the semantics of our sequents, let us first provide an intuition for the complex rules of Figure 4 by presenting them informally from a proof search viewpoint.

Applying a modal rule bottom-up amounts to proving a sequent by considering all the possible descendants of a current (hypothetical) position in a data tree. In Avron's calculus all the important information about the current position (i.e. the modal antecedents of the conclusion sequent) could be transferred to the descendant as modal antecedents of the premise. In our case, this transfer is performed through the history. Intuitively, the history keeps track of which previous (hypothetical) positions have been visited, and of which modal formulæ were known to hold at these positions. For the same reason that Avron did not need a history, we do not need to remember past positions labelled with the same data as the current position. In fact, we only need to consider past positions labelled with mutually distinct data values: one value for the current position and one for each history cell—these values do not actually show up in the calculus, because its purpose is to establish the validity of a sequent, i.e. it simultaneously considers all possible data assignments.

The (□=) rule is similar to Avron's rule, but also extracts information from the history: when we move to a strict descendant position with the same data value, it remains different from the data values of the past positions associated to history cells, and thus we know that all the $H_i^\ddagger$ formulæ hold at the new position. (Also note that this rule allows to weaken formulæ, namely the parts Γ and Δ of the conclusion sequent; this is, again, to avoid considering explicit structural rules.)

The (□_‡) rule is the most complex one, as it not only extracts information from the history but also updates it. When moving to a strict descendant with a different data, the new data may or may not be different from the data of the previously visited positions in the history, leading to |H| + 1 premises:

- The first premise of the (□_‡) rule covers the case of a totally fresh data value. In that case, we know that all the $H_i^\ddagger$ formulæ hold at the new position. We also update the history with a new cell corresponding to the position that we just left. Unsurprisingly, this cell contains the modal formulæ that were assumed about that position. It also contains □_‡φ as a way of enforcing the well-foundedness of □_‡.

- Each of the remaining premises corresponds to the case where the new position has the same data as the position corresponding to history cell $H_j$. In such a case, the formulæ in $H_j^\ddagger$ are not known to hold at the new position. Instead, $H_j^\ddagger$ holds, as well as $H_j$ itself, and thus there is no point in keeping a history cell for the past occurrence of the new data. As in the previous case, the history is updated with a new cell corresponding to the position we just left.

**Example 7.** Let us consider again the invalid formula (2) from Example 2. Since our calculus is sound (see Theorem 9), proof search ought to fail for this formula. The first steps up to the first application of the (□_‡) rule are:

$$ \frac{\frac{\Box \neq (\Box \neq \varphi \supset \varphi), \Box \neq \varphi; \Box \neq \varphi \supset \varphi \vdash \varphi}{\Box \neq (\Box \neq \varphi \supset \varphi) \vdash \Box \neq \varphi} \quad \Box \neq}{\vdash \Box \neq (\Box \neq \varphi \supset \varphi) \supset \Box \neq \varphi} \supset_R $$

This creates a first history cell $H_1 \stackrel{\text{def}}{=} \Box_\neq (\Box_\neq \varphi \supset \varphi)$, □_‡φ combining the modal formulæ of the antecedent and the principal formula. Soon after, proof search fails:

$$ \frac{\frac{\begin{array}{c} \text{ax} \\ H_1; \Box \neq \varphi; \Box \neq \varphi \supset \varphi, \varphi \vdash \varphi \end{array}}{\begin{array}{c} \text{ax} \\ H_1; \vdash \Box \neq \varphi, \varphi \end{array}} \text{no applicable rule} \qquad \frac{\begin{array}{c} \Box \neq \varphi; \Box \neq (\Box \neq \varphi \supset \varphi), \Box \neq \varphi \vdash \varphi \\ H_1; \varphi \vdash \varphi \end{array}}{H_1; \Box \neq \varphi \supset \varphi \vdash \varphi} \supset_L $$
This second application of (□_‡) to H₁; ⊢ □_‡ϕ, ϕ, creates a new history cell H₂ ≝_def □_‡ϕ, and has two premises: the first, which assumes a fresh data, copies the formulæ under □_‡ from H₁ into the antecedent; the second assumes we have encountered the same data value as in the position remembered through H₁, thus copies the formulæ under □_= in H₁ (there are none) into the antecedent, but also extracts H₁ itself from the history and puts it in the antecedent. Note that this search was deterministic: there were never any alternative applicable rule, hence formula (2) is unprovable. We present more examples in Appendix C.

## 3.3 Soundness

We now formally define the semantics of our sequents, and establish that the calculus is sound. An annotated sequent is a sequent H; Γ ⊢ Δ together with a data assignment d, which is an injective function from {0, ..., |H|} to D. We write d₀, ..., d|H| for those distinct data values: the data value d₀ is understood as being associated to the bare sequent Γ ⊢ Δ, while each dᵢ for 0 < i ≤ |H| is associated to the cell Hᵢ.

**► Definition 8 (Sequent Satisfiability and Validity).** A finite data tree t satisfies an annotated sequent H; Γ ⊢ Δ at a position w in dom t if and only if the following conditions together imply t, w |= ϕ for some ϕ ∈ Δ:

a. t, w |= ϕ for all ϕ ∈ Γ,

b. d(w) = d₀,

c. t, w' |= ϕ for all 1 ≤ i ≤ |H|, all □_=ϕ ∈ Hᵢ=, and all w' with w R w' and d(w') = dᵢ, and

d. t, w' |= ϕ for all 1 ≤ i ≤ |H|, all □_‡ϕ ∈ Hᵢ‡, and all w' with w R w' and d(w') ≠ dᵢ.

An annotated sequent is valid if and only if it is satisfied by all finite data trees at all positions. A finite data tree t satisfies a sequent S at a position w, written t, w |= S, if it satisfies some annotation of S at w. A sequent is valid if all its annotations are valid.

Note that the validity of one annotation of a sequent is equivalent to the validity of all of its annotations, because any two annotations are related by a bijective renaming of data values, and satisfaction of a formula is invariant under such renamings.

**► Theorem 9 (Soundness).** The sequent calculus for DataGL is sound, i.e. all provable sequents are valid.

**Proof.** It suffices to check that each rule preserves validity, which we only show here for the case of the (□_‡) rule. Considering an instance of that rule in which all premise sequents are valid, let us show that any annotation of the conclusion sequent H; Γ, □_=Γ=, □_‡Γ‡ ⊢ □_‡ϕ, Δ is valid. Let n ≝_def |H|. More precisely, we prove that for any data assignment d, any finite data tree t satisfies the annotated bottom sequent in any position w, by induction on h(t) - |w|. Assuming that t and w satisfy the conditions of Definition 8 for our annotated conclusion sequent, we shall show that t, w |= □_‡ϕ.

Consider a position w' with w R_‡ w'. By induction hypothesis, we know that for any w'' with w' R w'' and w R_‡ w'', t, w'' |= ϕ. We now establish t, w' |= ϕ, by distinguishing two cases:

- Assume d(w') is distinct from all the (dᵢ)₁≤i≤n (it is distinct from d₀ by hypothesis). Then we consider the first premise sequent

$$H; \Box=\Gamma^=, \Box\neq\Gamma^\ddagger, \Box\neq\varphi; \Gamma^\ddagger, \{H_i^\ddagger\}_{1\le i\le n} \vdash \varphi$$

with the data assignment d' defined by d'_i ≝_def dᵢ for 0 < i ≤ n for the cells of H, d'_{n+1} ≝_def d(w) for the newly added history cell, and d'_0 ≝_def d(w') for the current position.
We want to show that $w'$ satisfies the conditions of Definition 8 for that annotated sequent; then $t, w' \models \varphi$ will follow from the validity of the first premise.

- Condition (a) on $\Gamma^\nabla, \{H_i^\nabla\}_{1\le i\le n}$ for $w'$ on the first premise follows from conditions (a) and (d) for $w$ on the conclusion sequent.

- Condition (b) is satisfied by definition of $d'_0$.

- For conditions (c) and (d), it suffices to consider the new history cell $H_{n+1} = \Box=\Gamma^=, \Box\neq\Gamma^\nabla, \Box\neq\varphi$ with data annotation $d'_{n+1} = d(w)$, because $w R w'$ and $w$ already satisfies those conditions for $\mathcal{H}$ with the same data annotation. Regarding $\Box=\Gamma^=$ and $\Box\neq\Gamma^\nabla$, this follows from condition (a) for $w$ on the conclusion sequent. Regarding $\Box\neq\varphi$, by induction hypothesis, any $w''$ with $w R\neq w''$ will satisfy $\varphi$.

- Otherwise, $d(w') = d_j$ for some $1 \le j \le n$. This time we consider the premise sequent

$$ \mathcal{H} \setminus H_j; \Box=\Gamma^=, \Box\neq\Gamma^\nabla, \Box\neq\varphi; \Gamma^\nabla, \{H_i^\nabla\}_{1\le i\le n, i\neq j}, H_j^-, H_j \vdash \varphi $$

such that cell $H_i$ with $i \neq j$ receives data annotation $d_i$, the new cell is assigned $d(w)$ and the current position is assigned $d(w') = d_j$. As before, we can check the conditions of Definition 8 for $w'$ and that annotated sequent. The only interesting new case is condition (a), where $H_j^-$ and $H_j$ need to be satisfied by $w'$, but this follows from condition (c) for $w$ on the conclusion sequent. ◀

## 3.4 Completeness

We now turn to proving that our sequent calculus is complete: $\varphi$ is valid in **DataGL** if and only if $\vdash \varphi$ is provable. We show more generally that our calculus is complete with respect to sequent validity:

**Theorem 10 (Completeness).** *The sequent calculus for DataGL is complete, i.e. all valid sequents are provable.*

This result is obtained by constructing for any invalid sequent an appropriate *canonical* (counter-)model, which is a **DataGL** model. More specifically, we follow Avron [1] in building a model based on unprovable saturated sequents, rather than a model based on saturated sets of formulæ as in the Hilbert-style approach [5]. This is not a minor difference: it allows us to obtain a canonical model that enjoys irreflexivity and well-foundedness, two properties that are not directly obtained in the Hilbert-style approach.

Let us call a sequent $\mathcal{H}; \Gamma \vdash \Delta$ *saturated* if $\psi \supset \varphi \in \Gamma$ implies $\psi \in \Delta$ and $\varphi \in \Gamma$, and $\varphi \supset \psi \in \Delta$ implies $\varphi \in \Gamma$ and $\psi \in \Delta$. We can restrict ourselves to work with saturated sequents without loss of generality:

**Lemma 11 (Saturation Lemma).** *For any unprovable sequent $S = \mathcal{H}; \Gamma \vdash \Delta$ there exists an unprovable sequent $S' = \mathcal{H}; \Gamma' \vdash \Delta'$ using only subformulæ of $S$, which is saturated and such that $\Gamma \subseteq \Gamma'$, $\Delta \subseteq \Delta'$. Furthermore if $t, w \models S$ then $t, w \models S'$.*

**Proof sketch.** The total size of all formulæ for which the saturation condition fails can be decreased by repeatedly applying the rules of Figure 3 bottom-up. This process yields a set of saturated sequents $X$, and a simple inspection of the rules shows that for all the sequents $S'$ in $X$ the formulæ initially present in $\Gamma$ (resp. $\Delta$) are still present, that $S'$ only contains subformulæ of $S$, and that $t, w \models S$ implies $t, w \models S'$. Since $S$ was unprovable, $X$ contains at least one unprovable sequent. ◀

We shall build our canonical model based on annotated saturated sequents. In order to obtain a finite model, we restrict our sequents to only contain (sub)formulæ among a finite
set, and we forbid duplicates in histories. This, in turn, allows us to bound the number of
possible data assignments. In the remainder of this section, let us fix a finite set of formulæ
$\mathcal{F}$ that is closed under taking subformulæ.

**Definition 12 (Canonical Sequents).** A canonical sequent $S = (\mathcal{H}; \Gamma \vdash \Delta)^d$ over $\mathcal{F}$ is an unprovable saturated sequent $\mathcal{H}; \Gamma \vdash \Delta$ such that its formulæ belong to $\mathcal{F}$ and $H_i \neq H_j$ for $1 \le i \neq j \le |\mathcal{H}|$, together with a data assignment $d$ such that $0 \le d_i \le 2^{|\mathcal{F}|}$ for every $0 \le i \le |\mathcal{H}|$.

Since we want to exhibit a counter-model, we can indeed work here with $\mathbb{D} \stackrel{\text{def}}{=} \mathbb{N}$ without loss of generality. Given a finite $\mathcal{F}$, the set $C(\mathcal{F})$ of canonical sequents over $\mathcal{F}$ is also finite.

Given a sequent $S = \mathcal{H}; \Gamma \vdash \Delta$, we note $S_i \stackrel{\text{def}}{=} H_i$ for $1 \le i \le |\mathcal{H}|$ for its history cells and $S_0 \stackrel{\text{def}}{=} \{\Box_\star\varphi \mid \Box_\star\varphi \in \Gamma, \star \in \{=, \ne\}\}$ for the set of modal formulæ found in $\Gamma$.

**Definition 13 (Canonical Relation).** Given two sequents $S = \mathcal{H}; \Gamma \vdash \Delta$ and $S' = \mathcal{H}'; \Gamma' \vdash \Delta'$, $S$ embeds modally into $S'$, written $S \sqsubseteq S'$, if there exists an injective function $f: \{0, \dots, |\mathcal{H}|\} \to \{0, \dots, |\mathcal{H}'|\}$ such that $S_i \subseteq S'_{f(i)}$ for all $0 \le i \le |\mathcal{H}|$.

Given annotations $d$ and $d'$ for $S$ and $S'$, we define $S R^c S'$ to hold whenever $S \sqsubseteq S'$ and

i. for all $0 \le i \le |\mathcal{H}|$, $d_i = d'_{f(i)}$,

ii. $\varphi \in \Gamma'$ whenever $\Box_\varphi \varphi \in S_i$ with $f(i) = 0$,

iii. $\psi \in \Gamma'$ whenever $\Box_\psi \psi \in S_i$ with $f(i) \neq 0$, and

iv. there exists some formula $\Box_\star\varphi \in (\Delta \setminus \Gamma) \cap S'_{f(0)}$ for $\star \in \{=, \ne\}$; that formula is called the witness associated to $S R^c S'$.

**Lemma 14 (Transitivity and Irreflexivity).** The relation $R^c$ is transitive and irreflexive.

**Proof.** Transitivity is obvious for $\sqsubseteq$ and conditions (i–iii). For condition (iv), it comes from the fact that witnesses are propagated by $\sqsubseteq$. Indeed, if $S R^c S' R^c S''$, then the witness $\Box_\star\varphi$ for $S R^c S'$ belongs to $\Delta \setminus \Gamma$ and to $S'_{f(i)}$ such that $d'_i = d_0$. Thus by condition (i) it also belongs to $S''_j$ for $d''_j = d'_i = d_0$. Regarding irreflexivity, if $S R^c S$ then the witness would have to belong to $(\Delta \setminus \Gamma) \cap S'_0$ since $d_0 = d'_0$ (and all other data values are distinct from $d_0$), but that set is empty since $S'_0 = \Gamma$. ◀

**Definition 15 (Canonical Structure).** The canonical structure over $\mathcal{F}$ is the data Kripke structure $\mathcal{C}(\mathcal{F}) \stackrel{\text{def}}{=} (C(\mathcal{F}), R^c, d^c, \ell^c)$ over canonical sequents. The data label of a sequent $S = (\mathcal{H}; \Gamma \vdash \Delta)^d$ is $d^c(S) \stackrel{\text{def}}{=} d_0$ and its propositional label is the set of atomic propositions found in $\Gamma$, i.e. $\ell^c(S) \stackrel{\text{def}}{=} \{p \in A \mid p \in \Gamma\}$.

By Lemma 14 and the finiteness of $\mathcal{C}(\mathcal{F})$, it is a **DataGL** model. Hence Proposition 4 can be invoked to show the existence of a finite data tree satisfying the same sequents. The following lemma shows that $\mathcal{C}(\mathcal{F})$ provides counter-models to validity in the sense of Definition 8:

**Lemma 16 (Falsification Lemma).** For any canonical sequent $S = (\mathcal{H}; \Gamma \vdash \Delta)^d$ we have:

- $\mathcal{C}(\mathcal{F}), S \models \varphi$ for all $\varphi \in \Gamma$;

- $\mathcal{C}(\mathcal{F}), S' \models \varphi$ for all $1 \le i \le |\mathcal{H}|$, all $\Box_\varphi \varphi \in H_i$, and all $S'$ with $S R^c S'$ and $d^c(S') = d_i$;

- $\mathcal{C}(\mathcal{F}), S' \models \varphi$ for all $1 \le i \le |\mathcal{H}|$, all $\Box_\varphi \varphi \in H_i$, and all $S'$ with $S R^c S'$ and $d^c(S') \neq d_i$;

- $\mathcal{C}(\mathcal{F}), S \nvDash \varphi$ for all $\varphi \in \Delta$.

**Proof.** All the clauses are established simultaneously, by structural induction on $\varphi$. We only develop the case of $\Box_\neq\varphi$, which is the most complex one.
$\Box_{\neq} \varphi \in \Gamma$: For any $S' = (\mathcal{H}'; \Gamma' \vdash \Delta')^{d'}$ with $S R_{\neq} S'$, we have $\varphi \in \Gamma'$ by condition (iii) of Definition 13 with $i=0$, and thus $\mathcal{C}(\mathcal{F})$, $S' \models \varphi$ by induction hypothesis. Hence, $\mathcal{C}(\mathcal{F})$, $S' \models \Box_{\neq} \varphi$.

$\Box_{\neq} \varphi \in H_i$: Assume $S R^c S'$ with $d^c(S') \neq d_i$. By condition (iii) of Definition 13 we have $\varphi \in \Gamma'$ and thus by induction hypothesis $\mathcal{C}(\mathcal{F})$, $S' \models \varphi$.

$\Box_{\neq} \varphi \in \Delta$: Our goal is to exhibit a canonical sequent $S'$ with $S R_{\neq}^c S'$ and $\mathcal{C}(\mathcal{F})$, $S' \not\models \varphi$. Rule ($\Box_{\neq}$) applies to our sequent $S$ and, since $S$ is not provable, at least one of its premises is not provable: call it $S^\dagger$.

We first show that $S^\dagger$ cannot have a duplicated history cell. Since this is not the case of $S$ (by definition of a canonical sequent) the duplicate can only come from the new history cell $\Box_{=\Gamma}=, \Box_{\neq}\Gamma^\ddagger, \Box_{\neq}\varphi$, which is equal to some cell $H_i$. If $S^\dagger$ was the first premise of the ($\Box_{\neq}$) rule, then $\varphi$ would belong to the antecedent $\Gamma^\dagger$ of $S^\dagger$ (as part of $H_i^\ddagger$) and thus $S^\dagger$ would be immediately provable by an application of the (ax) rule: contradiction. If $S^\dagger$ was another premise, then the duplicate $H_i$ is not the $j$th cell, and again $\varphi$ would belong to $\Gamma^\dagger$ as part of $H_i^\ddagger$: contradiction again.

Now, applying Lemma 11 to $S^\dagger$, we obtain a saturated sequent $S^\ddagger$ that is unprovable, with the same history as $S^\dagger$, that only uses formulæ in $\mathcal{F}$ since our sequent calculus has the subformula property, and such that $\varphi$ belongs to its consequent $\Delta^\ddagger$.

It remains to annotate $S^\ddagger$ consistently with the data annotation of $S$. Because the length of the history in $S^\dagger$ and $S^\ddagger$ is at most $2^{|\mathcal{F}|}$, this can be done while keeping data values within the range $\{0, \dots, 2^{|\mathcal{F}|}\}$. Let $S'$ be the canonical sequent obtained in this way from $S^\ddagger$. Inspecting the ($\Box_{\neq}$) rule, $S R_{\neq}^c S'$, the witness being $\Box_{\neq} \varphi$ itself. We can then conclude, since by induction hypothesis we have $\mathcal{C}(\mathcal{F})$, $S' \not\models \varphi$. ◀

We can finally establish our result:

**Proof of Theorem 10.** Consider a sequent $\mathcal{H}; \Gamma \vdash \Delta$ that is unprovable. We can assume without loss of generality that it has no duplicate cell, as we can always add dummy formulæ to differentiate between identical cells, without making the sequent provable. Define $\mathcal{F}$ as its set of subformulæ. By Lemma 11 we obtain an unprovable saturated sequent $\mathcal{H}; \Gamma, \Gamma' \vdash \Delta, \Delta'$. By Lemma 16 we have a counter-model of that sequent, which is also a counter-model of $\mathcal{H}; \Gamma \vdash \Delta$. ◀

# 4 Proof Search

In this section we analyse further the structure of our proof system, deriving properties that are useful for proof search. We first discuss a straightforward complete proof search strategy in Section 4.1. In spite of its simplicity, it yields a polynomial bound on the depth of proofs (see Section 4.2) and therefore a PSPACE upper bound on DataGL validity, which is optimal (see Section 4.3).

## 4.1 Proof Search Strategy

Proof search can be understood intuitively as a game between two players Prover and Spoiler with sequents as positions. Given a sequent $S$, Prover first chooses an applicable rule, i.e. a rule whose conclusion matches $S$. Spoiler then chooses the new current sequent among the premises of the rule application. Any player with no possible move loses: Prover if no rule is applicable, and Spoiler if there are no premises, as with rules (ax) and ($\perp_L$); furthermore Spoiler wins if the play is infinite. A sequent is valid if and only if Prover has a winning strategy in this game.
When several rules are applicable, which one should Prover select?

- Clearly, if either (ax) or ($\perp_L$) is applicable, then she should pick it since she wins immediately.

- Furthermore, the rules ($\supset_L$) and ($\supset_R$) are *invertible*, i.e. their premises are provable if and only if their conclusion is provable: one direction is immediate since the premises allow to derive the conclusion, and conversely we can appeal to weakening (recall Lemma 6) to show the provability of the premises from that of the conclusion. An obvious complete proof search strategy is then to apply ($\supset_L$) and ($\supset_R$) eagerly, decomposing any Boolean formula that is not yet decomposed.

- After this phase, the only hope to prove a sequent is to use a modal rule: Prover has to select one principal modal formula on the right of the sequent and apply the corresponding ($\sqsubseteq$) or ($\sqsupsetneq$) rule.

Although the obtained strategy only makes essential choices, it may *a priori* diverge: each application of a modal rule imports new Boolean formulas into the antecedent, which may yield new modal rules, and so on and so forth. It turns out, however, that the 'GL component' of our modal rules allows us to derive a small bound on the length of branches that should be considered in proof search attempts.

## 4.2 Small Proof Property

The depth of a proof $\Pi$ is the maximal number of rule applications in any of its branches, in other words the maximal length of a play in the proof search game. The size of a proof $|\Pi|$ is the total number of rule applications in the proof tree. A proof is minimal if no other proof of its conclusion sequent is of strictly smaller size. Note that a minimal proof must necessarily apply the (ax) and ($\perp_L$) rules as soon as possible; it also cannot decompose twice the same Boolean formula between two applications of a modal rule ($\sqsubseteq$) or ($\sqsupsetneq$). Hence minimal proofs follow the proof search strategy discussed above.

Inspecting the rules of our calculus, it appears that a cell in the history may be displaced, perhaps moved to the antecedent of the sequent, be enriched with new modal formulæ, but can never be lost:

**Lemma 17.** If a sequent $S$ is derivable from a set of sequents $X$, then $S \sqsubseteq S'$ for all $S'$ in $X$.

**Proposition 18 (Bounded ($\sqsupsetneq$) Applications).** Let $\Pi$ be a minimal proof. For any formula $\sqsupsetneq \psi$, all the branches of $\Pi$ contain at most three applications of the ($\sqsupsetneq$) rule with $\sqsupsetneq \psi$ as principal formula.

*Proof.* Let $\Pi$ be a minimal proof of $\mathcal{H}^0; \Gamma^0 \vdash \Delta^0$. Consider a branch of $\Pi$ that contains three applications of $\sqsupsetneq$ on the same formula $\sqsupsetneq \psi$. Let $S^k = (\mathcal{H}^k; \Gamma^k \vdash \Delta^k)_{0 \le k \le B}$ be the (unannotated) sequents along that branch, of length $B$, and let $p < q < r$ be the indices of the conclusion sequents of the three successive applications of ($\sqsupsetneq$) with $\sqsupsetneq \psi$ as principal formula. We shall establish that the axiom rule applies after the third rule application, thus a fourth application is impossible in a minimal proof.

The first application of ($\sqsupsetneq$) with $\sqsupsetneq \psi$ as principal formula introduces (in its premise sequent) a new history cell containing $\sqsupsetneq \psi$. By Lemma 17, for all $k > p$, there exists $0 \le i_k \le |\mathcal{H}^k|$ such that $\sqsupsetneq \psi \in S_{i_k}^k$.

By minimality of $\Pi$ we know that the axiom rule does not apply when the second ($\sqsupsetneq$) rule with $\sqsupsetneq \psi$ as principal formula is performed, thus $\sqsupsetneq \psi \notin \Gamma^q$ and $i_q > 0$. For the same reason we also have $\psi \notin \Gamma^{q+1}$. Thus the premise of this second rule application cannot be the
first premise of the (□_≠) rule, for otherwise ψ would belong to Γq+1. For the same reason, it
cannot correspond to one of the other premises with j ≠ i_q. Hence, it must be the premise
with j = i_q, and Sq+1 contains two distinct cells containing □_≠ψ. By Lemma 17 again, it
follows that for all k > q, □_≠ψ ∈ S_{j_k}^k for some cell index 0 ≤ j_k ≠ i_k ≤ |H^k|.

For the third rule application, the same argument applies, but this time all the premises
of the rule contain ψ in their antecedent Γr+1, i.e. the axiom rule is applicable immediately
after the third (□_≠) application.

◀

Note that we can create a new history cell only when we apply a modal rule (□_≠), thus Proposition 18 indirectly provides a bound on the length of the history in minimal proofs.

**► Proposition 19 (Bounded (□=) Applications).** Let Π be a minimal proof in which history lengths are bounded by h. For any formula □=ϕ, all branches of Π contain at most h + 1 applications of the (□=) rule with □=ϕ as principal formula.

**Proof sketch.** Each application of (□_=) can only occur with conclusion sequents where □_=ϕ does not appear in the antecedent Γ, or the axiom rule could be applied instead. Thus its premise sequent has one more cell containing □_=ϕ than its conclusion sequent, namely in the antecedent. By Lemma 17, we can only repeat this operation h + 1 times before being forced to see □_=ϕ in the antecedent Γ.

◀

From the previous two results we easily obtain the following statement, which also takes
Boolean rules into account to obtain a polynomial bound on the depth of minimal proofs.

**► Theorem 20 (Polynomial Proof Depth).** Let $S = \mathcal{H}$; $\Gamma \vdash \Delta$ be a sequent, $m^\ne$ (resp. $m^=$) be the number of distinct $\Box_\ne$ subformulæ (resp. $\Box=$ subformulæ) occurring in $S$, and $p$ be the number of other subformulæ. If $S$ is provable, then it has a proof of depth at most $(3m^\ne + m^=)(3m^\ne + 1) + 1)(p + 1) + 1$.

**Proof.** By Proposition 18 and the subformula property, the number of (□_≠) rule applications along any branch is bounded by $3m^\ne$, which is also a bound on the length of histories in minimal proofs. By Proposition 19 and the subformula property, the total number of modal rule applications is thus bounded by $3m^\ne + m^= (3m^\ne + 1)$. In between any two modal rules we can apply at most $p$ Boolean rules without introducing the same formula twice, and possibly conclude by an axiom.

◀

## 4.3 Computational Complexity

The polynomial bound of Theorem 20 on the length of branches in minimal proofs yields a proof search algorithm working in alternating polynomial time. The algorithm implements the proof search game with Prover as existential player and Spoiler as universal player. Actually, Prover can follow the strategy of Section 4.1 without loss of generality nor of efficiency. Since our calculus is sound and complete for **DataGL**, and AP = PSPACE [9], it yields a PSPACE upper bound for the validity problem for **DataGL**. Because **DataGL** is closed under negation and PSPACE under complement, the same bound holds for the satisfiability problem. We show that this is actually a tight bound.

**► Theorem 21.** *The validity and satisfiability problems for DataGL are PSPACE-complete.*

The lower bound is obtained by reducing the satisfiability problem for **GL** to its **DataGL** counterpart. PSPACE-hardness follows since **GL** validity is known to be PSPACE-hard [8, Theorem 7]. We can indeed think of a finite tree without data as a finite data tree where all
the nodes share the same datum, and in such a tree □_ behaves exactly as the **GL** modality
□. Given a **GL** formula $\varphi$ we define the **DataGL** formula $[\varphi]$ by substituting □_ for □:

$$
[\mathbf{p}] \stackrel{\text{def}}{=} \mathbf{p}, \quad [\perp] \stackrel{\text{def}}{=} \perp, \quad [\varphi \supset \psi] \stackrel{\text{def}}{=} [\varphi] \supset [\psi], \quad [\Box \varphi] \stackrel{\text{def}}{=} \Box_= [\varphi].
$$

► Claim 21.1. For any **GL** formula $\varphi$, $\varphi$ is satisfiable in **GL** if and only if $[\varphi] \wedge \Box \neq \bot$ is satisfiable in **DataGL**.

**Proof sketch.** The formula □_≠⊥ ensures that a single data value is used throughout its models. Given such a finite single-data data tree t, a straightforward structural induction over φ establishes that t, w |= [φ] if and only if [t], w |= φ, where [t] is the tree obtained by erasing all data information from t.

◀

A final observation about proof search is that the polynomial bound of Theorem 20 on the
depth also applies to failed searches that follow the strategy of Section 4.1. This is exploited
by Lunel [15] to extract small counter-models from failed proof attempts when focusing on
saturated sequents (the completeness proof in Section 3.4 is indeed essentially based on proof
search): if a sequent is unprovable, then it has a counter-model of polynomial height. Hence
**DataGL** has a strong finite model property. It yields a different proof of the PSPACE upper
bound of Theorem 21 when combined with Proposition 6.7 of [11], though with a rather less
concrete algorithm than proof search.

5 Concluding Remarks

The sequent calculus for **DataGL** is to the best of our knowledge the first instance of a
proof system for a data-aware logic on finite data trees. It provides an optimal proof search
algorithm to establish the validity of **DataGL** formulæ, with a PSPACE complexity.

The logic **DataGL** is still a rather small syntactic fragment of **CoreDataXPath**. There
are two natural directions for extending our proof system towards full **CoreDataXPath**:

- one is allowing path expressions as in **CoreDataXPath**(↓⁺), which is EXP-complete [11],

- the other is to add other navigational axes, starting with the ancestor axis ↑⁺, as in the non primitive recursive **CoreDataXPath**(↑⁺, ↓⁺) [13].

On both accounts, the use of sequents enriched with histories is a promising starting point.

From a proof theory perspective, two lines of inquiry seem interesting. The first would
be to develop a cut elimination procedure for our sequent calculus; by completeness of the
calculus, the (cut) rule is admissible, but this is a semantic proof rather than a syntactic one.
The second is to consider an extension of **DataGL** where histories are integrated as logical
connectives in the syntax instead of being a mere extra-logical mechanism; this might help
in designing Hilbert-style axiomatisations for data logics.

**Acknowledgements** This work benefited from helpful discussions with Diego Figueira and Luc Segoufin.

References

1 A. Avron. On modal systems having arithmetical interpretations. *J. Symb. Log.*, 49(3): 935–942, 1984.

2 M. Benedikt and C. Koch. XPath leashed. *ACM Comput. Surv.*, 41(1:3), 2009.

3 M. Benedikt, W. Fan, and G. Kuper. Structural properties of XPath fragments. *Theor. Comput. Sci.*, 336(1):3–31, 2005.
4 M. Benedikt, W. Fan, and F. Geerts. XPath satisfiability in the presence of DTDs. *J. ACM*, 55(2:8), 2008.

5 P. Blackburn, M. de Rijke, and Y. Venema. *Modal Logic*, volume 53 of *Cambridge Tracts in Theoretical Computer Science*. Cambridge University Press, 2001.

6 M. Bojańczyk, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data trees and XML reasoning. *J. ACM*, 56(3:13), 2009.

7 K. Brünnler and L. Straßburger. Modular sequent systems for modal logic. In *Tableaux 2009*, volume 5607 of *LNCS*, pages 152–166. Springer, 2009.

8 A. V. Chagrov and M. N. Rybakov. How many variables does one need to prove PSPACE-hardness of modal logics? In *AiML 2002*, pages 71–82. King's College Publications, 2003.

9 A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation. *J. ACM*, 28(1):114–133, 1981.

10 D. Figueira. Alternating register automata on finite words and trees. *Logic. Meth. in Comput. Sci.*, 8(1:22), 2012.

11 D. Figueira. Decidability of downward XPath. *ACM Trans. Comput. Logic*, 13(4:34), 2012.

12 D. Figueira. On XPath with transitive axes and data tests. In *PODS 2013*, pages 249–260. ACM, 2013.

13 D. Figueira and L. Segoufin. Bottom-up automata on data trees and vertical XPath. In *STACS 2011*, volume 9 of *LIPIcs*, pages 93–104. LZI, 2011.

14 M. Jurdziński and R. Lazić. Alternating automata on data trees and XPath satisfiability. *ACM Trans. Comput. Logic*, 12(3:19), 2011.

15 S. Lunel. Systèmes de preuves pour logiques modales à données. Mémoire de Master, LMFI, Université Paris-Diderot, Sept. 2015.

16 S. Negri. Proof analysis in modal logic. *J. Phil. Log.*, 34(5–6):507–544, 2005.

17 F. Poggiolesi. The method of tree-hypersequents for modal propositional logic. In *Towards Mathematical Philosophy*, volume 28 of *Trends in Logic*, pages 31–51. Springer, 2009.

18 J. Robie, D. Chamberlin, M. Dyck, and J. Snelson. XML Path Language (XPath) 3.0. W3C Recommendation, 2014. URL http://www.w3.org/TR/xpath-30/.

19 B. ten Cate and M. Marx. Axiomatizing the logical core of XPath 2.0. *Theor. Comput. Sys.*, 44(4):561–589, 2009.

20 B. ten Cate, G. Fontaine, and T. Litak. Some modal aspects of XPath. *J. Appl. Non-Classical Log.*, 20(3):139–171, 2010.

21 B. ten Cate, T. Litak, and M. Marx. Complete axiomatizations for XPath fragments. *J. Appl. Logic*, 8(2):153–172, 2010.

22 H. Wansing. Sequent calculi for normal modal propositional logics. *J. Logic Comput.*, 4(2): 125–142, 1994.
A Basic Model Theory

► **Proposition 4** (Tree-Model Property). For any DataGL model $\mathfrak{M}$ and world $w_0$, there exists a finite data tree $\mathfrak{t}_\mathfrak{M}$ of the same height and a surjective bounded morphism $f$ from $\mathfrak{t}_\mathfrak{M}$ to $\mathfrak{M}$ with $f(\varepsilon) = w_0$. Hence, for all DataGL formulæ $\varphi$ and positions $w$ in dom $\mathfrak{t}_\mathfrak{M}$, $\mathfrak{t}_\mathfrak{M}, w \models \varphi$ if and only if $\mathfrak{M}, f(w) \models \varphi$.

**Proof.** We follow essentially the unfolding construction of Blackburn et al. [5, Proposition 2.15]. We want to construct a transitive tree $\mathfrak{M}' \stackrel{\text{def}}{=} (W', R', d', \ell')$, where the root $w_0$ is such that $w_0 R' w$ for all $w \in W' \setminus \{w_0\}$, and for any world $w$, its genealogy $\{w' \in W' | w' R' w\}$ is finite and linearly ordered by $R'$:

$$W' \stackrel{\text{def}}{=} \{w_0 w_1 \cdots w_n \mid n \in \mathbb{N} \text{ and } w_0 R w_1 R \cdots R w_n\},$$

i.e. the worlds in $\mathfrak{M}'$ are the finite $R$-chains starting from $w_0$ in $\mathfrak{M}$—note that since $R$ is transitive irreflexive, such chains are simple: $w_i \neq w_j$ for all $i \neq j$, hence $W'$ is finite—,

$$R' \stackrel{\text{def}}{=} \{(w_0 w_1 \cdots w_n, w_0 w_1 \cdots w_n \cdots w_{n+m}) \mid m > 0 \text{ and } w_0 w_1 \cdots w_{n+m} \in W'\},$$

i.e. $R'$ is the strict prefix relation over finite $R$-chains,

$$d'(w_0 w_1 \cdots w_n) \stackrel{\text{def}}{=} d(w_n),$$

$$\ell'(w_0 w_1 \cdots w_n) \stackrel{\text{def}}{=} \ell(w_n),$$

i.e. the labelling is inherited from the last element $w_n$ in a chain $w_0 w_1 \cdots w_n$.

Then $W'$ is finite, $R'$ is transitive irreflexive, $w_0$ in $W'$ is the root of $\mathfrak{M}'$, and the genealogy of an element $w_0 w_1 \cdots w_n$ is its set of strict prefixes and is therefore finite and linearly ordered by $R'$. Hence $\mathfrak{M}'$ is a finite transitive tree, i.e. a finite data tree, of height equal to that of $\mathfrak{M}$.

Finally, $f: W' \to W$ defined by $f(w_0 w_1 \cdots w_n) \stackrel{\text{def}}{=} w_n$ is a surjective bounded morphism from $\mathfrak{M}'$ to $\mathfrak{M}$ for the modal similarity type $\{\Diamond_{=}, \Diamond_{\neq}\}$: following [5, Definition 2.12],

i. $w_0 w_1 \cdots w_n$ and $f(w_0 w_1 \cdots w_n)$ satisfy the same atomic propositions since $\ell'(w_0 w_1 \cdots w_n) = \ell(w_n) = \ell(f(w_0 w_1 \cdots w_n))$;

ii. $f$ is a homomorphism: if $w_0 w_1 \cdots w_n R'_\star w_0 w_1 \cdots w_{n+m}$ for $\star$ in $\{=, \neq\}$, then $f(w_0 w_1 \cdots w_n) = w_n R w_{n+m} = f(w_0 w_1 \cdots w_{n+m})$ by definition of $R'$ and $d(w_n) = d'(w_0 w_1 \cdots w_n) \star d'(w_0 w_1 \cdots w_{n+m}) = d(w_{n+m})$ by definition of $d'$, i.e. $w_n R_\star w_{n+m}$;

iii. $f$ satisfies the back condition: if $f(w_0 w_1 \cdots w_n) = w_n R_\star w'$ for some $\star$ in $\{=, \neq\}$, then $w_0 w_1 \cdots w_n R' w_0 w_1 \cdots w_n w'$ by definition of $R'$ and $d'(w_0 w_1 \cdots w_n) = d(w_n) \star d(w') = d'(w_0 w_1 \cdots w_n w')$ by definition of $d'$, i.e. $w_0 w_1 \cdots w_n R'_\star w_0 w_1 \cdots w_n w'$ with $f(w_0 w_1 \cdots w_n w') = w'$.

Hence for all DataGL formulæ $\varphi$ and all worlds $w, \mathfrak{M}, f(w) \models \varphi$ if and only if $\mathfrak{M}', w \models \varphi$ by [5, Proposition 2.14]. ▼

B Relation with CoreDataXPath($\downarrow^+$)

The logic DataGL is a fragment of XPath: when naming @d the unique data attribute of data trees, in concrete XPath syntax, $\Diamond_{=}\varphi$ could be expressed as [./@d = ./descendant::*[$\chi$]/@d] assuming $\chi$ is the XPath translation of $\varphi$. More precisely, we only need the union-free fragment of CoreDataXPath$^\varepsilon(\downarrow^+)$ as defined by Figueira [11], with simplified syntax

$$\pi ::= \downarrow^+ | \pi\pi | [\chi], \qquad (\text{path formulæ})$$

$$\chi ::= \perp | p | \chi \supset \chi | \langle\varepsilon = \pi\rangle | \langle\varepsilon \neq \pi\rangle, \qquad (\text{node formulæ})$$
<figure><img src="image_6.png" /><figcaption>■ **Figure 5** Two data trees with $\Sigma \stackrel{\text{def}}{=} \{\emptyset, \{p\}\}$ and $\mathbb{D} \stackrel{\text{def}}{=} \mathbb{N}$. The bisimulation relation is depicted by dotted grey lines. The left tree satisfies formula (4) at its root, but the right tree does not.</figcaption></figure>

where $p$ is in $A$. The semantics $[[\pi]]_t$ of a path formula $\pi$ over a data tree $t$ is a binary relation over its domain:

$$[[\downarrow^+]]_t \stackrel{\text{def}}{=} R, \quad [[\pi\pi')]_t \stackrel{\text{def}}{=} [[\pi]]_t \circled{\circ} [[\pi')]_t, \quad [[[\chi]]]_t \stackrel{\text{def}}{=} \{(w, w) \mid t, w \models \chi\},$$

where ‘$\circled{\circ}$’ denotes relational composition, and $t, w \models \chi$ is defined inductively over node formulæ $\chi$ as usual with the addition of

$$t, w \models \langle\epsilon = \pi\rangle \quad \text{iff} \quad \exists w'. (w, w') \in [[\pi]]_t \text{ and } d(w) = d(w'),$$

$$t, w \models \langle\epsilon \neq \pi\rangle \quad \text{iff} \quad \exists w'. (w, w') \in [[\pi]]_t \text{ and } d(w) \neq d(w').$$

## Expressiveness

Any **DataGL** formula $\varphi$ can be translated as an equivalent **CoreDataXPath**$^\epsilon(\downarrow^+)$ node formula $X(\varphi)$ using $X(\bot) \stackrel{\text{def}}{=} \bot$, $X(p) \stackrel{\text{def}}{=} p$, $X(\varphi \supset \varphi') \stackrel{\text{def}}{=} X(\varphi) \supset X(\varphi')$, $X(\diamond=\varphi) \stackrel{\text{def}}{=} \langle\epsilon = \downarrow^+[X(\varphi)]\rangle$, and $X(\diamond\neq\varphi) \stackrel{\text{def}}{=} \langle\epsilon \neq \downarrow^+[X(\varphi)]\rangle$. This satisfies $t, w \models \varphi$ if and only if $t, w \models X(\varphi)$.

The logic **DataGL** is however less expressive than union-free **CoreDataXPath**$^\epsilon(\downarrow^+)$.
Figure 5 shows indeed two bisimilar (and thus **DataGL** indistinguishable) data trees, whose roots can be distinguished by the union-free **CoreDataXPath**$^\epsilon(\downarrow^+)$ node formula

$$\langle\epsilon = \downarrow^+[p]\downarrow^+ [\neg p]\rangle. \qquad (4)$$

This is as expected, since satisfiability of union-free **CoreDataXPath**$^\epsilon(\downarrow^+)$ node formulæ is EXP-hard [11, Theorem 6.5]—the proof heavily relies on formulæ similar to (4)—, but **DataGL** is in PSPACE by Theorem 21.

## The Data-Oblivious Case

The difference in expressiveness in the data-aware case should be contrasted with the situation in the data-oblivious case [20]: **CoreXPath**(↓$^+$) employs the following syntax for node formulæ:

$$\chi ::= \bot | p | \chi \supset \chi | \langle\pi\rangle\chi$$

with semantics $t, w \models \langle\pi\rangle\chi$ if there exists $w'$ with $(w, w') \in [[\pi]]_t$ and $t, w' \models \chi$. Then the following translation of **CoreXPath**(↓$^+$) node formulæ into equivalent **GL** formulæ shows their expressive equivalence:

$$G(\bot) \stackrel{\text{def}}{=} \bot$$

$$G(\chi \supset \chi') \stackrel{\text{def}}{=} G(\chi) \supset G(\chi')$$

$$G(\langle\pi\pi'\rangle\chi) \stackrel{\text{def}}{=} G(\langle\pi\rangle\langle\pi'\rangle\chi)$$

$$G(p) \stackrel{\text{def}}{=} p$$

$$G(\langle\downarrow^+\rangle\chi) \stackrel{\text{def}}{=} \diamond G(\chi)$$

$$G(\langle[\chi]\rangle\chi') \stackrel{\text{def}}{=} G(\chi) \wedge G(\chi').$$
C Examples of DataGL Proofs

► Lemma 6 (Admissibility of Weakening). The following rules are admissible:

$$ \frac{\mathcal{H}; \Gamma \vdash \Delta}{\mathcal{H}; \Gamma, \varphi \vdash \Delta} W_L $$

$$ \frac{\mathcal{H}; \Gamma \vdash \Delta}{\mathcal{H}; \Gamma \vdash \Delta, \varphi} W_R $$

**Proof.** We show by induction over proofs in the sequent calculus with $(W_L)$ and $(W_R)$ included that applications of the weakening can be eliminated. Consider the bottom-most application of a weakening along a branch of a proof. If the rule immediately above it is (ax), $(\perp_L)$, $(\Box=)$, or $(\Box \neq)$—which already incorporate weakening—, then the application of the weakening can simply be removed. If the rule immediately above is $(\supset_L)$ or $(\supset_R)$, then the proof can be rewritten by pushing the application of the weakening upwards, and applying the induction hypothesis on the smaller proofs for the premises yields the result. ◀

► Lemma 22 (Admissibility of $(\neg_L)$ and $(\neg_R)$). The following rules are admissible:

$$ \frac{\mathcal{H}; \Gamma \vdash \varphi, \Delta}{\mathcal{H}; \Gamma, \neg \varphi \vdash \Delta} \neg_L $$

$$ \frac{\mathcal{H}; \Gamma, \varphi \vdash \Delta}{\mathcal{H}; \Gamma \vdash \neg \varphi, \Delta} \neg_R $$

**Proof.** Recall that $\neg \varphi \stackrel{\text{def}}{=} \varphi \supset \perp$. We can replace any application of $(\neg_L)$ or $(\neg_R)$ by the following derivations:

$$ \frac{\mathcal{H}; \Gamma \vdash \varphi, \Delta}{\mathcal{H}; \Gamma, \varphi \supset \perp \vdash \Delta} \perp_L $$

$$ \frac{\mathcal{H}; \Gamma, \varphi \vdash \Delta}{\mathcal{H}; \Gamma, \varphi \vdash \perp, \Delta} W_R \\ \frac{\mathcal{H}; \Gamma \vdash \varphi \supset \perp, \Delta}{\mathcal{H}; \Gamma \vdash \varphi \supset \perp, \Delta} \supset_R $$

► Lemma 23 (Admissibility of $(\vee_L)$ and $(\vee_R)$). The following rules are admissible:

$$ \frac{\mathcal{H}; \Gamma, \varphi \vdash \Delta}{\mathcal{H}; \Gamma, \varphi \vee \psi \vdash \Delta} \vee_L $$

$$ \frac{\mathcal{H}; \Gamma \vdash \varphi, \psi, \Delta}{\mathcal{H}; \Gamma \vdash \varphi \vee \psi, \Delta} \vee_R $$

**Proof.** Recall that $\varphi \vee \psi \stackrel{\text{def}}{=} (\neg \varphi) \supset \psi$. We can replace any application of $(\vee_L)$ or $(\vee_R)$ by the following derivations:

$$ \frac{\mathcal{H}; \Gamma, \varphi \vdash \Delta}{\mathcal{H}; \Gamma, \neg \varphi, \Delta} \neg_R \\ \frac{\mathcal{H}; \Gamma, \varphi \vdash \Delta}{\mathcal{H}; \Gamma, \neg \varphi \supset \psi, \Delta} \supset_L $$

$$ \frac{\mathcal{H}; \Gamma \vdash \varphi, \psi, \Delta}{\mathcal{H}; \Gamma, \neg \varphi \vdash \psi, \Delta} \neg_L \\ \frac{\mathcal{H}; \Gamma \vdash \neg \varphi \supset \psi, \Delta}{\mathcal{H}; \Gamma \vdash \neg \varphi \supset \psi, \Delta} \supset_R $$

► Lemma 24 (Admissibility of $(\wedge_L)$ and $(\wedge_R)$). The following rules are admissible:

$$ \frac{\mathcal{H}; \Gamma, \varphi, \psi \vdash \Delta}{\mathcal{H}; \Gamma, \varphi \wedge \psi \vdash \Delta} \wedge_L $$

$$ \frac{\mathcal{H}; \Gamma \vdash \varphi, \Delta}{\mathcal{H}; \Gamma \vdash \varphi \wedge \psi, \Delta} \wedge_R $$

**Proof.** Recall that $\varphi \wedge \psi \stackrel{\text{def}}{=} (\neg \varphi \vee \neg \psi)$. We can replace any application of $(\wedge_L)$ or $(\wedge_R)$ by the following derivations:

$$ \frac{\mathcal{H}; \Gamma, \varphi, \psi \vdash \Delta}{\mathcal{H}; \Gamma, \varphi \vdash \neg \psi, \Delta} \neg_R \\ \frac{\mathcal{H}; \Gamma \vdash \varphi, \neg \psi, \Delta}{\mathcal{H}; \Gamma \vdash \neg \varphi, \neg \psi, \Delta} \supset_L \\ \frac{\mathcal{H}; \Gamma \vdash \neg \varphi \vee \neg \psi, \Delta}{\mathcal{H}; \Gamma, \neg (\neg \varphi \vee \neg \psi) \vdash \Delta} \neg_L $$

$$ \frac{\mathcal{H}; \Gamma \vdash \varphi, \Delta}{\mathcal{H}; \Gamma, \neg \varphi \vdash \Delta} \neg_L \\ \frac{\mathcal{H}; \Gamma \vdash \psi, \Delta}{\mathcal{H}; \Gamma, \neg \psi \vdash \Delta} \neg_L \\ \frac{\mathcal{H}; \Gamma, \neg \varphi \vee \neg \psi \vdash \Delta}{\mathcal{H}; \Gamma \vdash \neg (\neg \varphi \vee \neg \psi), \Delta} \neg_R $$

► Example 25 (Proof of L in the DataGL Calculus). Let us consider again the L axiom. Recall that $\Box \varphi \stackrel{\text{def}}{=} \Box=\varphi \wedge \Box \neq \varphi$. We shall prove that L is valid in DataGL; the proof is a variant of the one presented in Example 5 and needs to distinguish between several cases. We start proof search by applying the Boolean rules: