1 Introduction↩︎

In this paper, we introduce labelled sequent calculi for a family of propositional logics based on team semantics. Team semantics is a generalization of Tarskian semantics where formulas are evaluated over sets of evaluation points (called teams) rather than single evaluation points. It was introduced by Hodges [@hodges:1997] to characterize dependence and independence between variables. This framework was later systematically developed in dependence logic [@vaananen:2007]. Inquisitive semantics [@ciardelli:roelofsen:2011] also uses the framework to formalize the meaning of interrogative sentences in natural language. Team semantics has found applications in diverse areas, such as database theory (e.g., [@HannulaKL16]), formal semantics of natural language [@ciardelli:2016; @Aloni2022], social choice theory [@PacuitYan16] and quantum information theory [@CoranderHKPV16; @AlbertGradel2022; @AbramskyPuljVaan2026].

Most prominent logics based on team semantics are downward closed, i.e., their satisfaction relation is preserved under taking subteams. In this work, we focus on this class of logics, and in particular we consider basic inquisitive logic (\(\mathsf{InqB}\), from [@ciardelli:roelofsen:2011]), propositional intuitionistic dependence logic (\(\mathsf{PID}\), from  [@yang:vaananen:2016]) and their respective extensions with tensor disjunction \(\vee\) (\(\mathsf{InqB}_{\vee}\) and \(\mathsf{PID}_{\vee}\)). All these logics include operators for intuitionistic implication \(\to\) and global (or inquisitive) disjunction \(\mathbin{\mathpalette\d@vee\relax}\). The logics \(\mathsf{PID}\) and \(\mathsf{PID}_{\vee}\) additionally include dependence atoms. A Hilbert-style system for the logic \(\mathsf{InqB}\) was presented in [@ciardelli:roelofsen:2011], while natural deduction systems for propositional dependence logic (which does not have an implication) and its variants (including \(\mathsf{PID}\), \(\mathsf{PID}_{\vee}\) and \(\mathsf{InqB}_{\vee}\)) were introduced in [@yang:vaananen:2016; @ciardelli:2016].

While the semantic properties of downward closed team logics are well understood in the literature, their proof theory has not been fully investigated. In particular, designing analytic proof systems for these logics remains a challenging task. All the calculi in the literature are generalizations of the Gentzen-style sequent formalism. For instance, Frittella et al. [@frittella2016multi-type] introduced a multi-type display calculus for \(\mathsf{InqB}\) in the style of Belnap [@belnap1982display], and Anttila, Iemhoff and Yang [@anttila2025deep] developed a sequent calculus for \(\mathsf{InqB}_{\vee}\) employing a form of deep inference. Both systems enrich the structure of Gentzen sequents.

An alternative approach is to enrich the language of the calculus instead, which is the approach we take in this paper for our labelled sequent calculi for the logics \(\mathsf{InqB}\), \(\mathsf{InqB}_{\vee}\), \(\mathsf{PID}\) and \(\mathsf{PID}_{\vee}\). The calculi we present for these logics are modular, meaning that by adding rules they can be adapted to capture logics built up from different sets of connectives or atoms. For instance, by extending our calculi for \(\mathsf{InqB}\) and \(\mathsf{InqB}_{\vee}\) with two natural rules for dependence atoms, we obtain calculi for \(\mathsf{PID}\) and \(\mathsf{PID}_{\vee}\). The modularity feature sets our proof systems apart from the structured calculi presented in [@frittella2016multi-type; @anttila2025deep].

Labelled sequent calculi for the logic \(\mathsf{InqB}\) (which does not include the tensor disjunction \(\vee\)) have already been presented by Chen and Ma [@chen:ma:2017] and later by Müller [@muller:msc:2023]¹ as well as by Litak and Sano [@litak:sano:2026]. Our calculi for the four logics under consideration have a similar design as the ones presented in [@chen:ma:2017; @muller:msc:2023], i.e., we also use labels to represent arbitrary teams, singleton teams as well as certain set-theoretic operations on them. Our labelled calculus for \(\mathsf{InqB}\), however, is simpler than the ones from [@chen:ma:2017] and [@muller:msc:2023], since it does not include labels representing intersections. In fact, we will use such labels only for the logics involving tensor disjunction (i.e., for \(\mathsf{InqB}_{\vee}\) and \(\mathsf{PID}_{\vee}\)).

A key technical challenge in designing calculi for logics with tensor disjunction is its different behaviour on classical and general formulas, which makes it difficult to define labelled rules for \(\mathsf{InqB}_{\vee}\) and \(\mathsf{PID}_{\vee}\) using the standard techniques. To address this difficulty, we restrict our attention to languages containing only finitely many propositional variables. This assumption (which does not affect validity in \(\mathsf{InqB}_{\vee}\) or \(\mathsf{PID}_{\vee}\)) restricts the semantics to finitely many valuations and teams, thus allowing us to introduce a new order rule (\(\mathsf{fin}\)) that provides enough labels to describe arbitrary valuations and teams. Thanks to this rule, we can simulate the behaviour of the tensor over classical formulas.

Using syntactic arguments, we prove that all our calculi enjoy cut-admissibility. This property, together with the admissibility of additional rules capturing key semantic properties, allows us to establish the completeness of our proof systems. We then present a family of terminating labelled calculi for all the logics under consideration. These calculi are obtained by simplifying the structure of labels in our systems. Their construction crucially relies on the assumption that the language has finitely many propositional variables. Our terminating calculus for \(\mathsf{InqB}\) is similar to the ones introduced by Litak and Sano [@litak:sano:2026] for basic inquisitive logic and for bounded versions of inquisitive predicate logic. We extend this approach to cover \(\mathsf{InqB}_{\vee}\), \(\mathsf{PID}\) and \(\mathsf{PID}_{\vee}\), and provide an explicit proof search algorithm for all the calculi.

