Axiomatizing first-order consequences in inclusion logic

TL;DR

This paper develops a natural deduction system that is sound and complete for deriving first-order consequences in inclusion logic, a dependence logic variant with fixed-point expressiveness.

Contribution

It provides the first explicit partial axiomatization for first-order consequences in inclusion logic using a natural deduction system.

Findings

The deduction system is sound for first-order consequences.

The deduction system is complete for first-order consequences.

The system enables formal reasoning within inclusion logic.

Abstract

Inclusion logic is a variant of dependence logic that was shown to have the same expressive power as positive greatest fixed-point logic. Inclusion logic is not axiomatizable in full, but its first-order consequences can be axiomatized. In this paper, we provide such an explicit partial axiomatization by introducing a system of natural deduction for inclusion logic that is sound and complete for first-order consequences in inclusion logic.

Tables

Table 1. Table 1. Rules for equality, connectives and quantifiers

$=𝖨$   $t=t$	$t=t^{\prime }$        $\varphi \left(t/x\right)$  $=\mathrm{𝖲𝗎𝖻}$          $\varphi \left(t^{\prime }/x\right)$
$\left[\alpha \right]$    $D$      $\perp$  $\neg 𝖨$ (1)   $\neg \alpha$               $\alpha$         $\neg \alpha$  $\neg 𝖤$         $\varphi$         [$\neg \alpha$]     $D$        $\perp$     $\mathrm{𝖱𝖠𝖠}$  (1)     $\alpha$
$\varphi$        $\psi$  $\wedge 𝖨$     $\varphi \wedge \psi$	$\varphi$  $\vee 𝖨$   $\varphi \vee \psi$         $\varphi$  $\vee 𝖨$   $\psi \vee \varphi$
$\varphi \wedge \psi$  $\wedge 𝖤$      $\varphi$                 $\varphi \wedge \psi$  $\wedge 𝖤$      $\psi$	$\varphi \vee \psi$          [$\varphi$]   $D_0$    $\chi$              [$\psi$]    $D_1$      $\chi$  $\vee 𝖤$ (2)                $\chi$
$\varphi \left(t/x\right)$  $\exists 𝖨$     $\exists x\varphi$	$D_0$   $\exists x\varphi$              $\left[\varphi \right]$   $D_1$    $\psi$  $\exists 𝖤$ (3)          $\psi$
$D$    $\varphi$  $\forall 𝖨$ (4)   $\forall x\varphi$                  $\forall x\alpha$  $\forall 𝖤$   $\alpha \left(t/x\right)$               $\forall x\varphi \left(𝗒\right)$  $\forall {𝖤}_0$ (5)     $\varphi \left(𝗒\right)$	$D_0$   $\forall x\varphi$                      $\left[\varphi \left(y/x\right)\right]$        $D_1$              $\psi$  $\forall \mathrm{𝖲𝗎𝖻}$ (6)          $\forall y\psi$                                      $\forall x\forall y\varphi$  $\forall \mathrm{𝖤𝗑𝖼}$   $\forall y\forall x\varphi$
$\forall x\varphi$               $\forall x\psi$  ${\forall }_{\wedge }\mathrm{𝖤𝗑𝗍}$      $\forall x\left(\varphi \wedge \psi \right)$	$\forall x\varphi (x,𝗏)\vee \psi \left(𝗏\right)$  ​${\forall }_{\vee }\mathrm{𝖤𝗑𝗍}$ (7)   $\exists y\exists z\forall x\left(\left(\varphi \wedge y=z\right)\vee \left(\psi \wedge y\ne z\right)\right)$
(1) The undischarged assumptions in the derivation $D$ contain first-order formulas only.
(2) The undischarged assumptions in the derivations $D_0$ and $D_1$ contain first-order formulas only.
(3) $x$ does not occur freely in $\psi$ or in any formula in the undischarged assumptions of $D_1$.
(4) $x$ does not occur freely in any formula in the undischarged assumptions of $D$.
(5) $x$ is not in the sequence $𝗒$ of free variables of $\varphi$.
(6) $y$ does not occur freely in $\forall x\varphi$ or in any formula in the undischarged assumptions of $D_1$.
(7) $x$ does not occur freely in $\psi \left(𝗏\right)$, and $y,z$ are fresh variables.

Table 2. Table 2. Rules for inclusion atoms

$\mathrm{𝗑𝗒𝗓}\subseteq \mathrm{𝗎𝗏𝗐}$  $\subseteq \mathrm{𝖤𝗑𝖼}$  $\mathrm{𝗒𝗑𝗓}\subseteq \mathrm{𝗏𝗎𝗐}$                      $\mathrm{𝗑𝗒}\subseteq \mathrm{𝗎𝗏}$  $\subseteq \mathrm{𝖢𝗍𝗋}$    $𝗑\subseteq 𝗎$                     $𝗑\subseteq 𝗒$     $𝗒\subseteq 𝗓$  $\subseteq \mathrm{𝖳𝗋𝗌}$      $𝗑\subseteq 𝗓$
$𝗒\subseteq 𝗑$     $\alpha \left(𝗑/𝗓\right)$  $\subseteq \mathrm{𝖢𝗆𝗉}$ (1)      $\alpha \left(𝗒/𝗓\right)$	[$𝗒\subseteq 𝗑$]                       [$\neg \alpha \left(𝗒/𝗓\right)$]              $D$                  $\perp$            $\subseteq \mathrm{𝖤𝗑𝗉}$ (2)           $\alpha \left(𝗑/𝗓\right)$
$𝗑\subseteq 𝗒$  $\subseteq {𝖶}_{\exists }$ (3)  $\exists w\left(𝗑w\subseteq 𝗒z\right)$	$𝗑\subseteq 𝗒$  $\subseteq {𝖶}_{\forall }$ (3)  $\forall w\left(𝗑z\subseteq 𝗒w\right)$
$\forall 𝗑\varphi (𝗑,𝗓)$  $\forall \subseteq \mathrm{𝖲𝗂𝗆}$ (4)  $\exists 𝗑\forall 𝗒\left(\mathrm{𝗓𝗒}\subseteq \mathrm{𝗓𝗑}\wedge \varphi (𝗑,𝗓)\right)$	$\exists 𝗑\left(\underset{i\in I}{\bigwedge }{\rho }_{𝗑}^i\subseteq {\sigma }_{𝗑}^i\wedge \alpha \right)\vee \varphi$  $\exists \subseteq \mathrm{𝖤𝗑𝗍}$ (5)  $\exists 𝗑\exists uv(\underset{i\in I}{\bigwedge }{\rho }_{𝗑}^{i}uv\subseteq {\sigma }_{𝗑}^{i}uv\wedge (\alpha \leftrightarrow u=v)\wedge (\alpha \vee \varphi ))$
(1) The free variables of $\alpha \left(𝗑/𝗓\right)$ are among $𝗑$.
(2) The free variables of $\alpha \left(𝗒/𝗓\right)$ are among $𝗒$, and the variables in $𝗒$ do not occur freely in any undischarged assumptions in $D$.
(3) $w$ is not among $\mathrm{𝗑𝗒}z$.
(4) $𝗒$ is a sequence of fresh variables.
(5) $u,v$ are fresh variables.

Equations

$$\Gamma \models \varphi ⟺\Gamma ⊢\varphi$$

$$\alpha ::=\perp \mid t_1=t_2\mid R{t}_1,\dots ,t_n\mid \neg \alpha \mid \alpha \wedge \alpha \mid \alpha \vee \alpha \mid \exists x\alpha \mid \forall x\alpha .$$

$$\varphi ::=\perp \mid \alpha \mid \neg \alpha \mid x_1\dots x_n\subseteq y_1\dots y_n\mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \exists x\varphi \mid \forall x\varphi$$

$$\text{Fv}(x_1\cdots x_n\subseteq y_1\cdots y_n):=\{x_1,\dots ,x_n,y_1,\dots ,y_n\}.$$

$$s(a/x)(y)=\{\begin{array}{ll}a,& \text{if }y=x;\\ s(y),& \text{otherwise.}\end{array}$$

$$X(F/x)=\{s(a/x)\mid s\in X\text{ and }a\in F(s)\}.$$

$$M{\models }_X\alpha ⟺M{\models }_{\{s\}}\alpha \text{ for all }s\in X.$$

$$M{\models }_X\varphi ⟺(M,rel(X)){\models }_s\psi (R)\text{ for all }s\in X;$$

$$\mathbb{N}\models \alpha \text{ iff }\models \alpha \vee \neg {\gamma }_{\mathbf{PA}}\vee \varphi ,$$

$$\Gamma ⊢\alpha ⟺\Gamma \models \alpha$$

$$Q^1{x}_1\dots Q^n{x}_n\theta (\mathsf{x},\mathsf{z}),$$

$$\exists\mathsf{x}\forall y\big{(}\mathop{\bigwedge_{1\leq j\leq n}}_{Q^{j}=\forall}\mathsf{z}x_{1}\dots x_{j-1}y\subseteq\mathsf{z}x_{1}\dots x_{j-1}x_{j}\wedge\theta(\mathsf{x},\mathsf{z})\big{)},$$

$$\forall vQ\mathsf{x}\psi (v,\mathsf{x},\mathsf{z})\equiv \exists vQ\mathsf{x}\forall y(\mathsf{z}y\subseteq \mathsf{z}v\wedge \psi (v,\mathsf{x},\mathsf{z})),$$

$$\exists\mathsf{w}\Big{(}\bigwedge_{i\in I}\mathsf{u}_{i}\subseteq\mathsf{v}_{i}\wedge\alpha(\mathsf{w},\mathsf{z})\Big{)},$$

$${\iota }_0({\mathsf{w}}_0)=\underset{i\in I}{\bigwedge }{\mathsf{u}}_i\subseteq {\mathsf{v}}_i\text{ and }{\iota }_1({\mathsf{w}}_1)=\underset{j\in J}{\bigwedge }{\mathsf{u}}_j\subseteq {\mathsf{v}}_j.$$

$$\begin{split}\psi=\exists\mathsf{w}_{0}\exists\mathsf{w}_{1}\exists pqp^{\prime}q^{\prime}\Big{(}&\bigwedge_{i\in I}(\mathsf{u}_{i}pq\subseteq\mathsf{v}_{i}pq)\,\wedge\bigwedge_{j\in J}(\mathsf{u}_{j}p^{\prime}q^{\prime}\subseteq\mathsf{v}_{j}p^{\prime}q^{\prime})\\ &\wedge(\alpha_{0}\vee\alpha_{1})\wedge(\alpha_{0}\leftrightarrow p=q)\wedge(\alpha_{1}\leftrightarrow p^{\prime}=q^{\prime})\Big{)}.\end{split}$$

$$\exists\mathsf{x}\big{(}\bigwedge_{i\in I}\mathsf{u}_{i}\subseteq\mathsf{v}_{i}\,\wedge\alpha\big{)}\vee\phi\equiv\exists\mathsf{x}\exists pq\Big{(}\bigwedge_{i\in I}\mathsf{u}_{i}pq\subseteq\mathsf{v}_{i}pq\,\wedge(\alpha\leftrightarrow p=q)\wedge(\alpha\vee\phi)\Big{)},$$

$$\displaystyle\exists\mathsf{w}_{0}\Big{(}\bigwedge_{i\in I}\mathsf{u}_{i}\subseteq\mathsf{v}_{i}\,\wedge\alpha_{0}\Big{)}\vee\theta_{1}$$

$$\equiv$$

$$\displaystyle\quad\wedge\exists\mathsf{w}_{1}\exists p^{\prime}q^{\prime}\Big{(}\bigwedge_{j\in J}\mathsf{u}_{j}p^{\prime}q^{\prime}\subseteq\mathsf{v}_{j}p^{\prime}q^{\prime}\,\wedge(\alpha_{1}\leftrightarrow p^{\prime}=q^{\prime})\wedge(\alpha_{0}\vee\alpha_{1})\Big{)}\Big{)}$$

$$\equiv$$

$$Y({\mathsf{F}}^{\prime }/\mathsf{x})=Y(\mathsf{F}/\mathsf{x})\text{ and }(X\setminus Y)({\mathsf{F}}^{\prime }/\mathsf{x})=(X\setminus Y)(a/\mathsf{x}),$$

$$H(s)=\{\begin{array}{ll}\{a\}& \text{if }M{\models }_s\alpha ;\\ \{b\}& \text{otherwise.}\end{array}$$

$$U=Y({\mathsf{F}}^{\prime }/\mathsf{x})(G/p)(H/q)\text{ and }V=Z({\mathsf{F}}^{\prime }/\mathsf{x})(G/p)(H/q).$$

$$\exists\mathsf{w}\exists\mathsf{x}\forall y\Big{(}\bigwedge_{i\in I}\mathsf{u}_{i}\subseteq\mathsf{v}_{i}\,\wedge\bigwedge_{j\in J}\mathsf{z}x_{1}\dots x_{j-1}y\subseteq\mathsf{z}x_{1}\dots x_{j-1}x_{j}\,\wedge\alpha(\mathsf{w},\mathsf{x},\mathsf{z})\Big{)},$$

$$Q^{1}x_{1}\dots Q^{n}x_{n}\exists\mathsf{w}\Big{(}\bigwedge_{i\in I}\mathsf{u}_{i}\subseteq\mathsf{v}_{i}\,\wedge\alpha(\mathsf{w},\mathsf{x},\mathsf{z})\Big{)}.$$

$$\exists\mathsf{w}\exists\mathsf{x}\forall y\Big{(}\bigwedge_{i\in I}\rho^{i}_{\mathsf{w}}\subseteq\sigma^{i}_{\mathsf{w}}\,\wedge\bigwedge_{j\in J}\pi^{j}_{\mathsf{x}}y\subseteq\tau^{j}_{\mathsf{x}}\wedge\alpha(\mathsf{w},\mathsf{x})\Big{)}.$$

$$\Phi :=$$

$$\displaystyle\exists\mathsf{w}^{1}\mathsf{x}^{1}\forall y_{1}\Big{(}\alpha_{1}(\mathsf{w}^{1}\mathsf{x}^{1})\wedge\gamma_{1}(\mathsf{w}_{0}\mathsf{w}^{1})\wedge\delta_{1}(y_{0},\mathsf{x}_{0}\mathsf{x}^{1})\wedge$$

$$\dots \dots$$

$$\displaystyle\exists\mathsf{w}^{n}\mathsf{x}^{n}\forall y_{n}\Big{(}\alpha_{n}(\mathsf{w}^{n}\mathsf{x}^{n})\wedge\gamma_{n}(\mathsf{w}^{n-1}\mathsf{w}^{n})\wedge\delta_{n}(y_{0}\dots y_{n},\mathsf{x}_{0}\mathsf{x}^{1}\dots\mathsf{x}^{n})\wedge\dots\Big{)}\quad\dots\quad\Big{)}\Big{)},$$

$$A_n=\{\xi \eta \mid ⟨\xi \eta ,j⟩\in U_n\text{ for some }j\in J\},$$

$$\mathfrak{s}({\mathsf{w}}^n{\mathsf{x}}^n)={\mathsf{a}}^n{\mathsf{b}}^n\text{ and }\mathfrak{s}(y_n)=c_n.$$

