1 Introduction↩︎

Inquisitive logics [@Ciardelli:18book; @Ciardelli:23book; @Puncochar:16generalization; @Puncochar:19] extend existing versions of classical or non-classical logics with formulas representing questions. This extension is typically achieved by lifting the semantics from standard points of evaluations (e.g., valuation functions, relational models, or possible worlds) to sets of such points, called information states (or just states for short), relative to which a notion of support is defined.¹

The standard system of inquisitive first-order logic, InqBQ, extends classical first-order logic with two question-forming operators: inquisitive disjunction, \(\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\), and the inquisitive existential quantifier, \(\mathord{\exists\exists}\). In terms of \(\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\), a polar question operator \(?\) is defined by letting \({?}\varphi:=(\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\neg\varphi)\). In spite of important advances [@Grilletti:17; @Grilletti:21; @GrillettiCiardelli:23; @CiardelliGrilletti:22], the meta-theoretic properties of this system remain rather mysterious: in particular, it is not known whether InqBQis recursively axiomatizable, or whether it is entailment-compact.²

Recent work [@CiardelliGrilletti:22; @Conti25] has focused on the \(\mathord{\exists\exists}\)-free fragment of this logic, denoted InqWQ. This fragment is sufficiently expressive to regiment a broad variety of questions; for instance, in addition to standard sentences like \(\forall xPx\), regimenting the statement “every object is \(P\)”, InqWQalso contains sentences like \({?}\forall xPx\) and \(\forall x{?}Px\), regimenting, respectively, the questions “whether or not every object is \(P\)” and “which objects are \(P\)”. At the same time, InqWQenjoys a strong semantic property which is not shared by all of InqBQ: finite coherence.³ A formula \(\varphi\) is said to be \(n\)-coherent for a number \(n\in \mathbb{N}\) if, in order to decide whether \(\varphi\) is supported by a state \(s\), it suffices to check whether it is supported by the subsets \(s'\subseteq s\) of cardinality up to \(n\). As shown by Ciardelli and Grilletti [@CiardelliGrilletti:22], every formula \(\varphi\) in InqWQis \(n\)-coherent for some number \(n\) which is computable from \(\varphi\). This fact has far-reaching repercussions: one can use it to show, among other things, that InqWQis entailment-compact and recursively axiomatizable [@CiardelliGrilletti:22].

In recent work, two complete proof systems have been provided for InqWQ: Conti [@Conti25], building on [@CiardelliGrilletti:22], gave a natural deduction system, while Litak and Sano [@LitakSano:25] gave a labelled sequent calculus. Both systems rely crucially on the finite coherence property of InqWQ. In the former system, this property shows up through a specific coherence rule which allows one to discharge certain assumptions about the cardinality of the state of evaluations. In the latter system, coherence ensures that it is sufficient to work with labels which are finite sequences of indices, representing finite states.

In recent work, Ciardelli [@Ciardelli:25] investigated a modal logic \(\textsf{InqQML}^{-}_{\Box}\)obtained by extending InqWQwith a generalization of the Kripke modality \(\Box\). The motivation for this work came from the analysis of global supervenience, a notion of dependence that has received attention in the philosophical literature [@Kim:84; @Stalnaker:96; @McLaughlin:97; @Bennett:04; @Leuenberger:09], where it has been invoked to give a precise formulation of certain philosophical theses, such as David Lewis’s thesis of Humean supervenience [@Lewis:86]. Intuitively, global supervenience captures the idea that the overall distribution of certain properties or relations in the world is fully determined by the overall distribution of other properties or relations. An example: if we fix who is a parent of whom, we thereby also fix who is a grandparent of whom; so, the grandparent-of relation globally supervenes on the parent-of relation. Formally, we may say that a predicate \(Q\) globally supervenes on another predicate \(P\) at a possible world \(w\) if any two successors of \(w\) which assign the same extension to \(P\) also assign the same extension to \(Q\). (The notion extends straightforwardly to the case of several predicates supervening on several other predicates.) Thus, global supervenience captures functional dependencies between the extensions of predicates across a space of possibilities. As Ciardelli [@Ciardelli:25] showed, global supervenience claims cannot be expressed in standard quantified modal logic, but they can be expressed in \(\textsf{InqQML}^{-}_{\Box}\)in a particularly perspicuous way, namely, as strict conditionals whose antecedents and consequents are questions. Thus, e.g., the claim that \(Q\) globally supervenes on \(P\) is formalized by the strict conditional \[\Box(\forall x{?}Px\to\forall x{?}Qx)\] having as its antecedent the subvenient question \(\forall x{?}Px\) (“which objects are \(P\)”), and as its consequent the supervenient question \(\forall x{?}Qx\) (“which objects are \(Q\)”). As discussed in [@Ciardelli:25], this analysis is insightful, since it allows us to trace back logical properties of global supervenience to familiar properties of strict conditionals and questions. The inquisitive modal logic \(\textsf{InqQML}^{-}_{\Box}\), then, provides an attractive system to reason about global supervenience claims, as well as modal dependence claims more generally [@Ciardelli:18aiml].

In view of this motivation, it seems important to have a proof system for this logic: such a system would allow one to formally establish the validity of certain inferences concerning modal dependencies and, ideally, it could be used to get further insight about the logic of these dependence notions. While Ciardelli [@Ciardelli:25] proved (by means of a translation to two-sorted first-order logic) that the set of validities of \(\textsf{InqQML}^{-}_{\Box}\)is recursively enumerable, he left the development of a proof system as an open problem.

In this paper, we fill this gap, providing a labelled sequent calculus for \(\textsf{InqQML}^{-}_{\Box}\). Our calculus builds on Litak and Sano’s calculus for InqWQ [@LitakSano:25], where labels are finite sequences \(\textsf{w}_1\dots \textsf{w}_n\) of indices;⁴ intuitively, indices represent worlds, and so, labels represent finite states. To this calculus we add rules for the modality \(\Box\). These rules are inspired by the standard rules for \(\Box\) in labelled sequent calculi [@Negri:05] but, at the same time, they use in a crucial way the finite coherence property of \(\textsf{InqQML}^{-}_{\Box}\), inherited from InqWQ: every formula \(\varphi\) in \(\textsf{InqQML}^{-}_{\Box}\)is \(n_\varphi\)-coherent for some number \(n_\varphi\) computable from \(\varphi\) [@Ciardelli:25]. This is crucial, in particular, for our right rule for \(\Box\). Semantically, \(\Box\varphi\) is true at a world \(w\) if \(\varphi\) is supported by the state consisting of all the successors of \(w\); however, by finite coherence, this reduces to \(\varphi\) being supported by all sets consisting of at most \(n_\varphi\)-many successors of \(w\). This fact allows us to formulate a right rule for \(\Box\) that, in essence, says the following: in order to prove a labelled formula \(\textsf{w}:\Box\varphi\), introduce \(n_\varphi\)-many fresh indices \(\textsf{v}_1\dots \textsf{v}_{n_\varphi}\) standing for successors of \(\textsf{w}\), and aim to prove that \(\textsf{v}_1\dots \textsf{v}_{n_\varphi}:\Box\varphi\).

In addition to establishing the soundness and completeness of this system, we prove the invertibility of its rules, and the admissibility of the rules of weakening, contraction, and cut.

Inquisitive modal logic is currently an active and rapidly growing field. While several proof systems have been developed for propositional inquisitive modal logics, including labelled sequent calculi [@Muller:24; @Muller:26], our calculus represents the first example of a proof system for a first-order inquisitive modal logic. We think that, in addition to its direct relevance as a tool to study the logic \(\textsf{InqQML}^{-}_{\Box}\), our contribution might serve as a model to build proof systems for other first-order inquisitive modal logics.

The paper is structured as follows: Section 2 provides the relevant background on the logic \(\textsf{InqQML}^{-}_{\Box}\); Section 3 presents our contribution; Section 4 outlines directions for future work.

2 Background↩︎

In this section, we provide the necessary technical background on the inquisitive modal logic \(\textsf{InqQML}^{-}_{\Box}\). For a thorough presentation of this logic and proofs of the facts mentioned in this section, we refer to [@Ciardelli:25]. For a more general introduction to inquisitive logic, see [@Ciardelli:23book].

2.0.0.1 Syntax.

We start with a countable first-order signature \(\Sigma\). For simplicity, we focus on the case where \(\Sigma\) is a set of predicates (each having an associated arity), and doesn’t contain function symbols nor the identity symbol. The language of \(\textsf{InqQML}^{-}_{\Box}\) is given by the following definition, where \(P\in\Sigma\) is an \(n\)-ary predicate and \(x,x_1,\dots,x_n\) range over \(Var\), a countably infinite set of variables: \[\varphi\Coloneqq\bot\mid P(x_1,\dots,x_n)\mid\varphi\land\varphi\mid\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\varphi\mid\varphi\to\varphi\mid\forall x\varphi\mid\Box\varphi\] We also consider the following defined symbols: \(\lnot\varphi=\varphi\to\bot\), \(\varphi\lor\psi=\lnot(\lnot\varphi\land\lnot\psi)\), \(\exists x\varphi=\lnot\forall x\lnot\varphi\) and the inquisitive operator \({?}\varphi=\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\lnot\varphi\). We call formulas where \(\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\) does not appear classical formulas. These formulas can be identified with those of standard modal logic, with a particular choice of primitive operators. The operator \(\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\) is called inquisitive disjunction; informally, it is intended to formalize disjunctive questions. Thus, for instance, whereas the classical disjunction \(P(x)\lor\neg P(x)\) regiments the (tautological) statement that either \(x\) is \(P\) or it isn’t, the inquisitive disjunction \(P(x)\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\lnot P(x)\) regiments the question whether \(x\) is \(P\) or not (which explains why this formula is abbreviated as \({?}P(x)\)).

2.0.0.2 Semantics.

Models for \(\textsf{InqQML}^{-}_{\Box}\) are defined as tuples \(M=\langle W,D,R,I\rangle\), where \(W\neq\emptyset\) is a set of possible worlds, \(D\neq\emptyset\) is a domain of individuals, \(R\subseteq W\times W\) is an accessibility relation, associating each world \(w\in W\) with a set of successors \(R[w]=\{v\in W\mid w R v\}\), and \(I\) maps each \(w\in W\) to an interpretation function that assigns to each \(n\)-ary predicate \(P\) a corresponding extension \(I_w(P)\subseteq D^n\). An information state (or, simply, a state) is a subset of \(W\). As usual, an assignment is a function \(g:Var\to D\). Given an assignment \(g\), a variable \(x\), and an individual \(d\in D\), \(g[x\mapsto d]\) is the assignment that maps \(x\) to \(d\) and agrees with \(g\) on all other variables.

In \(\textsf{InqQML}^{-}_{\Box}\), formulas \(\varphi\) are evaluated in terms of a relation of support, written as \(M,s\models_g\varphi\), relative to a model \(M\), a state \(s\) and an assignment \(g\). We define support conditions inductively as follows:

• \(M,s\models_g \bot \iff s=\emptyset\)

• \(M,s\models_g P(x_1,...,x_n)\iff \text{for all }w\in s,\;\langle g(x_1),...,g(x_n)\rangle\in I_w(P)\)

• \(M,s\models_g \varphi\land\psi \iff M,s\models_g \varphi \text{ and } M,s\models_g\psi\)

• \(M,s\models_g \varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi\iff M,s\models_g\varphi \text{ or } M,s\models_g\psi\)

• \(M,s\models_g\varphi\rightarrow\psi\iff \text{for all }t\subseteq s,\;M,t\models_g \varphi \text{ implies }M,t\models_g\psi\)

• \(M,s\models_g \forall x \varphi\iff \text{for all }d\in D,\;M,s\models_{g[x\mapsto d]}\varphi\)

• \(M,s\models_g \Box\varphi\iff\text{for all }w\in s:\;M,R[w]\models_g \varphi\)

Entailment is defined as preservation of support: for a set of formulas \(\Phi\cup\{\psi\}\), \(\Phi\models\psi\) if for all models \(M\), states \(s\) and assignments \(g\), \(M,s\models_g\varphi\) for all \(\varphi\in\Phi\) implies \(M,s\models_g\psi\). Additionally, we define a restriction of entailment to states \(s\) of cardinality at most \(n\) (in symbols, \(\#s\le n\)): \(\Phi\models_n\psi\) if for all models \(M\), states \(s\) such that \(\# s\leq n\) and assignments \(g\), \(M,s\models_g\varphi\) for all \(\varphi\in\Phi\) implies \(M,s\models_g\psi\).

The above semantics for \(\textsf{InqQML}^{-}_{\Box}\) satisfies the following standard properties of inquisitive logics:

• Persistency: if \(M,s\models_g\varphi\), then for all \(t\subseteq s\), \(M,t\models_g\varphi\)

• Empty state property: \(M,\emptyset\models_g\varphi\) for any formula \(\varphi\)

Another important desideratum of inquisitive extensions is conservativity over the original system being extended. We say that a formula \(\varphi\) is true at a world \(w\) (under \(g\)) if \(\{w\}\models_g\varphi\). It is easy to check that, for classical formulas, the truth conditions delivered by our definition coincide with those given by standard Kripke semantics. Moreover, classical formulas are truth-conditional, meaning that they are supported by a state iff they are true at each of its possible worlds. Using these facts, it is easy to see that entailment among classical formulas in \(\textsf{InqQML}^{-}_{\Box}\)coincides with entailment in standard constant-domain quantified modal logic. \(\textsf{InqQML}^{-}_{\Box}\) can thus be seen as a conservative extension of the latter logic. Note, furthermore, that the support clause for \(\Box\) implies that \(\Box\varphi\) is always truth-conditional for any \(\varphi\).

2.0.0.3 Coherence.

A key property of formulas in \(\textsf{InqQML}^{-}_{\Box}\)is finite coherence [@Kontinen:13; @CiardelliGrilletti:22], defined as follows.

Intuitively, \(n\)-coherence of \(\varphi\) means that in order to check if \(\varphi\) is supported at a state, it suffices to check if it is supported by all substates of cardinality at most \(n\). Crucially, this implies that if \(\varphi\) is not supported at a state, then there is some finite, at most \(n\)-sized substate that doesn’t support \(\varphi\). Notice that, in particular, \(1\)-coherence coincides with being truth-conditional.

Importantly, combining this result with persistency implies that the validity of any \(\textsf{InqQML}^{-}_{\Box}\) entailment can be reduced to its validity over a class of finite states with bounded cardinality.

Using this fact, one can show that \(\textsf{InqQML}^{-}_{\Box}\)is entailment-compact, in the following sense.

3 Labelled sequent calculus and completeness proof↩︎

In this section, we describe a labelled sequent calculus called IWMC (for inquisitive weak modal calculus) and prove its soundness and strong completeness for \(\textsf{InqQML}^{-}_{\Box}\).

Intuitively, labels represent finite states, and labelled formulas translate the support relation. Formally, labels are non-empty finite sets of indices, where each index is a natural number. ⁵ We use the meta-variables \(\textsf{w},\textsf{v},\textsf{u}\) for indices, and \(\textsf{s},\textsf{t},\textsf{u},\dots\) for labels. We consider two kinds of expressions:

• Labelled formulas of the form \(\textsf{s}:\varphi\), where \(\varphi\) is a formula and \(\textsf{s}\subseteq_{\text{fin}}\mathbb{N}\)

• Relational atoms of the form \(\textsf{w}\textsf{R}\textsf{v}\) where \(\textsf{w},\textsf{v}\in\mathbb{N}\).

As suggested by the notation, the former intuitively represent support at a state, while the latter syntactically encode instances of the accessibility relation. A sequent is an ordered pair \(\Gamma\Rightarrow\Delta\) consisting of finite multisets \(\Gamma\) and \(\Delta\), where \(\Gamma\) can contain labelled formulas and relational atoms, while \(\Delta\) contains only labelled formulas.

Below, we provide the rules of the sequent calculus IWMC. We write \(\textsf{w}\textsf{R}\textsf{t}\) for the set \(\{\textsf{w}\textsf{R}\textsf{v}\mid \textsf{v}\in\textsf{t}\}\). The universe \(\textsf{W}_{\Gamma,\Delta}\) of a sequent \(\Gamma\Rightarrow\Delta\) is the set of indices that occur in it, within labels or in relational atoms.

As mentioned in the introduction, the rules \((\Box{\Rightarrow})\) and \(({\Rightarrow}\Box)\) are inspired by standard rules for \(\Box\) in labelled sequent calculi [@Negri:05]. The side condition for the right rule, however, is connected to the finite coherence property stated in Proposition [Finite-coherence]. The rule can be read as follows: if for each world \(w\) in a state \(s\), an arbitrary set \(t\) of successors of \(w\) of cardinality \(\le n_\varphi\) supports \(\varphi\), then \(s\) supports \(\Box\varphi\). This rule is sound (as we will see) since the support of \(\varphi\) on an arbitrary set \(t\) of at most \(n_\varphi\)-many successors of \(w\) guarantees its support on the whole set \(R[w]\) of successors by Proposition [Finite-coherence].

It is clear by inspecting the rules that IWMC satisfies an appropriate notion of analyticity. Let the set of subformulas of a formula \(\varphi\), \(\textsf{SubF}(\varphi)\) be given in the usual way. Then, if we define the set of subexpressions of \(\varphi\) as \(\textsf{Sub}(\varphi)=\textsf{SubF}(\varphi)\cup\{\psi[y/x]\mid \psi\in\textsf{SubF}(\varphi),\;y\text{ free for x in \psi}\}\), the following holds.

3.1 Interpretation and validity for sequents↩︎

We start by defining a notion of satisfaction for labelled formulas, relational atoms and labelled sequents. For this, we make use of the notion of mappings into a model, i.e. functions associating each natural number to some possible world in the universe of the model.

We may now define a sequent to be valid if it is satisfied under any interpretation.

The notion of validity for sequents is connected to the notion of entailment between \(\textsf{InqQML}^{-}_{\Box}\)-formulas via coherence. Indeed, due to Proposition [Entailment-finite-coherence], an entailment \(\Phi\models\psi\) is valid iff it is valid on arbitrary states of cardinality at most \(n_\psi\) (where \(n_\psi\) is the coherence estimate for \(\psi\) given by [Finite-coherence]). These states are exactly the possible interpretations, via mappings, of a label \(\textsf{s}\) of cardinality \(n_\psi\). This underpins the following connection.

Given this connection, we say that a derivation in our proof system is a proof of an entailment \(\Phi\models\psi\) in case its conclusion is a sequent of the form \(\textsf{s}:\varphi_1,\dots,\textsf{s}:\varphi_n\Rightarrow\textsf{s}:\psi\) for some formulas \(\varphi_1,\dots,\varphi_n\in\Phi\) and some label \(\textsf{s}\) with \(\#\textsf{s}\ge n_\psi\).

3.2 Illustration↩︎

To illustrate the calculus, we provide a proof of the \(\textsf{InqQML}^{-}_{\Box}\) entailment \(\Box\forall x{?}Px\models \Box{?}\forall xPx\). Since the coherence estimate for the conclusion is \(n_{\Box{?}\forall xPx}=1\), it suffices to give a proof of a sequent of the form \(\{\textsf{w}\}:\Box\forall x{?Px}\Rightarrow\{\textsf{w}\}:\Box{?\forall x Px}\), involving a label of size 1.

To ease notation, we display labels as sequences of indices rather than sets; for instance, instead of \(\{1\}:\varphi\) we write simply \(1:\varphi\). For simplicity, we make use of weakening rules, whose admissibility will be proved in Section 3.4, and we occasionally apply multiple rules in one step, when no ambiguity arises. We also derive two branches, \(\bigstar_2\) and \(\bigstar_3\), separately, due to space constraints.

The steps of this first half of the derivation are straightforward, and no choices need to be made to perform them. The only exception is the final application of (\(\forall{\Rightarrow}\)) in the leftmost branch, where using the variable \(y\) is the only reasonable choice to obtain an (\(\textsf{id}\)) initial sequent. The application of rule \(({\Rightarrow\to})\) generates three branches, one for each non-empty subset of the label \(23\). The branch corresponding to the subset \(23\) is displayed in the proof; the branch \(\bigstar_2\) corresponding to the subset \(2\) is shown below; finally, the branch \(\bigstar_3\) is analogous to \(\bigstar_2\), but with the label 3 playing the role of the label 2.

Semantically, providing a derivation of branch \(\bigstar_2\) corresponds to showing that, if the truth value of \(Py\) is uniform in the state \(23\) (which we know from \(23:\forall x{?}Px\)) and the world \(2\) makes \(Py\) true (from \(2:\forall x Px\)), then we can show that \(Py\) is true across the whole state \(23\). Therefore, we proceed as follows: we apply (\(\forall{\Rightarrow}\)) twice and instantiate it using the variable \(y\). Then, in the right branch generated by (\(\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}{\Rightarrow}\)), we apply (\({\to}{\Rightarrow}\)) picking \(2\) as our choice of subset for the label \(23\). This allows us to use the information that \(Py\) is true at world \(2\) to conclude the derivation.

3.3 Soundness.↩︎

The soundness of our system amounts to the claim that if a sequent is derivable, it is valid.

We have thus proved that our proof system IWMC is sound for \(\textsf{InqQML}^{-}_{\Box}\). Before proving that it is also complete, we study the proof-theoretic properties of the calculus.

3.4 Structural properties↩︎

In this section, we show the admissibility of weakening, contraction and cut rules for IWMC, as well as the invertibility of all rules in the system. Besides their intrinsic interest, these results will play a role below in the completeness proof.

We will use the notion of height of a derivation, defined as the length of one of its longest branches, and we will write \(\vdash_n\Gamma\Rightarrow\Delta\) when there is a derivation of \(\Gamma\Rightarrow\Delta\) of height at most \(n\). We will say that a rule is admissible if whenever its premisses are derivable, then its conclusion is also derivable. A rule is said to be height-preserving admissible if whenever all its premisses have a derivation of height at most \(n\), then its conclusion also has a derivation of height at most \(n\). By a rule being invertible, we mean that all rules having its conclusion as premiss and one of its premisses as conclusion are admissible.

3.5 Completeness↩︎

We prove completeness by showing that from any non-derivable sequent we can build a canonical model that refutes it. The proof generalizes the approach of [@LitakSano:25] to the modal case. First, we define a notion of saturation and prove that non-derivable sequents can be extended to saturated ones. Then, we show how to obtain a canonical model from a saturated sequent, and prove that this model refutes the original sequent. This establishes that each valid sequent is derivable. Finally, we lift this to a strong completeness theorem for \(\textsf{InqQML}^{-}_{\Box}\) by using the compactness and coherence properties of the logic.

For the proof, we need to extend our range of syntactic objects to include infinite sequents. Therefore, we start by defining a generalized class of sequents which we will call g-sequents. A g-sequent is an ordered pair \(\Gamma\Rightarrow\Delta\) consisting of (possibly infinite) multisets \(\Gamma\) and \(\Delta\), where \(\Gamma\) can contain labelled formulas and relational atoms, while \(\Delta\) contains only labelled formulas. For a g-sequent \(\Gamma\Rightarrow\Delta\), we define derivability in IWMC, denoted by \(\vdash\Gamma\Rightarrow\Delta\), as the existence of a finite sequent \(\Gamma'\Rightarrow\Delta'\) with \(\Gamma'\subseteq\Gamma\), and \(\Delta'\subseteq\Delta\) which is derivable in the sense of Definition 2. Note that every sequent \(\Gamma\Rightarrow\Delta\) is also a \(g\)-sequent, and that the derivability of \(\Gamma\Rightarrow\Delta\) as a sequent, as given by Definition 2, coincides with its derivability as a \(g\)-sequent by the admissibility of weakening.

3.5.0.1 Saturation.

We say that a g-sequent \(\Gamma\Rightarrow\Delta\) is saturated if it satisfies the following conditions:

• \((\textsf{unprov})\) \(\not\vdash\Gamma\Rightarrow\Delta\)

• If \(\textsf{s}:P(x_1,\dots,x_n)\in\Gamma\), then \(\{\textsf{w}\}:P(x_1,\dots,x_n)\in\Gamma\) for all \(\textsf{w}\in\textsf{s}\).

• If \(\textsf{s}:P(x_1,\dots,x_n)\in\Delta\), then \(\{\textsf{w}\}:P(x_1,\dots,x_n)\in\Delta\) for some \(\textsf{w}\in\textsf{s}\).

• If \(\textsf{s}:\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi\in\Delta\), then \(\textsf{s}:\varphi\in\Delta\) and \(\textsf{s}:\psi\in\Delta\).

• If \(\textsf{s}:\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi\in\Gamma\), then \(\textsf{s}:\varphi\in\Gamma\) or \(\textsf{s}:\psi\in\Gamma\).

• If \(\textsf{s}:\Box\varphi\in\Delta\), then for some \(\textsf{w}\in\textsf{s}\) there is a \(\textsf{t}\subseteq\textsf{W}_{\Gamma,\Delta}\) s.t. \((1)\) \(\#\textsf{t}= n_\varphi\) \((2)\) \(\textsf{w}\textsf{R}\textsf{t}\subseteq\Gamma\) \((3)\) \(\textsf{t}:\varphi\in\Delta\)

• If \(\textsf{s}:\Box\varphi\in\Gamma\), then for all \(\textsf{w}\in\textsf{s}\) and all finite \(\textsf{t}\) s.t. \(\textsf{w}\textsf{R}\textsf{t}\subseteq\Gamma\), \(\textsf{t}:\varphi\in\Gamma\)

• If \(\textsf{s}:\varphi\land\psi\in\Delta\), then \(\textsf{s}:\varphi\in\Delta\) or \(\textsf{s}:\psi\in\Delta\)

• If \(\textsf{s}:\varphi\land\psi\in\Gamma\), then \(\textsf{s}:\varphi\in\Gamma\) and \(\textsf{s}:\psi\in\Gamma\)

• If \(\textsf{s}:\varphi\to\psi\in\Delta\), then for some \(\textsf{t}\subseteq\textsf{s}\) \(\textsf{t}:\varphi\in\Gamma\) and \(\textsf{t}:\psi\in\Delta\)

• If \(s:\varphi\to\psi\in\Gamma\), then for all \(\textsf{t}\subseteq\textsf{s}\), \(\textsf{t}:\varphi\in\Delta\) or \(\textsf{t}:\psi\in\Gamma\)

• If \(\textsf{s}:\forall x\varphi\in\Delta\), then for some \(z\in Var\), \(\textsf{s}:\varphi[z/x]\in\Delta\)

• If \(\textsf{s}:\forall x\varphi\in\Gamma\), then for all \(z\in Var\), \(\textsf{s}:\varphi[z/x]\in\Gamma\)

We have thus shown that any non-derivable sequent can be extended to a saturated \(g\)-sequent. From any such \(g\)-sequent, we can then construct a canonical model that refutes it. The saturation conditions will guarantee that this model acts as a countermodel for the original sequent.

3.5.0.2 Canonical model construction

Let \(\Gamma\Rightarrow\Delta\) be a saturated g-sequent. We define a canonical model \(M_{\Gamma,\Delta}^c=\langle\textsf{W}_{\Gamma,\Delta},D^c,R^c,I^c\rangle\) as follows:

• \(\textsf{W}_{\Gamma,\Delta}\) is the universe of the g-sequent \(\Gamma\Rightarrow\Delta\), i.e. the set of all indices that occur in it;

• \(D^c\) is the set of variables occurring in \(\Gamma\Rightarrow\Delta\);

• \(\textsf{w}R^c \textsf{v}\iff \textsf{w}\textsf{R}\textsf{v}\in\Gamma\);

• \(\langle x_1,\dots,x_n\rangle\in I^c_\textsf{w}(P)\iff \{\textsf{w}\}:P(x_1,\dots,x_n)\in\Gamma\).

Proof. By induction on \(\varphi\). We consider the cases of \(\varphi=P(\bar{x})\) and \(\varphi=\Box\psi\) (we omit the subscript for the assignment, for readability).

• Suppose \(\textsf{s}:P(\bar{x})\in\Gamma\). By saturation (at\(L\)), for all \(\textsf{w}\in\textsf{s}\) we have that \(\textsf{w}:P(\bar{x})\in\Gamma\). By definition of \(M^c_{\Gamma,\Delta}\), for all \(\textsf{w}\in\textsf{s}\): \(\bar{x}\in I^c_w(P)\). Therefore, \(M^c,\textsf{s}\models P(\bar{x})\).

• Suppose \(\textsf{s}:P(\bar{x})\in\Delta\). By saturation (at\(R\)), for some \(\textsf{w}\in\textsf{s}\), we have that \(\textsf{w}:P(\bar{x})\in\Delta\). Clearly, then, \(\textsf{w}:P(\bar{x})\notin\Gamma\), or we would have that \(\Gamma\Rightarrow\Delta\) is an instance of (id), contradicting (unprov). This implies that \(\bar{x}\notin I^c_\textsf{w}(P)\), meaning that \(M^c,\textsf{s}\not\models P(\bar{x})\).

• Suppose \(\textsf{s}:\Box\psi\in\Gamma\). We need to show that for any \(\textsf{w}\in\textsf{s}\), \(M^c_{\Gamma,\Delta},R^c[\textsf{w}]\models\psi\). Since \(\psi\) is finitely coherent, it suffices to show that for any \(\textsf{w}\in\textsf{s}\) and any finite \(\textsf{t}\subseteq R^c[\textsf{w}]\), \(M^c_{\Gamma,\Delta},\textsf{t}\models\psi\).

  So, take a \(\textsf{w}\in\textsf{s}\) and a finite \(\textsf{t}\subseteq R^c[\textsf{w}]\). By definition of \(R^c\), the latter means that for each \(\textsf{v}\in\textsf{t}\), \(\textsf{w}\textsf{R}\textsf{v}\in\Gamma\). So, we have \(\textsf{w}\textsf{R}\textsf{t}\subseteq\Gamma\). By saturation, \(\textsf{s}:\Box\psi\in\Gamma\) and \(\textsf{w}\textsf{R}\textsf{t}\subseteq\Gamma\) together imply \(\textsf{t}:\psi\in\Gamma\). By induction hypothesis, \(M^c_{\Gamma,\Delta},\textsf{t}\models\psi\), as required.

• Suppose \(\textsf{s}:\Box\psi\in\Delta\). By saturation, for some \(\textsf{w}\in\textsf{s}\) and some finite set \(\textsf{t}\) we have \(\textsf{w}\textsf{R}\textsf{t}\subseteq\Gamma\) and \(\textsf{t}:\psi\in\Delta\). By induction hypothesis, this gives \(M^c_{\Gamma,\Delta},\textsf{t}\not\models\psi\). Since \(\textsf{w}\textsf{R}\textsf{t}\subseteq\Gamma\) we have \(\textsf{t}\subseteq R^c[\textsf{w}]\). By persistency, \(M^c_{\Gamma,\Delta},R^c[\textsf{w}]\not\models\psi\). Since \(\textsf{w}\in\textsf{s}\), we conclude \(M^c_{\Gamma,\Delta},\textsf{s}\not\models\Box\psi\).\(\Box\)

We can now prove that IWMC is complete in the sense that it derives any valid (finite) sequent.

We have thus established that IWMC is complete with respect to sequents: it derives all and only the valid ones. Via the connection provided by Proposition [prop:connection], it follows that IWMC is also complete (and indeed, by compactness, strongly complete) with respect to entailment in the logic \(\textsf{InqQML}^{-}_{\Box}\).

3.6 Adding identity.↩︎

In this section, we show how to generalize our approach to the case of signatures including the identity predicate. We start with a brief introduction to the implementation of identity in \(\textsf{InqQML}^{-}_{\Box}\). For a more complete presentation of identity in first-order inquisitive logic, we refer to [@Ciardelli:23book].

3.6.0.1 Identity in \(\textsf{InqQML}^{-}_{\Box}\)

In first-order inquisitive logics, identity is seen as a binary predicate whose interpretation can change across possible worlds. Syntactically, we extend the definition of the language of \(\textsf{InqQML}^{-}_{\Box}\) to include, amongst the predicate atoms, identity atoms of the form \(x=y\), where \(x,y\in Var\).

Semantically, the identity predicate \(=\) is interpreted as a standard binary predicate. Therefore, in a model \(M=\langle W,D,R,I\rangle\), for any world \(w\in W\), \(I_w(=)\subseteq D^2\). However, the interpretation of the identity predicate must satisfy two additional constraints. For a predicate \(P\) and world \(w\), let \(P_w\) and \(=_w\) denote, respectively, \(I_w(P)\) and \(I_w(=)\). Then, for any \(w\in W\):

• Congruence: for any \(d_1,d'_1,\dots,d_n,d'_n\in D\) and \(n\)-ary predicate \(P\), if \(d_1=_w d'_1,\dots, d_n=_w d'_n\), then: \[\text{\langle d_1,\dots,d_n\rangle\in P_w\iff \langle d'_1,\dots,d'_n\rangle\in P_w}\]

• Equivalence: \(=_w\) is an equivalence relation on \(D\)

The recursive definition of the support relation remains the same as in the case without identity, and the clause for identity atoms can be obtained from the one for predicates:

• \(M,s\models_g x=y\iff \text{for all w\in s, }\langle g(x),g(y)\rangle\in I_w(=)\)

3.6.0.2 Extending the proof system.

Since we see identity as a binary predicate, we extend the applicability of \(({\Rightarrow}\textsf{at})\) and \((\textsf{id})\) to labelled identity atoms \(\textsf{s}:x=y\). However, we also need to extend IWMC with rules encoding the specific properties of identity. We add two rules, inspired by [@Negri:01], and call the extended calculus \(\textrm{\textsf{IWMC}}^=\). In the rules, \(x,y\in Var\), \(\bar z\) is a sequence of variables, and \(\varphi[[y/x]]\) denotes the substitution of an arbitrary number of instances of \(x\) in \(\varphi\) with instances of \(y\):

The extended system \(\textrm{\textsf{IWMC}}^=\) satisfies analyticity and the structural properties that we proved for IWMC in Section 3.4. Additionally, the following rules encoding the properties of \(=\) as an equivalence relation are admissible:

For any formula \(\varphi\), the replacement axiom \(\textsf{s}:x= y,\;\textsf{s}:\varphi\Rightarrow\textsf{s}:\varphi[[y/x]]\) can be shown to be derivable by adapting the argument provided in [@Negri:01]. Our proof uses the admissibility of the following sub-label replacement rule:

We give an informal sketch of the proof, which is mostly routine. We prove, by induction on the length of \(\varphi\), the stronger claim that \(\textsf{s}:x= y,\;\textsf{s}':\varphi\Rightarrow\textsf{s}':\varphi[[y/x]]\) is derivable for any \(s'\subseteq s\). The base case for \(\varphi\) atomic is immediate by the admissibility of (Sub-Repl). The stronger claim is needed to prove the inductive case of implication, where subsets of \(s\) are generated by the rules for \(\to\). Here, the structure of the derivation is the same as in the original proof, but the inductive hypotheses involve subsets of the initial label. The remaining cases, including the inductive case of \(\Box\), follow from standard arguments.

Combining the structural properties of \(\textrm{\textsf{IWMC}}^=\) with the derivability of the replacement axiom and the admissibility of the above rules makes it straightforward to prove the admissibility of (\(\textsf{G-Repl}\)), which generalizes (Repl) to arbitrary formulas, and of (\({\Rightarrow}\)G-Repl), a generalized right-replacement rule:

Using analogous arguments, one can prove the admissibility of their sub-label versions (Sub-G-Repl) and (\({\Rightarrow}\)Sub-G-Repl), where \(\textsf{s}:\varphi\) and \(\textsf{s}:\varphi[[y/x]]\) are replaced, respectively, by \(\textsf{s}':\varphi\) and \(\textsf{s}':\varphi[[y/x]]\), with the requirement that \(\textsf{s}'\subseteq\textsf{s}\) (notice that the stronger claim used in the derivability proof for the replacement axiom above is exactly what is needed in this more general case).

3.6.0.3 Completeness proof.

To adapt the definition of saturated sequent, we extend (at\(L\)) and (at\(R\)) to labelled identity atoms of the form \(\textsf{s}:x=y\) and we add the following clauses:

• \((= L)\) If \(\textsf{s}:x= y\in\Gamma\), then: (i) if \(\textsf{s}:\varphi\in\Gamma\), then for any possible substitution \(\varphi[[y/x]]\), \(\textsf{s}:\varphi[[y/x]]\in\Gamma\) and (ii) if \(\textsf{s}:\varphi\in\Delta\), then for any possible substitution \(\varphi[[y/x]]\), \(\textsf{s}:\varphi[[y/x]]\in\Delta\)

• \((= Ref)\) For all \(x\in Var\) that occur in \(\Gamma\cup\Delta\), for all singleton labels \(\textsf{w}\in W_{\Gamma,\Delta}\), \(\textsf{w}:x= x\in\Gamma\)

The proof of the saturation lemma requires two changes. We fix an enumeration \((z_i)_{i\in\mathbb{N}}\) of all variables in the extended language. First, for each \(i\in\mathbb{N}\), we add to \(\Gamma_{i+1}\) the finite set of labelled formulas \(\textsf{Id}(i)\mathrel{\vcenter{:}}=\{k:z_j= z_j\mid 0\leq k,j\leq i,\;k\in W_{\Gamma_i,\Delta_i} \text{, and }z_j\text{ occurs in }\Gamma_i\cup\Delta_i\}\). Underivability holds by (Ref). We also extend the case of an atom \(\textsf{s}_i:P(\bar{x})\) being in \(\Delta_i\) to include identity atoms of the form \(\textsf{s}_i:x=y\).

Then, we include one additional inductive case for identity atoms. If \(\varphi_i\) is \(x= y\) and \(\textsf{s}_i:x= y\in\Gamma_i\), we let \(\Gamma_i^{\textsf{at}}=\Gamma_i\cup\{\textsf{w}:x=y\mid\textsf{w}\in\textsf{s}_i\}\) and we let \(Sub_i(\varphi)\) be the set of all possible substitutions \(\textsf{s}':\varphi[[y/x]]\) for all \(\textsf{s}'\subseteq\textsf{s}_i\). We define \(\Gamma_{i+1}=\Gamma_i^{\textsf{at}}\cup(\bigcup_{\textsf{s}_i:\varphi\in\Gamma_i^{\textsf{at}}}Sub_i(\varphi))\;\cup\;\textsf{Id}(i)\). and \(\Delta_{i+1}=\Delta_i\cup(\bigcup_{\textsf{s}_i:\varphi\in\Delta_i}Sub_i(\varphi))\). To prove that \(\Gamma_i^{\textsf{at}}\Rightarrow\Delta_i\) is underivable, we proceed as in the proof of Lemma 2 for the atomic case. The underivability of \(\Gamma_{i+1}\Rightarrow\Delta_{i+1}\) is guaranteed by the rule \((\textsf{Ref})\) in the case of \(\textsf{Id}(i)\) and by the rules \((\textsf{Sub-G-Repl})\) and \(({\Rightarrow}\textsf{Sub-G-Repl})\) for the remaining additions to \(\Gamma_{i+1}\) and \(\Delta_{i+1}\). With this construction, verifying the saturation conditions is straightforward.
The definition of the canonical model remains unchanged from the case without identity, since we view identity as a binary predicate. In particular, the derived definition for the extension of identity is \(\langle x,y\rangle\in I^c_\textsf{w}(=)\iff \textsf{w}:x=y\in\Gamma\). The verification of the congruence property of \(=\) is immediate thanks to the saturation conditions. The fact that \(=\) is an equivalence relation also follows easily: for symmetry, if \(\textsf{w}:x=y\in\Gamma\), then \(\textsf{w}:x=x\in\Gamma\) by (\(=Ref\)) and, therefore, \(\textsf{w}:y=x\in\Gamma\) by (\(=L\)); for transitivity, if \(\textsf{w}:x=y,\;\textsf{w}:y=z\in\Gamma\), then we have that \(\textsf{w}:y=x\in\Gamma\), which can be used in combination with \(\textsf{w}:y=z\in\Gamma\) to get that \(\textsf{w}:x=z\in\Gamma\) by (\(=L\)). The remaining steps of the completeness proof are analogous to the identity-free case.

4 Future work↩︎

We conclude by outlining some directions for potential future extensions of this work.

A natural question is whether the approach can be extended to arbitrary signatures containing function symbols as well as the identity predicate. In inquisitive first-order logics, the interpretation of function symbols can vary between possible worlds. For this reason, there is a distinction between rigid function symbols and terms, whose interpretation is constant, and non-rigid ones. We denote the first in bold (e.g., f, t). These two classes of syntactic objects are known to satisfy different properties semantically (see [@Ciardelli:23book] for a detailed discussion). For signatures containing function symbols, it seems natural to assume that \(\textrm{\textsf{IWMC}}^=\) could be adapted by using arbitrary terms instead of variables in the rules \((\textsf{id})\) and \(({\Rightarrow}\textsf{at})\), and by replacing \((\forall{\Rightarrow})\) with the following two rules, where \(\alpha\) stands for a classical formula, \(t\) for an arbitrary fresh term and \(\boldsymbol{t}\) for a fresh rigid term:

In Section 3.4, we showed that IWMC enjoys key structural properties. It remains an open question whether the properties of our calculus can be used to obtain metatheoretical results about the logic \(\textsf{InqQML}^{-}_{\Box}\), such as interpolation. The structural properties we established, and in particular invertibility, may also allow us to define a systematic proof search procedure for our calculus; completeness could then be established by showing that a failed proof search always produces a countermodel, following a well-established strategy for labelled sequent calculi for modal logics (see, e.g., [@GargGenoveseNegri:12; @Negri:14]).

Other inquisitive modalities are natural candidates for extending the present approach. A particularly interesting case is that of neighborhood-based inquisitive modalities (see, for instance, the ones proposed in [@CiardelliInqNL:25] and [@CiardelliRoelofsen:15idel]). In neighborhood frames, the accessibility relation associates to each possible world a set of sets of possible worlds. It would be interesting to explore whether our labelled sequent calculus can be adapted to this semantic setting with similarly positive results.

---

1. An analogous move is made in the team semantics tradition, where assignments are replaced by sets of assignments called teams (see, a.o., [@Hodges:97; @Vaananen:07; @Galliani:12; @GradelVaananen:13]). For connections between these two lines of work see, among others, [@YangVaananen:16; @Ciardelli:16dependency].↩︎

2. A logic is said to be entailment-compact if whenever a formula \(\psi\) follows from a set of formulas \(\Phi\), it follows from a finite subset \(\Phi_0\subseteq\Phi\). In inquisitive logic, this is not equivalent to the more common formulation of compactness in terms of satisfiability, essentially due to the fact that the double negation law does not hold in general.↩︎

3. The notion of coherence goes back to the team semantics literature, where it was first investigated by Jarmo Kontinen [@Kontinen:13].↩︎

4. One may wonder if it is also possible to obtain a proof system for \(\textsf{InqQML}^{-}_{\Box}\)by extending the natural deduction system in [@Conti25]. This seems difficult, since the completeness proof in [@Conti25] relies on the finite model property of InqWQ, which does not extend to \(\textsf{InqQML}^{-}_{\Box}\). Regardless of this problem, the labelled approach of [@LitakSano:25] seems preferable due to its better proof-theoretic properties.↩︎

5. We exclude empty labels for simplicity. While the empty state is officially allowed in the semantics of \(\textsf{InqQML}^{-}_{\Box}\), it plays a trivial role, since it supports any formula whatsoever, and can be omitted without affecting the logic.↩︎