The paper is structured as follows. In Section 2, we recall the semantics and axiom systems of the logics we consider, and in Section 3, we introduce our labelled calculi. In Section 4, we discuss the structural properties of the calculi, and in Section 5, we establish their completeness. In Section 6, finally, we present an explicit proof search algorithm for terminating variants of our calculi.

2 Preliminaries↩︎

We start by recalling some basic notions. For further details, see [@ciardelli:roelofsen:2011; @ciardelli:phd:2016; @yang:vaananen:2016]. Throughout this paper, we will assume a non-empty set \(\mathsf{P}\) of propositional variables (or atoms). For reasons that will become apparent later on, we assume that \(\mathsf{P}\) is finite.² Elements of \(\mathsf{P}\) are denoted by the letters \(p\) and \(q\) (possibly with subscripts). The language of downward-closed team logic, notation \(\mathcal{L}\), is given by the grammar \[\varphi ::= p \mid \bot \mid {=}(p) \mid \varphi\wedge\varphi \mid \varphi\vee\varphi \mid \varphi\mathbin{\mathpalette\d@vee\relax}\varphi \mid \varphi\rightarrow\varphi \quad (p\in\mathsf{P}).\] We also define \(\neg\varphi := \varphi\rightarrow\bot\) and \(\varphi\leftrightarrow\psi := (\varphi\rightarrow\psi)\wedge(\psi\rightarrow\varphi)\). We will refer to \(\vee\), \(\mathbin{\mathpalette\d@vee\relax}\) and \(\rightarrow\) as tensor disjunction, global disjunction and intuitionistic implication, respectively. In the literature on dependence logic, expressions of the form \({=}(p)\) are known as constancy dependence atoms and used to express that \(p\) has a fixed value [@yang:vaananen:2016]. Dependence atoms with multiple arguments can be defined from constancy atoms by putting \({=}(q_1,\ldots,q_n,p) := ({=}(q_1)\wedge\ldots\wedge{=}(q_n))\rightarrow {=}(p)\). Intuitively, \({=}(q_1,\ldots,q_n,p)\) expresses that the value of \(p\) depends on the values of \(q_1,\ldots,q_n\). In the literature on inquisitive logic, the global disjunction is also known as inquisitive disjunction and used to form alternative questions. Thus, in this framework, \(\varphi\mathbin{\mathpalette\d@vee\relax}\psi\) is interpreted as the question whether \(\varphi\) or \(\psi\) [@ciardelli:phd:2016].

Formulas of our language are evaluated over teams (a.k.a.information states). A team over \(\mathsf{P}\) is a set of valuations \(v:\mathsf{P}\rightarrow\{0,1\}\). The set of all valuations is given by \(\mathcal{V}(\mathsf{P}):= \{v\mid v:\mathsf{P}\rightarrow\{0,1\}\}\). Note that, since \(\mathsf{P}\) is finite, \(\mathcal{V}(\mathsf{P})\) is also finite, and each team \(T\subseteq\mathcal{V}(\mathsf{P})\) contains at most \(|\mathcal{V}(\mathsf{P})| = 2^{|\mathsf{P}|}\) elements.

It is easy to show that all \(\mathcal{L}\)-formulas satisfy the empty team property and downward closure.

A formula \(\varphi\in\mathcal{L}\) is said to be classical, if it does not contain any occurrences of the connectives \(\mathbin{\mathpalette\d@vee\relax}\) and \({=}(\cdot)\). Classical formulas will be denoted by the letters \(\alpha\), \(\beta\), \(\gamma\). We also write \(\mathcal{L}_{c}\) for the set of all classical formulas. Classical formulas satisfy both union closure and flatness (or truth-conditionality).

The first column of Table 1 contains four team-based logics: basic inquisitive logic (\(\mathsf{InqB}\)), propositional intuitionistic dependence logic (\(\mathsf{PID}\)), and their respective extensions with tensor disjunction (\(\mathsf{InqB}_{\vee}\) and \(\mathsf{PID}_{\vee}\)). The second column specifies the corresponding fragment of the language \(\mathcal{L}\). So, for example, the language of \(\mathsf{InqB}\) consists of all formulas built up from the variables in \(\mathsf{P}\) by means of the connectives \(\bot,\wedge,\mathbin{\mathpalette\d@vee\relax},\rightarrow\), and the language of \(\mathsf{PID}\) consists of all formulas built up from the variables by means of the connectives \(\bot,\wedge,\mathbin{\mathpalette\d@vee\relax},\rightarrow,{=}(\cdot)\). The language associated with one of our four logics \(L\) will also be denoted by \(\mathcal{L}(L)\). Observe that, in particular, \(\mathcal{L}(\mathsf{PID}_{\vee})\) coincides with the full language \(\mathcal{L}\).

The last column of Table 1 contains the names of four Hilbert-style systems. The axiom schemes of these systems are presented in the upper section of Figure 1. Note that, in the schemes \(\mathrm{(S)}\), \(\mathrm{(DN)}\), \(\mathrm{(Elim)}\), we require \(\alpha\) to range over classical formulas only. The lower section of Figure 1 contains the definitions of our Hilbert calculi. For example, \(\mathsf{HInqB}_{\vee}\) consists of the basic axioms, the tensor axioms and the rule of modus ponens. The Hilbert system associated with a logic \(L\) will also be denoted by \(\mathcal{H}(L)\).