Full text

1. Introduction

In this paper, we axiomatize first-order consequences of inclusion logic. Inclusion logic was introduced by Galliani [6]. Together with independence logic, introduced by Grädel and Väänänen [11], inclusion logic is an important variant of dependence logic, which was introduced by Väänänen [29] as an extension of first-order logic and a new framework for characterizing dependency notions. Inclusion logic aims to characterize inclusion dependencies by extending first-order logic with inclusion atoms, which are strings of the form $x_{1}\dots x_{n}\subseteq y_{1}\dots y_{n}$, where $\langle x_{1},\dots,x_{n}\rangle=\mathsf{x}$ and $\langle y_{1},\dots,y_{n}\rangle=\mathsf{y}$ are sequences of variables of the same length. Inclusion logic adopts the team semantics of Hodges [21, 22], in which inclusion atoms and other formulas are evaluated in a model with respect to sets of assignments (called teams), in contrast to single assignments as in the usual first-order logic. Intuitively the inclusion atom $\mathsf{x}\subseteq\mathsf{y}$ specifies that all possible values for $\mathsf{x}$ in a team $X$ are included in the values of $\mathsf{y}$ in the same team $X$.

Galliani and Hella proved that inclusion logic is expressively equivalent to positive greatest fixed-point logic [8]. It then follows from the results of Immerman [23] and Vardi [31] that over finite ordered structures inclusion logic captures PTIME. Building on these results, Grädel defined model-checking games for inclusion logic [9], which then found applications in [10]. There also emerged some studies [16, 13, 27, 14] on the computational complexity and syntactical fragments of inclusion logic. Embedding the semantics of inclusion atoms into the semantics of the quantifiers, Rönnholm [28] introduced the interesting inclusion quantifiers that generalize the idea of the slashed quantifiers of independence-friendly logic [20] (a close relative to dependence logic). Inclusion atoms have also found natural applications in a recent formalization of Arrow’s Theorem in social choice in dependence and independence logic [26]. Motivated by the increasing interest in inclusion logic, we present in this paper a proof-theoretic investigation of inclusion logic, which is currently missing in the literature.

It is worth noting that inclusion atoms correspond exactly to the inclusion dependencies studied in database theory. The implication problem of inclusion dependencies, i.e., the problem of deciding whether $\Gamma\models\phi$ for a set $\Gamma\cup\{\phi\}$ of inclusion dependencies (or inclusion atoms), is completely axiomatized in [4] by the following three rules/axioms:

• •

$\mathsf{x}\subseteq\mathsf{x}$ (identity)

• •

$x_{1}\dots x_{n}\subseteq y_{1}\dots y_{n}/x_{i_{1}}\dots x_{i_{k}}\subseteq y_{i_{1}}\dots y_{i_{k}}$ for $i_{1},\dots,i_{k}\in\{1,\dots,n\}$ (projection and permutation)

• •

$\mathsf{x}\subseteq\mathsf{y},\mathsf{y}\subseteq\mathsf{z}/\mathsf{x}\subseteq\mathsf{z}$ (transitivity)

The team semantics interpretation for inclusion atoms has recently been ulitized to study the implication problems of inclusion atoms together with other dependency atoms [15, 18, 19]. In this paper, we study, instead, the axiomatization problem of inclusion logic, i.e., inclusion atoms enriched with connectives and quantifiers of first-order logic. We investigate the problem of finding a deduction system for which the completeness theorem

[TABLE]

holds for $\Gamma\cup\{\phi\}$ being a set of formulas of the logic.

It is known that dependence logic is not (effectively) axiomatizable, since the sentences of the logic are equi-expressive with sentences of existential second-order logic (ESO) [29]. Nevertheless, if one restrict the consequence $\phi$ in (1) to a first-order sentence and $\Gamma$ to a set of sentences in dependence logic, the axiomatization can be found. This is because, finding a model for such a set $\Gamma\cup\{\neg\phi\}$ of sentences of dependence logic is the same as finding a model for a set of ESO sentences (i.e., sentences of the form $\exists f_{1}\dots f_{n}\alpha$ for some first-order $\alpha$), which is then reduced to finding a model for a set of first-order sentences (of the form $\alpha$). A concrete system of natural deduction for dependence logic admitting this type of completeness theorem was given in [25]. The proof of the completeness theorem uses a nontrivial technique based on the equivalence between a dependence logic sentence and its so-called game expression (an infinitary first-order sentence describing a semantic game) over countable models, and the fact that the game expression can be finitely approximated over recursively saturated models. Subsequently, using the similar method a system of natural deduction axiomatizing completely the first-order consequences in independence logic with respect to sentences was also introduced [12]. These partial axiomatizations for sentences were first generalized in [24] to cover the cases for formulas by expanding the language with a new predicate symbol to interpret the teams, and later generalized further in [32] to cover the case when the consequence $\phi$ in (1) is not necessarily first-order itself but has an essentially first-order translation by applying a trick that involves the weak classical negation $\mathop{\dot{\sim}}$ and the addition of the $\mathsf{RAA}$ rule for $\mathop{\dot{\sim}}$.

As we will demonstrate formally in this paper, inclusion logic is not (effectively) axiomatizable either. Since inclusion logic is less expressive than ESO, by the same argument as above, the first-order consequences of inclusion logic can also be axiomatized. In this paper, we give explicitly such an axiomatization. To be more precise, we introduce a system of natural deduction for inclusion logic for which the completeness theorem (1) holds for $\phi$ being a first-order formula and $\Gamma$ being a set of $\mathsf{Inc}$-formulas. Our completeness proof uses the technique developed in [25] together with the trick in [32]. Our system of inclusion logic is a conservative extension of the system of first-order logic, in the sense that it has the same rules as that of first-order logic when restricted to first-order formulas only. The rules for inclusion atoms include some of those introduced in [12], and the rules characterizing the interactions between inclusion atoms and the connectives and quantifiers appear to be simpler than the corresponding ones in the systems of dependence and independence logic defined in [25, 12]. The $\mathsf{RAA}$ rule for $\mathop{\dot{\sim}}$, being a crucial (yet generally not effective) rule for applying the trick of [32], also behaves better in our system of inclusion logic than in the systems of dependence and independence logic. In particular, in the inclusion logic system, with respect to first-order formulas, the $\mathsf{RAA}$ rule for $\mathop{\dot{\sim}}$ becomes effective and also derivable from other more basic rules.

The paper is organized as follows. In Section 2 we recall the basics of inclusion logic, and also give a proof that inclusion logic is not (effectively) axiomatizable. Section 3 discusses the normal form for inclusion logic. In Section 4, we define the game expressions and their finite approximations that are crucial for the proof of the completeness theorem of the system of natural deduction for inclusion logic. We introduce this system in Section 5, and also prove the soundness theorem as well as some useful derivable clauses in the section. The proof of the completeness theorem will be given in Section 6. We conclude in Section 7 by showing some applications of our system; in particular, we derive in our system the axioms for anonymity atoms proposed recently by Väänänen [30].

2. Preliminaries

In this section, we recall the basics of inclusion logic and prove formally that inclusion logic is not (effectively) axiomatizable. We consider first-order signatures $\mathscr{L}$ with a built-in equality symbol $=$. Fix a set $\mathsf{Var}$ of first-order variables, and denote its elements by $u,v,w,x,y,\dots$ (with or without subscripts). First-order $\mathscr{L}$-terms $t$ are built recursively as usual. First-order $\mathscr{L}$-formulas $\alpha$ are defined by the grammar:

[TABLE]

Throughout the paper, we reserve the first greek letters $\alpha,\beta,\gamma,\delta$ (with or without subscripts) for first-order formulas. As usual, we write $\alpha\to\beta:=\neg\alpha\vee\beta$ and $\alpha\leftrightarrow\beta:=(\alpha\to\beta)\wedge(\beta\to\alpha)$ for first-order formulas $\alpha$ and $\beta$. Formulas $\phi$ of inclusion logic ($\mathsf{Inc}$) are defined recursively as follows:

[TABLE]

where $\alpha$ is an arbitrary first-order formula. The formula $x_{1}\cdots x_{n}\subseteq y_{1}\dots y_{n}$ is called an inclusion atom. Note that in the literature on inclusion logic, $\mathsf{Inc}$-formulas are usually assumed to be in negation normal form (i.e., negation occurs only in front of atomic formulas). We do not adopt this convention in this paper, but we do require that negation in $\mathsf{Inc}$ applies only to first-order formulas.

The set $\textsf{Fv}(\phi)$ of free variables of an $\mathsf{Inc}$-formula $\phi$ is defined inductively as usual except that we now have the new case

[TABLE]

We write $\phi(x_{1},\dots,x_{k})$ to indicate that the free variables of $\phi$ are among $x_{1},\dots,x_{k}$. $\mathsf{Inc}$-formulas with no free variable are called sentences. We write $\phi(t/x)$ for the formula obtained by substituting uniformly $t$ for $x$ in $\phi$, where we assume that $t$ is free for $x$.

We assume that the domain of a first-order model $M$ has at least two elements, and use the same letter $M$ to stand for both the model and its domain. An assignment of an $\mathscr{L}$-model $M$ for a set $V\subseteq\mathsf{Var}$ of variables is a function $s:V\to M$. The interpretation of an $\mathscr{L}$-term $t$ under $M$ and $s$ (denoted $s(t^{M})$) is defined as usual. For any sequence $\mathsf{x}=\langle x_{1},\dots,x_{k}\rangle$ of variables, we write $s(x_{1},\dots,x_{k})$ or $s(\mathsf{x})$ for $\langle s(x_{1}),\dots,s(x_{k})\rangle$. For any element $a\in M$, $s(a/x)$ is the assignment defined as

[TABLE]

A set $X$ of assignments of a model $M$ with the same domain $\mathsf{dom}(X)$ is called a team (of $M$). In particular, the empty set $\emptyset$ is a team, and the singleton $\{\emptyset\}$ is a team with the empty domain.

\definitionname** 2.1**

For any $\mathscr{L}$-formula $\phi$ of $\mathsf{Inc}$, any $\mathscr{L}$-model $M$ and any team $X$ of $M$ with $\mathsf{dom}(X)\supseteq\mathsf{Fv}(\phi)$, we define the satisfaction relation $M\models_{X}\phi$ inductively as follows:

• •

$M\models_{X}\bot$  iff   $X=\emptyset$.

• •

$M\models_{X}\alpha$  iff   for all $s\in X$, $M\models_{s}\alpha$ in the usual sense.

• •

$M\models_{X}\neg\alpha$  iff   for all $s\in X$, $M\not\models_{s}\alpha$ in the usual sense.

• •

$M\models_{X}\mathsf{x}\subseteq\mathsf{y}$  iff   for all $s\in X$, there is $s^{\prime}\in X$ such that $s(\mathsf{x})=s^{\prime}(\mathsf{y})$.

• •

$M\models_{X}\phi\wedge\psi$  iff   $M\models_{X}\phi$ and $M\models_{X}\psi$.

• •

$M\models_{X}\phi\vee\psi$  iff   there exist $Y,Z\subseteq X$ with $X=Y\cup Z$ such that $M\models_{Y}\phi$ and $M\models_{Z}\psi$.

• •

$M\models_{X}\exists x\phi$  iff   $M\models_{X(F/x)}\phi$ for some function $F:X\to\wp(M)\setminus\{\emptyset\}$, where

[TABLE]

• •

$M\models_{X}\forall x\phi$  iff   $M\models_{X(M/x)}\phi$, where $X(M/x)=\{s(a/x)\mid s\in X\text{ and }a\in M\}.$

For any set $\Gamma$ of $\mathsf{Inc}$-formulas, we write $M\models_{X}\Gamma$ if $M\models_{X}\phi$ for all $\phi\in\Gamma$. We write $\Gamma\models\phi$ if $M\models_{X}\Gamma$ implies $M\models_{X}\phi$ for all models $M$ and teams $X$. We write simply $\models\phi$ for $\emptyset\models\phi$, and $\psi\models\phi$ for $\{\psi\}\models\phi$. If both $\phi\models\psi$ and $\psi\models\phi$, we wire $\phi\equiv\psi$.

Our version of the team semantics for disjunction and existential quantifier is known in the literature as lax semantics; see [6] for further discussion. In some literature (e.g., [6]) inclusion atoms are allowed to have arbitrary terms as arguments, namely strings of the form $t_{1}\dots t_{n}\subseteq t_{1}^{\prime}\dots t_{n}^{\prime}$ are considered well-formed formulas, and the semantics of these inclusion atoms are defined (naturally) as:

• •

$M\models_{X}t_{1}\cdots t_{n}\subseteq t_{1}^{\prime}\cdots t_{n}^{\prime}$  iff  for all $s\in X$, there is $s^{\prime}\in X$ such that $s(t_{1}^{M},\dots,t_{n}^{M})=s^{\prime}((t_{1}^{\prime})^{M},\dots,(t_{n}^{\prime})^{M}).$

It is easy to verify that inclusion atoms of this type are definable in our version of inclusion logic, since $\mathsf{t}\subseteq\mathsf{t}^{\prime}\equiv\exists\mathsf{x}\mathsf{y}(\mathsf{x}=\mathsf{t}\wedge\mathsf{y}=\mathsf{t}^{\prime}\wedge\mathsf{x}\subseteq\mathsf{y})$, where $\exists\mathsf{v}$ abbreviates $\exists v_{1}\dots\exists v_{k}$ for some $k$, and $\mathsf{u}=\mathsf{v}$ is short for $\bigwedge_{i}u_{i}=v_{i}$.

For any assignment $s$ and any set $V\subseteq\mathsf{Var}$ of variables, we write $s\upharpoonright V$ for the assignment $s$ restricted to $V$. For any team $X$, define $X\upharpoonright V=\{s\upharpoonright V\mid s\in X\}$. We list the most important properties of $\mathsf{Inc}$-formulas in the following lemma. The reader is referred to [6, 8] for other properties.

\lemmaname** 2.2**

Let $\phi$ be an $\mathscr{L}$-formula, $M$ an $\mathscr{L}$-model, and $X$, $Y$, $X_{i}$ ($i\in I$) arbitrary teams of $M$ with $\mathsf{dom}(X),\mathsf{dom}(Y),\mathsf{dom}(X_{i})\supseteq\mathsf{Fv}(\phi)$.

**Locality: **

If $X\upharpoonright\mathsf{Fv}(\phi)=Y\upharpoonright\mathsf{Fv}(\phi)$, then $M\models_{X}\phi\iff M\models_{Y}\phi$.

**Union Closure: **

If $M\models_{X_{i}}\phi$ for all $i\in I$, then $M\models_{\bigcup_{i\in I}X_{i}}\phi$.

**Flatness of First-order Formulas: **

For any first-order $\mathscr{L}$-formula $\alpha$,

[TABLE]

Consequently, first-order formulas are also downwards closed, that is, $M\models_{X}\alpha$ and $Y\subseteq X$ imply $M\models_{Y}\alpha$.

If $\theta$ is a sentence, the locality property implies that $M\models_{\{\emptyset\}}\theta$ iff $M\models_{X}\theta$ for all teams $X$ of $M$. We call $M$ a model of $\theta$, written $M\models\theta$, if $M\models_{\{\emptyset\}}\theta$.

