Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Negation and partial axiomatizations of dependence and independence logic have been studied in the literature. In this paper, we take a new look at these topics.

Dependence logic was introduced by Väänänen [23] as a development of Henkin quantifier [11] and independence-friendly logic [12]. Recently, Grädel and Väänänen [9] defined a variant of dependence logic, called independence logic. The two logics add to first-order logic new types of atomic formulas \(\mathop {=\!} (\vec {x},y)\) and \(\vec {x}\perp _{\vec {z}}\vec {y}\), called dependence atom and independence atom, to explicitly specify the dependence and independence relations between variables. Intuitively, \(\mathop {=\!} (\vec {x},y)\) states that “the value of y is completely determined by the values of the variables in the tuple \(\vec {x}\) ”, and \(\vec {x}\perp _{\vec {z}}\vec {y}\) states that “given the values of the variables \(\vec {z}\), the values of \(\vec {x}\) and the values of \(\vec {y}\) are completely independent of each other”. These properties cannot be meaningfully manifested in single assignments of the variables. Therefore unlike in the case of the usual Tarskian semantics, formulas of dependence and independence logic are evaluated on sets of assignments (called teams) instead. This semantics is called team semantics and was introduced by Hodges [13, 14].

Dependence and independence logic are known to have the same expressive power as existential second-order logic \(\varSigma ^1_1\) (see [5, 18]). This fact has two negative consequences: The logics are not closed under classical negation and are not axiomatizable. The aim of this paper is to shed some new light on these problems.

Regarding the first problem, “negation”, which is usually a desirable connective for a logic, turns out to be a tricky connective in the context of team semantics. The negation that dependence and independence logic inherit from first-order logic (denoted by \(\lnot \)) is a type of “syntactic negation”, in the sense that in order to compute the meaning of the formula \(\lnot \phi \), the negation \(\lnot \) has to be brought to the very front of atomic formulas by applying De Morgen’s laws and the double negation law. It was proved that this negation \(\lnot \) is actually not a semantic operator [19], meaning that \(\phi \) and \(\psi \) are semantically equivalent does not necessarily imply that \(\lnot \phi \) and \(\lnot \psi \) are semantically equivalent. The classical (contradictory) negation (denoted by \(\sim \) in the literature), on the other hand, is a semantic operator. Since the \(\varSigma ^1_1\) fragment of second-order logic is not closed under classical negation, neither dependence nor independence logic is closed under classical negation. Dependence logic extended with the classical negation \(\sim \) is called team logic in the literature, and it has the same expressive power as full second-order logic (see [17, 23]).

Since every formula of dependence and independence logic is satisfied on the empty team, the classical contradictory negation \(\sim \phi \) of any formula will not be satisfied on the empty team, implying that \(\sim \phi \) cannot possibly be definable in dependence or independence logic for any single formula \(\phi \). This technical subtlety makes the classical contradictory negation \(\sim \) less interesting. In this paper, we will, instead, consider the weak classical negation, denoted by \(\mathop {\dot{\sim }}\), which behaves exactly as the classical negation except that on the empty team \(\mathop {\dot{\sim }} \phi \) is always satisfied. We will give a characterization for negatable formulas in independence logic and negatable sentences in dependence logic by generalizing an argument in [23]. We also identify an interesting class of formulas that are negatable in independence logic. First-order formulas, dependence and independence atoms belong to this class. Formulas of this class are closely related to the dependency notions considered in [6] and the generalized dependence atoms studied in [16, 21].

As for the axiomatization problem, since \(\varSigma ^1_1\) is not axiomatizable, dependence and independence logic cannot possibly be axiomatized in full. Nevertheless, [10, 20] defined natural deduction systems for the logics such that the equivalence

$$\begin{aligned} \varGamma \,\models \,\phi \iff \varGamma \vdash \phi \end{aligned}$$
(1)

holds if \(\varGamma \) is a set of sentences of dependence or independence logic and \(\phi \) is a first-order sentence. It was left open whether these partial axiomatizations can be generalized such that the above equivalence (1) holds if \(\varGamma \) is a set of formulas (that possibly contain free variables) and \(\phi \) is a (possibly open) first-order formula. Kontinen [15] gave such a generalization by expanding the signature with an extra relation symbol so as to interpret the teams associated with the free variables. In this paper, we will generalize the partial axiomatization results in [10, 20] via a different approach, an approach that makes use of the weak classical negation. We will define extensions of the systems given in [10, 20] such that the equivalence (1) holds if \(\varGamma \) is a set of formulas and \(\phi \) is a formula that is negatable in the logics.

2 Preliminaries

Let us start by recalling the syntax and semantics (i.e. team semantics) of dependence and independence logic.

Although team semantics is intended for extensions of first-order logic obtained by adding dependence or independence atoms, for the sake of comparison we will now introduce the team semantics for first-order logic too. First-order atomic formulas \(\alpha \) for a given signature \(\mathcal {L}\) are defined as usual. Well-formed formulas of first-order logic, also called first-order formulas, (in negation normal form) are defined by the following grammar:

$$\begin{aligned} \phi \,{:}{:=}\,\alpha \mid \lnot \alpha \mid \bot \mid \phi \wedge \phi \mid \phi \vee \phi \mid \exists x\phi \mid \forall x\phi \end{aligned}$$

Formulas will be evaluated on the usual first-order models over an appropriate signature \(\mathcal {L}\). We will use the same notation M for both a model and its domain. Let R be a fresh k-ary relation symbol and \(R^M\) a k-ary relation on M. We write \(\mathcal {L}(R)\) for the expanded signature and \((M,R^M)\) denotes the \(\mathcal {L}(R)\)-expansion of M in which the relation symbol R is interpreted as \(R^M\). We write \(\phi (R)\) to emphasize that the relation symbol R occurs in the formula \(\phi \).

Definition 2.1

Let M be a model and V a set of first-order variables. A team X of M over V is a set of assignments of M over V, i.e., a set of functions \(s:V\rightarrow M\). The set V is called the domain of X, denoted by \(\mathrm{dom}(X)\).

There is one and only one assignment of M over the empty domain, namely the empty assignment \(\emptyset \). The singleton of the empty assignment \(\{\emptyset \}\) is a team of M, and the empty set \(\emptyset \) is a team of M over any domain.

Let s be an assignment of M over V and \(a\in M\). We write s(a / x) for the assignment of M over \(V\cup \{x\}\) defined as \(s(a/x)(x)=a\) and \(s(a/x)(y)=s(y)\) for all \(y\in V\setminus \{x\}\). For any set \(N\subseteq M\) and any function \(F:X\rightarrow \wp (M)\setminus \{\emptyset \}\), define

$$\begin{aligned} X(N/x)=\{s(a/x): a\in N,~s\in X\}\text { and }X[F/x]=\{s(a/x):s\in X\text { and }a\in F(s)\} \end{aligned}$$

We write \(\vec {x}\) for a sequence \(x_1,\dots ,x_n\) of variables and the length n will always be clear from the context or does not matter; similarly for a sequence \(\vec {F}\) of functions and a sequence \(\vec {s}\) of assignments. A team \(X(M/x_1)\dots (M/x_n)\) will sometimes be abbreviated as \(X(M/\vec {x})\), and \(X[F_1/x_1]\dots [F_n/x_n]\) as \(X[F_1/x_1,\dots ,F_n/x_n]\) or \(X[\vec {F}/\vec {x}]\).

We now define the team semantics for first-order formulas. Note that our version of the team semantics for disjunction and existential quantifier is known as the lax semantics in the literature.

Definition 2.2

Define inductively the notion of a first-order formula \(\phi \) being satisfied on a model M and a team X, denoted by \(M\models _X\phi \), as follows:

  • \(M\models _X\alpha \) with \(\alpha \) a first-order atomic formula iff for all \(s\in X\), \(M\models _s\alpha \) in the usual sense

  • \(M\models _X\lnot \alpha \) with \(\alpha \) a first-order atomic formula iff for all \(s\in X\), \(M\models _s\lnot \alpha \) in the usual sense

  • \(M\models _X\bot \) iff \(X=\emptyset \)

  • \(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\rightarrow \wp (M)\setminus \{\emptyset \}\)

  • \(M\models _X\forall x\phi \) iff \(M\models _{X(M/x)}\phi \)

A routine inductive proof shows that first-order formulas have the downward closure property and the union closure property:

  • (Downward Closure Property). \(M\models _X\phi \) and \(Y\subseteq X\) imply \(M\models _Y\phi \)

  • (Union Closure Property). \(M\models _{X_i}\phi \) for all \(i\in I\) implies \(M\models _{\bigcup _{i\in I}X_i}\phi \)

which combined are equivalent to the flatness property:

  • (Flatness Property). \(M\models _X\phi \iff M\models _{\{s\}}\phi \text { for all }s\in X\)

It follows easily from the flatness property that the team semantics for first-order formulas coincides with the usual single-assignment semantics in the sense that

$$\begin{aligned} M\models _{\{s\}}\phi \iff M\models _s\phi \end{aligned}$$
(2)