Let now \(L\) be any of the logics from Table 1 and let \(\Gamma\cup\{\varphi\}\subseteq\mathcal{L}(L)\). We write \(\Gamma\vdash\varphi\) and say that \(\varphi\) is provable from \(\Gamma\) in \(\mathcal{H}(L)\), if there exists a sequence \(\psi_1,\ldots,\psi_n\) of formulas from \(\mathcal{L}(L)\) such that \(\varphi = \psi_n\) and every \(\psi_i\) with \(1\leq i\leq n\) is either an axiom of \(\mathcal{H}(L)\) or an element of \(\Gamma\), or it can be obtained from two formulas occurring earlier in the sequence by modus ponens. Moreover, we write \(\Gamma\models_{L}\varphi\) and say that \(\varphi\) is entailed by \(\Gamma\) in \(L\), if for every team \(T\subseteq\mathcal{V}(\mathsf{P})\), \(T\models\psi\) for all \(\psi\in\Gamma\) implies \(T\models\varphi\).

3 Labelled Sequent Calculi↩︎

We will now introduce labelled sequent calculi for each of the logics presented in Table 1. The labels used in our calculi are built up from two infinite sets of team variables, denoted by \(\mathfrak{S}\) and \(\mathfrak{A}\). The variables from \(\mathfrak{S}\) range over singleton teams and the variables from \(\mathfrak{A}\) range over teams of arbitrary size. Elements of \(\mathfrak{S}\) are denoted by the letters \(u\), \(v\), \(w\), and elements of \(\mathfrak{A}\) are denoted by the letters \(x\), \(y\), \(z\).

The set of labels \(\mathsf{Lab}\) will be used in our calculi for \(\mathsf{InqB}\) and \(\mathsf{PID}\), and the set of labels \(\mathsf{Lab}_{\cap}\) will be used in our calculi for \(\mathsf{InqB}_{\vee}\) and \(\mathsf{PID}_{\vee}\). Arbitrarily complex labels from any of the sets \(\mathsf{Lab}\) and \(\mathsf{Lab}_{\cap}\) will be denoted by the meta-variables \(\pi\), \(\sigma\), \(\tau\). Intuitively, \(\pi\cup\sigma\) represents the union and \(\pi\cap\sigma\) represents the intersection of the teams denoted by \(\pi\) and \(\sigma\). The constant \(\emptyset\) stands for the empty team.

A labelled formula is an expression of the form \(\pi:\varphi\), where \(\pi\) is a label and \(\varphi\) is a formula. Labelled formulas internalise the satisfaction relation into our calculi, so \(\pi:\varphi\) may be read as “The team \(\pi\) satisfies the formula \(\varphi\)”. A relational atom is an expression of the form \(\pi\subseteq \sigma\), where \(\pi\) and \(\sigma\) are labels, meaning that \(\pi\) is a subset of \(\sigma\). A sequent is an expression of the form \(\Gamma\Rightarrow\Delta\), where \(\Gamma\) is a finite multiset of labelled formulas and relational atoms and \(\Delta\) is a finite multiset containing only labelled formulas.

We say that a labelled formula \(\pi:\varphi\) is satisfied by an interpretation \(I\) if it holds that \(I(\pi)\models\varphi\). And a relational atom \(\pi\subseteq \sigma\) is satisfied by \(I\) if \(I(\pi)\subseteq I(\sigma)\). A sequent \(\Gamma\Rightarrow\Delta\) is valid if for every interpretation \(I\), it is the case that, if \(I\) satisfies all elements of \(\Gamma\), then \(I\) satisfies at least one element of \(\Delta\).

The axioms and rules of our labelled sequent calculi are presented in the upper section of Figure 2. Note that, in the rule \(\mathsf{fin}\), we use the notation “\(\sigma = \tau\)” as an abbreviation for the pair of atoms “\(\sigma\subseteq \tau,\tau\subseteq \sigma\)”. Furthermore, certain rules come with additional side conditions. For example, \(v\in\mathfrak{S}\) has to be a fresh variable in all rules marked with \((\ddagger)\), and \(x\in\mathfrak{A}\) has to be fresh in the rule marked with \((\S)\). Here, a variable is said to be fresh, if it does not occur in the conclusion of the respective rule application. The fresh variables introduced by the rules \(\mathsf{at}_{R}\), \(\bot_{R}\), \(\rightarrow_{R}\), \(\vee_{L}\), \(=_{R}\) and \(\mathsf{fin}\) are also referred to as the eigenvariables of these rules.

The rules of our proof systems are inspired by the \(\mathsf{G3}\)-style approach to labelled calculi as detailed, e.g., in [@negri:2005] for the case of modal logic. However, the richer semantics of team-based logics requires non-trivial adjustments and the addition of several more order rules than in the modal case. The basic logical rules, the tensor rules and the constancy rules simply mirror the satisfaction conditions from Definition 1. The basic and special order rules, on the other hand, formalize various set-theoretic properties of teams. The rule \(\mathsf{fin}\) plays a somewhat special role here, as it is directly linked to the assumption that \(\mathsf{P}\) is finite. Intuitively, this rule expresses the fact that every team \(\pi\) is either empty or composed of \(n = 2^{|\mathsf{P}|}\) not necessarily distinct valuations. Note that, in applications of \(\mathsf{fin}\), we do not require the union operators in the label \(v_{1}\cup\ldots\cup v_{n}\) to be grouped in any specific way. So, for example, in the case \(|\mathsf{P}| = 2\), the sequents \(\pi = ((v_{1}\cup v_{2})\cup v_{3})\cup v_{4}, \Gamma\Rightarrow\Delta\) and \(\pi = (v_{1}\cup v_{2})\cup (v_{3}\cup v_{4}), \Gamma\Rightarrow\Delta\) would both be correct instances of the right premise of \(\mathsf{fin}\).

The lower section of Figure 2 contains the definitions of our calculi. For example, the calculus \(\mathsf{GPID}\) consists of the initial sequents, the basic logical rules, the constancy rules and the basic order rules. Given any of the logics \(L\) from Table 1, we will write \(\mathcal{G}(L)\) for the corresponding calculus from Figure 2.