By the result of [6], $\mathsf{Inc}$ sentences can be translated into existential second-order logic (ESO), namely, for every $\mathsf{Inc}$-sentence $\theta$, there exists a ESO-sentence $\tau(\theta)$ such that $M\models\theta$ iff $M\models\tau(\theta)$. Since ESO is well-known to be compact, it follows that $\mathsf{Inc}$ is compact as well, that is, if every finite subset of a set $\Gamma$ of $\mathsf{Inc}$-sentences has a model, then the set $\Gamma$ itself has a model. It was further proved in [8] that $\mathsf{Inc}$ is expressively equivalent to positive greatest fixed point logic ($\mathsf{posGFP}$) in the sense of the following theorem.

\theoremname** 2.3**** **([8])

For any $\mathscr{L}$-formula $\phi$ of $\mathsf{Inc}$ with $\mathsf{Fv}(\phi)=\{x_{1},\dots,x_{n}\}$, there exists an $\mathscr{L}(R)$-formula $\psi(R)$ of $\mathsf{posGFP}$ with a fresh $n$-ary relation symbol $R$ such that for all $\mathscr{L}$-models $M$ and teams $X$ of $M$ with $\mathsf{dom}(X)=\{x_{1},\dots,x_{n}\}$,

[TABLE]

and vice versa, where $rel(X)=\{(s(x_{1}),\dots,s(x_{n}))\mid s\in X\}$ is an $n$-ary relation on $M$ that serves as the interpretation for $R$. In particular, $\mathsf{Inc}$-sentences can be translated into $\mathsf{posGFP}$ and vice versa.

As a consequence of [23], over finite models, $\mathsf{Inc}$ and least fixed point logic have the same expressive power. In particular, by [23, 31], over ordered finite models, $\mathsf{Inc}$ captures $\mathsf{PTIME}$.

Due to the strong expressive power, $\mathsf{Inc}$ is not (effectively) axiomatizable. We now give an explicit proof of this fact by following a similar argument to that in [25].222The author would like to thank Jouko Väänänen for suggesting this proof, and the formula used in Proposition 2.4 is taken essentially from [8].

Consider the signature $\mathscr{L}_{a}=(+,\times,<,0,1)$ of arithmetic. We first show that the non-well-foundedness of $<$ is definable in $\mathsf{Inc}$.

\propositionname** 2.4**

For any model $M$ in the signature $\mathscr{L}_{a}$ of arithmetic, $M\models\exists x\exists y(y\subseteq x\wedge y<x)$ iff $<^{M}$ is not well-founded.

• Proof.

It is easy to prove that $\exists x\exists y(y\subseteq x\wedge y<x)$ holds in $M$ iff $M$ contains an infinite $<$-descending chain $\dots<^{M}a_{n}<^{M}\dots<^{M}a_{1}<^{M}a_{0}$. We leave the proof details to the reader. ∎

Now, put $\phi=\exists x\exists y(y\subseteq x\wedge y<x)$, and let $\gamma_{\mathbf{PA}}$ be a (first-order) sentence stating that each of the (finitely many) axioms of Peano arithmetic except for the axiom schema of induction is true (or $\gamma_{\mathbf{PA}}$ is the conjunction of all axioms of Robinson arithmetic $\mathsf{Q}$). For any $\mathscr{L}_{a}$-sentence $\alpha$ of arithmetic, we have that

[TABLE]

where $\mathbb{N}$ is the standard model of Peano arithmetic. To see why, for the left to right direction, suppose that $\mathbb{N}\models\alpha$ and that $M$ is a model of $\gamma_{\mathbf{PA}}$ such that $M\not\models\phi$. By Proposition 2.4, $<^{M}$ is well-founded. Now, $M$ is a model satisfying all axioms of Robinson arithmetic (including the axiom $\forall x(x=0\vee\exists y(y+1=x))$ and the axioms stating that $<$ is a linear ordering), and the ordering $<^{M}$ is a well-ordering. It is then easy to verify that $M$ also satisfies the (second-order) induction axiom. Therefore $M$ is (isomorphic to) the standard model $\mathbb{N}$ of arithmetic, and $M\models\alpha$. Conversely, suppose $\models\alpha\vee\neg\gamma_{\mathbf{PA}}\vee\phi$. The standard model $\mathbb{N}$ of Peano arithmetic clearly satisfies $\gamma_{\mathbf{PA}}$, and by Proposition 2.4 the model $\mathbb{N}$ falsifies $\phi$. Thus we must have that $\mathbb{N}\models\alpha$.

The equivalence (2) shows that truth in the standard model $\mathbb{N}$ can be reduced to logical validity in inclusion logic. This means that validity in inclusion logic is not arithmetical, and therefore inclusion logic cannot have any (effective) complete axiomatization.

Nevertheless, there can be partial axiomatizations for the logic. The main objective of the present paper is to introduce a system of natural deduction for $\mathsf{Inc}$ that is complete for first-order consequences, in the sense that

[TABLE]

holds whenever $\Gamma$ is a set of $\mathsf{Inc}$-formulas, and $\alpha$ is a first-order formula. Our completeness proof will mainly follow the argument of [25], which roughly goes as follows: First, we show that any $\mathsf{Inc}$-sentence is semantically equivalent to a formula $\phi$ in certain normal form. Also, in the system to be introduced every $\mathsf{Inc}$-formula implies its normal form. Then, we show that $\phi$ is equivalent over countable models to a first-order sentence $\Phi$ of infinite length (called its game expression). Next, we show that the game expression $\Phi$ can be approximated in a certain sense (in the sense of Theorem 4.2) by some first-order sentences $\Phi^{n}$ ($n\in\omega$) of finite length. Finally, making essential use of these approximations $\Phi^{n}$ we will be able to prove the completeness theorem by certain model theoretic argument, together with a trick developed in [32] using the weak classical negation $\mathop{\dot{\sim}}$.

3. Normal form

In this section, we prove that every $\mathsf{Inc}$-formula $\phi(\mathsf{z})$ is (semantically) equivalent to a formula of the form $\exists\mathsf{x}\forall y(\iota(\mathsf{x},y)\wedge\alpha(\mathsf{x},\mathsf{z})),$ where $\iota$ is a conjunction of inclusion atoms, and $\alpha$ is a first-order quantifier-free formula. This normal form is similar to the normal forms for dependence and independence logic as introduced in [29, 12]. It is also more refined than the two normal forms for $\mathsf{Inc}$-formulas introduced in the literature, which we recall in the following.

\theoremname** 3.1**** **([7])

Every $\mathsf{Inc}$-formula $\phi(\mathsf{z})$ is semantically equivalent to a formula of the form

[TABLE]

where $Q^{i}\in\{\exists,\forall\}$ and $\theta$ is a quantifier free formula.

• Proof (sketch).

The theorem follows from the fact that

• –

$\neg\forall x\alpha\equiv\exists x\neg\alpha$ and $\neg\exists x\alpha\equiv\forall x\neg\alpha$ for any first-order formula $\alpha$,

and the fact that if $x\notin\textsf{Fv}(\psi)$, then

• –

$\exists x\phi\wedge\psi\equiv\exists x(\phi\wedge\psi)$,

• –

$\exists x\phi\vee\psi\equiv\exists x(\phi\vee\psi)$, (4)

• –

$\forall x\phi\wedge\psi\equiv\forall x(\phi\wedge\psi)$,

• –

\forall x\phi\vee\psi\equiv\exists y\exists z\forall x\big{(}(\phi\wedge y=z)\vee(\psi\wedge y\neq z)\big{)}, where $y,z$ are fresh variables.∎

\theoremname** 3.2**** **([13])

Every $\mathsf{Inc}$-formula $\phi(\mathsf{z})$ of the form (3) is semantically equivalent to a formula of the form

[TABLE]

where $\mathsf{x}=\langle x_{1},\dots,x_{n}\rangle$, $y$ is fresh and $\theta$ is the quantifier free formula in (3).

• Proof (idea).

This theorem is proved by exhaustively applying the equivalences

[TABLE]

and $\forall y_{1}\forall y_{2}(\mathsf{z}_{1}y_{1}\subseteq\mathsf{z}_{1}v_{1}\wedge\mathsf{z}_{2}y_{2}\subseteq\mathsf{z}_{2}v_{2}\wedge\chi(\mathsf{x},\mathsf{z}_{1},\mathsf{z}_{2},v_{1},v_{2}))\equiv\forall y(\mathsf{z}_{1}y\subseteq\mathsf{z}_{1}v_{1}\wedge\mathsf{z}_{2}y\subseteq\mathsf{z}_{2}v_{2}\wedge\chi(\mathsf{x},\mathsf{z}_{1},\mathsf{z}_{2},v_{1},v_{2})).$ ∎

We show next that the quantifier-free formula $\theta$ in the above two theorems can also be turned into an equivalent formula in some normal form.

\lemmaname** 3.3**

Every quantifier-free $\mathsf{Inc}$-formula $\theta(\mathsf{z})$ is semantically equivalent to a formula of the form

[TABLE]

where $\alpha$ is a first-order quantifier-free formula, and each $\mathsf{u}_{i}$ and $\mathsf{v}_{i}$ are sequences of variables from $\mathsf{w}$.

• Proof.

We prove the lemma by induction on $\theta$. The case when $\theta$ is a first-order formula (including the case $\theta=\neg\alpha$) is trivial. If $\theta=\mathsf{x}\subseteq\mathsf{y}$, clearly $\mathsf{x}\subseteq\mathsf{y}\equiv\exists\mathsf{w}\mathsf{u}(\mathsf{w}\subseteq\mathsf{u}\,\wedge\,\mathsf{w}=\mathsf{x}\,\wedge\,\mathsf{u}=\mathsf{y}).$

Assume that $\theta_{0}=\exists\mathsf{w}_{0}(\iota_{0}(\mathsf{w}_{0})\wedge\alpha_{0}(\mathsf{w}_{0},\mathsf{x}))\text{ and }\theta_{1}=\exists\mathsf{w}_{1}(\iota_{1}(\mathsf{w}_{1})\wedge\alpha_{1}(\mathsf{w}_{1},\mathsf{y})),$ where $\alpha_{0},\alpha_{1}$ are first-order and quantifier-free, the sequences $\mathsf{w}_{0}$ and $\mathsf{w}_{1}$ do not have variables in common,

[TABLE]

If $\theta=\theta_{0}\wedge\theta_{1}$, then by (– ‣ Proof (sketch).) we have $\theta_{0}\wedge\theta_{1}\equiv\exists\mathsf{w}_{0}(\iota_{0}\wedge\alpha_{0})\wedge\exists\mathsf{w}_{1}(\iota_{1}\wedge\alpha_{1})\equiv\exists\mathsf{w}_{0}\exists\mathsf{w}_{1}(\iota_{0}\wedge\iota_{1}\wedge\alpha_{0}\wedge\alpha_{1}).$

If $\theta=\theta_{0}\vee\theta_{1}$, we show that $\theta$ is equivalent to

[TABLE]

We first claim that for any first-order formula $\alpha$, any $\mathsf{Inc}$-formula $\phi$,

[TABLE]

where each $\mathsf{u}_{i}$ and $\mathsf{v}_{i}$ consist of variables from the sequence $\mathsf{x}=\langle x_{1},\dots,x_{n}\rangle$. Then can prove $\theta_{0}\vee\theta_{1}\equiv\psi$ by consecutively applying (10) as follows:

[TABLE]

We now complete the proof by verifying claim (10). For the direction left to right, suppose M\models_{X}\exists\mathsf{x}\big{(}\bigwedge_{i\in I}\mathsf{u}_{i}\subseteq\mathsf{v}_{i}\,\wedge\alpha(\mathsf{x},\mathsf{z})\big{)}\vee\phi(\mathsf{y},\mathsf{z}). Then there are teams $Y,Z\subseteq X$ and suitable sequence of functions $\mathsf{F}=\langle F_{1},\dots,F_{n}\rangle$ for $\exists\mathsf{x}$ such that $X=Y\cup Z$, $M\models_{Y(\mathsf{F}/\mathsf{x})}\bigwedge_{i\in I}\mathsf{u}_{i}\subseteq\mathsf{v}_{i}\,\wedge\alpha(\mathsf{x},\mathsf{z})$ and $M\models_{Z}\phi(\mathsf{y},\mathsf{z})$. We now define suitable (sequence of) functions $\mathsf{F}^{\prime}=\langle F_{1}^{\prime},\dots,F_{n}^{\prime}\rangle,G,H$ for the quantifications $\exists\mathsf{x},\exists p,\exists q$ as follows: Pick two distinct elements $a,b\in M$.

• –

Define $\mathsf{F^{\prime}}$ in such a way that the resulting team $(\mathsf{F^{\prime}}/\mathsf{x})$ satisfies

[TABLE]

where $(X\setminus Y)(a/\mathsf{x}):=\{s(a/x_{1})\cdots(a/x_{n})\mid s\in X\setminus Y\}$. We omit here the precise technical definition.

• –

Define $G:X(\mathsf{F^{\prime}}/\mathsf{x})\to\wp(M)\setminus\{\emptyset\}$ by taking $G(s)=\{a\}$.

• –

Define $H:X(\mathsf{F^{\prime}}/\mathsf{x})(G/p)\to\wp(M)\setminus\{\emptyset\}$ by taking

[TABLE]

Put $W=X(\mathsf{F^{\prime}}/\mathsf{x})(G/p)(H/q)$. Clearly, $M\models_{W}\alpha\leftrightarrow p=q$. It remains to show that $M\models_{W}\alpha\vee\phi$ and $M\models_{W}\mathsf{u}_{i}pq\subseteq\mathsf{v}_{i}pq$ for all $i\in I$.

For the former, define

[TABLE]

Clearly $W=U\cup V$, as $X=Y\cup Z$. Since $M\models_{Z}\phi(\mathsf{y},\mathsf{z})$, $M\models_{Y(\mathsf{F}/\mathsf{x})}\alpha(\mathsf{x},\mathsf{z})$ and $Y(\mathsf{F}/\mathsf{x})=Y(\mathsf{F^{\prime}}/\mathsf{x})$, we obtain $M\models_{V}\phi(\mathsf{y},\mathsf{z})$ and $M\models_{U}\alpha(\mathsf{x},\mathsf{z})$ by locality.

For the latter, let $s\in W$ be arbitrary. If $s\in U$, since $M\models_{Y}\mathsf{u}_{i}\subseteq\mathsf{v}_{i}$, there exists $t_{0}\in Y$ such that $t_{0}(\mathsf{v}_{i})=s(\mathsf{u}_{i})$. Now, since $M\models_{U}\alpha(\mathsf{x},\mathsf{z})$, by the definition of $H$ and $G$, we know that $s(q)=a=s(p)$. Thus, for $t=t_{0}(a/p)(a/q)\in W$, we have $t(\mathsf{v}_{i}pq)=\langle t_{0}(\mathsf{v}_{i}),a,a\rangle=s(\mathsf{u}_{i}pq).$