holds for any model M, any assignment s and any first-order formula \(\phi \). If \(\phi \) is a first-order formula, then the string \(\lnot \phi \), called the syntactic negation of \(\phi \), can be viewed as a first-order formula in negation normal form obtained in the usual way (i.e. by applying De Morgan’s laws, the double negation law, etc.), and we write \(\phi \rightarrow \psi \) for the formula \(\lnot \phi \vee \psi \). Since first-order formulas satisfy the Law of Excluded Middle \(\phi \vee \lnot \phi \) under the usual single-assignment semantics, Expression (2) implies that \(\mathop {M\models _{\{s\}}\phi \vee \lnot \phi }\) always holds, which, together with the flatness property, implies that \(M\models _X\phi \vee \lnot \phi \) holds for all teams X and all models M, namely, the Law of Excluded Middle holds for first-order formulas also in the sense of team semantics.

We now turn to dependence and independence logic. Well-formed formulas of independence logic (\(\mathcal {I}\)) are defined by the following grammar:

$$\begin{aligned} \begin{aligned} \phi \,{:}{:=}~&\alpha \mid \lnot \alpha \mid \bot \mid x_1\dots x_n\perp _{z_1\dots z_k} y_1\dots y_m\mid \mathop {=\!} (x_1,\dots , x_n,y)\mid x_1\dots x_n\subseteq y_1\dots y_n\mid \\&\phi \wedge \phi \mid \phi \vee \phi \mid \exists x\phi \mid \forall x\phi \end{aligned} \end{aligned}$$

where \(\alpha \) ranges over first-order atomic formulas. The formulas \(\mathop {=\!} (\vec {x},y)\), \(\vec {x}\perp _{\vec {z}}\vec {y}\) and \(\vec {x}\subseteq \vec {y}\) are called dependence atom, independence atom and inclusion atom, respectively. We refer to any of these atoms as atoms of dependence and independence. For the convenience of our argument in the paper, the independence logic as defined has a richer syntax than the standard one in the literature, which has the same syntax as first-order logic extended with independence atoms only. The other atoms are definable in the standard independence logic; for a proof see e.g., [4]. Dependence logic (\(\mathcal {D}\)), which is a fragment of \(\mathcal {I}\), is defined as first-order logic extended with dependence atoms, and first-order logic extended with inclusion atoms is called inclusion logic. In this paper we will only concentrate on dependence logic and independence logic.

The set \(\mathrm{{Fv}}(\phi )\) of free variables of a formula \(\phi \) of \(\mathcal {I}\) is defined as usual and we also have the new cases for dependence and independence atoms:

  • \(\mathrm{Fv}(x_1\dots x_n\perp _{z_1\dots z_k} y_1\dots y_m)=\{x_1,\dots ,x_n,y_1,\dots ,y_m,z_1,\dots ,z_k\}\)

  • \(\mathrm{Fv}(\mathop {=\!} (x_1,\dots ,x_n,y))=\{x_1,\dots ,x_n,y\}\)

  • \(\mathrm{Fv}(x_1,\dots ,x_n\subseteq y_1,\dots ,y_n)=\{x_1,\dots ,x_n,y_1,\dots ,y_n\}\)

We write \(\phi (\vec {x})\) to indicate that the free variables occurring in \(\phi \) are among \(\vec {x}\). A formula \(\phi \) is called a sentence if it has no free variable.

Definition 2.3