In each of the axioms and rules from Figure 2, we call \(\Gamma\) and \(\Delta\) the left context and the right context, respectively. An occurrence of an expression in an axiom or in the conclusion of a rule is called principal, if it does not belong to the context. To ensure that contraction is admissible, we adopt the closure condition from [@negri:plato:1998; @negri:2003; @negri:2005; @dyckhoff:negri:2012]: if an instance of a rule of one of our calculi contains two principal occurrences of a relational atom \(A\) in the conclusion, then also the contracted instance of the rule (in which the two occurrences of \(A\) are replaced by a single one) is taken to be part of the corresponding calculus. For example, in the special case where \(\pi=\sigma\), we permit not only the instance of the rule \(\mathsf{ul}\) shown on the left-hand side below, but also the contracted instance displayed on the right-hand side:

The following lemma contains several sequents that are derivable in our calculi. Observe that sequent ([gen:ax:i]) corresponds to downward closure and sequents ([gen:ax:ii]) and ([gen:ax:iii]) correspond to the empty team property.

4 Structural Properties↩︎

We now examine the structural properties of our labelled calculi. Specifically, we will prove the admissibility of weakening and contraction, the invertibility of all rules, and the admissibility of the cut rule. In Section 5, we will use these results to establish the completeness of our proof systems. In what follows, let \(L\) be any of the logics from Table 1 and let \(\mathcal{G}(L)\) be the associated sequent calculus from Figure 2.

We first recall some basic definitions. By the length of a branch in a derivation, we mean the number of sequents occurring in the branch. The height of a derivation \(\mathcal{D}\) is the length of one of its longest branches, minus one. A rule \(R\) is height-preserving admissible (or hp-admissible) in the calculus \(\mathcal{G}(L)\), if whenever each premise of \(R\) is derivable by a derivation of height at most \(n\), then the conclusion of \(R\) is derivable by a derivation of height at most \(n\). If derivability of the premises implies derivability of the conclusion, but the height is not preserved, \(R\) is just said to be admissible. A rule \(R\) is height-preserving invertible (or hp-invertible) in \(\mathcal{G}(L)\), if whenever the conclusion of \(R\) is derivable by a derivation of height at most \(n\), then each premise of \(R\) is derivable, with the same bound on height [@troelstra:schwichtenberg:1996].

Given any variable \(s\in\mathfrak{S}\cup\mathfrak{A}\) and labels \(\pi,\sigma\in\mathsf{Lab}_{\cap}\), we write \(\sigma(\pi/s)\) for the result of substituting \(\pi\) for all occurrences of \(s\) in \(\sigma\). The notation \(\Gamma(\pi/s)\) stands for the result of substituting \(\pi\) for \(s\) in all labels that occur in a multiset \(\Gamma\). By the substitution rules, we mean the first two rules displayed in Figure 3.

The admissibility of both substitution rules is established simultaneously, by induction on the height of a derivation for the premise. Further details are provided in [@muller:msc:2023]. Using this result, we can now prove the admissibility of the weakening rules, the contraction rules and the cut rule (see Figure 3).

The proof of this theorem follows the same structure as the standard admissibility proofs for structural rules in \(\mathsf{G3}\)-style systems (see [@negri:plato:2001; @negri:2005]). Further details are in Appendix 8, and similar proofs are in [@muller:msc:2023].

5 Completeness↩︎

To establish the completeness of our proof systems, we will now prove that each of the labelled sequent calculi from Figure 2 is complete with respect to the corresponding Hilbert-style system from Figure 1. For technical reasons, we first prove the admissibility of the rules \(\mathsf{aux}_{1}\) and \(\mathsf{aux}_{2}\) presented in Figure 4.

A proof is provided in Appendix 9. Next, we need to establish the admissibility of the rules \(\mathsf{mp}\) and \(\mathsf{flat}\) (see Figure 4). The rule \(\mathsf{mp}\) corresponds to modus ponens and the rule \(\mathsf{flat}\) accounts for the flatness of classical formulas: if a classical formula \(\alpha\) is true under every valuation \(v\) in a team, then it is also satisfied by this team (see Section 2). For the calculi not involving tensor (i.e., for \(\mathsf{GInqB}\) and \(\mathsf{GPID}\)), the admissibility of the rule \(\mathsf{flat}\) can simply be established by induction on the structure of \(\alpha\) (cf.[@muller:msc:2023]). For the other two calculi (i.e., for \(\mathsf{GInqB}_{\vee}\) and \(\mathsf{GPID}_{\vee}\)), we first need the following lemma.

We are now ready to prove the desired admissibility results.

In the case \(L\in\{\mathsf{InqB}_{\vee},\mathsf{PID}_{\vee}\}\), our admissibility proof for \(\mathsf{flat}\) crucially uses the rule \(\mathsf{fin}\) and thus relies on the assumption that \(\mathsf{P}\) is finite. Using the admissibility of the rules \(\mathsf{mp}\) and \(\mathsf{flat}\), we now prove that each of our calculi is complete with respect to the corresponding Hilbert-style system from Figure 1.

6 Proof Search↩︎

We now want to describe a terminating proof search algorithm for the logics presented in Section 2. To avoid certain complications arising from the complex syntax of the labels presented in Definition 2, we first introduce an alternative class of labelled sequent calculi for our logics, in which labels are defined as sets of variables.³ This eliminates the need for relational atoms and order rules, which simplifies the proof of termination significantly. Throughout this section, we will assume an infinite set \(\mathfrak{V}\) of variables ranging over propositional valuations. Elements of \(\mathfrak{V}\) are denoted by the meta-variables \(u\) and \(v\).