If $s\in W\setminus U$, then $s\upharpoonright\mathsf{dom}(X)\in X\setminus Y$ and thereby $s(\mathsf{x})=\langle a,\dots,a\rangle$ by the definition of $\mathsf{F^{\prime}}$. Thus, $s(\mathsf{v}_{i}pq)=\langle a,\dots,a,s(p),s(q)\rangle=s(\mathsf{u}_{i}pq)$, namely that $s$ itself is the witness of $\mathsf{u}_{i}pq\subseteq\mathsf{v}_{i}pq$ for $s$.

For the direction right to left of the claim (10), suppose there are suitable (sequence of) functions $\mathsf{F}=\langle F_{1},\dots,F_{n}\rangle,G,H$ for the quantifications $\exists\mathsf{x}\exists p\exists q$ such that for $W=X(\mathsf{F}/\mathsf{x})(G/p)(H/q)$, we have that $M\models_{W}\bigwedge_{i\in I}\mathsf{u}_{i}pq\subseteq\mathsf{v}_{i}pq\wedge(\alpha\leftrightarrow p=q)\wedge(\alpha(\mathsf{x},\mathsf{z})\vee\phi(\mathsf{y},\mathsf{z}))$. Then there are teams $U,V\subseteq W$ such that $W=U\cup V$, $M\models_{U}\alpha$ and $M\models_{V}\phi$. Since $\alpha$ is flat, we may let $U\subseteq W$ be the maximal such team.

Consider $Y=U\upharpoonright\mathsf{dom}(X)$ and $Z=V\upharpoonright\mathsf{dom}(X)$. Clearly, $X=Y\cup Z$, and $M\models_{Z}\phi(\mathsf{y},\mathsf{z})$ by locality. It remains to show that M\models_{Y}\exists\mathsf{x}\big{(}\bigwedge_{i\in I}\mathsf{u}_{i}\subseteq\mathsf{v}_{i}\,\wedge\alpha\big{)}.

Define a suitable sequence of functions $\mathsf{F^{\prime}}=\langle F_{1}^{\prime},\dots,F_{n}^{\prime}\rangle$ for $\exists\mathsf{x}$ in such a way that $Y(\mathsf{F^{\prime}}/\mathsf{x})=U\upharpoonright\mathsf{dom}(X)\cup\{x_{1},\dots,x_{n}\}$. We omit the precise technical definition here. Now, since $M\models_{U}\alpha(\mathsf{x},\mathsf{z})$, we have that $M\models_{Y(\mathsf{F^{\prime}}/\mathsf{x})}\alpha(\mathsf{x},\mathsf{z})$ by locality. To show that $Y(\mathsf{F^{\prime}}/\mathsf{x})$ satisfies each $\mathsf{u}_{i}\subseteq\mathsf{v}_{i}$, take any $s\in Y(\mathsf{F^{\prime}}/\mathsf{x})$. Let $\hat{s}\in W$ be an arbitrary extension of $s$. Since $M\models_{W}\mathsf{u}_{i}pq\subseteq\mathsf{v}_{i}pq$, there exists $t\in W$ such that $\hat{s}(\mathsf{u}_{i}pq)=t(\mathsf{v}_{i}pq)$. Since $M\models_{\hat{s}}\alpha(\mathsf{x},\mathsf{z})$ and $M\models_{W}\alpha\leftrightarrow p=q$, we have that $\hat{s}(p)=\hat{s}(q)$. It then follows that $t(p)=t(q)$, which in turn implies that $M\models_{t}\alpha$. Then $t\in U$, as $U$ was assumed to be the maximal subteam of $W$ that satisfies $\alpha(\mathsf{x},\mathsf{z})$. Hence, $t_{0}=t\upharpoonright\mathsf{dom}(X)\cup\{x_{1},\dots,x_{n}\}\in Y(\mathsf{F^{\prime}}/\mathsf{x})$ and $t_{0}(\mathsf{v}_{i})=t(\mathsf{v}_{i})=\hat{s}(\mathsf{u}_{i})=s(\mathsf{u}_{i})$. ∎

Finally, by using the above normal form results we obtain the desired more refined normal form as follows.

\theoremname** 3.4**

Every $\mathsf{Inc}$-formula $\phi(\mathsf{z})$ is semantically equivalent to a formula of the form

[TABLE]

where $\alpha$ is a first-order quantifier-free formula, and each $\mathsf{u}_{i}$ and $\mathsf{v}_{i}$ are sequences of variables from $\mathsf{w}$.

• Proof.

By Theorem 3.1, we may assume that $\phi$ is in prenex normal form (3). Furthermore, by Lemma 3.3, the quantifier free formula $\theta$ in (3) is equivalent to a formula of the form (7). Hence, $\phi(\mathsf{z})$ is equivalent to a formula of the form

[TABLE]

Finally, by applying Theorem 3.2 to the above formula (and rearranging the order of the existential quantifiers) we obtain an equivalent formula of the form (11). ∎

To simplify notations in the normal form (11), we now introduce some conventions. For any permutation $\mathsf{f}:\{1,\dots,n\}\to\{1,\dots,n\}$ and $k\leq n$, we define a function $\sigma^{\mathsf{f},k}_{(\cdot)}:\mathsf{Var}^{n}\to\mathsf{Var}^{k}$ by taking $\sigma^{\mathsf{f},k}_{\mathsf{x}}=x_{\mathsf{f}(1)}\dots x_{\mathsf{f}(k)}$ for any sequence $\mathsf{x}=\langle x_{1}\dots x_{n}\rangle$. That is, $\sigma^{\mathsf{f},k}_{\mathsf{x}}$ is a sequence of variables from $\mathsf{x}$. When no confusion arises we drop the superscripts in $\sigma^{\mathsf{f},k}_{\mathsf{x}}$ and write simply $\sigma_{\mathsf{x}}$. We reserve the greek letters $\pi,\rho,\sigma,\tau$ (with or without superscripts) for such functions. The normal form of an $\mathsf{Inc}$-sentence (with no free variables) can then be written as

[TABLE]

Observe that the formula in the above normal form has only one (explicit) universal quantifier (i.e., $\forall y$). Yet because of the inclusion atoms $\pi^{j}_{\mathsf{x}}y\subseteq\tau^{j}_{\mathsf{x}}$ in the formula, some existentially quantified variables from $\mathsf{x}$ are essentially universally quantified (cf. equivalence (6)).

4. Game expression and approximations

In this section, we define the game expression $\Phi$ for every $\mathsf{Inc}$-sentence $\phi$ (with no free variables) in normal form. Intuitively the formula $\Phi$ is a first-order sentence of infinite length that simulates all possible plays in the semantic game (in team semantics) of the formula $\phi$. Over countable models $\Phi$ and $\phi$ are equivalent, as we will show in Theorem 4.1. For a game of finite length $n$, we define a first-order formula $\Phi^{n}$ of finite length, called the $n$-approximation of $\Phi$. It follows from the model-theoretic argument in [25] that $\Phi$ is equivalent to the (infinitary) conjunction of all its approximations $\Phi^{n}$ over countable recursively saturated models. These game expressions and their finite approximations will be cruicial for proving the completeness theorem for the system of $\mathsf{Inc}$ to be introduced in the next section.

Now, let $\phi$ be an $\mathsf{Inc}$-sentence (with no free variables). By Theorem 3.4, we may assume that $\phi$ is in normal form (12). We now define the game expression of $\phi$ as the following first-order sentence $\Phi$ of infinite length:

[TABLE]

where

• •

$\mathsf{w}^{n}=\langle\mathsf{w}_{\xi}\mid\xi\in E_{n}\cup U_{n}\rangle$ and $\mathsf{x}^{n}=\langle\mathsf{x}_{\xi}\mid\xi\in E_{n}\cup U_{n}\rangle$ with

• –

$E_{n}$ being the set of indices $\langle\xi,i\rangle$ of variables $\mathsf{w}_{\xi,i}$ introduced as witnesses for each $\rho_{\mathsf{w}}^{i}\subseteq\sigma^{i}_{\mathsf{w}}$ with respect to the variables $\mathsf{w}_{\xi}$ from $\mathsf{w}^{n-1}$,

• –

$U_{n}$ being the set of indices $\langle\xi\eta,j\rangle$ of variables $\mathsf{x}_{\xi\eta,j}$ introduced as witnesses for each $\pi^{j}_{\mathsf{x}}y\subseteq\tau^{j}_{\mathsf{x}}$ with respect to all new pairs $\mathsf{x}_{\xi}y_{\eta}$ with $\mathsf{x}_{\xi}$ from $\mathsf{x}_{0}\mathsf{x}^{1}\dots\mathsf{x}^{n-1}$ and $y_{\eta}$ from $y_{0}\dots y_{n}$ (write

[TABLE]

and note that we are requiring that $\xi\eta\notin A_{1}\cup\dots A_{n-1}$);

• •

$\displaystyle\alpha_{n}(\mathsf{w}^{n}\mathsf{x}^{n}):=\bigwedge_{\xi\in E_{n}\cup U_{n}}\alpha(\mathsf{w}_{\xi},\mathsf{x}_{\xi})$;

• •

$\displaystyle\gamma_{n}(\mathsf{w}^{n-1}\mathsf{w}^{n}):=\bigwedge_{\xi\in E_{n-1}}\bigwedge_{i\in I}\rho_{\mathsf{w}_{\xi}}^{i}=\sigma^{i}_{\mathsf{w}_{\xi,i}}$;

• •

$\displaystyle\delta_{n}(y_{0}\dots y_{n-1},\mathsf{x}_{0}\mathsf{x}^{1}\dots\mathsf{x}^{n}):=\bigwedge_{\xi\eta\in A_{n}}\bigwedge_{j\in J}\pi^{j}_{\mathsf{x}_{\xi}}y_{\eta}=\tau^{j}_{\mathsf{x}_{\xi\eta,j}}$.

The formula $\Phi$ is defined in layers that correspond essentially to the plays in the semantic game of the formula $\phi$ (see e.g., [5] for the definition of the semantic game for $\mathsf{Inc}$). Each layer of $\Phi$ consists of the subformula $\exists\mathsf{w}^{n}\mathsf{x}^{n}\forall y_{n}(\alpha_{n}\wedge\gamma_{n}\wedge\delta_{n}\wedge\dots)$ with $\mathsf{w}^{0}\mathsf{x}^{0}=\mathsf{w}_{0}\mathsf{x}_{0}$ and $\alpha_{0}\wedge\gamma_{0}\wedge\delta_{0}=\alpha(\mathsf{w}_{0},\mathsf{x}_{0})\wedge\top\wedge\top\equiv\alpha(\mathsf{w}_{0},\mathsf{x}_{0})$. The intuitive reading of each layer is as follows: Each layer introduces new existentially quantified variables $\mathsf{w}^{n}\mathsf{x}^{n}$ and one universally quantified variable $y_{n}$, and specifies (in $\alpha_{n}$) that $\alpha$ holds for the existentially quantified variables $\mathsf{w}^{n}\mathsf{x}^{n}$. For each inclusion atom $\rho^{i}_{\mathsf{w}}\subseteq\sigma^{i}_{\mathsf{w}}$ in $\phi$, with respect to each sequence $\mathsf{w}_{\xi}$ of existentially quantified variables introduced in layer $n-1$, a witness sequence $\mathsf{w}_{\xi,i}$ of variables (as specified in the formula $\gamma_{n}$), together with the accompanying sequence $\mathsf{x}_{\xi,i}$, are introduced in layer $n$ as part of $\mathsf{w}^{n}\mathsf{x}^{n}$. Similarly, for each inclusion atom $\pi^{j}_{\mathsf{x}}y\subseteq\tau^{j}_{\mathsf{x}}$ in $\phi$, with respect to each new combination $\mathsf{x}_{\xi}y_{\eta}\in A_{n}$ of existentially quantified variables $\mathsf{x}_{\xi}$ introduced up to layer $n-1$ and universally quantified variables $y_{\eta}$ introduced up to layer $n$, a witness sequence $\mathsf{x}_{\xi\eta,j}$ of variables (as specified in the formula $\delta_{n}$) together with the accompanying sequence $\mathsf{w}_{\xi,i}$ are introduced in layer $n$ as part of $\mathsf{w}^{n}\mathsf{x}^{n}$. Note that $E_{n+1}=\{\langle\xi,i\rangle\mid\xi\in E_{n}\cup U_{n},i\in I\}$ and $U_{n+1}=\{\langle\xi\eta,j\rangle\mid\xi\eta\in A_{n+1},j\in J\}$.

We assume that the reader is familiar with the game-theoretic semantics of first-order and infinitary logic. Let us now recall the semantic game $\mathcal{G}(M,\Phi)$ of the formula $\Phi$ over a model $M$, which is an infinite game played between two players $\forall$belard and $\exists$loise. At each round the players take turns to pick elements from $M$ for the quantified variables $\mathsf{w}^{n}\mathsf{x}^{n}$ and $y_{n}$, as illustrated in the following table:

[TABLE]

The choices of the two players generate an assignment $\mathfrak{s}$ for the quantified variables $\mathsf{w}^{n}\mathsf{x}^{n}y_{n}$ defined as

[TABLE]

The player $\exists$loise wins the (infinite) game if for each natural number $n$,

[TABLE]

Finally,

[TABLE]

where a winning strategy for $\exists$loise is a function that tells her what to choose at each round, and also guarantees her to win every play of the game. We now show that an $\mathsf{Inc}$-sentence is semantically equivalent to its game expression over countable models by using the game-theoretic semantics.

\theoremname** 4.1**

Let $\phi$ be an $\mathsf{Inc}$-sentence, and $M$ a model. Then

1. (i)

$M\models\phi\Longrightarrow M\models\Phi$, 2. (ii)

and $M\models\Phi\Longrightarrow M\models\phi$, whenever $M$ is a countable model.

• Proof.

(i) Suppose $M\models\phi$. Then, there exists a suitable sequence $\mathsf{F}$ of functions for $\exists\mathsf{w}\exists\mathsf{x}$ such that for $X=\{\emptyset\}(\mathsf{F}/\mathsf{w}\mathsf{x})$,

[TABLE]

We prove $M\models\Phi$ by constructing a winning strategy for $\exists$loise in the semantic game $\mathcal{G}(M,\Phi)$ as follows:

• –

In round [math], choose any assignment $s_{0}$ in $X$, and let $\exists$loise choose $\mathsf{a}^{0}=s_{0}(\mathsf{w})$ and $\mathsf{b}^{0}=s_{0}(\mathsf{x})$. Let $\mathfrak{s}_{0}$ be the assignment for $\mathsf{w}_{0}\mathsf{x}_{0}$ generated by $\exists$loise’s choices so far. By (13), we have that $M\models_{s_{0}}\alpha(\mathsf{w},\mathsf{x})$, which implies $M\models_{\mathfrak{s}_{0}}\alpha_{0}(\mathsf{w}_{0},\mathsf{x}_{0})$, thus the winning condition is maintained.

• –