Define inductively the notion of a formula \(\phi \) of \(\mathcal {I}\) being satisfied on a model M and a team X, denoted by \(M\models _X\phi \). All the cases are identical to those defined in Definition 2.2 and additionally:

  • \(M\models _X\vec {x}\perp _{\vec {z}}\vec {y}\) iff for all \(s,s'\in X\), \(s(\vec {z})=s'(\vec {z})\) implies that there exists \( s''\in X\) such that

    $$\begin{aligned} s''(\vec {z})=s(\vec {z})=s'(\vec {z}),~s''(\vec {x})=s(\vec {x})\text { and }s''(\vec {y})=s'(\vec {y}). \end{aligned}$$

  • \(M\models _X\mathop {=\!} (\vec {x},y)\) iff for all \(s,s'\in X\), \(s(\vec {x})=s'(\vec {x})\) implies \(s(y)=s'(y)\).

  • \(M\models _X\vec {x}\subseteq \vec {y}\) iff for all \(s\in X\), there exists \(s'\in X\) such that \(s'(\vec {y})=s(\vec {x})\).

We write \(\vec {x}\perp \vec {y}\) for \(\vec {x}\perp _{\langle \rangle }\vec {y}\), and note that the semantic clause for \(\vec {x}\perp \vec {y}\) reduces to

  • \(M\models _X\vec {x}\perp \vec {y}\) iff for all \(s,s'\in X\), there exist \(s''\in X\) such that

    $$\begin{aligned} s''(\vec {x})=s(\vec {x})\text { and }s''(\vec {y})=s'(\vec {y}). \end{aligned}$$

A sentence \(\phi \) is said to be true in M, written \(M\,\models \,\phi \), if \(M\models _{\{\emptyset \}}\phi \). We write \(\varGamma \,\models \,\psi \) if for any model M and any team X, \(M\models _X \phi \text { for all }\phi \in \varGamma \) implies \(M\models _X \psi \). We also write \(\phi \,\models \,\psi \) for \(\{\phi \}\,\models \,\psi \). If \(\phi \,\models \,\psi \) and \(\psi \,\models \,\phi \), then we write \(\phi \equiv \psi \).

We leave it for the reader to verify that formulas of dependence logic have the downward closure property and formulas of independence logic have the empty team property and the locality property:

  • (Empty Team Property). \(M\models _\emptyset \phi \)

  • (Locality Property). If \(\{s\upharpoonright \mathrm{Fv}(\phi )\mid s\in X\}=\{s\upharpoonright \mathrm{Fv}(\phi )\mid s\in Y\}\) Footnote 1, then

    $$\begin{aligned} M\models _X\phi \iff M\models _Y\phi . \end{aligned}$$

Recall that the existential second-order logic (\(\varSigma ^1_1\)) consists of those formulas that are equivalent to some formulas of the form \(\exists R_1\dots \exists R_k\phi ,\) where \(\phi \) is a first-order formula. An \(\mathcal {L} (R)\)-sentence \(\phi (R)\) of \(\varSigma ^1_1\) is said to be downward monotone with respect to R if \((M,Q)\,\models \,\phi (R)\text { and }Q'\subseteq Q\) imply \((M,Q')\,\models \,\phi (R)\). It is known that \(\phi (R)\) is downward monotone with respect to R if and only if R occurs in \(\phi (R)\) only negatively (see e.g., [18]). A team X of M over \(\{x_1,\dots ,x_n\}\) induces an n-ary relation

$$\begin{aligned} rel(X):=\{(s(x_1),\dots ,s(x_n))\mid s\in X\} \end{aligned}$$

on M; conversely, an n-ary relation R on M induces a team

$$\begin{aligned} X_R:=\{\{(x_1,a_1),\dots ,(x_n,a_n) \}\mid (a_1,\dots ,a_n)\in R\}. \end{aligned}$$

Theorem 2.4

(see [5, 18, 23])

  • (i) Every \(\mathcal {L} \)-sentence \(\phi \) of \(\mathcal {D}\) or \(\mathcal {I}\) is equivalent to an \(\mathcal {L} \)-sentence \(\tau _\phi \) of \(\varSigma ^1_1\), i.e.,

    $$\begin{aligned} M\,\models \,\phi \iff M\,\models \,\tau _\phi \end{aligned}$$

    holds for any model M; and conversely, every \(\mathcal {L} \)-sentence of \(\varSigma ^1_1\) is equivalent to an \(\mathcal {L} \)-sentence \(\rho (\psi )\) of \(\mathcal {D}\) or \(\mathcal {I}\).

  • (ii) For every \(\mathcal {L}\)-formula \(\phi \) of \(\mathcal {I}\), there is an \(\mathcal {L} (R)\)-sentence \(\tau _\phi (R)\) of \(\varSigma ^1_1\) such that for all models M and all teams X,

    $$\begin{aligned} M\models _X\phi \iff (M,rel(X))\,\models \,\tau _\phi (R). \end{aligned}$$

    If, in particular, \(\phi \) is a formula of \(\mathcal {D}\), then the relation symbol R occurs in the sentence \(\tau _\phi (R)\) only negatively.

  • (iii) For every \(\mathcal {L} (R)\)-sentence \(\psi (R)\) of \(\varSigma ^1_1\) that is downward monotone with respect to R, there is an \(\mathcal {L}\)-formula \(\rho (\psi )\) of \(\mathcal {D}\) such that for all models M and all teams X,

    $$\begin{aligned} M\models _X\rho (\psi )\iff (M,rel(X))\,\models \,\psi (R)\vee \forall \vec {x}\lnot R\vec {x}. \end{aligned}$$
    (3)

  • (iv) For every \(\mathcal {L} (R)\)-sentence \(\psi (R)\) of \(\varSigma ^1_1\), there is an \(\mathcal {L}\)-formula \(\rho (\psi )\) of \(\mathcal {I}\) such that (3) holds for all models M and all teams X.

In the sequel, we will use the notations \(\tau _\phi \) and \(\tau _\phi (R)\) to denote the (up to semantic equivalence) unique formulas obtained in the above theorem and refer to them as the \(\varSigma ^1_1\) -translations of the formulas \(\phi \) of \(\mathcal {D}\) or \(\mathcal {I}\).

3 First-Order Formulas and Negatable Formulas

Formulas of dependence and independence logic can be translated into \(\varSigma ^1_1\) (Theorem 2.4). Therefore in the environment of team semantics a first-order formula \(\phi \) has two identities: It can be viewed either as a formula of \(\mathcal {D}\) or \(\mathcal {I}\) that is to be evaluated on teams, or as a usual formula of first-order logic that is to be evaluated on single assignments and is possibly (equivalent to) the \(\varSigma ^1_1\)-translation \(\tau _\psi \) of some formula \(\psi \) of \(\mathcal {D}\) or \(\mathcal {I}\). With the latter reading of a first-order formula \(\phi \), for all models M and all assignments s, \(M\models _s\lnot \phi \) iff \(M\not \models _s\phi \) holds. In this sense, the formula \(\lnot \phi \) can be interpreted as the “classical (contradictory) negation" of \(\phi \). However, on the team semantics side, unless the team X is a singleton, \(M\not \models _X\phi \) is in general not equivalent to \(M\models _X\lnot \phi \). To express the contradictory negation in the team semantics setting, let us define the classical negation \(\sim \) and the weak classical negation \(\mathop {\dot{\sim }} \) as follows:

  • \(M\models _X\sim \phi \) iff \(M\not \models _X\phi \)

  • \(M\models _X\mathop {\dot{\sim }} \phi \) iff either \(M\not \models _X\phi \) or \(X=\emptyset \)

Since formulas of dependence and independence logic have the empty team property, the classical negation \(\sim \phi \) of any formula \(\phi \) is not definable in the logics and we are therefore not interested in the classical negation \(\sim \) in this paper. On the other hand, the weak classical negation \(\mathop {\dot{\sim }} \phi \) can be definable in the logics for some formulas \(\phi \). We say that a formula \(\phi \) is negatable in \(\mathcal {I}\) (or \(\mathcal {D}\)) if there is a formula \(\psi \) of \(\mathcal {I}\) (or \(\mathcal {D}\)) such that \(\mathop {\dot{\sim }} \phi \equiv \psi \). If a formula \(\phi \) of \(\mathcal {I}\) is negatable in \(\mathcal {I}\), we also say that \(\phi \) is a negatable formula in \(\mathcal {I}\) or the formula \(\phi \) of \(\mathcal {I}\) is negatable; similarly for \(\mathcal {D}\).

For any first-order sentence \(\phi \), we have \(M\not \models _{\{\emptyset \}}\phi \) iff \(M\models _{\{\emptyset \}}\lnot \phi \) by the Law of Excluded Middle. Thus \(\mathop {\dot{\sim }} \phi \equiv \lnot \phi \), meaning that first-order sentences are negatable both in \(\mathcal {D}\) and in \(\mathcal {I}\). Next, we prove that negatable formulas in \(\mathcal {D}\) are, actually, all flat.

Fact 3.1

If a formula \(\phi \) of \(\mathcal {D}\) is negatable in \(\mathcal {D}\), then it is upward closed (i.e. \(M\models _X\phi \) and \(\emptyset \ne X\subseteq Y\) imply \(M\models _Y\phi \)), and thus flat.

Proof

Suppose \(\phi \) is a formula of \(\mathcal {D}\) that is not upward closed. Then, there exist a model M and two teams \(X\ne \emptyset \) and \(Y\supseteq X\) such that \(M\models _X\phi \) and \(M\not \models _Y\phi \). But this means that \(\mathop {\dot{\sim }} \phi \) is not downward closed and thus not definable in \(\mathcal {D}\).

We will see in the sequel that the above fact does not apply to independence logic. Also note that sentences are always upward closed (since to evaluate a sentence it is sufficient to consider the nonempty team \(\{\emptyset \}\) only). Thus, the other direction of the above fact, if true, would imply that all sentences of \(\mathcal {D}\) are negatable. But this is not the case, as we will see in the following characterization theorem for negatable sentences in \(\mathcal {D}\) and negatable formulas in \(\mathcal {I}\).

Theorem 3.2

 

  • (i) An \(\mathcal {L} \)-formula \(\phi \) of \(\mathcal {I}\) is negatable in \(\mathcal {I}\) if and only if its \(\varSigma ^1_1\)-translation \(\tau _\phi (R)\) is equivalent to a first-order sentence.

  • (ii) An \(\mathcal {L}\)-sentence \(\phi \) of \(\mathcal {D}\) is negatable in \(\mathcal {D}\) if and only if its \(\varSigma ^1_1\)-translation \(\tau _\phi \) is equivalent to a first-order sentence.

The above theorem states that negatable formulas in \(\mathcal {I}\) are exactly those formulas that have first-order translations, and negatable sentences in \(\mathcal {D}\) are exactly those sentences that have first-order translations. Therefore the problem of determining whether a formula of \(\mathcal {I}\) or a sentence of \(\mathcal {D}\) is negatable reduces to the problem of determining whether a \(\varSigma ^1_1\)-sentence (\(\tau _\phi \)) is equivalent to a first-order formula, or whether the second-order quantifiers in a \(\varSigma ^1_1\)-sentence can be eliminated. This problem is known to be undecidable (this follows from e.g.,[3]).

We devote the remainder of this section to the proof of Theorem 3.2. The item (ii) actually follows implicitly from the results in [23], and the item (i) can be proved by essentially the argument of Theorem 6.7 in [23]. To proceed, let us first direct our attention to the \(\varSigma ^1_1\) counterpart of dependence and independence logic and prove a general theorem for \(\varSigma ^1_1\). The proof below is inspired by Theorem 6.7 in [23].

Theorem 3.3

 

  • (i) Let \(\phi (R)\) be an \(\mathcal {L} (R)\)-formula of \(\varSigma ^1_1\) such that \((M,\emptyset )\,\models \,\phi (R)\) for any \(\mathcal {L} \)-model M. The formula \(\lnot \phi \vee \forall \vec {x}\lnot R\vec {x}\) belongs to \(\varSigma ^1_1\) if and only if \(\phi \) is equivalent to a first-order formula.

  • (ii) Let \(\phi \) be an \(\mathcal {L}\)-formula of \(\varSigma ^1_1\). The \(\mathcal {L}\)-formula \(\lnot \phi \) belongs to \(\varSigma ^1_1\) if and only if \(\phi \) is equivalent to a first-order formula.

Proof

(i) It suffices to prove the direction “\(\Longrightarrow \)”. Suppose both \(\phi \) and \(\lnot \phi \vee \forall \vec {x}\lnot R\vec {x}\) belong to \(\varSigma ^1_1\). We may assume without loss of generality that \(\phi \equiv \exists S_1\dots \exists S_k\psi \) and \((\lnot \phi \vee \forall \vec {x}\lnot R\vec {x})\equiv \exists T_1\dots \exists T_m\chi \) for some first-order formulas \(\psi \) and \(\chi \), and the relation variables \(S_1,\dots ,S_k,T_1,\dots ,T_m\) are pairwise distinct. Assume also that \(\phi (R)\) and \(\mathop {\exists S_1\dots \exists S_k\psi }\) are \(\mathcal {L} _1(R)\)-formulas, and \(\lnot \phi (R)\vee \forall \vec {x}\lnot R\vec {x}\) and \(\exists T_1\dots \exists T_m\chi \) are \(\mathcal {L} _2(R)\)-formulas.

Claim 1: \(\psi \,\models \,\lnot \chi \vee \forall \vec {x}\lnot R\vec {x}\).

Proof of Claim 1. Put \(\mathcal {L}=\mathcal {L}_1\cup \mathcal {L}_2\cup \{R,S_1,\dots ,S_k,T_1,\dots ,T_m\}\). For any \(\mathcal {L}\)-model M such that \(M\models \psi \), we have \(M\,\models \,\exists S_1\dots \exists S_k\psi \). If \(R^M=\emptyset \), then \(M\,\models \,\forall \vec {x}\lnot R\vec {x}\), thereby \(M\,\models \,\lnot \chi \vee \forall \vec {x}\lnot R\vec {x}\). If \(R^M\ne \emptyset \), then we have \(M\,\models \,\lnot \forall \vec {x}\lnot R\vec {x}\). By the assumption, we also have \(M\,\models \,\phi \). Thus, we derive

$$\begin{aligned} M\,\models \,\lnot \lnot \phi \wedge \lnot \forall \vec {x}\lnot R\vec {x}&\Longrightarrow M\,\models \,\lnot (\lnot \phi \vee \forall \vec {x}\lnot R\vec {x}) \Longrightarrow M\,\models \,\lnot \exists T_1\dots \exists T_m\chi \\&\Longrightarrow M\,\models \,\forall T_1\dots \forall T_m\lnot \chi \Longrightarrow M\,\models \,\lnot \chi \\&\Longrightarrow M\,\models \,\lnot \chi \vee \forall \vec {x}\lnot R\vec {x} \end{aligned}$$

as required.

Now, by Craig’s Interpolation Theorem of first-order logic, there exists a first-order \(\mathcal {L} _1(R)\cap \mathcal {L} _2(R)\)-formula \(\theta \) such that \(\psi \,\models \,\theta \) and \(\theta \,\models \,\lnot \chi \vee \forall \vec {x}\lnot R\vec {x}\).

Claim 2: \(\phi \equiv \theta \).

Proof of Claim 2. For any \(\mathcal {L} _1(R)\)-model M, if \(M\,\models \,\phi \), then \((M,S_1^M,\dots ,S_k^M)\,\models \,\psi \) for some relations \(S_1^M,\dots ,S_k^M\) on M. Hence, \(M\,\models \,\theta \).

Conversely, for any \(\mathcal {L} _1(R)\)-model M such that \(M\not \,\models \,\phi \), we have \(R^M\ne \emptyset \) and \(M\,\models \,\lnot \phi \vee \forall \vec {x}\lnot R\vec {x}\). The latter implies \((M,T_1^M,\dots ,T_m^M)\,\models \,\chi \) for some relations \(T_1^M,\dots ,T_m^M\) on M. It then follows that \((M,T_1^M,\dots ,T_m^M)\not \,\models \,\lnot \chi \vee \forall \vec {x}\lnot R\vec {x}\). Hence, \(M\not \,\models \,\theta \).

(ii) The nontrivial direction “\(\Longrightarrow \)” follows from a similar and simplified argument. Instead of proving Claim 1 as above, one proves \(\psi \,\models \,\lnot \chi \).    \(\square \)

Now, we are ready to give the proof of Theorem 3.2.

Proof

(of Theorem 3.2 ). (i) Let \(\phi \) be an \(\mathcal {L}\)-formula of \(\mathcal {I}\). By Theorem 2.4(ii) there exists an \(\mathcal {L} (R)\)-sentence \(\tau _\phi (R)\) of \(\varSigma ^1_1\) such that for any model M and any teamX,

$$\begin{aligned} M\models _X \mathop {\dot{\sim }} \phi \iff M\not \models _X\phi \text { or }X=\emptyset \iff (M,rel(X))\models \lnot \tau _\phi (R)\vee \forall \vec {x}\lnot R\vec {x}. \end{aligned}$$
(4)

Now, to prove the direction “\(\Longleftarrow \)”, assume that \(\tau _\phi (R)\) is equivalent to a first-order sentence. Then, the sentence \(\lnot \tau _\phi (R)\) is also equivalent to a first-order sentence, and thus by Theorem 2.4(iv) there exists a formula \(\rho (\lnot \tau _\phi )\) of \(\mathcal {I}\) such that for all \(\mathcal {L}\)-models M and all teams X,

$$\begin{aligned} M\models _X\rho (\lnot \tau _\phi )\iff (M,rel(X))\,\models \,\lnot \tau _\phi (R)\vee \forall \vec {x}\lnot R\vec {x}. \end{aligned}$$

It then follows from (4) that \(\rho (\lnot \tau _\phi )\equiv \mathop {\dot{\sim }} \phi \).

Finally, to prove the direction “\(\Longrightarrow \)”, assume that \(\mathop {\dot{\sim }} \phi \equiv \psi \) for some formula \(\psi \) of \(\mathcal {I}\). By Theorem 2.4(ii) there exists an \(\mathcal {L} (R)\)-sentence \(\tau _\psi (R)\) of \(\varSigma ^1_1\) such that for all models M and all teams X,

$$\begin{aligned} M\models _X\psi \iff (M,rel(X))\,\models \,\tau _\psi (R). \end{aligned}$$

By (4), \(\tau _\psi (R)\equiv \lnot \tau _\phi (R)\vee \forall \vec {x}\lnot R\vec {x}\) and thereby the formula \(\lnot \tau _\phi (R)\vee \forall \vec {x}\lnot R\vec {x}\) belongs to \(\varSigma ^1_1\). For any model M, since \(M\models _\emptyset \phi \), we have \((M,\emptyset )\,\models \,\tau _\phi (R)\). Then, by Theorem 3.3(i), we conclude that \(\tau _\phi (R)\) is equivalent to a first-order formula.

(ii) This item is proved by a similar argument that makes use of Theorem 2.4(i) and Theorem 3.3(ii).    \(\square \)

4 Axiomatizing Negatable Consequences in Dependence and Independence Logic

Dependence and independence logic are not axiomatizable, meaning that the consequence relation \(\varGamma \,\models \,\phi \) cannot be effectively axiomatized. Nevertheless, if we restrict \(\varGamma \cup \{\phi \}\) to a set of sentences and \(\phi \) to a first-order sentence, the consequence relation \(\varGamma \,\models \,\phi \) is axiomatizable and explicit axiomatizations for \(\mathcal {D}\) and \(\mathcal {I}\) are given in [10, 20]. Throughout this section, let \(\mathsf {L}\) denote one of the logics of \(\mathcal {D}\) and \(\mathcal {I}\), and \(\vdash _{\mathsf {L}}\) denote the syntactic consequence relation associated with the deduction system of \(\mathsf {L}\) defined in [20] or in [10].

Theorem 4.1

(see [10, 20]). Let \(\varGamma \) be a set of sentences of \(\mathsf {L}\), and \(\phi \) a first-order formula. We have \(\varGamma \,\models \,\phi \iff \varGamma \vdash _{\mathsf {L}}\phi \). In particular, \(\varGamma \,\models \,\bot \iff \varGamma \vdash _{\mathsf {L}}\bot \).

Kontinen [15] generalized the above axiomatization result to cover also the case when \(\varGamma \cup \{\phi \}\) is a set of formulas (that possibly contain free variables) by adding a new relation symbol to interpret the teams. In this section, we will generalize Theorem 4.1 without expanding the signature to cover the case when \(\varGamma \cup \{\phi \}\) is a set of formulas (that possibly contain free variables) and \(\phi \) is negatable.

We first prove that under certain constraint the (possibly open) formula \(\psi \) in the entailment \(\varDelta ,\psi \,\models \,\theta \) can be turned into a sentence without affecting the entailment relation.

Lemma 4.2

Let \(\varDelta \cup \{\chi ,\theta \}\) be a set of formulas of \(\mathsf {L}\). Let \(\mathrm{Fv}(\chi )=\{x_1,\dots ,x_n\}\) and \(\mathrm{Fv}(\varDelta )=\bigcup _{\delta \in \varDelta }\mathrm{Fv}(\delta )\). Suppose that \(\mathrm{Fv}(\chi )\cap \mathrm{Fv}(\varDelta )=\emptyset \) and \(\mathrm{Fv}(\chi )\cap \mathrm{Fv}(\theta )=\emptyset \). We have \(\varDelta ,\chi \,\models \,\theta \iff \varDelta ,\exists x_1\dots \exists x_n\chi \,\models \,\theta \).

Proof

“\(\Longrightarrow \)”: Suppose \(\varDelta ,\chi \,\models \,\theta \). If \(M\models _X\delta \) for all \(\delta \in \varDelta \) and \(M\models _X\exists \vec {x}\chi \), then \(M\models _{X[\vec {F}/\vec {x}]}\chi \) for some appropriate sequence of functions \(\vec {F}\). Since \(\mathrm{Fv}(\chi )\cap \mathrm{Fv}(\varDelta )=\emptyset \), we derive \(M\models _{X[\vec {F}/\vec {x}]}\delta \) for all \(\delta \in \varDelta \) by the locality property. Thus, by the assumption, we conclude that \(M\models _{X[\vec {F}/\vec {x}]}\theta \), which implies \(M\models _X\theta \) since \(\mathrm{Fv}(\chi )\cap \mathrm{Fv}(\theta )=\emptyset \).

“\(\Longleftarrow \)”: Suppose \(\varDelta ,\exists \bar{x}\chi \models \theta \), and suppose \(M\models _X\delta \) for all \(\delta \in \varDelta \) and \(M\models _{X}\chi \). Then, we have \(M\models _{X}\exists \vec {x}\chi \), which implies \(M\models _X\theta \) by the assumption.    \(\square \)

To understand why Theorem 4.1 can be generalized, let us consider a set \(\varGamma \cup \{\phi \}\) of formulas of \(\mathsf {L}\). Since \(\varSigma ^1_1\) admits the Compactness Theorem, we may assume that \(\varGamma \) is a finite set. Clearly, \(\varGamma \,\models \,\phi \) is equivalent to \(\varGamma ,\mathop {\dot{\sim }} \phi \,\models \,\bot \), and further to \(\exists \vec {x}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )\,\models \,\bot \) by Lemma 4.2, where \(\mathrm{Fv}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )=\{x_1,\dots ,x_n\}\). Adding appropriate rules to the deduction system to guarantee the equivalence of \(\exists \vec {x}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )\vdash \bot \) and \(\varGamma \vdash \phi \), the Completeness Theorem can be restated as \(\exists \vec {x}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )\not \vdash \bot \Longrightarrow \exists \vec {x}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )\not \,\models \,\bot .\) Now, assuming that \(\exists \vec {x}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )\) is deductively consistent, the problem reduces to the problem of constructing a model for the sentence \(\exists \vec {x}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )\). If \(\mathop {\dot{\sim }} \phi \) is definable in \(\mathsf {L}\), then the problem further reduces to the problem of constructing a model for the \(\varSigma ^1_1\) sentence \(\tau _{\exists \vec {x}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )}\), which can in principle be done in first-order logic. This argument shows that via the trick of weak classical negation Theorem 4.1 can, in principle, be generalized. Note that if \(\varGamma \) is a set of sentences and \(\phi \) is a first-order sentence, then \(\lnot \phi \equiv \mathop {\dot{\sim }} \phi \) and the foregoing argument reduces to the argument given in [20].