A label of the form \(\pi = \{v_{1},\ldots,v_{k}\}\) stands for the finite team consisting of the valuations represented by \(v_{1},\ldots,v_{k}\) (which do not need to be distinct). Arbitrary labels are denoted by \(\pi\), \(\sigma\), \(\tau\). A split of a label \(\pi\) is a pair of labels \((\sigma,\tau)\) such that \(\pi = \sigma\cup\tau\). The set of all splits of \(\pi\) is denoted by \(S(\pi)\), so \(S(\pi) := \{(\sigma,\tau) \mid \pi = \sigma\cup\tau\}\). A labelled formula is an expression of the form \(\pi:\varphi\), where \(\pi\subseteq\mathfrak{V}\) is a label and \(\varphi\in\mathcal{L}\) is a formula. If \(\pi = \{v\}\) is a singleton label, then we write \(v:\varphi\) instead of \(\pi:\varphi\). As before, \(\pi:\varphi\) may be read as “\(\varphi\) is satisfied by the team \(\pi\)”. A sequent is an expression of the form \(\Gamma\Rightarrow\Delta\), where \(\Gamma\) and \(\Delta\) are finite multisets of labelled formulas (thus, sequents do not contain relational atoms).

A labelled formula \(\pi:\varphi\) is satisfied by an interpretation \(I\), if \(I(\pi)\models\varphi\). And a sequent \(\Gamma\Rightarrow\Delta\) is valid, if for each interpretation \(I\), we have: if \(I\) satisfies all elements of \(\Gamma\), then \(I\) satisfies at least one element of \(\Delta\). The axioms and rules of our terminating calculi are presented in Figure 5. Note that, in the figure, we use square brackets to denote collections of premises. So, for example, an application of the rule \(\mathsf{at}_{R}\) with principal formula \(\pi:p\) now has exactly \(|\pi|\) premises—namely, one premise for each variable \(v\in\pi\). In the special case \(\pi = \emptyset\), we treat \(\mathsf{at}_{R}\), \(\bot_{R}\) and \(=_{R}\) as initial sequents (i.e., rules with zero premises). Some of our rules are also subject to additional side conditions, which are indicated on the right-hand side of the “inference line”. For instance, the pair \((\sigma,\tau)\) must be a split of \(\pi\) in applications of \(\vee_{R}\). The rules \(\mathsf{at}_{L}\), \(\bot_{L}\), \(\rightarrow_{L}\), \(\vee_{R}\), \(=_{L}\) are called cumulative, since their principal formulas are repeated in their premises.

Throughout the rest of this section, let \(L\) be any of the logics from Table 1. We will present an algorithm that performs root-first proof search in the calculus \(\mathcal{G}^{\star}(L)\). Our algorithm will construct a proof search tree for a given sequent by applying the rules of \(\mathcal{G}^{\star}(L)\) bottom-up to the topmost sequents in the tree. The rules will be applied exhaustively, as all possibilities need to be explored, but non-redundantly, to avoid repetitions. As a consequence, the search terminates within a finite number of steps, yielding either a proof or a saturated branch (Lemma 8). Intuitively, a branch is saturated if its topmost sequent is not an axiom and no further rules can be non-redundantly applied to it. We will then show that a saturated branch can always be used to define an interpretation that falsifies every sequent in the branch (Lemma 9). This will allow us to establish the completeness of our calculi. We start by introducing some terminology.

A branch \(B\) is closed if the topmost sequent of \(B\) is an instance of an axiom (note that sequents of the form \(\Gamma\Rightarrow\Delta,\emptyset:p\) or \(\Gamma\Rightarrow\Delta,\emptyset:\bot\) or \(\Gamma\Rightarrow\Delta,\emptyset:{=}(p)\) now also count as axioms). A branch that is not closed is open. A proof search tree \(\mathfrak{T}\) is closed if every branch in \(\mathfrak{T}\) is closed. Given a branch \(B\) of the form \(\Gamma_{1}\Rightarrow\Delta_{1}, \Gamma_{2}\Rightarrow\Delta_{2},\ldots,\Gamma_{n}\Rightarrow\Delta_{n}\), we also define \({\downarrow}\Gamma_{B}:= \bigcup_{1\leq i\leq n} \Gamma_{i}\) and \({\downarrow}\Delta_{B}:= \bigcup_{1\leq i\leq n} \Delta_{i}\), so \({\downarrow}\Gamma_{B}\) is the union of all the antecedents and \({\downarrow}\Delta_{B}\) is the union of all the succedents of the sequents in \(B\). Moreover, we write \(\mathsf{L}(B):= \Gamma_{n}\) for the antecedent and \(\mathsf{R}(B):= \Delta_{n}\) for the succedent of the topmost sequent of \(B\).

We are now ready to describe the desired proof search procedure for the calculus \(\mathcal{G}^{\star}(L)\). An excerpt from the pseudocode for this procedure is presented in Algorithm 6. Given a finite set \(\Gamma\subseteq\mathcal{L}(L)\) and a formula \(\varphi\in\mathcal{L}(L)\) as input, our algorithm first initializes \(\mathfrak{T}\) as the proof search tree consisting only of the root node \(\pi:\Gamma\Rightarrow\pi:\varphi\), where \(\pi\) is a label with \(|\pi| = 2^{|\mathsf{P}|}\) (line [alg:init]). Afterwards, the procedure successively extends \(\mathfrak{T}\) by applying the rules of \(\mathcal{G}^{\star}(L)\) root-first in all possible ways to the topmost sequents in \(\mathfrak{T}\). The corresponding while-loops for \(\rightarrow_{R}\), \(\rightarrow_{L}\), \(\vee_{R}\), \(=_{L}\) are displayed in lines [alg:start:expansion]–[alg:constancy:left:end] (the while-loops for the other rules are similar). In applications of the cumulative rules \(\mathsf{at}_{L}\), \(\bot_{L}\), \(\rightarrow_{L}\), \(\vee_{R}\), \(=_{L}\), we use a suitable loop-checking mechanism to prevent the algorithm from producing infinitely many copies of “equivalent” rule applications. For example, before performing a root-first application of \(\vee_{R}\) with principal formula \(\sigma:\psi\vee\chi\) for a split \((\tau_{1},\tau_{2})\in S(\sigma)\) in a branch \(B\), we first check whether \((\tau_{1}:\psi)\in{\downarrow}\Delta_{B}\) or \((\tau_{2}:\chi)\in{\downarrow}\Delta_{B}\). If one of these holds, the application is taken to be redundant and not performed in \(B\). Otherwise, the rule is applied in the usual way (lines [alg:tensor:right:start]–[alg:tensor:right:end]). The corresponding loop-checking conditions for \(\rightarrow_{L}\) and \(=_{L}\) are displayed in lines [alg:impl:left:start] and [alg:constancy:left:start], respectively. The expansion of \(\mathfrak{T}\) is stopped, if either \(\mathfrak{T}\) becomes closed or a saturated branch is found (lines [alg:end:condition:success]–[alg:end:condition:failure]). In the first case, the procedure outputs “success”, as \(\mathfrak{T}\) is now a derivation for the root sequent. In the second case, the output is “failure”, since a saturated branch will always allow us to construct an interpretation that falsifies the root sequent (see Lemma 9).