Let $\mathfrak{s}_{n-1}$ be the assignment generated by the choices of the two players up to round $n-1$. Assume that we have maintained that for each $\mathsf{w}_{\xi}\mathsf{x}_{\xi}$ in the domain of $\mathfrak{s}_{n-1}$, the assignment $s_{\xi}$ for $\mathsf{wx}$ defined as $s_{\xi}(\mathsf{w}\mathsf{x})=\mathfrak{s}_{n-1}(\mathsf{w}_{\xi}\mathsf{x}_{\xi})$ is in $X$, and assume that $\forall$belard has chosen $c_{n}$ in round $n$.

For any $\xi\eta\in A_{n}$ with $\mathsf{a}_{\xi}\mathsf{b}_{\xi}c_{\eta}$ the corresponding choices by the two players in (at most) two earlier than $n$ rounds, the assignment $s_{\xi}(c_{\eta}/y)$ must be in $X(M/y)$. For each $j\in J$, since $M\models_{X(M/y)}\pi^{j}_{\mathsf{x}}y\subseteq\tau^{j}_{\mathsf{x}}$, there exists $s^{\prime}\in X(M/y)$ such that $s^{\prime}(\tau^{j}_{\mathsf{x}})=\langle s_{\xi}(\pi^{j}_{\mathsf{x}}),c_{\eta}\rangle$. Let $\exists$loise choose $\mathsf{b}_{\xi\eta,j}=s^{\prime}(\mathsf{x})$ and $\mathsf{a}_{\xi\eta,j}=s^{\prime}(\mathsf{w})$. Clearly, $\delta_{n}$ is satisfied by the assignment generated by the players’ choices so far, and $s_{\xi\eta,j}=s^{\prime}\upharpoonright\mathsf{dom}(X)\in X$.

• *

Similarly, for any $\xi\in E_{n-1}$ and any $i\in I$, by using the fact that $s_{\xi}\in X$ and $M\models_{X(M/y)}\rho^{i}_{\mathsf{w}}\subseteq\sigma^{i}_{\mathsf{w}}$, we can let $\exists$loise choose $\mathsf{a}_{\xi,i}\mathsf{b}_{\xi,i}$ so that $\gamma_{n}$ is satisfied by the assignment generated by the players’ choices so far, and $s_{\xi,i}\in X$.

Moreover, since $M\models_{X(M/y)}\alpha(\mathsf{w},\mathsf{x})$ and we have maintained that $s_{\xi}\in X$ for each $\xi\in E_{n}\cup U_{n}$, we conclude that each $\alpha(\mathsf{w}_{\xi},\mathsf{x}_{\xi})$ is satisfied by the assignment $\mathfrak{s}_{n}$ generated by the choices of the players till round $n$.

(ii) Suppose $M$ is a countable model of $\Phi$, and $\exists$loise has a winning strategy in the game $\mathcal{G}(M,\Phi)$. Let $\langle c_{n}\rangle_{n<\omega}$ enumerate all elements of $M$, and let $\forall$belard play $c_{n}$ at each round $n$. Suppose $\mathfrak{s}$ is the assignment generated by such choices of $\forall$belard and the corresponding choices of $\exists$loise given by her winning strategy. Let

[TABLE]

where recall that $s_{\xi}$ is the assignment for $\mathsf{w}\mathsf{x}$ defined as $s_{\xi}(\mathsf{w}\mathsf{x})=\mathfrak{s}(\mathsf{w}_{\xi}\mathsf{x}_{\xi})$. Observe that $X=\{\emptyset\}(\mathsf{F}/\mathsf{wx})$ for some suitable sequence $\mathsf{F}$ of functions for $\exists\mathsf{w}\exists\mathsf{x}$. To show $M\models\phi$, it suffices to verify that the team $X(M/y)$ satisfies (13).

To see that $M\models_{X(M/y)}\alpha(\mathsf{w},\mathsf{x})$, for any $s_{\xi}(c_{\eta}/y)\in X(M/y)$, since $\exists$loise wins the game, we know that $M\models_{\mathfrak{s}}\alpha(\mathsf{w}_{\xi},\mathsf{x}_{\xi})$, which implies $M\models_{s_{\xi}}\alpha(\mathsf{w},\mathsf{x})$, as desired.

To see that $X(M/y)$ satisfies each $\pi^{j}_{\mathsf{x}}y\subseteq\tau^{j}_{\mathsf{x}}$, take any $s_{\xi}(c_{\eta}/y)\in X(M/y)$ and assume $\xi\eta\in A_{n}$. Since $\exists$loise wins the game, $\mathfrak{s}$ satisfies $\delta_{n}$, and in particular, $M\models_{\mathfrak{s}}\pi^{j}_{\mathsf{x}_{\xi}}y_{\eta}=\tau^{j}_{\mathsf{x}_{\xi\eta,j}}$. Thus, for any extension $\hat{s}\in X(M/y)$ of $s_{\xi\eta,j}\in X$, we have that $\hat{s}(\tau^{j}_{\mathsf{x}})=s_{\xi\eta,j}(\tau^{j}_{\mathsf{x}})=\mathfrak{s}(\tau^{j}_{\mathsf{x}_{\xi\eta,j}})=\mathfrak{s}(\pi^{j}_{\mathsf{x}_{\xi}}y_{\eta})=\langle\mathfrak{s}(\pi^{j}_{\mathsf{x}_{\xi}}),c_{\eta}\rangle=s_{\xi}(c_{\eta}/y)(\pi^{j}_{\mathsf{x}}y)$, as required.

By a similar argument, we can also show that $X(M/y)$ satisfies each $\rho^{i}_{\mathsf{w}}\subseteq\sigma^{i}_{\mathsf{w}}$. This then finishes the proof. ∎

For each natural number $n<\omega$, we define the $n$-approximation $\Phi_{n}$ of the infinitary sentence $\Phi$ as the finite first-order formula

[TABLE]

The semantic game for $\Phi_{n}$ over a model $M$, denoted by $\mathcal{G}(M,\Phi_{n})$, is defined exactly as the infinite game $\mathcal{G}(M,\Phi)$ except that $\mathcal{G}(M,\Phi_{n})$ has only $n+1$ rounds. Using the game theoretic-semantics we show, as in [25], that the $\Phi_{n}$’s do approximate $\Phi$ over recursively saturated models, which (recall from, e.g., [1]) are models $M$ such that for any recursive set $\{\phi_{n}(\mathsf{x},\mathsf{y})\mid n<\omega\}$ of formulas,

[TABLE]

\theoremname** 4.2**

If $M$ is a recursively saturated (or finite) model, then

[TABLE]

In particular, if $M$ is a recursively saturated countable (or finite) model, then

[TABLE]

• Proof.

The “in particular” part follows from Theorem 4.1. The direction “$\Longrightarrow$” of the main claim follows from the observation that a winning strategy for $\exists$loise in the infnite game $\mathcal{G}(M,\Phi)$ is clearly also a winning strategy for $\exists$loise in the finite game $\mathcal{G}(M,\Phi_{n})$ for every $n<\omega$. The other direction “$\Longleftarrow$” follows from a similar argument to that of Proposition 15 in [25], which we omit here. ∎

5. A system of natural deduction for $\mathsf{Inc}$

In this section, we introduce a system of natural deduction for inclusion logic and prove the soundness theorem of the system. We also prove in the system that every $\mathsf{Inc}$-formula implies its normal form.

\definitionname** 5.1**

The system of natural deduction for $\mathsf{Inc}$ consists of the rules for equality, connectives and quantifiers in Table 1, and the rules for inclusion atoms in Table 2, where $\alpha$ ranges over first-order formulas, and the letters $\mathsf{x},\mathsf{y},\mathsf{z},\dots$ in serif font stand for arbitrary (possibly empty) sequences of variables. The rules with double horizontal bars are invertible, i.e., they can be applied in both directions.

We write $\Gamma\vdash_{\mathsf{Inc}}\phi$ or simply $\Gamma\vdash\phi$ if $\phi$ is derivable from the set $\Gamma$ of formulas by applying the rules of the system of $\mathsf{Inc}$. We write simply $\phi\vdash\psi$ for $\{\phi\}\vdash\psi$. Two formulas $\phi$ and $\psi$ are said to be provably equivalent, written $\phi\dashv\vdash\psi$, if both $\phi\vdash\psi$ and $\psi\vdash\phi$.

As shown in Table 1, restricted to first-order formulas only our system contains all rules of first-order logic (with equality). But classical rules are in general not sound for non-classical $\mathsf{Inc}$-formulas, such as the rules for negation and $\forall\mathsf{E}$. As a consequence, our system does not admit uniform substitution.

Recall that the usual disjunction elimination rule ($\vee\mathsf{E}$) is not sound for dependence and independence logic (see [25, 12]). In our system of $\mathsf{Inc}$ the disjunction does admit the rule $\vee\mathsf{E}$ under the side condition that the undischarged assumptions in the sub-derivations contain classical formulas only. This side condition however, makes, among other things, the usual derivation of the distributive law $\phi\wedge(\psi\vee\chi)/(\phi\wedge\psi)\vee(\phi\wedge\chi)$ not applicable in the system. This distributive law actually fails in $\mathsf{Inc}$ in general, especially when $\phi$ is not closed downwards. The nonstandard features of the disjunction are also reflected in the rules $\forall_{\vee}\mathsf{Ext}$ and $\exists\!\subseteq\!\mathsf{Ext}$. The invertible rule $\forall_{\vee}\mathsf{Ext}$ extends the scope of a universal quantifier over a disjunction. The rule $\exists\!\subseteq\!\mathsf{Ext}$ extends over a disjunction the scope of a existential quantifier as well as that of inclusion atoms. These two rules are in a sense ad hoc to the present system. Simplifying these rules is left as future work.

The universal quantifier of $\mathsf{Inc}$ turns out to be a peculiar connective, especially the usual elimination rule $\forall x\phi/\phi(t/x)$ is not in general sound for arbitrary formulas. For instance, we have $\models\forall x(y\subseteq x)$, whereas $\not\models y\subseteq z$. The two weaker elimination rules $\forall\mathsf{E}$ and $\forall\mathsf{E}_{0}$ we include in the system restrict the subformula $\phi$ in the premise either to a first-order formula or a formula in which $x$ is not free. To compensate the weakness of the elimination rules we also add to our system a substitution rule $\forall\mathsf{Sub}$, an exchange rule $\forall\mathsf{Exc}$, and two rules $\forall_{\wedge}\mathsf{Ext}$ and $\forall_{\vee}\mathsf{Ext}$ for extending the scope of universal quantifier over conjunction and disjunction. In this nonstandard setting, the derivations of some natural and simple rules for universal quantifier become not entirely trivial, as we will illustrate in the next proposition.

\propositionname** 5.2**

1. (i)

$\forall x\phi\vdash\forall y\phi(y/x)$* if $y\notin\mathsf{Fv}(\forall x\phi)$.* 2. (ii)

$\forall x(\phi\wedge\psi)\dashv\vdash\forall x\phi\wedge\forall x\psi$*. *

• Proof.

(i). Follows from $\forall\mathsf{Sub}$, since $y\notin\mathsf{Fv}(\forall x\phi)$.

(ii). The direction $\forall x\phi\wedge\forall x\psi\vdash\forall x(\phi\wedge\psi)$ follows from $\forall_{\wedge}\mathsf{Ext}$. For the other direction, since $\phi\wedge\psi\vdash\phi$, by $\forall\mathsf{Sub}$ we derive $\forall x(\phi\wedge\psi)\vdash\forall x\phi$. Similarly $\forall x(\phi\wedge\psi)\vdash\forall x\psi$. Thus $\forall x(\phi\wedge\psi)\vdash\forall x\phi\wedge\forall x\psi$ by $\wedge\mathsf{I}$. ∎

The exchange rule $\subseteq\!\mathsf{Exc}$ and contraction rule $\subseteq\!\mathsf{Ctr}$ for inclusion atoms in our system, together with the rule $\mathsf{xy}\subseteq\mathsf{uv}/\mathsf{xyy}\subseteq\mathsf{uvv}$ that we will derive in the next proposition, are clearly equivalent to the projection rule $x_{1}\dots x_{n}\subseteq y_{1}\dots y_{n}/x_{i_{1}}\dots x_{i_{k}}\subseteq y_{i_{1}}\dots y_{i_{k}}$ ($i_{1},\dots,i_{k}\subseteq\{1,\dots,n\}$). As we mentioned in the introduction, the projection rule, the transitivity rule $\subseteq\!\mathsf{Trs}$ and the reflexivity axiom $\mathsf{x}\subseteq\mathsf{x}$ (that we will also derive in the proposition below) form a complete axiomatization of the implication problem of inclusion dependencies in database theory ([4]). The inclusion compression rule $\subseteq\!\mathsf{Cmp}$ is a slight generalization of a similar rule introduced in [12]. The inclusion expansion rule $\subseteq\!\mathsf{Exp}$ characterizes the fact that

[TABLE]

whenever variables in $\mathsf{y}$ are not free in $\Gamma$ (observe that in this case $\Gamma,\mathsf{y}\subseteq\mathsf{x},\neg\alpha(\mathsf{y}/\mathsf{z})\models\bot$ iff $\Gamma,\mathsf{y}\subseteq\mathsf{x}\models\alpha(\mathsf{y}/\mathsf{z})$). The weakening rule via existential quantifier $\subseteq\!\mathsf{W}_{\exists}$ was introduced in [17], and the weakening rule via universal quantifier $\subseteq\!\mathsf{W}_{\forall}$ has a similar flavor. The invertiable simulation rule $\forall\!\!\subseteq\!\mathsf{Sim}$ characterizes the fact that universal quantifiers can be simulated by existential quantifiers with the help of inclusion atoms.

\propositionname** 5.3**

1. (i)

$\vdash\mathsf{x}\subseteq\mathsf{x}$. 2. (ii)

If $|\mathsf{x}|=|\mathsf{y}|=|\mathsf{z}|$, then $\mathsf{xy}\subseteq\mathsf{zz}\vdash\mathsf{x}=\mathsf{y}$.333$|\mathsf{x}|$ denotes the length of the sequence $\mathsf{x}$. 3. (iii)

$\mathsf{xy}\subseteq\mathsf{uv}\vdash\mathsf{x}\mathsf{yy}\subseteq\mathsf{u}\mathsf{vv}$*. *

• Proof.

(i) By $=\!\mathsf{I}$ we have that $\vdash\mathsf{x}=\mathsf{x}$, which implies $\vdash\forall z(\mathsf{x}=\mathsf{x})$ by $\forall\mathsf{I}$. Now, by applying $\forall\!\!\subseteq\!\mathsf{Sim}$ we derive $\vdash\exists z\forall y(\mathsf{x}y\subseteq\mathsf{x}z\,\wedge\,\mathsf{x}=\mathsf{x})$. Thus $\vdash\exists z\forall y(\mathsf{x}\subseteq\mathsf{x})$ by $\subseteq\!\mathsf{Ctr}$. Finally we obtain $\vdash\mathsf{x}\subseteq\mathsf{x}$ by applying $\exists\mathsf{E}$ and $\forall\mathsf{E}_{0}$.

(ii) By $\subseteq\!\mathsf{Cmp}$ we have $\mathsf{xy}\subseteq\mathsf{zz},\,\mathsf{z}=\mathsf{z}\vdash\mathsf{x}=\mathsf{y}$. Then, since $\vdash\mathsf{z}=\mathsf{z}$ by $=\!\mathsf{I}$, we obtain $\mathsf{xy}\subseteq\mathsf{zz}\vdash\mathsf{x}=\mathsf{y}$.