Let us now make this idea precise. Given the Completeness Theorems in [10, 20], it suffices to extend the natural deduction systems of [10, 20] by adding the two rules below to ensure the equivalence of \(\varGamma \vdash \phi \) and \(\exists \vec {x}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )\vdash \bot \), where \(\mathop {\dot{\sim }} \phi \) denotes the formula of \(\mathsf {L}\) that is equivalent to the weak negation of \(\phi \).

figure a

Let \(\vdash _{\mathsf {L}}^*\) denote the syntactic consequence relation associated with the system of \(\mathsf {L}\) extended with the rules \(\mathop {\dot{\sim }}\) Tr and \(\mathop {\dot{\sim }}\) E. We now prove the Soundness and Completeness Theorem for this extended system.

Theorem 4.3

Let \(\varGamma \cup \{\phi \}\) be a set of formulas of \(\mathsf {L}\) such that \(\phi \) is negatable in \(\mathsf {L}\). We have \(\varGamma \,\models \,\phi \iff \varGamma \vdash _{\mathsf {L}}^*\phi \).

Proof

“\(\Longleftarrow \)”: The Soundness of the system follows from Lemma 4.2; see Appendix I for the detailed proof.

“\(\Longrightarrow \)”: Since \(\mathsf {L}\) is compact, without loss of generality we may assume that \(\varGamma \) is finite. By Lemma 4.2 and the Completeness Theorem of \(\mathsf {L}\) (Theorem 4.1), we derive