We will now prove that, from a saturated branch \(B\), one can always extract an interpretation \(I_{B}\) such that all elements of \({\downarrow}\Gamma_{B}\) are satisfied and all elements of \({\downarrow}\Delta_{B}\) are not satisfied by \(I_{B}\). This shows that our proof search procedure is in fact exhaustive: if the algorithm does not find a proof for the root sequent \(\pi:\Gamma\Rightarrow\pi:\varphi\) of the search tree, then this sequent can always be falsified by some interpretation.

7 Conclusion↩︎

We presented two kinds of labelled sequent calculi for a family of team-based propositional logics. We first introduced the systems \(\mathcal{G}(L)\), whose labels are strings of symbols representing arbitrary teams, their unions and intersections. The order rules of these calculi explicitly reflect the semantic reasoning on teams. We then defined the systems \(\mathcal{G}^{\star}(L)\), whose labels are finite sets of variables. This simpler framework made it possible to provide a terminating proof search procedure for the calculi.

The proof systems \(\mathcal{G}^{\star}(L)\) have the clear advantage of inducing a decision algorithm for the logics under consideration. The calculi \(\mathcal{G}(L)\), on the other hand, seem to have two other advantages. First, each rule of \(\mathcal{G}(L)\) has a fixed number of premises, whereas in \(\mathcal{G}^{\star}(L)\), the number of premises of certain rules depends on the size of the label associated with the principal formula. Thus, at least for the tensor-free systems, proofs in \(\mathcal{G}(L)\) can be significantly shorter than proofs in \(\mathcal{G}^{\star}(L)\). Second, in the calculi \(\mathcal{G}(L)\), one may use variables to reason about arbitrary teams (or arbitrary subsets of a given team), which more closely mirrors the actual mathematical reasoning one would employ to show that a certain formula is satisfied by a team or that all formulas of a certain form are valid in the corresponding logic.

For future work, we intend to further simplify our calculi by circumventing the need for intersection labels, and by extending our proof systems for \(\mathsf{InqB}_{\vee}\) and \(\mathsf{PID}_{\vee}\) to languages with infinitely many atomic propositions. Moreover, we plan to develop labelled calculi for broader families of team-based logics. A primary goal is to find proof systems for downward-closed team logics without the intuitionistic implication \(\rightarrow\), most notably for propositional dependence logic [@yang:vaananen:2016]. For such logics, only natural deduction systems [@yang:vaananen:2016] and deep-inference-style sequent calculi [@anttila2025deep] are known. We also intend to investigate team logics with the union closure property [@Yan2022; @yang:vaananen:2017], for which no sequent-style proof systems have been developed up to now. Another natural step would be to extend our calculi to logics based on modal or intuitionistic variants of team semantics [@Vaa2008; @ciardelli:iemhoff:yang:2020]. Finally, we plan to use our calculi to establish meta-theoretical properties, such as syntactic interpolation, for the logics under consideration.

Acknowledgements. We are grateful to the anonymous reviewers for their valuable feedback and helpful suggestions for improvement. Fausto Barbero was supported by the Research Council of Finland under grant number 349803. Valentin Müller was supported by the Swiss National Science Foundation (SNSF) under grant number 10000440 (Epistemic Group Attitudes).

8 Proof of Theorem 2↩︎

[thm:struct:i]. The weakening rules are hp-admissible in \(\mathcal{G}(L)\). This is proved by an easy induction on the height of a derivation for the premise \(\Gamma\Rightarrow\Delta\) of the respective rule. More details can be found in [@muller:msc:2023].

[thm:struct:ii]. All rules of \(\mathcal{G}(L)\) are hp-invertible. The hp-invertibility of the basic and special order rules follows immediately from the hp-admissibility of weakening. The same holds for the rules \(\mathsf{at}_{L}\), \(\bot_{L}\), \(\rightarrow_{L}\), \(\vee_{R}\), \(=_{L}\). For all other rules, we reason by induction on the height of a derivation for the conclusion of the rule. We only show the invertibility of the rule \(\vee_{L}\) (the other cases are similar). Let \(\mathcal{D}\) be a derivation for the sequent \(\pi:\varphi\vee\psi, \Gamma\Rightarrow\Delta\), and let \(n\) be the height of \(\mathcal{D}\).

If \(n = 0\), then \(\pi:\varphi \vee\psi, \Gamma\Rightarrow\Delta\) must be an axiom. Consequently, \(\pi:\varphi \vee\psi\) cannot be principal, as it is not atomic. Thus, for all variables \(x, y \in \mathfrak{A}\), the sequent \(\pi\subseteq x \cup y, x:\varphi, y:\psi, \Gamma\Rightarrow\Delta\) is also an axiom.