(iii) By $\subseteq\!\mathsf{W}_{\exists}$ we have that $\mathsf{xy}\subseteq\mathsf{uv}\vdash\exists\mathsf{z}(\mathsf{xyz}\subseteq\mathsf{uvv})$. Since $\mathsf{xyz}\subseteq\mathsf{uvv}\vdash\mathsf{y}=\mathsf{z}$ by item (ii), we conclude that $\mathsf{xy}\subseteq\mathsf{uv}\vdash\exists\mathsf{z}(\mathsf{xyz}\subseteq\mathsf{uvv}\wedge\mathsf{y}=\mathsf{z})\vdash\mathsf{xyy}\subseteq\mathsf{uvv}$ by $=\!\mathsf{Sub}$. ∎

We now prove the Soundness Theorem of our system.

\theoremname** 5.4**** **(Soundness)

Let $\Gamma\cup\{\phi\}$ be a set of $\mathsf{Inc}$-formulas. Then

[TABLE]

• Proof.

We only verify the soundness of the nontrivial rules $\vee\mathsf{E}$, $\forall_{\vee}\mathsf{Ext}$, $\subseteq\!\mathsf{Cmp}$, $\subseteq\!\mathsf{Exp}$, $\subseteq\!\mathsf{W}_{\exists}$, $\subseteq\!\mathsf{W}_{\forall}$ and $\forall\!\!\subseteq\!\mathsf{Sim}$. The soundness of $\exists\!\subseteq\!\mathsf{Ext}$ follows from (10) in the proof of the disjunction case of Lemma 3.3.

$\vee\mathsf{E}$: It suffices to show that $\Delta_{0},\phi\models\chi$ and $\Delta_{1},\psi\models\chi$ imply $\Delta_{0},\Delta_{1},\phi\vee\psi\models\chi$ for any two sets $\Delta_{0},\Delta_{1}$ of first-order formulas. Suppose that $M\models_{X}\Delta_{0}\cup\Delta_{1}$, and also that $M\models_{X}\phi\vee\psi$. Then there exist $Y,Z\subseteq X$ such that $X=Y\cup Z$, $M\models_{Y}\phi$ and $M\models_{Z}\psi$. Since formulas in $\Delta_{0}\cup\Delta_{1}$ are closed downwards, we have that $M\models_{Y}\Delta_{0}$ and $M\models_{Z}\Delta_{1}$. It then follows from the assumption that $M\models_{Y}\chi$ and $M\models_{Z}\chi$. Now, since $\chi$ is closed under unions, we conclude that $M\models_{X}\chi$, as required.

$\forall_{\vee}\mathsf{Ext}$: We first show that $\forall x\phi(x,\mathsf{v})\vee\psi(\mathsf{v})\models\exists y\exists z\forall x((\phi\wedge y=z)\vee(\psi\wedge y\neq z))$, where $x\notin\textsf{Fv}(\psi)$ and $y,z\notin\textsf{Fv}(\phi)\cup\textsf{Fv}(\psi)$. Suppose $M\models_{X}\forall x\phi\vee\psi$, where we may w.l.o.g. assume $x,y,z\notin dom(X)$. Then there exist $Y,Z\subseteq X$ such that $X=Y\cup Z$, $M\models_{Y(M/x)}\phi$ and $M\models_{Z}\psi$. Define functions $F:X\to\wp(M)\setminus\{\emptyset\}$ and $G:X(F/y)\to\wp(M)\setminus\{\emptyset\}$ as follows: Let $a,b$ be two distinct elements in $M$.

[TABLE]

Now, we split the team $X^{\prime}=X(F/y)(G/z)(M/x)$ into $W=\{s\in X^{\prime}\mid s(y)=a\}$ and $U=\{s\in X^{\prime}\mid s(y)=b\}$. Clearly, $M\models_{W}y=z$ and $M\models_{U}y\neq z$. Observe that $W\upharpoonright(dom(X)\cup\{x\})=Y(M/x)$ and $U\upharpoonright dom(X)=Z$. Since $M\models_{Y(M/x)}\phi$ and $M\models_{Z}\psi$, we conclude that $M\models_{W}\phi$ and $M\models_{U}\psi$.

Conversely, suppose $M\models_{X}\exists y\exists z\forall x((\phi(x,\mathsf{v})\wedge y=z)\vee(\psi(\mathsf{v})\wedge y\neq z))$. Then there are suitable functions $F,G$ and teams $Y,Z\subseteq X(F/y)(G/z)(M/x)$ such that $X(F/y)(G/z)(M/x)=Y\cup Z$, $M\models_{Y}\phi\wedge y=z$ and $M\models_{Z}\psi\wedge y\neq z$. Put $Y^{\prime}=Y\upharpoonright dom(X)$ and $Z^{\prime}=Z\upharpoonright dom(X)$. Clearly $X=Y^{\prime}\cup Z^{\prime}$. To show that $M\models_{X}\forall x\phi(x,\mathsf{v})\vee\psi(\mathsf{v})$, it then suffices to verify $M\models_{Y^{\prime}}\forall x\phi$ and $M\models_{Z^{\prime}}\psi$. The latter is clear, since $M\models_{Z}\psi$ and $x,y,z\notin\mathsf{Fv}(\psi)$. To see the former, first observe that for any $s\in Y$ and any $a\in M$, since $s(a/x)(y)=s(y)=s(z)=s(a/x)(z)$, we must have that $s(a/x)\notin Z$, or $s(a/x)\in Y$. This shows that $Y=Y(M/x)$, thus $Y\upharpoonright(dom(X)\cup\{x\})=(Y\upharpoonright dom(X))(M/x)=Y^{\prime}(M/x)$. Now, since $Y\upharpoonright(dom(X)\cup\{x\})$ satisfies $\phi$, we conclude $M\models_{Y^{\prime}(M/x)}\phi$, and thus $M\models_{Y^{\prime}}\forall x\phi$ as required.

$\subseteq\!\mathsf{Cmp}$: Suppose $M\models_{X}\mathsf{y}\subseteq\mathsf{x}$ and $M\models_{X}\alpha(\mathsf{x}/\mathsf{z})$, where the free variables of $\alpha(\mathsf{x}/\mathsf{z})$ are among $\mathsf{x}$. We show that $M\models_{X}\alpha(\mathsf{y}/\mathsf{z})$. For any $s\in X$, since $M\models_{X}\mathsf{y}\subseteq\mathsf{x}$, there exists $s^{\prime}\in X$ such that $s^{\prime}(\mathsf{x})=s(\mathsf{y})$. Since $M\models_{X}\alpha(\mathsf{x}/\mathsf{z})$ and $\alpha$ is first-order, we have that $M\models_{s^{\prime}}\alpha(\mathsf{x}/\mathsf{z})$, which implies $M\models_{s}\alpha(\mathsf{y}/\mathsf{z})$ by the locality property. Hence, we conclude that $M\models_{X}\alpha(\mathsf{y}/\mathsf{z})$.

$\subseteq\!\mathsf{Exp}$: Assume $\Gamma,\mathsf{y}\subseteq\mathsf{x},\neg\alpha(\mathsf{y}/\mathsf{z})\models\bot$, where the free variables of $\alpha(\mathsf{y}/\mathsf{z})$ are among $\mathsf{y}$, and the variables in $\mathsf{y}$ do not occur freely in $\Gamma$. We show that $\Gamma\models\alpha(\mathsf{x}/\mathsf{z})$. Suppose that $M\models_{X}\Gamma$ for some nonempty team $X$. It suffices to show that $M\models_{s}\alpha(\mathsf{x}/\mathsf{z})$ for any $s\in X$. Consider the team $X(s(\mathsf{x})/\mathsf{y})$. Clearly, $M\models_{X(s(\mathsf{x})/\mathsf{y})}\mathsf{y}\subseteq\mathsf{x}$. On the other hand, since the variables in $\mathsf{y}$ do not occur freely in $\Gamma$, by locality we obtain that $M\models_{X(s(\mathsf{x})/\mathsf{y})}\Gamma$. Now, since $X(s(\mathsf{x})/\mathsf{y})\neq\emptyset$, the assumption $\Gamma,\mathsf{y}\subseteq\mathsf{x},\neg\alpha(\mathsf{y}/\mathsf{z})\models\bot$ gives that $M\not\models_{X(s(\mathsf{x})/\mathsf{y})}\neg\alpha(\mathsf{y}/\mathsf{z})$, which by locality implies that $M\models_{s}\alpha(\mathsf{x}/\mathsf{z})$, as required.

$\subseteq\!\mathsf{W}_{\exists}$: It suffices to show that $\Gamma\models\mathsf{x}\subseteq\mathsf{y}$ implies $\Gamma\models\exists w(\mathsf{x}w\subseteq\mathsf{y}z)$, where $w$ is not among $\mathsf{xy}z$. Suppose $M\models_{X}\Gamma$. By the assumption, $M\models_{X}\mathsf{x}\subseteq\mathsf{y}$, meaning that for any $s\in X$, there exists $s^{\prime}\in X$ such that $s^{\prime}(\mathsf{y})=s(\mathsf{x})$. Now, to show that $M\models_{X}\exists w(\mathsf{x}w\subseteq\mathsf{y}z)$, we define a function $F:X\to\wp(M)\setminus\{\emptyset\}$ by taking $F(s)=\{s^{\prime}(z)\}.$

To show that $M\models_{X(F/w)}\mathsf{x}w\subseteq\mathsf{y}z$, take any $s\in X(F/w)$. Consider the witness $s_{0}^{\prime}\in X$ for $\mathsf{x}\subseteq\mathsf{y}$ with respect to $s_{0}=s\upharpoonright dom(X)$. We have $s(\mathsf{x}w)=s_{0}(\mathsf{x})s(w)=s_{0}^{\prime}(\mathsf{y})s_{0}^{\prime}(z).$ Hence, any extension of $s_{0}^{\prime}$ in $X(F/w)$ witnesses $\mathsf{x}w\subseteq\mathsf{y}z$.

$\subseteq\!\mathsf{W}_{\forall}$: It suffices to show that $\Gamma\models\mathsf{x}\subseteq\mathsf{y}$ implies $\Gamma\models\forall w(\mathsf{x}z\subseteq\mathsf{y}w)$, where $w$ is not among $\mathsf{xy}z$. Suppose $M\models_{X}\Gamma$, where we may assume w.l.o.g. that $w\notin dom(X)$ (if not, rename the bound variable $w$ in $\forall w(\mathsf{x}z\subseteq\mathsf{y}w)$). It then follows by locality that $M\models_{X(M/w)}\Gamma$ as well, and thus $M\models_{X(M/w)}\mathsf{x}\subseteq\mathsf{y}$ by assumption. To show $M\models_{X(M/w)}\mathsf{x}z\subseteq\mathsf{y}w$, take an arbitrary $s\in X(M/w)$. Since $M\models_{X(M/w)}\mathsf{x}\subseteq\mathsf{y}$, there exists $s^{\prime}\in X(M/w)$ such that $s^{\prime}(\mathsf{y})=s(\mathsf{x})$. Clearly, the assignment $s^{\prime\prime}=s^{\prime}(s(z)/w)$ belongs to the team $X(M/w)$, and $s^{\prime\prime}(\mathsf{y}w)=s^{\prime}(\mathsf{y})s(z)=s(\mathsf{x}z)$, as required.

$\forall\!\!\subseteq\!\mathsf{Sim}$: For the top to bottom direction, suppose $M\models_{X}\forall\mathsf{x}\phi(\mathsf{x},\mathsf{z})$. We show that M\models_{X}\exists\mathsf{x}\forall\mathsf{y}\big{(}\mathsf{z}\mathsf{y}\subseteq\mathsf{z}\mathsf{x}\wedge\phi(\mathsf{x},\mathsf{z})\big{)}, where variables from $\mathsf{y}$ are fresh. Let $\mathsf{x}=\langle x_{1},\dots,x_{n}\rangle$. Define a sequence $\mathsf{F}=\langle F_{1},\dots,F_{n}\rangle$ of functions for $\exists\mathsf{x}$ by taking $F_{i}(s)=M$ for each $F_{i}$ from $\mathsf{F}$, namely, we let $X(\mathsf{F}/\mathsf{x})=X(M/\mathsf{x})$. It suffices to show that $M\models_{X(\mathsf{F}/\mathsf{x})(M/\mathsf{y})}\mathsf{z}\mathsf{y}\subseteq\mathsf{z}\mathsf{x}\wedge\phi(\mathsf{x},\mathsf{z})$, or $M\models_{X(M/\mathsf{x})(M/\mathsf{y})}\mathsf{z}\mathsf{y}\subseteq\mathsf{z}\mathsf{x}\wedge\phi(\mathsf{x},\mathsf{z})$

By assumption, $M\models_{X(M/\mathsf{x})}\phi(\mathsf{x},\mathsf{z})$, which implies $M\models_{X(M/\mathsf{x})(M/\mathsf{y})}\phi(\mathsf{x},\mathsf{z})$. To show that $\mathsf{z}\mathsf{y}\subseteq\mathsf{z}\mathsf{x}$ is also satisfied by $X(M/\mathsf{x})(M/\mathsf{y})$, take any $s\in X(M/\mathsf{x})(M/\mathsf{y})$. Observe that the function $s^{\prime}=s(s(\mathsf{y})/\mathsf{x})$ belongs to the team $X(M/\mathsf{x})(M/\mathsf{y})$, and we have that $s^{\prime}(\mathsf{z}\mathsf{x})=s(\mathsf{z})s(\mathsf{y})$, as required.

For the bottom to top direction, suppose M\models_{X}\exists\mathsf{x}\forall\mathsf{y}\big{(}\mathsf{z}\mathsf{y}\subseteq\mathsf{z}\mathsf{x}\wedge\phi(\mathsf{x},\mathsf{z})\big{)}, where no variable from $\mathsf{y}$ are free in $\phi$, and we may assume w.l.o.g. that $\mathsf{dom}(X)$ consists of all variables from $\mathsf{z}$. Then there are suitable sequence $\mathsf{F}$ of functions for $\exists\mathsf{x}$ such that $M\models_{X(\mathsf{F}/\mathsf{x})(M/\mathsf{y})}\mathsf{z}\mathsf{y}\subseteq\mathsf{z}\mathsf{x}\wedge\phi(\mathsf{x},\mathsf{z})$. We show that $M\models_{X}\forall\mathsf{x}\phi(\mathsf{x},\mathsf{z})$, or $M\models_{X(M/\mathsf{x})}\phi(\mathsf{x},\mathsf{z})$, which, by locality, is further reduced to showing that $X(\mathsf{F}/\mathsf{x})=X(M/\mathsf{x})$.