$$\begin{aligned} \varGamma \,\models \,\phi \iff \exists \bar{x}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )\,\models \,\bot \iff \exists \bar{x}(\bigwedge \varGamma \wedge \mathop {\dot{\sim }} \phi )\vdash _{\mathsf {L}} \bot \iff \varGamma \vdash _{\mathsf {L}}^*\phi \end{aligned}$$

by applying the rules \(\mathop {\dot{\sim }}\) Tr and \(\mathop {\dot{\sim }}\) E.    \(\square \)

A key issue in the application of the extended system is the issue of computing the weak negation of formulas in \(\mathsf {L}\), or, as the first step, deciding which formulas are negatable in \(\mathsf {L}\). As we already remarked, even if we have established in Theorem 3.2 a characterization for negatable formulas, the latter problem is undecidable. Nevertheless, it is possible to identify some interesting classes of negatable formulas. This is what we will pursue in the next section. Let us proceed now to prove that first-order formulas are negatable in \(\mathcal {I}\). This will show that for independence logic Theorem 4.3 is indeed a generalization of Theorem 4.1 and also [15].

Given a first-order formula \(\phi \), consider its syntactic negation \(\lnot \phi \). By the flatness property and the Law of Excluded Middle, we have

$$\begin{aligned} M\models _X\lnot \phi \iff M\not \models _{\{s\}}\phi \text { for all }s\in X \end{aligned}$$
(5)