If \(n \geq 1\), we distinguish cases according to the last rule \(R\) applied in \(\mathcal{D}\). If \(\pi:\varphi \vee\psi\) is not principal in \(R\), we apply the induction hypothesis to the premises of \(R\) (possibly with a renaming of eigenvariables), and apply \(R\) again. If \(\pi:\varphi \vee\psi\) is principal, then \(R\) is an application of \(\vee_{L}\). The premise of \(\vee_{L}\) is of the form \(\pi\subseteq x' \cup y', x':\varphi, y':\psi, \Gamma\Rightarrow\Delta\), where \(x', y' \in \mathfrak{A}\) are fresh. This sequent is derivable by a derivation of height \(n-1\). By hp-substitution, we obtain a derivation of height \(\leq n\) for \(\pi\subseteq x \cup y, x:\varphi, y:\psi, \Gamma\Rightarrow\Delta\).

[thm:struct:iii]. The contraction rules are hp-admissible in \(\mathcal{G}(L)\). The hp-admissibility of both contraction rules is proved simultaneously, by induction on the height of a derivation \(\mathcal{D}\) for the premise, and by distinguishing cases according to the last rule applied in \(\mathcal{D}\). Let \(\Gamma\Rightarrow\Delta\) be a sequent that contains a duplication of some relational atom or labelled formula \(E\) in the antecedent or in the succedent. Let \(\mathcal{D}\) be a derivation for \(\Gamma\Rightarrow\Delta\) in \(\mathcal{G}(L)\) and let \(n\) be the height of \(\mathcal{D}\). Using induction on \(n\), we show that also the contracted version of \(\Gamma\Rightarrow\Delta\) (in which the two occurrences of \(E\) are replaced by a single one) is derivable by a proof tree of height \(\leq n\). If \(\mathcal{D}\) is of height \(n=0\), then \(\Gamma\Rightarrow\Delta\) is an axiom, so the contracted version of \(\Gamma\Rightarrow\Delta\) is also an axiom and therefore derivable by a proof tree of height \(n=0\).

Suppose now that \(n\geq 1\). If \(E\) is not principal in the last rule \(R\) applied in \(\mathcal{D}\), we apply the induction hypothesis to the premises of \(R\), and then apply \(R\) again. And if \(E\) is principal in \(R\), we distinguish two cases.

Case 1: \(E\) is a relational atom. If only one of the two occurrences of \(E\) is principal in the last rule application \(R\) in \(\mathcal{D}\), then we use the same argument as above. And if both occurrences of \(E\) are principal in \(R\), then we use the closure condition introduced in Section 3.

Case 2: \(E\) is a labelled formula. In this case, we use the hp-invertibility of the logical rules of \(\mathcal{G}(L)\). For example, if \(\mathcal{D}\) ends with an application of \(\vee_{L}\) for which \(E\) is principal, the premise of the rule is of the form \(\pi\subseteq x \cup y,x:\varphi, y:\psi,\pi:\varphi \vee\psi, \Sigma\Rightarrow\Delta\), for some fresh \(x, y \in \mathfrak{A}\). The height of the derivation of this sequent is \(n-1\). By hp-invertibility and hp-substitution, we obtain a derivation of height \(\leq n-1\) for the sequent \(\pi\subseteq x \cup y, \pi\subseteq x \cup y,x:\varphi,x:\varphi, y:\psi,y:\psi, \Sigma\Rightarrow\Delta\). Using three applications of the inductive hypothesis (which do not increase the height) we obtain a derivation of height \(\leq n-1\) for \(\pi\subseteq x \cup y,x:\varphi, y:\psi, \Sigma\Rightarrow\Delta\). An application of \(\vee_{L}\) now yields a derivation of height \(\leq n\) for \(\pi:\varphi\vee\psi, \Sigma\Rightarrow\Delta\).

[thm:struct:iv]. The cut rule is admissible in \(\mathcal{G}(L)\). The proof works in the standard way (see, e.g., [@negri:plato:2001]) and proceeds by induction on two parameters: the height of a cut rule application and the rank of the cut formula, which is a measure of the complexity of labelled formulas.⁵ The height of a cut rule application is the sum of the heights of the two subderivations ending with the premises of the cut. Our measure of the complexity of a labelled formula \(\pi:\varphi\) takes into account both the complexity of \(\varphi\) and the complexity of the label \(\pi\) (this is needed to deal with cuts involving the rules \(\mathsf{at}_{L}\), \(\mathsf{at}_{R}\), \(\bot_{L}\), \(\bot_{R}\)).

Formally, the degree of a label \(\pi\in\mathsf{Lab}_{\cap}\), notation \(dg(\pi)\), is defined by setting \(dg(\pi) := 0\), if \(\pi\in\mathfrak{S}\), and \(dg(\pi) := 1\), if \(\pi\notin\mathfrak{S}\). The degree of a formula \(\varphi \in \mathcal{L}(L)\), notation \(dg(\varphi)\), is defined to be the number of occurrences of the connectives \(\bot,\wedge,\mathbin{\mathpalette\d@vee\relax},\rightarrow,{=}(\cdot),\vee\) in \(\varphi\). The rank of a labelled formula is the pair of natural numbers given by \(rk(\pi:\varphi) := (dg(\varphi),dg(\pi))\). As in [@muller:2024], we assume that ranks of labelled formulas are ordered lexicographically. That is, we write \(rk(\pi:\varphi)< rk(\sigma:\psi)\), if we either have \(dg(\varphi) < dg(\psi)\), or we have both \(dg(\varphi) = dg(\psi)\) and \(dg(\pi) < dg(\sigma)\). It is easy to verify that, if \(\pi\) is a label with \(\pi\notin\mathfrak{S}\), then \(rk(v:\varphi)< rk(\pi:\varphi)\) for all variables \(v\in\mathfrak{S}\) and all formulas \(\varphi\in\mathcal{L}(L)\).