For any $s\in X(M/\mathsf{x})$, consider an arbitrary assignment $t\in X(\mathsf{F}/\mathsf{x})(M/\mathsf{y})$ satisfying $t(\mathsf{z})=s(\mathsf{z})$ and $t(\mathsf{y})=s(\mathsf{x})$. Since $M\models_{X(\mathsf{F}/\mathsf{x})(M/\mathsf{y})}\mathsf{z}\mathsf{y}\subseteq\mathsf{z}\mathsf{x}$, there exists $t^{\prime}\in X(\mathsf{F}/\mathsf{x})(M/\mathsf{y})$ such that $t^{\prime}(\mathsf{z}\mathsf{x})=t(\mathsf{z}\mathsf{y})=s(\mathsf{z})s(\mathsf{x}),$ meaning that $s=t^{\prime}\upharpoonright\mathsf{dom}(X)\cup\{x_{1},\dots,x_{n}\}\in X(\mathsf{F}/\mathsf{x})$. Thus, $X(M/\mathsf{x})\subseteq X(\mathsf{F}/\mathsf{x})$, thereby $X(M/\mathsf{x})=X(\mathsf{F}/\mathsf{x})$. ∎

We will prove the completeness theorem of our system in the next section. An important lemma for this proof is that every formula provably implies its normal form (12). To prove this lemma we first prove a few useful propositions. The next three propositions concern the standard properties of quantifications as well as the monotonicity of the entailment relation in $\mathsf{Inc}$. In the sequel, we will often apply Propositions 5.5 and 5.6 without explicit reference to them.

\propositionname** 5.5**

Let $\alpha$ be a first-order formula, and $x\notin\textsf{Fv}(\psi)$.

1. (i)

$\neg\forall x\alpha\dashv\vdash\exists x\neg\alpha$* and $\neg\exists x\alpha\dashv\vdash\forall x\neg\alpha$.* 2. (ii)

$\forall x\phi\wedge\psi\dashv\vdash\forall x(\phi\wedge\psi)$. 3. (iii)

$\exists x\phi\wedge\psi\dashv\vdash\exists x(\phi\wedge\psi)$. 4. (iv)

$\exists x\phi\vee\psi\dashv\vdash\exists x(\phi\vee\psi)$.

• Proof.

Since our system behaves exactly like first-order logic when restricted to first-order formulas only, item (i) can be proved as usual. Items (iii) and (iv) are proved also as usual. We only derive item (ii). For the right to left direction, we have by Proposition 5.2(ii) that $\forall x(\phi\wedge\psi)\vdash\forall x\phi\wedge\forall x\psi$. Since $x\notin\textsf{Fv}(\psi)$, $\forall x\psi\vdash\psi$ by $\forall\mathsf{E}_{0}$. Thus $\forall x(\phi\wedge\psi)\vdash\forall x\phi\wedge\psi$. For the other direction, since $\phi,\psi\vdash\phi\wedge\psi$ and $x\notin\textsf{Fv}(\psi)$, we derive by applying $\forall\mathsf{Sub}$ that $\forall x\phi,\psi\vdash\forall x(\phi\wedge\psi)$, thus $\forall x\phi\wedge\psi\vdash\forall x(\phi\wedge\psi)$. ∎

We write $\phi(\theta)$ to indicate that $\phi$ is a formula with an occurrence of $\theta$ as a subformula, and write $\phi[\theta^{\prime}/\theta]$ for the formula obtained from $\phi$ by replacing the occurrence of $\theta$ by $\theta^{\prime}$.

\propositionname** 5.6**

If $\theta\dashv\vdash\theta^{\prime}$, then $\phi(\theta)\dashv\vdash\phi[\theta^{\prime}/\theta]$. Moreover, if the occurrence of $\theta$ in $\phi(\theta)$ is not in the scope of a negation, then $\theta\vdash\theta^{\prime}$ implies $\phi(\theta)\vdash\phi[\theta^{\prime}/\theta]$.

• Proof.

A routine inductive proof. Apply $\forall\mathsf{Sub}$ in the case $\phi=\forall x\psi$. ∎

\propositionname** 5.7**

Let $\phi$ be a formula and $\mathsf{Q}\mathsf{x}\theta$ the semantically equivalent formula in prenex normal form as given in Theorem 3.1, where $\mathsf{Qx}=Q^{1}x_{1}\cdots Q^{n}x_{n}$ ($Q^{i}\in\{\forall,\exists\}$) is a sequence of quantifiers and $\theta$ is a quantifier free formula. Then $\phi\dashv\vdash\mathsf{Q}\mathsf{x}\theta$.

• Proof.

Repeatedly apply Propositions 5.5, 5.6 and $\forall_{\vee}\mathsf{Ext}$ (c.f. the proof of Theorem 3.1). ∎

The next technical proposition shows, as a generalization of the rule $\forall\!\!\subseteq\!\mathsf{Sim}$, that universal quantifiers in a more general context can also be simulated using existential quantifiers and inclusion atoms.

\propositionname** 5.8**

\forall\mathsf{x}\mathsf{Qu}\phi(\mathsf{u},\mathsf{x},\mathsf{z})\dashv\vdash\exists\mathsf{x}\mathsf{Qu}\forall\mathsf{y}\big{(}\mathsf{z}\mathsf{y}\subseteq\mathsf{z}\mathsf{x}\wedge\phi(\mathsf{u},\mathsf{x},\mathsf{z})\big{)}.

• Proof.

We derive the proposition as follows:

[TABLE]

∎

\lemmaname** 5.9**

For any $\mathsf{Inc}$-formula $\phi$, we have that $\phi\vdash\phi^{\prime}$, where $\phi^{\prime}$ is the semantically equivalent formula in normal form (11) as given in Theorem 3.4.

• Proof.

We follow a similar argument to that of the semantic proof of Theorem 3.4. First, by Proposition 5.7, we obtain $\phi\vdash\mathsf{Qx}\theta$, where $\mathsf{Qx}\theta$ is the semantically equivalent formula of $\phi$ as given in Theorem 3.1 with $\mathsf{Qx}=Q^{1}x_{1}\cdots Q^{n}x_{n}$ ($Q^{i}\in\{\forall,\exists\}$) a sequence of quantifiers and $\theta$ a quantifier free formula.

If we can show that $\theta\vdash\exists\mathsf{w}\theta^{\prime}$ for some formula $\theta^{\prime}=\bigwedge_{i\in I}\mathsf{u_{i}}\subseteq\mathsf{v_{i}}\,\wedge\alpha(\mathsf{w},\mathsf{x},\mathsf{z})$ as given in Lemma 3.3, we may obtain $\phi\vdash\mathsf{Qx}\exists\mathsf{w}\theta^{\prime}$ by Proposition 5.6. Next, we derive

[TABLE]

Putting all these together, we will complete the proof.

Now, we show that $\theta\vdash\exists\mathsf{w}\theta^{\prime}$ by induction on $\theta$. The case $\theta$ is a first-order formula (including the case $\theta=\neg\alpha$) is trivial. If $\theta=\mathsf{x}\subseteq\mathsf{y}$, we have that \mathsf{x}\subseteq\mathsf{y}\vdash\exists\mathsf{w}\mathsf{u}\big{(}\mathsf{w}\subseteq\mathsf{u}\,\wedge\,\mathsf{w}=\mathsf{x}\,\wedge\,\mathsf{u}=\mathsf{y}\big{)}. Indeed, we first derive that $\vdash\mathsf{x}=\mathsf{x}\wedge\mathsf{y}=\mathsf{y}\vdash\exists\mathsf{w}\exists\mathsf{u}(\mathsf{w}=\mathsf{x}\wedge\mathsf{u}=\mathsf{y})$ by $=\!\mathsf{I}$ and $\exists\mathsf{I}$. Then, by $=\!\mathsf{Sub}$ we derive that \mathsf{x}\subseteq\mathsf{y}\vdash\exists\mathsf{w}\mathsf{u}\big{(}\mathsf{x}\subseteq\mathsf{y}\,\wedge\,\mathsf{w}=\mathsf{x}\,\wedge\,\mathsf{u}=\mathsf{y}\big{)}\vdash\exists\mathsf{w}\mathsf{u}\big{(}\mathsf{w}\subseteq\mathsf{u}\,\wedge\,\mathsf{w}=\mathsf{x}\,\wedge\,\mathsf{u}=\mathsf{y}\big{)}.

Assume that $\theta_{0}\vdash\exists\mathsf{w_{0}}(\iota_{0}(\mathsf{w}_{0})\wedge\alpha_{0}(\mathsf{w}_{0},\mathsf{x}))\text{ and }\theta_{1}\vdash\exists\mathsf{w_{1}}(\iota_{1}(\mathsf{w}_{1})\wedge\alpha_{1}(\mathsf{w}_{1},\mathsf{y})),$ where $\alpha_{0},\alpha_{1}$ are first-order and quantifier-free, the sequences $\mathsf{w}_{0}$ and $\mathsf{w}_{1}$ do not have variables in common, and $\iota_{0}$ and $\iota_{1}$ are as in (8) in the proof of Lemma 3.3.

If $\theta=\theta_{0}\wedge\theta_{1}$, then we derive that $\theta_{0}\wedge\theta_{1}\vdash\exists\mathsf{w_{0}}(\iota_{0}\wedge\alpha_{0})\wedge\exists\mathsf{w_{1}}(\iota_{1}\wedge\alpha_{1})\vdash\exists\mathsf{w_{0}}\exists\mathsf{w_{1}}(\iota_{0}\wedge\iota_{1}\wedge\alpha_{0}\wedge\alpha_{1})$ by Proposition 5.5(iii).

If $\theta=\theta_{0}\vee\theta_{1}$, let $\psi$ be the formula (9) as in the proof of the disjunction case of Lemma 3.3. We derive $\theta\vdash\psi$ by following the semantic argument as in Lemma 3.3, in which we apply the rule $\exists\!\subseteq\!\mathsf{Ext}$ in the crucial steps.∎

We end this section by proving some facts concerning the weak classical negation $\mathop{\dot{\sim}}$ in the context of $\mathsf{Inc}$. This connective was introduced in [32], and a trick using $\mathop{\dot{\sim}}$ was developed in the paper to generalize the proof of the completeness theorem of dependence logic given in [25]. We will also apply this trick to prove the completeness theorem for our system in the next section. Recall that the team semantics of $\mathop{\dot{\sim}}$ is defined as

• •

$M\models_{X}\mathop{\dot{\sim}}\phi$   iff   $X=\emptyset$ or $M\not\models_{X}\phi$.

The weak classical negations $\mathop{\dot{\sim}}\phi$ of $\mathsf{Inc}$-formulas $\phi$ are not in general expressible in $\mathsf{Inc}$ (because positive greatest fixed point logic, being expressively equivalent to $\mathsf{Inc}$, is not closed under classical negation). Nevertheless, the weak classical negations $\mathop{\dot{\sim}}\alpha$ of first-order formulas $\alpha$ are expressible (uniformly) in $\mathsf{Inc}$,:

Fact 5.10

If $\alpha(\mathsf{x})$ is a first-order formula, then $\mathop{\dot{\sim}}\alpha(\mathsf{x})\equiv\exists\mathsf{y}(\mathsf{y}\subseteq\mathsf{x}\wedge\neg\alpha(\mathsf{y}/\mathsf{x}))$, where $\mathsf{y}$ is a sequence of fresh variables.

• Proof.

Since $\alpha$ is flat, for any nonempty team $X$, $M\not\models_{X}\alpha(\mathsf{x})$, iff $M\models_{s}\neg\alpha(\mathsf{x})$ for some $s\in X$, iff $M\models_{X}\exists\mathsf{y}(\mathsf{y}\subseteq\mathsf{x}\wedge\neg\alpha(\mathsf{y}/\mathsf{x}))$. ∎

Stipulating the string $\mathop{\dot{\sim}}\alpha(\mathsf{x})$ as a shorthand for the formula $\exists\mathsf{y}(\mathsf{y}\subseteq\mathsf{x}\wedge\neg\alpha(\mathsf{y}))$ of $\mathsf{Inc}$, we show next that the reductio ad absurdum ($\mathsf{RAA}$) rule for $\mathop{\dot{\sim}}$ with respect to first-order formulas $\alpha$, i.e., the rule

[TABLE]

is derivable in our system from the rule $\subseteq\!\mathsf{Exp}$.

\lemmaname** 5.11**

If $\Gamma,\mathop{\dot{\sim}}\alpha\vdash\bot$, then $\Gamma\vdash\alpha$.

• Proof.

Let $\alpha=\alpha(\mathsf{x})$ and $\mathop{\dot{\sim}}\alpha(\mathsf{x})=\exists\mathsf{y}(\mathsf{y}\subseteq\mathsf{x}\wedge\neg\alpha(\mathsf{y}/\mathsf{x}))$, where $\mathsf{y}$ is a sequence of fresh variables. Suppose $\Gamma,\mathop{\dot{\sim}}\alpha\vdash\bot$. By $\subseteq\!\mathsf{Exp}$, it suffices to show that $\Gamma,\mathsf{y}\subseteq\mathsf{x},\neg\alpha(\mathsf{y}/\mathsf{x})\vdash\bot$. But this follows easily from $\exists\mathsf{I}$ and the assumption $\Gamma,\mathop{\dot{\sim}}\alpha\vdash\bot$. ∎

6. The completeness theorem

In this section, we prove the completeness theorem for our system of $\mathsf{Inc}$ with respect to first-order consequences. To be precise, we prove that

[TABLE]

holds whenever $\Gamma$ is a set of $\mathsf{Inc}$-formulas, and $\alpha$ is a first-order formula. As sketched in Section 2, our proof combines the technique introduced in [25] and a trick developed in [32] using the weak classical negation $\mathop{\dot{\sim}}$ and the $\mathsf{RAA}$ rule for $\mathop{\dot{\sim}}$. The former treats the case when the set $\Gamma\cup\{\alpha\}$ of formulas in (14) are sentences (with no free variables) only, while the trick of the latter allows us to handle (open) formulas as well. Since the weak classical negation $\mathop{\dot{\sim}}\alpha$ of first-order formulas $\alpha$ are definable uniformly in $\mathsf{Inc}$ (Fact 5.10), and the $\mathsf{RAA}$ rule for $\mathop{\dot{\sim}}$ is derivable in our system of $\mathsf{Inc}$ (Lemma 5.11), we will be able to apply the trick of [32] in a smoother manner than in the systems of dependence and independence logic [32] (in which the $\mathsf{RAA}$ rule for $\mathop{\dot{\sim}}$ was added in an ad hoc and non-effective manner).

We have prepared in the previous sections most relevant lemmas for the argument in [25] concerning the normal form of $\mathsf{Inc}$-formulas (especially Lemma 5.9), the game expression and its approximations. Another important lemma for the completeness theorem is that any $\mathsf{Inc}$-formula $\phi$ implies every approximation $\Phi_{n}$ of its game expression (as introduced in Section 4).

\lemmaname** 6.1**

For any $\mathsf{Inc}$-sentence $\phi$, we have that $\phi\vdash\Phi_{n}$ for every $n<\omega$.

In order to prove the above lemma, we first need to prove a number of technical propositions and lemmas.

\propositionname** 6.2**

Let $\rho:\mathsf{Var}^{n}\to\mathsf{Var}^{k},\sigma:\mathsf{Var}^{n}\to\mathsf{Var}^{m}$ be functions. Then

[TABLE]