for all models M and all nonempty teams X. This also shows that \(\lnot \phi \) is in general not equivalent to \(\mathop {\dot{\sim }} \phi \), not even for atomic first-order formulas. Moreover, that the \(\varSigma ^1_1\)-translation \(\tau _\phi (R)\) of a first-order formula \(\phi \) is equivalent to a first-order sentence is not a trivial consequence of Theorem 2.4 either, because, for instance, the translation of a first-order disjunction \(\phi \vee \psi \), as given in [23], is \(\tau _{\phi \vee \psi }(R)=\exists S\exists S'(\tau _\phi (S)\wedge \tau _\psi (S')\wedge \forall \vec {x}(R\vec {x}\rightarrow (S\vec {x}\vee S'\vec {x})))\).

Proposition 4.4

If \(\phi \) is a first-order formula, then \(\mathop {\dot{\sim }} \phi (\vec {x})\equiv \exists \vec {w}(\vec {w}\subseteq \vec {x}\wedge \lnot \phi (\vec {w}))\). In particular, first-order formulas are negatable in \(\mathcal {I}\).

Proof

For all models M and all teams X, since \(\phi \) is flat,

$$\begin{aligned} M\models _X\mathop {\dot{\sim }} \phi \iff X=\emptyset \text { or }M\not \models _X\phi \iff X=\emptyset \text { or }\exists s\in X(M\not \models _{\{s\}}\phi (\vec {x})). \end{aligned}$$

By the empty team property of independence logic, it suffices to show that

$$\begin{aligned} \exists s\in X(M\not \models _{\{s\}}\phi (\vec {x}))\iff M\models _X\exists \vec {w}(\vec {w}\subseteq \vec {x}\wedge \lnot \phi (\vec {w})). \end{aligned}$$

for all models M and all nonempty teams X.

“\(\Longrightarrow \)”: Assume \(M\not \models _{\{s\}}\phi (\vec {x})\) for some \(s\in X\) and \(\vec {x}=x_1\dots x_n\). For each \(1\le i\le n\), inductively define a constant function \(F_i\) as follows:

  • \(F_1:X\rightarrow \wp (M)\setminus \{\emptyset \}\) is defined as \(F_1(t)=\{s(x_1)\}\);

  • \(F_i:X[F_1/w_1,\dots ,F_{i-1}/w_{i-1}]\rightarrow \wp (M)\setminus \{\emptyset \}\) is defined as \(F_i(t)=\{s(x_i)\}\).

Consider the team \(X[\vec {F}/\vec {w}]\) (see Fig. 1 in Appendix II for an example of such a team). Clearly, \(M\models _{X[\vec {F}/\vec {w}]}\vec {w}\subseteq \vec {x}\). On the other hand, for any \(t\in X[\vec {F}/\vec {w}]\), since \(t(\vec {w})=s(\vec {x})\) and \(M\not \models _{\{s\}}\phi (\vec {x})\), we obtain \(M\not \models _{\{t\}}\phi (\vec {w})\) by the locality property. Hence, \(M\models _{X[\vec {F}/\vec {w}]}\lnot \phi (\vec {w})\) by (5).

“\(\Longleftarrow \)”: Conversely, suppose \(M\models _X\exists \vec {w}(\vec {w}\subseteq \vec {x}\wedge \lnot \phi (\vec {w}))\). Then there are appropriate functions \(F_i\) for each \(1\le i\le n\) such that \(M\models _{X[\vec {F}/\vec {w}]}\vec {w}\subseteq \vec {x}\) and \(M\models _{X[\vec {F}/\vec {w}]}\lnot \phi (\vec {w})\). By (5), the latter implies that \(M\not \models _{\{t\}}\phi (\vec {w})\) for some \(t\in X[\vec {F}/\vec {w}]\). By the former, there exists \(s'\in X[\vec {F}/\vec {w}]\) such that \(s'(\vec {x})=t(\vec {w})\). This means, by the definition of \(X[\vec {F}/\vec {w}]\), that there exists \(s\in X\) such that \(s(\vec {x})=s'(\vec {x})=t(\vec {w})\). Hence, \(M\not \models _{\{s\}}\phi (\vec {x})\) by the locality property.    \(\square \)

We remarked that the \(\varSigma ^1_1\)-translation of a disjunction \(\phi \vee \psi \) of two negatable formulas \(\phi \) and \(\psi \) is not itself a first-order formula. In the literature there is another disjunction , under which the set of negatable formulas is closed:

  • iff \(M\models _X\phi \) or \(M\models _X\psi \)

In the presence of the downward closure property this disjunction is called intuitionistic disjunction, and in the environment of \(\mathcal {I}\) we shall call it Boolean disjunction. The disjunction is uniformly definable in \(\mathcal {D}\) or \(\mathcal {I}\) since

and clearly

Without going into detail we remark that the extended system can be applied to give a new formal proof of Arrow’s Impossibility Theorem [2] in social choice theory. In [22] the theorem is formulated as an entailment \(\varGamma _{\textsf {Arrow}}\,\models \,\phi _{\textsf {dictator}}\) in independence logic, where \(\varGamma _{\textsf {Arrow}}\) is a set of formulas expressing the conditions in Arrow’s Impossibility Theorem and \(\phi _{\textsf {dictator}}\) is a formula expressing the existence of a dictator. The formula \(\phi _{\textsf {dictator}}\) is of the form , where \(\phi _i\) is a first-order formula expressing that voter i is a dictator (among n voters). By what we just obtained, the formula \(\phi _{\textsf {dictator}}\) is negatable in \(\mathcal {I}\) and the Completeness Theorem guarantees that \(\varGamma _{\textsf {Arrow}}\vdash _{\mathcal {I}}^*\phi _{\textsf {dictator}}\) is derivable in our extended system.

5 A Hierarchy of Negatable Atoms

In this section, we define an interesting class of formulas that are negatable in \(\mathcal {I}\). This class will be presented in the form of an alternating hierarchy of atoms that are definable in \(\mathcal {I}\). These atoms are closely related to the dependency notions considered in [6], and the generalized dependence atoms studied in [16, 21]. We will demonstrate that all first-order formulas, dependence atoms, independence atoms and inclusion atoms belong to this class. It then follows from the completeness result we obtained in the previous section that consequences of these types in \(\mathcal {I}\) are derivable in the extended system.

Let us start by defining the notion of abstract relation. A k-ary relation R is a class of pairs \((M,R^M)\) that is closed under taking isomorphic images, where M ranges over first-order models and \(R^M\!\subseteq \! M^k\). For instance, the familiar equality \(=\) is a binary relation defined by the class

$$\begin{aligned} \{ (M, =^M)\mid M\text { is a first-order model} \},\text { where }=^M:=\{(a,a)\mid a\in M\}. \end{aligned}$$

Every first-order formula \(\phi (x_1,\dots ,x_k)\) with k free variables is associated with a k-ary relation

$$\begin{aligned} \pmb {\phi }:=\{(M,\pmb {\phi }^M)\mid M\text { is a first-order model}\}, \end{aligned}$$

where \(\pmb {\phi }^M:=\{(s(x_1),\dots ,s(x_k))\mid M\models _s\phi \}\). A k-ary relation R is said to be (first-order) definable if there exists a (first-order) formula \(\phi _R(w_1,\dots ,w_k)\) such that for all models M and all assignments s,

$$\begin{aligned} s(\vec {w})\in R^M \iff M\models _{s}\phi _{R}(\vec {w}). \end{aligned}$$

Clearly, the first-order formula \(w=u\) defines the equality relation, and every first-order formula \(\phi \) defines its associated relation \(\pmb {\phi }\).

If R is a k-ary relation, then we write \(\overline{R}\) for the complement of R that is defined by letting \(\overline{R}^M=M^k\setminus R^M\) for all models M. Clearly, if a first-order formula \(\phi \) defines R, then its negation \(\lnot \phi \) defines \(\overline{R}\).

If \(\vec {s}=\langle s_1,\dots ,s_k\rangle \), then we write \(\vec {s}(\vec {x})\) for \(\langle s_1(\vec {x}),\dots ,s_k(\vec {x})\rangle \). For every sequence \(\mathsf {k}=\langle k_1,\dots ,k_n\rangle \) of natural numbers and every \((k_1+\dots +k_n)m\)-ary relation R, we introduce two new atomic formulas \(\varSigma _{n,\mathsf {k}}^R(x_1,\dots ,x_m)\) and \(\varPi _{n,\mathsf {k}}^R(x_1,\dots ,x_m)\) with the semantics defined as follows:

  • \(M\models _\emptyset \varSigma _{n,\mathsf {k}}^R(\vec {x})\) and \(M\models _\emptyset \varPi _{n,\mathsf {k}}^R(\vec {x})\).

  • If n is odd, then define for any model M and any nonempty team X

    • \(M\models _X\varSigma _{n,\mathsf {k}}^R(\vec {x})\) iff there exist \(s_{11},\dots ,s_{1k_1}\in X\) such that for all \(s_{21},\dots ,s_{2k_2}\in X\), \(\dots \) there exist \(s_{n1},\dots ,s_{nk_n}\in X\) such that \((\vec {s_1}(\vec {x}),\dots ,\vec {s_{n}}(\vec {x}))\in R^M\);

    • \(M\models _X\varPi _{n,\mathsf {k}}^R(\vec {x})\) iff for all \(s_{11},\dots ,s_{1k_1}\in X\), there exist \(s_{21},\dots ,s_{2k_2}\in X\) such that \(\dots \) for all \(s_{n1},\dots ,s_{nk_n}\in X\), it holds that \((\vec {s_1}(\vec {x}),\dots ,\vec {s_{n}}(\vec {x}))\in R^M\).

  • Similarly if n is even.

Fact 5.1

\(\mathop {\dot{\sim }} \varSigma _{n,\mathsf {k}}^R(\vec {x})\equiv \varPi _{n,\mathsf {k}}^{\overline{R}}(\vec {x})\) and \(\mathop {\dot{\sim }} \varPi _{n,\mathsf {k}}^R(\vec {x})\equiv \varSigma _{n,\mathsf {k}}^{\overline{R}}(\vec {x})\).

Let us now give some examples of the \(\varSigma _{n,\mathsf {k}}^R\) and \(\varPi _{n,\mathsf {k}}^R\) atoms.

Example 5.2

 

  • (a) The dependence atom \(\mathop {=\!} (x_1,\dots ,x_k,y)\) is a \(\varPi ^{\mathbf {dep}_k}_{1,\langle 2\rangle }(x_1,\dots ,x_k,y)\) atom, where \(\mathbf {dep}_k\) is a \(2(k+1)\)-ary relation defined as

    $$\begin{aligned} (a_1,\dots ,a_k,b,a_1',\dots ,a_k',b')\in ( \mathbf {dep}_k)^M ~\text { iff }~[\,(a_1,\dots ,a_k)=(a_1',\dots ,a_k')\Longrightarrow b=b'\,]. \end{aligned}$$

    The first-order formula \(\big ((w_1=w_1')\wedge \dots \wedge (w_k=w_k')\big )\rightarrow (u=u')\) defines \(\mathbf {dep}_k\).

  • (b) The independence atom \(x_1,\dots ,x_k\perp _{z_1,\dots ,z_n} y_1,\dots ,y_m\) is a

    $$\begin{aligned} \varPi ^{\mathbf {ind}_{k,m,n}}_{2,\langle 2,1\rangle }(x_1,\dots ,x_k,y_1,\dots ,y_m,z_1,\dots ,z_n) \end{aligned}$$

    atom, where \(\mathbf {ind}_{k,m,n}\) is a (first-order definable) \((2+1)(k+m+n)\)-ary relation defined as \((\vec {a},\vec {b},\vec {c},\vec {a'},\vec {b'},\vec {c'},\vec {a''},\vec {b''},\vec {c''})\in (\mathbf {ind}_{k,m,n})^M\) iff

    $$\begin{aligned} (c_n,\dots ,c_n)=&(c_1',\dots ,c_n')=(c_1'',\dots ,c_n'')\\ \Longrightarrow&[\,(a''_1,\dots ,a''_k)=(a_1,\dots ,a_k)\text { and } (b''_1,\dots ,b''_m)=(b_1',\dots ,b_m')\,]. \end{aligned}$$

  • (c) The inclusion atom \(x_1,\dots ,x_k\subseteq y_1,\dots ,y_k\) is a \(\varPi ^{\mathbf {inc}_k}_{2,\langle 1,1\rangle }(x_1,\dots ,x_k,y_1,\dots ,y_k)\) atom, where \(\mathbf {inc}_k\) is a (first-order definable) \((1+1)2k\)-ary relation defined as

    $$\begin{aligned} (a_1,\dots ,a_k,b_1,\dots ,b_k,a_1',\dots ,a_k',b_1',\dots ,b_k')\!\in \! (\mathbf {inc}_k)^M~\!\!\text { iff }~(a_1,\dots ,a_k)\!=\!(b_1',\dots ,b_k'). \end{aligned}$$

  • (d) Every first-order formula \(\phi (x_1,\dots ,x_k)\) is a \(\varPi ^{\pmb {\phi }}_{1,\langle 1\rangle }(x_1,\dots ,x_k)\) atom, where \(\pmb {\phi }\) is a (first-order definable) \(1\cdot k\)-ary relation defined as

    $$\begin{aligned} (a_1,\dots ,a_k)\in \pmb {\phi }^M~\text { iff }~M\models _{s_{\vec {a}}}\phi \text { where }s_{\vec {a}}(x_i)=a_i\text { for all }i. \end{aligned}$$

In what follows, let \(\mathsf {k}=\langle k_1,\dots ,k_n\rangle \) be an arbitrary sequence of natural numbers, \(\vec {x}=\langle x_1,\dots ,x_m\rangle \) an arbitrary sequence of variables, and R an arbitrary \((k_1+\dots +k_n)m\)-ary relation. Suppose R is definable by a formula \(\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\), where \(\overrightarrow{\mathsf {w_i}}=\langle \mathsf {w_{i,1}},\dots ,\mathsf {w_{i,k_i}}\rangle \) and \(\mathsf {w_{i,j}}=\langle w_{i,j,1},\dots ,w_{i,j,m} \rangle \). The \(\varSigma _{n,\mathsf {k}}^R(\vec {x})\) and \(\varPi _{n,\mathsf {k}}^R(\vec {x})\) atoms can be translated into second-order logic in the same manner as in Theorem 2.4. For instance, if n is even, let S be a fresh m-ary relation symbol and let \(\tau _{\varSigma ^R_{n,\mathsf {k}}(\vec {x})}(S):=\)

$$\begin{aligned} \begin{array}{rl} \exists \overrightarrow{\mathsf {w_1}}\Big (S(\mathsf {w_{1,1}})\wedge \dots \wedge S(\!\!&{}\!\mathsf {w_{1,k_1}})\wedge \forall \overrightarrow{\mathsf {w_2}}\Big (S(\mathsf {w_{2,1}})\wedge \dots \wedge S(\mathsf {w_{2,k_2}})\rightarrow \exists \overrightarrow{\mathsf {w_3}}\cdots \\ &{}\cdots \exists \overrightarrow{\mathsf {w_n}}\Big (S(\mathsf {w_{n,1}})\wedge \dots \wedge S(\mathsf {w_{n,k_n}})\wedge \phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\underbrace{\Big )\cdots \Big )\Big )}_{n}. \end{array} \end{aligned}$$

Then, we have \(M\models _X\varSigma _{n,\mathsf {k}}^R(\vec {x})\iff (M,rel(X))\,\models \,\tau _{\varSigma _{n,\mathsf {k}}^R(\vec {x})}(S)\) for any model M and any team X. If \(\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\) is a first-order formula, i.e., if R is first-order definable, then \(\tau _{\varSigma _{n,\mathsf {k}}^R(\vec {x})}(S)\) is a first-order sentence. This shows, by Theorem 3.2(i), that \(\varSigma _{n,\mathsf {k}}^R(\vec {x})\) and \(\varPi _{n,\mathsf {k}}^R(\vec {x})\) atoms are negatable in \(\mathcal {I}\) as long as R is first-order definable.

Yet, in order to apply the rules of the extended deduction system defined in Sect. 4 to derive the \(\varSigma _{n,\mathsf {k}}^R(\vec {x})\) and \(\varPi _{n,\mathsf {k}}^R(\vec {x})\) consequences in \(\mathcal {I}\), one needs to compute the formulas that are equivalent to the weak classical negations of the \(\varSigma _{n,\mathsf {k}}^R(\vec {x})\) and \(\varPi _{n,\mathsf {k}}^R(\vec {x})\) atoms in the original language of \(\mathcal {I}\). This can be done by applying Fact 5.1 and going through the \(\varSigma ^1_1\)-translation (i.e. applying Theorem 2.4(ii) and (iv)). However, as the \(\varSigma ^1_1\)-translation creates a number of dummy symbols (see [5, 23]), such an algorithm is inefficient. In the remainder of this section, we will give a direct definition of the atoms \(\varSigma _{n,\mathsf {k}}^R(\vec {x})\) and \(\varPi _{n,\mathsf {k}}^R(\vec {x})\) in the original language of \(\mathcal {I}\).

For each \(1\le i\le n\), define

  • \(\displaystyle \mathsf {inc}(\mathsf {w_{i,1}},\dots ,\mathsf {w_{i,k_i}};\vec {x})\,:=\,\bigwedge _{j=1}^{k_i}(\mathsf {w_{i,j}}\subseteq \vec {x})\)

  • \(\mathsf {pro}(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_{i-1}}};\vec {x};\mathsf {w_{i,1}},\dots ,\mathsf {w_{i,k_i}})\,:=\)

    $$\begin{aligned} \,\left( \bigwedge _{j=1}^{k_i}(\vec {x}\subseteq \mathsf {w_{i,j}})\right) \wedge \left( \bigwedge _{j=1}^{k_i} (\langle \mathsf {w_{i,j'}}\mid j'\ne j\rangle \perp \mathsf {w_{i,j}})\right) \wedge (\overrightarrow{\mathsf {w_1}}\dots \overrightarrow{\mathsf {w_{i-1}}}\perp \mathsf {w_{i,1}}\dots \mathsf {w_{i,k_i}}) \end{aligned}$$

and inductively define formulas \(\sigma _i\) and \(\pi _i\) as follows:

  • \(\sigma _{1}[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]:=\exists \overrightarrow{\mathsf {w_n}}\Big ( \mathsf {inc}(\mathsf {w_{n,1}},\dots ,\mathsf {w_{n,k_n}};\vec {x})\wedge \phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\Big )\)

  • \(\pi _{1}[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]:=\exists \overrightarrow{\mathsf {w_n}}\Big (\mathsf {pro}(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_{n-1}}};\vec {x};\mathsf {w_{n,1}},\dots ,\mathsf {w_{n,k_n}})\wedge \phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\Big )\)

  • \(\sigma _{i+1}[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]:=\exists \overrightarrow{\mathsf {w_{n-i}}}\Big ( \mathsf {inc}(\mathsf {w_{n-i,1}},\dots ,\mathsf {w_{n-i,k_{n-i}}};\vec {x})\)

    \(\wedge \pi _{i}[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]\Big )\)

  • \(\pi _{i+1}[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]\displaystyle :=\exists \overrightarrow{\mathsf {w_{n-i}}}\Big (\mathsf {pro}(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_{n-i-1}}};\vec {x};\mathsf {w_{n-i,1}},\dots ,\mathsf {w_{n-i,k_{n-i}}})\)

    \( \wedge \sigma _{i}[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]\Big )\) Footnote 2

Theorem 5.3

Let R and \(\phi _R\) be as above. Then

  • \(\varSigma _{n,\mathsf {k}}^R(x_1,\dots ,x_m)\equiv \sigma _n[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]\)

  • \(\varPi _{n,\mathsf {k}}^R(x_1,\dots ,x_m)\equiv \pi _n[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]\)

Proof

We only give the detailed proof for \(\varSigma _{n,\mathsf {k}}^R(x_1,\dots ,x_m)\) when n is odd. The other case and the other equivalence can be proved analogously.

Our proof makes use of Lemma A in Appendix III. First, note that

$$\begin{aligned} \sigma _n[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]:=\exists&\overrightarrow{\mathsf {w_1}}\Big ( \mathsf {inc}(\mathsf {w_{1,1}},\dots ,\mathsf {w_{1,k_1}};\vec {x})\wedge \\&\displaystyle \exists \overrightarrow{\mathsf {w_2}}\Big (\mathsf {pro}(\overrightarrow{\mathsf {w_1}};\vec {x};\mathsf {w_{2,1}},\dots ,\mathsf {w_{2,k_2}}) \wedge \cdots \,\cdots \wedge \\&~~~~~\exists \overrightarrow{\mathsf {w_n}}\Big ( \mathsf {inc}(\mathsf {w_{n,1}},\dots ,\mathsf {w_{n,k_n}};\vec {x})\wedge \phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\underbrace{\Big )\cdots \Big )\Big )}_{n} \end{aligned}$$

Suppose \(M\models _X\varSigma _{n,\mathsf {k}}^R(\vec {x})\) for some model M and some nonempty team X. Then

$$\begin{aligned} (\exists \overrightarrow{s_1}\in X^{k_1})(\forall \overrightarrow{s_2}\in X^{k_2})\cdots \cdots ( \exists \overrightarrow{s_{n}}\in X^{k_n}) (\overrightarrow{s_1}(\vec {x}),\dots ,\overrightarrow{s_{n}}(\vec {x}))\in R^M. \end{aligned}$$
(6)

Let \(\varGamma _1=\langle \gamma _{1,1},\dots ,\gamma _{1,k_1}\rangle \) be a sequence of constant choice functions \(\gamma _{1,j}:X\rightarrow X\) defined as \(\gamma _{1,j}(t)=s_{1,j}\). Let \(\overrightarrow{F_{1,1}},\dots ,\overrightarrow{F_{1,k_1}}\) be the group of simulating functions for \(\varGamma _1[X]\upharpoonright \vec {x}\) on \(\mathsf {w_{1,1}},\dots ,\mathsf {w_{1,k_1}}\) and \(Y_1\) its associated team defined as in Lemma A(i) in Appendix III. Then, \(M\models _{Y_1}\mathsf {inc}(\mathsf {w_{1,1}},\dots ,\mathsf {w_{1,k_1}};\vec {x})\). It then remains to show that \(M\models _{Y_1} \pi _{n-1}[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]\).

Let \(\vec {F_{2,1}},\dots ,\vec {F_{2,k_2}}\) be the group of duplicating functions for \(Y_1\upharpoonright \vec {x}\) on \(\mathsf {w_{2,1}},\dots ,\mathsf {w_{2,k_2}}\), and \(Y_2\) its associated team defined as in Lemma A(ii) in Appendix III. Then, \(M\models _{Y_2}\mathsf {pro}(\overrightarrow{\mathsf {w_1}};\vec {x};\mathsf {w_{2,1}},\dots ,\mathsf {w_{2,k_2}})\).

It remains to show that \(M\models _{Y_2} \sigma _{n-2}[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]\). By Lemma A(ii), for each \(t\in Y_2\), there exists \(\overrightarrow{s_{t,2}}=( s^t_{2,1},\dots ,s^t_{2,k_2})\in X^{k_2}\) satisfying

$$\begin{aligned} s^t_{2,1}(\vec {x})=t(\mathsf {w_{2,1}}),\dots ,s^t_{2,k_2}(\vec {x})=t(\mathsf {w_{2,k_2}}). \end{aligned}$$

Hence, by (6), there exists \(\overrightarrow{s_{t,3}}=( s^t_{3,1},\dots ,s^t_{3,k_3})\in X^{k_3}\) such that

$$\begin{aligned} (\forall \overrightarrow{s_4}\in X^{k_4})\cdots \cdots ( \exists \overrightarrow{s_{n}}\in X^{k_n}) (\overrightarrow{s_1}(\vec {x}),\overrightarrow{s_{t,2}}(\vec {x}),\overrightarrow{s_{t,3}}(\vec {x}),\overrightarrow{s_4}(\vec {x})\dots ,\overrightarrow{s_{n}}(\vec {x}))\in R^M. \end{aligned}$$

Let \(\varGamma _3=\langle \gamma _{3,1},\dots ,\gamma _{3,k_3}\rangle \) be a sequence of choice functions \(\gamma _{3,j}: Y_2\rightarrow Y_2\) defined as \(\gamma _{3,j}(t)=s_{3,j}^t\). Let \(\overrightarrow{F_{3,1}},\dots ,\overrightarrow{F_{3,k_3}}\) be the group of simulating functions for \(\varGamma _3[Y_2]\upharpoonright \vec {x}\) on \(\mathsf {w_{3,1}},\dots ,\mathsf {w_{3,k_3}}\), and \(Y_3\) its associated team defined as in Lemma A(i) in Appendix III. Then, \(M\models _{Y_3}\mathsf {inc}(\mathsf {w_{3,1}},\dots ,\mathsf {w_{3,k_3}};\vec {x})\) and it remains to show that \(M\models _{Y_3} \pi _{n-3}[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]\).

Repeat the argument n times. In the last step we have \(Y_n\) and \(\varGamma _n\) defined and \(M\models _{Y_n}\mathsf {inc}(\mathsf {w_{n,1}},\dots ,\mathsf {w_{n,k_n}};\vec {x})\) by Lemma A(i). It then only remains to show that \(M\models _{Y_n}\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\). Since \(\phi _R\) is flat, it suffices to show that \(M\models _{\{t\}}\phi _R\) holds for all \(t\in Y_n\). By the definition of \(Y_n\) and Lemma A(i)(ii), we have

$$\begin{aligned} (\overrightarrow{s_1}(\vec {x}),\overrightarrow{s_{t,2}}(\vec {x}),\overrightarrow{s_{t,3}}(\vec {x}),\overrightarrow{s_{t,4}}(\vec {x})\dots ,\overrightarrow{s_{t,n}}(\vec {x}))\in R^M \end{aligned}$$
$$\begin{aligned} \text {and } t(\overrightarrow{\mathsf {w_1}})=\overrightarrow{s_1}(\vec {x}),~t(\overrightarrow{\mathsf {w_2}})=\overrightarrow{s_{t,2}}(\vec {x}),~\dots ,~t(\overrightarrow{\mathsf {w_n}})=\overrightarrow{s_{t,n}}(\vec {x}). \end{aligned}$$

Thus, \(M\models _{\{t\}}\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\), as the first-order formula \(\phi _R\) defines R.

Conversely, suppose \(M\models _X\sigma _n[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]\) for some model M and some nonempty team X. Let Y be a team generated by the formula \(\sigma _n[\vec {x};\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})]\) from X such that \(M\models _Y\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\).

Pick any \(t\in Y\). Since \(M\models _Y \mathsf {inc}(\mathsf {w_{1,1}},\dots ,\mathsf {w_{1,k_1}};\vec {x})\), there exist \(s_{1,1},\dots ,s_{1,k_1}\in X\) such that

$$\begin{aligned} s_{1,1}(\vec {x})=t(\mathsf {w}_{1,1}),\dots ,s_{1,k_1}(\vec {x})=t(\mathsf {w}_{1,k_1}). \end{aligned}$$

Let \(s_{2,1},\dots ,s_{2,k_2}\in X\) be arbitrary. Since \(M\models _Y\mathsf {pro}(\overrightarrow{\mathsf {w_1}};\vec {x};\mathsf {w_{2,1}},\dots ,\mathsf {w_{2,k_2}})\), it is not hard to see that there exist \(t_2\in Y\) such that

$$\begin{aligned} t_2(\overrightarrow{\mathsf {w}_1})=t(\overrightarrow{\mathsf {w}_1})=\overrightarrow{s_{1}}(\vec {x})\text { and }s_{2,1}(\vec {x})=t_2(\mathsf {w}_{2,1}),\dots ,s_{2,k_2}(\vec {x})=t_2(\mathsf {w}_{2,k_2}). \end{aligned}$$

Repeat the argument n times to find in the same manner the corresponding assignments \(\overrightarrow{s_{3}}\in X^{k_3},\overrightarrow{s_{5}}\in X^{k_5},\dots ,\overrightarrow{s_{n}}\in X^{k_n}\) and the corresponding assignments \(t_4,t_6,\dots ,\) \(t_{n-1}\in Y\) for arbitrary \(\overrightarrow{s_{4}}\in X^{k_4},\overrightarrow{s_{6}}\in X^{k_6},\dots ,\overrightarrow{s_{n-1}}\in X^{k_{n-1}}\). In the last step we have

$$\begin{aligned} t_{n-1}(\overrightarrow{\mathsf {w}_1})=\overrightarrow{s_{1}}(\vec {x}),\dots ,t_{n-1}(\overrightarrow{\mathsf {w}_{n-1}})=\overrightarrow{s_{n-1}}(\vec {x}) \end{aligned}$$

and there exist \(s_{n,1},\dots ,s_{n,k_n}\in X\) such that

$$\begin{aligned} s_{n,1}(\vec {x})=t_{n-1}(\mathsf {w}_{n,1}),\dots ,s_{n,k_n}(\vec {x})=t_{n-1}(\mathsf {w}_{n,k_n}). \end{aligned}$$

Since \(M\models _Y\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\), we have \(M\models _{\{t_{n-1}\}}\phi _R(\overrightarrow{\mathsf {w_1}},\dots ,\overrightarrow{\mathsf {w_n}})\) by the downward closure property. Since the first-order formula \(\phi _R\) defines R, we conclude

$$\begin{aligned} (t_{n-1}(\overrightarrow{\mathsf {w}_1}),\dots ,t_{n-1}(\overrightarrow{\mathsf {w}_n}))\in R^M\text { yielding } (\overrightarrow{s_1}(\vec {x}),\dots ,\overrightarrow{s_{n}}(\vec {x}))\in R^M. \end{aligned}$$

   \(\square \)

6 Concluding Remarks

In this paper, we have extended the natural deduction systems of dependence and independence logic defined in [10, 20] and obtained complete axiomatizations of the negatable consequences in these logics. We also gave a characterization of negatable formulas in \(\mathcal {I}\) and negatable sentences in \(\mathcal {D}\). Determining whether a formula of \(\mathcal {I}\) or \(\mathcal {D}\) is negatable is an undecidable problem. Nevertheless, we identified an interesting class of negatable formulas. Formulas in this class are presented as \(\varSigma _{n,\mathsf {k}}^R\) and \(\varPi _{n,\mathsf {k}}^R\) atoms. First-order formulas, dependence and independence atoms belong to this class. Since the set of negatable formulas is closed under the Boolean connectives \(\wedge \) and , Boolean combinations of \(\varSigma _{n,\mathsf {k}}^R\) and \(\varPi _{n,\mathsf {k}}^R\) atoms are also negatable.

An interesting corollary of the paper is that Armstrong’s Axioms [1] that characterize dependence atoms and the Geiger-Paz-Pearl axioms [8] that characterize independence atoms can be derived in our extended system of \(\mathcal {I}\). We leave the derivations of these axioms for future work.

The results of this paper can be generalized in two directions. The first direction is to identify other negatable formulas than those in the set of the Boolean combinations of atoms from our hierarchy. The other direction is to analyze the \(\varSigma _{n,\mathsf {k}}^R\) and \(\varPi _{n,\mathsf {k}}^R\) atoms in more detail. As we saw in Example 5.2, first-order formulas and the atoms of dependence and independence situate only on the \(\varPi _1\) or \(\varPi _2\) level. Identifying interesting properties that situate on higher levels of the hierarchy and studying the logics that the higher level atoms induce would be an interesting topic for future research. For example, it is easy to verify that \(\varPi _{1,\mathsf {k}}^R\) atoms (including first-order formulas and dependence atoms) are closed downward, and \(\varSigma _{1,\mathsf {k}}^R\) atoms are closed upward. First-order logic extended with upward closed atoms is shown in [7] to be equivalent to first-order logic. Adding other such atoms to first-order logic results in many new logics that are expressively less than \(\varSigma ^1_1\) or independence logic and possibly stronger than first-order logic. These logics are potentially interesting, because, for instance, by the argument of this paper, the negatable consequences in these logics can in principle be axiomatized.