The cut-admissibility proof proceeds by a main induction on the rank of the cut formula and a subinduction on the height of the cut. We distinguish three main cases, depending on the two premises of the cut: (i) one of the two premises of the cut is an axiom; (ii) neither of the two premises is an axiom and the cut formula is not principal on one side; and (iii) neither of the two premises of the cut is an axiom and the cut formula is principal on both sides. We show only two subcases of case (iii); the other cases follow quite standardly, and a discussion for several of them can be found in [@muller:msc:2023].

First, suppose that the cut formula is a propositional atom. In this case, the cut must be of the form

where \(\pi\) is a label with \(\pi\notin\mathfrak{S}\) and \(v\) is a fresh variable from \(\mathfrak{S}\). Using the hp-admissibility of substitution and contraction, this application of the cut rule is converted into

where \(\mathsf{c}_{L}, \mathsf{c}_{R}\) denote multiple applications of the contraction rules. The new cut on \(\pi:p\) is of smaller height than the original one, and the cut on \(u:p\) is of smaller rank (since \(u\in\mathfrak{S}\) and \(\pi\notin\mathfrak{S}\)). Next, suppose that the cut formula is of the form \(\pi:\varphi\vee\psi\). Our derivation then has the following shape:

Without loss of generality, we may assume that the eigenvariables \(x\) and \(y\) do not occur in the labels \(\sigma\) and \(\tau\) (if this condition is not satisfied, we simply apply the hp-admissibility of substitution). We construct the following derivation, where \(\mathcal{E}\), the subderivation for the sequent \(\pi\subseteq \sigma\cup\tau, \Gamma, \Pi \Rightarrow\Delta, \Sigma, \tau:\psi\), is constructed in a similar way as the subderivation for \(\pi\subseteq \sigma\cup\tau, \Gamma, \Pi \Rightarrow\Delta, \Sigma, \sigma:\varphi\) displayed below:

The cut on \(\pi:\varphi \vee\psi\) has smaller height than the original one, and is thus justified by the inductive hypothesis. Another such cut is contained in the subderivation \(\mathcal{E}\). The cut on \(\sigma:\varphi\) and the one on \(\tau:\psi\) have smaller rank than the original cut, and are also justified by the inductive hypothesis.0◻

9 Proof of Lemma 3↩︎

Let \(L\) be any of the logics from Table 1 and let \(\mathcal{G}(L)\) be the corresponding labelled calculus from Figure 2. We only prove the admissibility of the rule \(\mathsf{aux}_{1}\) (the admissibility proof for \(\mathsf{aux}_{2}\) works in the same way). Suppose that the premise \(\pi\subseteq (\sigma\cup\tau)\cup(\sigma'\cup\tau'),\Gamma\Rightarrow\Delta\) is derivable in \(\mathcal{G}(L)\). Using the admissibility of weakening, we can then derive the conclusion of \(\mathsf{aux}_{1}\) in the following way:

10 Supplement to the Proof of Lemma 6↩︎

We need to show that all axioms of the Hilbert system \(\mathcal{H}(L)\) are provable in the labelled calculus \(\mathcal{G}(L)\) (see Definition 4). For the sake of brevity, we only consider the case \(L=\mathsf{PID}_{\vee}\) (the other cases are treated in the same way). Showing the provability of the schemes \(\mathrm{(A1)}\)–\(\mathrm{(A7)}\), \(\mathrm{(Intro)}\), \(\mathrm{(Dis)}\), \(\mathrm{(C)}\) is straightforward. The scheme \(\mathrm{(S)}\) can be derived in the same way as in [@muller:msc:2023] and [@muller:2024]. And for the schemes \(\mathrm{(DN)}\), \(\mathrm{(Com)}\), \(\mathrm{(Mon)}\), \(\mathrm{(Elim)}\), we can construct the following derivations in \(\mathsf{GPID}_{\vee}\):

Note that, in the derivations for \(\mathrm{(DN)}\) and \(\mathrm{(Elim)}\), we also use the admissible rule \(\mathsf{flat}\) from Figure 4.

---

1. In [@muller:msc:2023], Müller also presents labelled sequent calculi for intuitionistic inquisitive logic [@ciardelli:iemhoff:yang:2020] and inquisitive Kripke logics [@ciardelli:phd:2016]. The calculi for the latter were subsequently extended to various systems of inquisitive modal logic (see [@muller:2024; @muller:2026]).↩︎

2. Strictly speaking, this assumption is only needed in our treatment of systems involving tensor disjunction (i.e., for the logics \(\mathsf{InqB}_{\vee}\) and \(\mathsf{PID}_{\vee}\) introduced below). For simplicity, however, we also make this assumption for logics without tensor.↩︎

3. A very similar calculus for \(\mathsf{InqB}\) was already presented by Litak and Sano [@litak:sano:2026]. In fact, their system essentially coincides with the calculus for \(\mathsf{InqB}\) introduced in Definition 7 below. The only noteworthy differences are that Litak and Sano use slightly different axioms and require labels to be non-empty.↩︎

4. So, for example, the calculus \(\mathcal{G}^{\star}(\mathsf{InqB})\) consists of the initial sequents, the rules for atoms and the rules for \(\bot,\wedge,\mathbin{\mathpalette\d@vee\relax},\rightarrow\). The calculus \(\mathcal{G}^{\star}(\mathsf{PID}_{\vee})\), on the other hand, consists of the initial sequents, the rules for atoms and the rules for \(\bot,\wedge,\mathbin{\mathpalette\d@vee\relax},\rightarrow,{=}(\cdot),\vee\).↩︎

5. By the cut formula, we mean the labelled formula \(\pi:\varphi\) displayed in the presentation of the cut rule in Figure 3.↩︎