where $|\mathsf{x}|=|\mathsf{x}_{0}|=|\mathsf{x}_{1}|$, $|\mathsf{y}|=|\mathsf{y}_{0}|=|\mathsf{y}_{1}|$ and $|\mathsf{z}|=|\mathsf{z}_{0}|$. In particular, when $\mathsf{z}$ and $\mathsf{z}_{0}$ are the empty sequence we have that $\rho_{\mathsf{x}}\subseteq\sigma_{\mathsf{x}},\mathsf{x}_{0}\mathsf{y}_{0}\subseteq\mathsf{x}\mathsf{y}\vdash\exists\mathsf{x}_{1}\mathsf{y}_{1}(\mathsf{x}_{1}\mathsf{y}_{1}\subseteq\mathsf{x}\mathsf{y}\,\wedge\,\rho_{\mathsf{x}_{0}}=\sigma_{\mathsf{x}_{1}})$.

• Proof.

Assume that $\mathsf{p}(\mathsf{x})=\sigma_{\mathsf{x}}\tau_{\mathsf{x}}$ for some permutation $\mathsf{p}$ of the sequence $\mathsf{x}$. Then we have

[TABLE]

∎

We say that an occurrence of a subformula $\theta$ in $\phi(\theta)$ is not in the scope of a disjunction or negation if (1) $\phi=\theta$; or (2) $\phi=\psi(\theta)\wedge\chi$ or $\chi\wedge\psi(\theta)$, and $\theta$ is not in the scope of a disjunction or negation in $\psi(\theta)$; or (3) $\phi=Qx\psi(\theta)$ ($Q\in\{\forall,\exists\}$) and $\theta$ is not in the scope of a disjunction or negation in $\psi(\theta)$. For example, in the formula $(\phi(\theta)\vee\psi)\wedge\exists x\theta$, the leftmost occurrence of $\theta$ is in the scope of a disjunction, while the rightmost occurrence of $\theta$ is not.

\lemmaname** 6.3**

If the occurrence of the subformula $\theta$ in $\phi(\theta)$ is not in the scope of a disjunction or negation, then $\phi(\theta),\psi\vdash\phi[\theta\wedge\psi/\theta]$.

• Proof.

A routine inductive proof. Apply $\forall\mathsf{Sub}$, $\exists\mathsf{E}$, $\exists\mathsf{I}$ in the quantifier cases. ∎

\propositionname** 6.4**

Suppose that $\phi(\mathsf{x}\subseteq\mathsf{y})$ is a formula in which the occurrence of $\mathsf{x}\subseteq\mathsf{y}$ is not in the scope of a disjunction or negation, and the variables from $\mathsf{y}$ are free in $\phi$. If $\mathsf{z}$ does not have any common variable with $\mathsf{x}\mathsf{y}$, and $\mathsf{w}$ contains some variables occurring in $\phi$ (either free or bound), then $\forall\mathsf{z}\phi(\mathsf{x}\subseteq\mathsf{y})\vdash\forall\mathsf{z}\phi[\mathsf{x}\mathsf{w}\subseteq\mathsf{y}\mathsf{z}/\mathsf{x}\subseteq\mathsf{y}]$.

• Proof.

We prove the proposition by induction on $\phi$. If $\phi=\mathsf{x}\subseteq\mathsf{y}$, since no variable from $\mathsf{z}$ occurs in $\mathsf{x}\subseteq\mathsf{y}$, we derive by $\forall\mathsf{E}_{0}$ that $\forall\mathsf{z}(\mathsf{x}\subseteq\mathsf{y})\vdash\mathsf{x}\subseteq\mathsf{y}$. Next, we obtain by $\subseteq\!\mathsf{W}_{\forall}$ that $\mathsf{x}\subseteq\mathsf{y}\vdash\forall\mathsf{z}(\mathsf{x}\mathsf{w}\subseteq\mathsf{y}\mathsf{z})$. Thus, $\forall\mathsf{z}(\mathsf{x}\subseteq\mathsf{y})\vdash\forall\mathsf{z}(\mathsf{x}\mathsf{w}\subseteq\mathsf{y}\mathsf{z})$ follows.

If $\phi=\psi(\mathsf{x}\subseteq\mathsf{y})\wedge\chi$, then we have that

[TABLE]

The case $\phi=\chi\wedge\psi(\mathsf{x}\subseteq\mathsf{y})$ is symmetric.

If $\phi=\forall v\psi(\mathsf{x}\subseteq\mathsf{y})$, then we have that

[TABLE]

If $\phi=\exists v\psi(\mathsf{x}\subseteq\mathsf{y})$, where $\mathsf{Fv}(\exists v\psi)=\mathsf{u}$ (note that all variables from $\mathsf{y}$ are among $\mathsf{u}$), then we have that

[TABLE]

∎

Now we are ready to give the proof of Lemma 6.1.

• Proof of Lemma 6.1.

By Lemma 5.9, we may assume that $\phi$ is in normal form (12). We prove the lemma by proving a stronger claim that $\phi\vdash\Phi_{n}^{\prime}$ holds for every $n<\omega$, where

[TABLE]

where each $\lambda_{n}=\alpha_{n}\wedge\gamma_{n}\wedge\delta_{n}$,

[TABLE]

If $n=0$, then $\Phi_{0}^{\prime}:=\exists\mathsf{w}_{0}\mathsf{x}_{0}\forall y_{0}(\alpha(\mathsf{w}_{0},\mathsf{x}_{0})\wedge\mu_{0})$, and $\phi\vdash\Phi_{0}^{\prime}$ can be derived by simply renaming the variables. Now, assuming $\phi\vdash\Phi^{\prime}_{n}$, we show that $\phi\vdash\Phi^{\prime}_{n+1}$ by deriving $\Phi^{\prime}_{n}\vdash\Phi^{\prime}_{n+1}$.

First, for each $\xi\in E_{n}$ and each $i\in I$, by Proposition 6.2 we derive that

[TABLE]

which, by $\subseteq\!\mathsf{Cmp}$, yields

[TABLE]

Similarly, for each $\xi\eta\in A_{n+1}$ and $j\in J$, we derive also by Proposition 6.2 and $\subseteq\!\mathsf{Cmp}$ that

[TABLE]

Next, we derive that

[TABLE]

This finishes the proof. ∎

Finally, we are in a position to prove the completeness theorem of our system.

\theoremname** 6.5**** **(Completeness)

Let $\Gamma$ be a set of $\mathsf{Inc}$-formulas, and $\alpha$ a first-order formula. Then

[TABLE]

• Proof.

The direction “$\Longleftarrow$” follows from the soundness theorem. For the direction “$\Longrightarrow$”, since $\mathsf{Inc}$ is compact, we may without loss of generality assume that $\Gamma$ is finite. Suppose now $\Gamma\models\alpha$ and $\Gamma\nvdash_{\mathsf{Inc}}\alpha$. Claim that $\exists\mathsf{z}(\bigwedge\Gamma\wedge\mathop{\dot{\sim}}\alpha)\nvdash_{\mathsf{Inc}}\bot$, where $\mathsf{z}$ lists all free variables in $\Gamma$ and $\mathop{\dot{\sim}}\alpha$. Indeed, if $\exists\mathsf{z}(\bigwedge\Gamma\wedge\mathop{\dot{\sim}}\alpha)\vdash_{\mathsf{Inc}}\bot$, then we derive $\Gamma,\mathop{\dot{\sim}}\alpha\vdash_{\mathsf{Inc}}\bot$ by $\exists\mathsf{I}$, and further $\Gamma\vdash_{\mathsf{Inc}}\alpha$ by Lemma 5.11; a contradiction.

Now, let $\Delta=\{\Phi_{n}\mid\phi=\exists\mathsf{z}(\bigwedge\Gamma\wedge\mathop{\dot{\sim}}\alpha)\text{ and }n<\omega\}$. By Lemma 6.1, we must have that $\Delta\nvdash_{\mathsf{Inc}}\bot$. It follows that $\Delta\nvdash_{\mathbf{FO}}\bot$, since $\Delta\cup\{\bot\}$ is a set of first-order formulas, and the deduction system of $\mathsf{Inc}$ has the same rules as that of first-order logic when restricted to first-order formulas. By the completeness theorem of first-order logic, we know that the set $\Delta$ of approximations of $\phi$ has a model $M$. By [1], every infinite model is elementary equivalent to a recursively saturated countable model. Thus, we may assume that $M$ is a recursively saturated countable or finite model. By Theorem 4.2, $M$ is also a model of $\exists\mathsf{z}(\bigwedge\Gamma\wedge\mathop{\dot{\sim}}\alpha)$, thereby $M\models_{\{\emptyset\}(\mathsf{F}/\mathsf{z})}\Gamma$ and $M\not\models_{\{\emptyset\}(\mathsf{F}/\mathsf{z})}\alpha$ for some suitable sequence $\mathsf{F}$ of functions for $\exists\mathsf{z}$. Hence $\Gamma\not\models\alpha$. ∎

7. Applications

In this final section of the paper, we illustrate the power of our system of $\mathsf{Inc}$ by discussing some applications.

Recall from Proposition 2.4 that the sentence $\exists x\exists y(y\subseteq x\wedge y<x)$ defines the fact that $<$ is not well-founded. By the completeness theorem (Theorem 6.5) we proved in the previous section, all first-order consequences of the non-well-foundedness of $<$ are derivable in our system. For instance, the property that there is a $<$-chain of length $n$ for any natural number $n$, and the property that this $<$-chain of length $n$ descends from the greatest element (if exists). We now give explicit derivations of these properties in the example below.

\examplename** 7.1**

Write $x_{1}<x_{2}<\dots<x_{n}$ for $\bigwedge_{i=1}^{n-1}x_{i}<x_{i+1}$. For any $n\in\mathbb{N}$,

1. (i)

$\exists x\exists y(y\subseteq x\wedge y<x)\vdash\exists x_{1}\dots\exists x_{n}(x_{1}<x_{2}<\dots<x_{n})$, 2. (ii)

$\exists x\exists y(y\subseteq x\wedge y<x),\forall y(y<x_{0}\vee y=x_{0})\vdash\exists x_{1}\dots\exists x_{n}(x_{1}<\dots<x_{n}<x_{0})$.

• Proof.

(i) We only give an example of the proof for $n=3$.

[TABLE]

(ii) In view of item (i), it suffices to show $\exists x_{1}\dots\exists x_{n}(x_{1}<\dots<x_{n}),\forall y(y<x_{0}\vee y=x_{0})\vdash\exists x_{1}\dots\exists x_{n}(x_{1}<\dots<x_{n}<x_{0})$. But this is derivable in the system of first-order logic, and the same proof can also be performed in the system of $\mathsf{Inc}$. ∎

In Proposition 5.3 in section 5 we have derived some interesting clauses in our system of $\mathsf{Inc}$. It is interesting to note that the formulas on the right side of the turnstile ($\vdash$) in items (i)(iii) of the proposition are not first-order formulas. While our completeness theorem (Theorem 6.5) does not apply to these cases, these clauses are indeed derivable. We now give some more examples in which our system can be successfully applied to derive non-first-order consequences in $\mathsf{Inc}$.

Consider the so-called anonymity atoms, introduced in [5] and studied recently by Väänänen [30] motivated by concerns in data safety. These atoms are strings of the form $x_{1}\dots x_{n}\Upsilon y_{1}\dots y_{m}$ with the team semantics:

• •

$M\models_{X}\mathsf{x}\Upsilon\mathsf{y}$    iff    for all $s\in X$, there exists $s^{\prime}\in X$ such that $s(\mathsf{x})=s^{\prime}(\mathsf{x})$ and $s(\mathsf{y})\neq s^{\prime}(\mathsf{y})$.

Note that the anonymity atoms corresponds exactly to afunctional dependencies studied in database theory (see e.g., [3, 2]). It was proved in [5] that first-order logic extended with anonymity atoms is expressively equivalent to inclusion logic, and in particular,

[TABLE]

where $\mathsf{v}\neq\mathsf{y}$ is short for $\bigvee_{i}v_{i}\neq y_{i}$. We will then use $\mathsf{x}\Upsilon\mathsf{y}$ as a shorthand for the above equivalent $\mathsf{Inc}$-formula. Write $\Upsilon\mathsf{x}$ for $\langle\,\rangle\Upsilon\mathsf{x}$, and stipulate $\mathsf{x}\Upsilon=\mathsf{x}\Upsilon\langle\,\rangle:=\bot$. The implication problem of anonymity atoms is shown in [30] to be completely axiomatized by the rules listed in the next example (read the clauses in the example as rules). We now illustrate that in our system of $\mathsf{Inc}$ all these rules are derivable.

\examplename** 7.2**

1. (i)

$\mathsf{xyz}\Upsilon\mathsf{uvw}\vdash\mathsf{yxz}\Upsilon\mathsf{uvw}\wedge\mathsf{xyz}\Upsilon\mathsf{vuw}$ (permutation). 2. (ii)

$\mathsf{xy}\Upsilon\mathsf{z}\vdash\mathsf{x}\Upsilon\mathsf{zu}$ (monotonicity). 3. (iii)

$\mathsf{xy}\Upsilon\mathsf{zy}\vdash\mathsf{xy}\Upsilon\mathsf{z}$ (weakening). 4. (iv)

$\mathsf{x}\Upsilon\vdash\bot$.

• Proof.

Item (i) follows easily from $\subseteq\!\mathsf{Exc}$, and item (iv) is trivial. We only prove the other two items. For item (ii), note that $\mathsf{xy}\Upsilon\mathsf{z}:=\exists\mathsf{v}(\mathsf{xyv}\subseteq\mathsf{xyz}\wedge\mathsf{v}\neq\mathsf{z})$, and we have that

[TABLE]

For item (iii), note that $\mathsf{xy}\Upsilon\mathsf{zy}:=\exists\mathsf{uv}(\mathsf{xyuv}\subseteq\mathsf{xyzy}\wedge\mathsf{uv}\neq\mathsf{zy})$, and we have

[TABLE]

∎

The above example indicates that the actual strength of our deduction system of $\mathsf{Inc}$ goes beyond the completeness theorem (Theorem 6.5) proved in this paper. How far can we actually go then? There are obviously barriers, as inclusion logic cannot be effectively axiomatized after all. For instance, in the context of anonymity atoms, the author was not able to derive a simple (sound) implication “$\Upsilon\mathsf{x}$ and $\mathsf{x}\subseteq\mathsf{y}$ imply $\Upsilon\mathsf{y}$” in the system of $\mathsf{Inc}$. An easy solution for generating derivations of simple facts like this one would be to extend the current system with new rules. But then how many new rules or which new rules should we add to the current system in order to derive “sufficient” amount of sound consequences of $\mathsf{Inc}$? One such candidate that is worth mentioning is the natural and handy rule $\phi\vee\neg\alpha,\alpha\vee\psi/\phi\vee\psi$ (for $\alpha$ being first-order) that is sound and does not seem to be derivable in our system. Finding other such rules is left for future research.

{acknowledgement}

The author would like to thank Miika Hannula and Jouko Väänänen for interesting discussions related to this paper, and Davide Quadrellaro and an anonymous referee for pointing out some mistakes in an earlier version of the paper.