{'fraction_non_alphanumeric': 0.04966241022977595, 'fraction_numerical': 0.00796962587531565, 'mean_word_length': 3.9801997859436318, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 1, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 17, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Pooling Modalities and Pointwise Intersection: Axiomatization and Decidability

We establish completeness and the finite model property for logics featuring the pooling modalities that were introduced in Van De Putte and Klein (Pooling modalities and pointwise intersection: semantics, expressivity, and applications). The definition of our canonical models combines standard techniques with a so-called “puzzle piece construction”, which we first illustrate informally. After that, we apply it to the weakest classical logics with pooling modalities and investigate the technique’s potential for the axiomatization of stronger logics, obtained by imposing well-known frame conditions on the models.


Introduction
Pooling modalities are a specific type of modal operators, interpreted in terms of neighbourhood models and the operation of pointwise intersection. Logics featuring such modalities were introduced in [8], where their relation to normal modal logics, their expressive power, and some potential applications of these logics are studied. The main aim of this more technical paper is to give sound and strongly complete axiomatizations for various logics with pooling modalities and to show that they satisfy the finite model property (and hence are decidable). We do so using an altogether new technique for building canonical models in combination with other, familiar techniques from the general theory of modal logics.
In the remainder of this introduction, we briefly recapitulate the central notions from [8] in an informal, loose way. Exact definitions are recalled in Section 2. We refer the reader to [8] for an elaborate discussion, motivation, and investigation of the language and semantics of pooling modalities.
Somewhat loosely speaking, pooling modalities are classical modal operators in the sense of [3] that allow us to express that a given proposition ϕ coincides with the intersection of various propositions that are each associated with a given index i. According to one specific interpretation, such modalities allow us to formalize reasoning about the aggregation of evidence of a given agent i or of several agents i 1 , . . . , i n . In this context, {1,1,2} p may be read as: "aggregating two pieces of evidence of agent 1 with one piece of evidence of agent 2, we can obtain the evidence that p".
This way, pooling modalities allow to express information that is implicit among agents having various pieces of evidence, but that can be obtained by pooling their evidence. The multiset {1, 1, 2} that is attached to the modal operator indicates (a) the agents whose evidence we are combining, and (b) the number of pieces of evidence that we may take from each agent.
It should however be noted that this is only one among many potential applications of pooling modalities. Alternatively, one may use them to interpret notions of group agency and coalitional abilities, distributed (nonnormal) belief or knowledge, implicit obligations, or collective norms [8,Section 6]. In the present paper we abstract from those various applications of the logics and focus on their axiomatization and related issues.
Semantically, pooling modalities are interpreted over multi-index neighbourhood models, i.e. possible worlds models with a domain W that have a distinctive neighbourhood function N i : W → ℘(℘(W )) for each index i in a given index set I. Here, each neighbourhood function N i records the set of propositions that are associated with the index i at each world w in the model. Pooling modalities are interpreted over such models in terms of the operation of pointwise intersection of neighbourhood sets. Loosely speaking, pointwise intersection is the intersections of neighbourhoods X ∈ N i (w) (rather than the entire neighbourhood sets or collections N i (w)), where the number of neighbourhoods that we may take from each neighbourhood set is specified by the index of the pooling modality, cf. (a) and (b) above. So for instance {1,1,2} (p ∧ q) will be true at the world w if and only if the proposition denoted by p ∧ q in the model coincides with the intersection of three sets X, Y, Z, where X, Y ∈ N 1 (w) and Z ∈ N 2 (w).
The plan for this paper is as follows. In Section 2 we recapitulate the notation and definitions from [8] that are required for present purposes. In the three subsequent sections, we focus on the weakest modal logics that can be interpreted in terms of pointwise intersection. While arguably, many applications require stronger logics, focusing on the weakest modal logics first allows us to present our results in their most general form. We present the axiomatization of these logics in Section 3 and show our axioms to be logically independent. Section 4 provides an informal explanation of the new technique for constructing canonical models that is implemented in Section 5. In Section 6, we turn to a range of stronger logics that are suited for various applications. These logics are obtained by imposing various wellknown frame conditions on our models. An overview of our main results is given in Section 7, after which we conclude with a number of pointers to open issues and future work (Section 8).

Preliminaries
In this section, we recall the notion of a pooling profile, and subsequently introduce the formal languages and semantics of classical logics with pooling modalities from [8]. We will introduce some new notation and observations along the way, but clearly indicate this when doing so.
where p ∈ P and M ∈ M f Intuitively, a pooling profile M indicates, for each i ∈ I, the number of sets X ∈ N i (w) that we can use in order to obtain a member Y of the neighbourhood set N M (w). The symbol ∞ can be read as "arbitrarily many". Thus, X ∈ N {(1,∞)} (w) means that X is the result of intersecting an arbitrary number of members of N 1 (w), whereas Y ∈ N { (1,2),(2,∞)} (w) expresses that Y can be obtained by intersecting two members of N 1 (w) with an arbitrary number of members of N 2 (w). 1 Table 1 gives the Backus Naur Forms of the four formal languages that will be studied in this paper. All of them extend the standard classical propositional language (based on a countable set of propositional variables P) with unary modal operators of the type M . The richest of these, L In examples and informal digressions, we will sometimes use more sloppy notation, writing e.g. 1,1,2 p instead of { (1,2),(2,1)} p. We will also abbreviate a sequence of index i repeated k times by i k , and use i ∞ to refer to "any arbitrary number of i's". Finally we require some additional notation that has not yet been introduced in [8]:

Semantics
The formal language L [∀] ∞ is interpreted in terms of neighbourhood models, where each index i ∈ I receives a distinct neighbourhood function N i : Where w ∈ W and i ∈ I, we refer to the members of a given N i (w) as the neighbourhoods for i at w, where we call N i (w) the neighbourhood set for i at w. In order to spell out the semantics for the pooling modalities in exact terms, we first define the notion of pointwise intersection, after which we apply it to the models from Definition 4.
The neighbourhood function N M in M is defined as follows: for every w ∈ W , With these preliminary definitions, we can now give the semantic clauses for the formulas in L ∞ , and hence, by restriction, also for L ∞ , L [∀] f and L f Definition 7. Where M = W, N i i∈I , V is a model and w ∈ W : Validity ( ϕ) and semantic consequence (Γ ϕ) are defined in the standard way, viz. as truth, resp. truth-preservation at all worlds in all models. Since we consider four distinct formal languages (cf. Table 1), these definitions give us four distinct logics. We will henceforth refer to the latter as the base logics, and denote them by BL ∞ , BL [∀] ∞ , BL f , and BL [∀] f respectively. Note that up to this point, we did not impose any specific frame conditions on the models. Such frame conditions and the associated logics are discussed in Section 6.
New facts Before continuing, we note some properties of pointwise intersections that we will rely upon in the remainder of this paper. The verification of these facts is safely left to the reader.
Fact 1. For all sets X of sets, each of the following hold: Fact 2. For all sets X , Y, . . . of sets, each of the following hold:

Axiomatization of the Four Base Logics
In this section, we start by noting a number of key validities of the four base logics (Section 3.1) and showing the independence of these validities (Section 3.2). After that, we present the axiomatization of the four base logics (Section 3.3) and clarify an issue related to their compactness (Section 3.4).

Validities
First, as usual, [∀] behaves like a normal operator of type S5 in BL [∀] ∞ and BL [∀] f . Second, since the models we work with are a specific type of neighbourhood models, it follows immediately that if two propositions ϕ, ψ are equivalent in any of the logics, then M ϕ entails M ψ and vice versa. In other words, pooling modalities are classical modal operators in the sense of [3]: In the languages with the global modality [∀], we can moreover express that in a given model, ϕ and ψ are co-extensive (i.e. they are true at the same set of worlds). This gives us the stronger property of replacement under global equivalents: Third, the base logics satisfy four central bridging principles, i.e. validities that link distinct operators M , M , . . . to one another. For the fourth of these, we use the convention that The four key bridging principles to be discussed can now be written as follows: Theorem 1. Each of (B1)-(B4) are valid in every model.
Proof. (B1) follows from a simple observation, that is itself an immediate consequence of Fact 2: For (B2), suppose that M, w |= M N . Hence, for every i ∈ I(M N ), there is an X i ∈ N i (w) such that X i = W . Note that I(M ) ⊆ I(M N ), and i∈I(M ) X i = W ∈ N M (w). Hence, W ∈ N M (w).
For (B3), suppose that M, w |= M ϕ and M, w |= M N N ϕ. Applying Fact 3 twice, we obtain: Finally, for (B4), it suffices to observe that, by Fact 1, for all M ∈ M ∞ , Let us briefly comment on each of the bridging principles. First, (B1) is probably the most expected among the four; it simply expresses that whenever X ∈ N M (w) and Y ∈ N N (w), then X ∩ Y ∈ N M N (w). When applied to M = N = {i}, this principle gives us a more fine-grained variant of the aggregation axiom (C), keeping track of the number of pieces of information one needs to combine in order to arrive at a given proposition: Principle (B2) concerns the border cases where W ∈ N M N (w); in that case, each i ∈ I(M N ) must contain the unit W . Note that the consequent of this principle is vacuously true for models in which every neighbourhood contains the unit.
(B3) is perhaps the least intuitive property of the four. Applied to the case with M = {1}, N = {2}, and N = {3}, it expresses the following: if X is a member of N 1 (w) and X is a member of the pointwise intersection of N 1 (w), N 2 (w), and N 3 (w), then X is also a member of the pointwise intersection of N 1 (w) and N 2 (w).
Finally, (B4) deals explicitly with the pooling profiles M ∈ M ∞ \M f . As we show below, one can use the other axioms to derive a kind of iteration principle (see Theorem 3.3). (B4) essentially generalizes this principle to the case where we have infinitely many indices in the consequent.

Proof of Independence
Importantly, none of the four principles (B1), (B2), (B3), and (B4) can be derived from any combination of the others. In order to show this, we need to define a more general semantics that allows us to invalidate some of the principles while validating the others.
is a neighbourhoud function, and V : P → ℘(W ) is a valuation function.
The basic idea behind a g-model is that it associates a distinct neighbourhood function with each pooling profile, rather than taking N M to be defined in terms of the primitive neighbourhood functions N i . In other words, pointwise intersection corresponds to the additional assumption on g-models that they be pooled, i.e., that for every M ∈ M ∞ , N M (w) satisfies the equation in Definition 6. With this generalized semantics at hand we can prove the following theorem: Note that at w 1 , 1 p∧ 1,2,3 p holds, but 1,2 p fails. So it remains to check the validity of the other axioms. For (B1), suppose that G, w |= M ϕ∧ N ψ for a w ∈ W . This implies that, for both M and N , Case 1 of the above definition applies. From this we can infer that Case 1 also applies to M N , (B2) holds trivially, since, for any M , M is false at both w 1 and w 2 . Finally, for (B4), suppose that G, w |= M ϕ. This again means that Case 1 of our definition applies, and hence also Case 1 applies to M ∞ . Consequently,  Table 2. Axioms and rules and the four base logics. " " indicates that the axiom schema is included in the logic; "D" indicates that the axiom schema or rule is derivable All S5-axioms and rules for [∀] (CL) Classical propositional logic

Axiomatization
Throughout this paper, we work with Hilbert-style axiomatizations in terms of axiom schemata. As usual, ϕ is a theorem of a given logic ( ϕ) if and only if ϕ can be derived from the axioms of the logic by application of the rules that are valid in the logic. Syntactic consequence is defined as follows: Note that by this very definition, the syntactic consequence relations we will be working with are compact. In Section 5 we show that, using (B1)-(B3) in combination with either (RE) or (RGE), we obtain sound and strongly complete axiomatizations for the languages L f , resp. L [∀] f . If we moreover add (B4), then we obtain sound and strongly complete axiomatizations for the languages L ∞ and L ∞ . See Table 2 for an overview of the resulting logics.
In order to illustrate their strength, we list a number of schemata that can be derived from the above principles in combination with (RE). Theorem 3.1 gives a (weak) sufficient condition for deriving M N ϕ from M ϕ: there has to be some ψ such that N (ϕ∨ψ) holds. Theorem 3.2 illustrates the strength of (B3), when combined with (B1). Theorem 3.3 gives a kind of iteration property: e.g. it allows us to derive 1,1 p from 1 p, and 1,1,2,2,3 q from 1,2,3 q. Finally, Theorem 3.4 shows that, in the presence of necessitation, bigger pooling profiles inherit the neighbourhoods of smaller ones.

Compactness
As we will show in the next sections, the above axiomatizations are strongly complete with respect to the respective base logics. As an immediate corollary, the semantic consequence relations of these logics are compact. This may come as a surprise, in view of the seemingly infinitary character of pointwise intersection for pooling profiles M ∈ M ∞ \M f .
In order to explain this feature, we note two crucial design choices of the logics. First, consider the case of a simple pooling profile M = {(1, ∞)}. Note that p M ∈ N M (w) means that there is some subset X ⊆ N M (w) such that X = p M . In particular, and as pointed out in Section 2.1, the size of X is arbitrary. As a result, the following infinite set is satisfiable: All it takes to satisfy Δ is a countably infinite model, in which only the intersection of a (countably) infinite number of neighbourhoods X i ∈ N 1 (w) gives us the truth set of p. An example in case is one where W = N, p M = ∅ and N 1 (w) = {W \{0, . . . , k} | k ∈ N} for some w ∈ W .
Those familiar with Propositional Dynamic Logic (PDL) may compare this to the fact that the set {¬ π p, ¬ π; π p, ¬ π; π; π p, . . .}∪{ π * p} is not satisfiable in PDL, even though all its finite subsets are. This is so because in PDL, π * p expresses that a p-world can be reached by some finite sequence of π-executions. In "Appendix", we discuss a notion of "finitary pooling" and the associated modal operators. There, we show that the resulting logic is not compact and that, in view of our main results, one can easily give a sound and weakly complete axiomatization for it.
Second, note that we excluded pooling profiles whose range is infinite, cf. our clause (a) in Definition 1. As a result, the formal languages cannot express that some X ⊆ W is obtained by intersecting a countably infinite set of neighbourhoods X 1 ∈ N 1 (w), X 2 ∈ N 2 (w), . . .. Suppose, indeed, that we would allow for an "infinitary pooling profile" such as M ω = {(1, 1), (2, 1), (3, 1), . . .}, which we interpret as follows: With such an enrichment, compactness fails, as witnessed by the following example: To see why (1) holds, it suffices to check that if we take infinitely many intersections of p M , we end up with p M again. It is also fairly easy to construct a model that serves as witness for the failure of implication in (2), for any given n ∈ N.
The valuation function is such that p is true at w. Then N M ω (w) = ∅, and hence M, w |= ¬ M ω p. 2 In the example we just used, the frame has the particular property that for all j ∈ I with j > n, N j (w) is empty. Note however that one can also construct different examples where each of the N j (w) for j > n are nonempty, but there are no X ∈ N j (w) with X ⊆ p . One condition that does exclude such examples, and more generally trumps cases like (2), is the requirement that W ∈ N i (w) for all i ∈ I, w ∈ W , corresponding to necessitation (NEC) for the operators i . Indeed, if that requirement is satisfied, then we already have 1 p → M ω p.
One other obvious difficulty with logics that allow for "infinitary pooling profiles" is that the language may not be countable, hence making it impossible to set up the standard Lindenbaum construction in the completeness proof. This is not a definitive argument against studying such languages, but rather an invitation to consider additional conditions or new techniques for their axiomatization. Having said this much, we leave a full study of such languages for future work and focus again on the four languages introduced in Table 1.

Canonical Model Construction: Puzzle Pieces
Before diving into technicalities, let us sketch the main novelty of our construction, compared to existing completeness proofs for normal and classical modal logics. This should give the reader a feel of how this construction works, and serve as a guideline in reading the definitions and lemmata of the actual proofs that are given in Section 5. We assume familiarity with the technique of constructing canonical models as it is applied in the context of normal modal logics, cf. [2].

General Outline
Focusing on the richest of the four base logics, the general outline of our proof goes as follows. Suppose we have a set Θ ⊆ L [∀] ∞ that is consistent with respect to the base logic BL [∀] ∞ . To prove strong completeness, we should show that this set is satisfiable in some model M = W, N i i∈I , V of that logic, at some state w ∈ W . Moreover-in order to obtain the finite model property in one fell swoop-we should show that W is finite whenever Θ is finite. We will focus first on completeness; we return to the finite model property at the end of this section.
Following common practice in modal logic, one can start by taking W = MCS, where MCS is the set of all maximal consistent subsets of L ∞ . This way, we are guaranteed that some of the worlds in W will contain Θ as a subset. If we can then prove the Truth Lemma (TL): we are done. For non-modal formulas, it is easy to obtain (TL). To do so just put V (Λ) = {p ∈ P | p ∈ Λ} for all Λ ∈ MCS and apply the wellknown structural induction for the classical connectives. For formulas of the type i ϕ, hence, "degenerate" pooling modalities that only speak about a single index i, the standard way to ensure the truth lemma is by defining the neighbourhoods for the indexes i ∈ I as follows: Relying on (RGE), one can then show in relatively few steps that (TL) holds for formulas of the form i ϕ as well. 3

Problem: Pooling Modalities
Trouble arises however if we want to preserve (TL) for proper pooling modalities. In order to sketch the problem and our solution to it, we will use the following set of formulas as our running example: The set Θ is consistent, and hence in line with the preceding, we need to construct a model M such that, for some w in the domain of this model, M, w |= ψ for all ψ ∈ Θ. As noted before, we do this by associating worlds with maximal consistent sets, one of those sets including all members of Θ, and then proving a truth lemma about the model: each formula ψ is true at a world w in M iff ψ is a member of the maximal consistent set associated with w.
In particular, where Θ is associated with w, we need to ensure that a given formula M ϕ is true at w in our constructed model, iff M ϕ ∈ Θ. So, moving to the object level: where M = {1, 1, 2} and ϕ = p, we should "add" neighbourhoods X and Y to N 1 (w), and a neighbourhood Z to N 2 (w), in such a way that X ∩ Y ∩ Z is (exactly) the set of all w that are associated with an MCS Δ for which p ∈ Δ. Let us henceforth denote the latter set of worlds by |p|. More generally, we let |ψ| = df {w ∈ W | ψ ∈ Δ for the Δ that is associated to w}. 4 Note however that, by thus making 1,1,2 p true, we should make sure we are not making other formulas like 1 p, 2 p, 1,2 p, or 1,1 p trueotherwise we cannot end up with a model of Θ. Consequently, neither X, Y , Z, nor X ∩ Y , X ∩ Z, Y ∩ Z should themselves already correspond to |p| in this model. To put it differently, only by intersecting all three sets, we should arrive at |p|.

Solution: Copying and Puzzle Pieces
To solve the problem just sketched, we take two steps. First, rather than identifying worlds with maximal consistent sets, we make copies of those maximal consistent sets and distinguish them by labels. For the time being, let us distinguish the copies of a given Δ ∈ MCS by one of the following three labels: (1, 1), (1,2), and (2, 1). Note that 4 We distinguish between w and Δ here, since later on we will associate various worlds of the canonical model with the same MCS Δ. More technically, in constructing the canonical model W , we introduce several copies of each Λ ∈ MCS, each creating a distinct member of W . Second, we refine our definition of the neighbourhoods. For all formulas of the type i ϕ, we do just as before, following the above definition. However, this time we ensure that we take every copy (Δ, f), for every Δ that contains ϕ. We describe the neighborhoods in greater detail. First, note that, since be no ψ such that X = |ψ|. In other words, by making copies of the maximal consistent sets, we can construct neighbourhoods that cannot be "seen" by the formal language L ∞ . This is illustrated by Figure 1, for the simple case of ϕ = p.
In order to obtain (a), we need to coordinate the construction of these neighbourhoods in such a way that (only) intersecting all of them yields |ϕ|. For the set Θ we have been working with so far, this is relatively easy. That is, we may define: The reader can easily verify that 1,1,2 p will be true at every world (Λ, f), , while each of 1,1 p, 1,2 p, 1 p, 2 p will be false. So far, things were relatively easy since we focused on a single formula of the type M ϕ. In the general case, we need to use as labels functions f that . Importantly, f (M, ϕ) can be distinct from f (N, ψ), both when M = N (but ϕ = ψ) and when ϕ = ψ (but M = N ). This will ensure that, by intersecting puzzle pieces that have been added as witnesses for distinct formulas, we can again not obtain any truth set |ψ|-see Figure 2 for an illustration. Of course, in the limiting case where we do use all the witnessing puzzle pieces for M ϕ and all the witnessing puzzle pieces for N ψ, we will obtain |ϕ∧ψ|. This is however as it should be, since the axiom (B1) ensures that whenever M ϕ ∈ Λ and N ψ ∈ Λ, then M N (ϕ ∧ ψ) ∈ Λ. Finite Models If we apply the above strategy in its full generality, we make uncountably many copies of each maximal consistent set. As far as completeness is concerned, this is all fine. However, to prove the finite model property, two additional tweaks are called for: (i) restricting the language; and (ii) restricting the number of copies.
We discuss each of these adaptations in turn.
Technique (i) is well-known from the study of classical modal logics, dating back at least to [4], cf. [5, 2.4.1.1]. The basic idea is that we only look at the single ([∀], ¬)-closure of the set of all subformulas of members of Θ. This way we get a finite set of maximal consistent sets to start with. Moreover, we only need to make puzzle pieces for a finite number of formulas M ϕ, since we need only worry about the members of the finite language when proving the truth lemma. We refer to Section 5.1 for the exact way this technique is implemented here.
Adaptation (ii) is more specific to the context of pooling modalities. Here, it is instructive to consider the following set: The set Θ expresses that, by intersecting an arbitrary number of neighbourhoods associated with index 2 with a single neighbourhood associated with index 1, we obtain the proposition p . In contrast, p is not a member of the neighbourhood of 1, and it can also not be obtained by combining just one, two, or three neighbourhoods of 2 with a neighbourhood of 1.
In order to arrive at the truth lemma, we need to construct the neighbourhoods for our canonical model in such a way that we make 1,2 ∞ p true, but without thereby making 1 p, 1,2 p, 1,2,2 p, or 1,2,2,2 p true. Naively, one may proceed by making copies (Λ, f) of every maximal consistent set (in the finite language), for every label (i, k) ∈ δ({1, 2 ∞ }). Unfortunately, the latter set is infinite, which would mean our canonical model is also infinite.
Note however that Θ does not say anything about what would happen if we intersect one neighbourhood of 1 with, say, four or more neighbourhoods of 2. That is, Θ is compatible with 1,2,2,2,2 p. So we needn't make infinitely many copies; it suffices to make sure that we make more copies than can be "seen" from the viewpoint of the finitary pooling profiles that occur in Θ . In other words, it suffices to take as labels of our worlds all and only those functions f that map each of the pooling profiles that occur in Θ to some Again, in our above example we were focusing on only a few pooling profiles of increasing magnitude. Things get slightly more complicated if the set Θ under consideration also refers to other, unrelated pooling profiles. Still, as long as Θ is finite, one can always specify a natural number k such that, beyond k, arbitrary intersection (∞) and finite intersections can be safely identified from the viewpoint of Θ. We refer to Section 5.2 for the exact definitions that make this idea exact.

The Base Logics
In this section, we prove completeness and the finite model property for the four base logics. In Sections 5.1-5.5 we focus on BL ∞ , as it requires various complications. In Section 5.6, we show how (slightly simpler) variants of our proof work for the other three logics with pooling modalities.

Sublanguage and Maximal Consistent Sets
∞ . We start by defining a sublanguage L Θ that will be used to construct maximal consistent subsets, following the general methodology mentioned under (i) at the end of Section 4.
Let SF Θ be the closure of Θ under subformulas. Let By compactness and the deduction theorem, there is a finite Φ ⊆ Φ such that By well-known S5-properties, But that means that, for every Δ ∈ MCS Θ Γ , Δ [∀]( Φ → ϕ).

Some More Preparatory Definitions
Just like in standard completeness proofs for classical modal logics, MCS Θ Γ will be used to construct a model of Γ, and hence also of Θ. However, as explained in Section 4, we will need to make a number of copies of each such Δ in order to handle the pooling modalities. We should moreover do so with care, making sure that we only introduce finitely many copies whenever Θ is finite. This requires several preparatory steps.
Intuitively, our definition of K Θ guarantees that this is a subset of N∪{∞} that is "large enough" that we can make all the required distinctions in view of Θ, but also small enough to ensure finiteness whenver Θ is finite. In our example from Section 4, K Θ = {1, 2, 3, ∞}.
Note that, if Θ is finite, then so is D Θ . Also, if that is the case, then I Θ and K Θ are both finite. As a result,

The Relativized Canonical Model
With MCS Θ Γ and F Θ in hand, we are finally ready to define the construction that plays central stage in our completeness proofs of this paper.
Definition 10. The relativized canonical model for Θ, Γ is defined In this and the next two subsections, we hold both Θ and Γ fixed and continue to use W , V , N i to refer to the sets defined from them.
Note that, by the second clause of Definition 10, whenever some p is not in L [∀] Θ , then V (p) = ∅. It is not hard to check that M Θ Γ is well-defined; it suffices to show that W is non-empty, which follows immediately from the fact that Γ ∈ MCS Θ Γ . Moreover, in view of Fact 4, the definition of MCS Θ Γ , and Fact 7, we have: So we have constructed a model that is finite whenever Θ is finite. It remains to prove that this model verifies all the members of Θ at the state (Γ, f). As usual, this is done by proving the truth lemma for M Θ Γ (cf. Lemma 12 in Section 5.4). In preparation for this, we state three auxiliary lemmata.
Intuitively, Lemma 9 expresses that all puzzle pieces X that are used in the construction are distinct, and hence one can associate a unique pair (M, ϕ) with each of them-with the exception of the neighbourhoods that were added for "degenerate" pooling modalities of the type i and neighbourhoods that coincide with the unit W . Lemma 10 implies that, unless we intersect all puzzle pieces that are associated with a given pair (M, ϕ), we will always end up with a subset of W that contains all worlds (Λ, f 0 ) for some f 0 ∈ F Θ . Lemma 11 says that if we do intersect all those puzzle pieces for (M, ϕ), we get exactly the set of all worlds (Λ, f) for which ϕ ∈ Λ.

Nothing but the Truth Lemma
With the above lemmas in hand, we can finally state and prove the truth lemma for BL [ So it remains to prove that, for all M ϕ ∈ L Right to left direction of (TL ). Suppose that M ϕ ∈ Λ. By Lemma 11, By the induction hypothesis and since ϕ ∈ L Taking everything together, we obtain: Moreover, by Definition 10.3, for every Left to right direction of (TL ).   N, ψ, j, l). By the construction, again (N, ψ, j, l) ∈ A † , so that we can put t(N, ψ, j, l) = (i, k).

Completeness and Finite Model Property
From here, it is a matter of routine to derive the following two key results: As shown in [6], the finite model property does not always guarantee decidability, if one is working with a recursively enumerable, rather than a finite, axiomatization. Roughly, the question whether some structure is indeed a model of the logic (hence validates all its axioms) may itself not be decidable. One may be checking this ad infinitum for a single model, before ever being able to turn to the next model that could falsify a given formula.
This problem does not arise for our models. More generally, both the set of BL [∀] ∞ -proofs and the set of finite BL [∀] ∞ -models are easily seen to be recursively enumerable, and hence we have: ∞ is decidable.

Adaptations for L [∀]
f , L f , and L ∞ The above proofs can be adapted in a relatively straightforward way to obtain similar completeness and decidability results for each of BL [∀] f , BL ∞ , and BL f . We will not state the theorems as such, but refer to Section 7 for the overview of all our results.
Let us start with the simplest adaptation. In our completeness proof, we only relied on the axiom schema (B4) when dealing with infinite pooling profiles. In fact, we only applied those axiom schemas at the very end in the two cases of Lemma 12, in order to obtain the conclusion that ϕ ∈ Λ. Hence, leaving out those applications immediately gives us completeness and the finite model property for BL [∀] f . For the languages without the universal modality, the proof also consists in a simplification of the above proof, with some minor adjustments. We sketch them here.
The definitions in Section 5.2 remain unchanged. We define the canonical model M Θ just like M Θ Γ , but replacing MCS Θ Γ with MCS Θ . The facts and lemmas from Sections 5.2 and 5.3 remain unchanged.
In the proof of the Truth Lemma (Lemma 12), we obviously skip the case ϕ = [∀]ψ. Further down in that proof, we replace every expression of the type "Γ [∀]τ " with " τ ", and use (RE) instead of (RGE). So for instance, in the proof of the left-to-right direction of (TL ), Case 1 becomes: ϕ. In Case 2, equation (22) is rewritten to Then, using (28), we can derive K ϕ from (N,ψ)∈C ψ, by means of (RE) instead of (RGE). Similar rewriting of the proof's final steps results in the conclusion that Λ M ϕ and hence M ϕ ∈ Λ. Finally, a completeness proof for BL f is immediately obtained from the completeness proof for BL ∞ , just by skipping the parts that concern pooling profiles in M ∞ \M f . By the same token, we obtain the finite model property and hence decidability for each of the three logics BL [∀] f , BL ∞ , and BL f . Let us insert a brief aside. Relying on Lewis' finitary construction developed in [4], one can also establish the decidability of these logics, as they are all axiomatized by non-iterative modal axioms. 5 However, this method cannot be used to prove completeness with respect to our intended semantics, let alone strong completeness and the semantic compactness that follows from it. 6

Extensions
In this section we prove completeness and the finite model property for a range of stronger logics that are obtained by imposing one or several standard frame conditions on the neighbourhood functions. In all cases, the proofs are variations on the one for the base logic (Section 5), making essential use of the puzzle construction that we illustrated in Section 4. We will also indicate simplified axiomatizations for the studied extensions whenever possible. An overview of all completeness results is given in Section 7.
Some notation will prove useful in the statement of theorems and properties. In the remainder, let BL be a metavariable for any of the four base logics. Where (X 1 ), (X 2 ), . . . are axioms (axiom schemata), we write BL + X 1 + X 2 + · · · to denote the logic obtained by adding (all instances of) (X 1 ), (X 2 ), . . . to the axioms of BL, and closing the resulting set under (RE) and (MP). When we state soundness and completeness results of a given logic with respect to a certain class of frames, we always assume fixed the underlying language of that logic, and we only require the addition of axioms in that language.

Monotonic Models
Recall that a neighourhood model M = W, N i i∈I , V is monotonic iff for all i ∈ I and all w ∈ W , N i (w) is closed under supersets. In the remainder, we will use X ↑ to refer to the closure of X under supsersets. Monotony thus means that N i (w) = N ↑ i (w) for all i ∈ I. In simple (monomodal) classical modal logics, closure of the neighbourhood set N (w) under supersets corresponds to the axiom 7 In the presence of (RE), (AM) entails the monotony rule (RM): if ϕ and ϕ → ψ, then ψ. Conversely, we may characterize monotonic modal logic by replacing (RE) with (RM). Another equivalent formulation is in terms of disjunction: ϕ → (ϕ ∨ ψ). We will focus on a multi-modal variant of (AM) in the remainder, but all our observations readily apply to these alternative characterizations.
Semantically, there are various characterizations of monotonic logics with pooling modalities, besides our official characterization obtained by imposing monotony on the models defined in Section 2-this is spelled out in Section 4.3 of [8]. We briefly recall the semantics in terms of the monotonic semantic clause, as this will turn out useful for our completeness proof: As shown in [8], closing the neighbourhood sets of a model M under supersets-resulting in the supplementation M ↑ -is equivalent to using the indirect semantic clause for that model. That is: In order to axiomatize the logics with pooling modalities over the class of monotonic models, one needs to add all instances of the following schema to BL: Before we prove completeness, we note two properties of these logics. Theorem 7 implies that these logics allow for a slightly simpler axiomatization, skipping the axiom schema (B3). Theorem 8 records a derived rule in the logics with the universal modality, which will turn out useful for our completeness proof.
is derivable in BL Proof. Soundness is, as usual, safely left to the reader. For completeness and the finite model property, we give the argument for BL [∀] ∞ + M. Just as for the base logics, the analogous results for the other three logics are obtained by simplifications of this argument (cf. Section 5.6).
We need to prove that for every (finite) consistent set of formulas Θ, there is a (finite) monotonic model M and a world w in its domain such that M, w |= Θ. So let us hold fixed such a Θ. We define L [∀] Θ , Γ, and the model M Θ Γ in exactly the same way as we did in Section 5. Note that Lemmas 5 , 9, 10, and 11 (and their corollaries) and Facts 4, 6 and 7 are all preserved.
The crucial change occurs in the truth lemma. That is, we now prove the truth lemma given the indirect semantic clause, cf. Definition 11: The proof is exactly the same as the one for Lemma 12, except for the left-to-right direction of (TL ). So suppose that M Θ Γ , (Λ, f) |= M ϕ. We distinguish the same two cases as in the original proof. For Case 1, note that, since each N i (Λ, f) for i ∈ I(M ) is non-empty, we have Applying Lemma 5, we can derive that here is a finite C ⊆ B such that, for all Δ ∈ MCS Θ Γ , Δ [∀]( (N,ψ)∈C ψ → ϕ). Consequently, Let again K = (N,ψ)∈C N . As before, we have K M . Using Lemma 5 and (M[∀]), we derive that K ϕ ∈ Λ. Finally, we rely on (29) to derive that M ϕ ∈ Λ, using (B1) for the finite case and (B4) for the infinite case. This completes the proof of Proposition 1.
Let f ∈ F Θ be arbitrary. By Proposition 1, Once there, we rely on the equivalence of the semantics in terms of the indirect semantic clause and the one in terms of monotonic models. Let M Θ,↑ Γ be the supplementation of M Θ Γ . By Theorem 6, and, by its very definition , M Θ,↑ Γ is a monotonic model. So this model serves as a witness to the consistency of Θ, and is moreover finite whenever Θ is finite. 8 One may wonder whether it is not sufficient to add the following singleagent version of (M) to BL in order to axiomatize the logic of monotonic models: The answer is negative: although such axioms characterize the closure of the N i (w) under supersets at the level of frames, they do not yield a complete axiomatization. 9 That is, consider a model M ex with two worlds w, w that verify the same propositional variables, and with the (uniform) neighbourhood functions that put N 1 (w) = N 1 (w ) = {{w}, {w }}. Note that the neighbourhood sets of w and w are not closed under supersets. However, all axioms of the base logics and (M 1 ) are valid at both w and w . This is so because no formula of the form 1 ϕ holds true at either w or w , whence the antecedent of any instance of (M 1 ) is false. However, 1,1 ⊥ is true at both w and w , while 1,1 is false at both. Hence, we really need axiom schemata like 1,1 (ϕ ∧ ψ) → 1,1 ϕ in order to obtain all validities obtained by imposing monotony. This lesson applies to most of the other extensions of the base logics that we will study in this paper. That is, one often needs to add counterparts of the standard (monomodal) axioms for all the operators M , not just for the operators i . This is an immediate consequence of the fact that pooling modalities make the languages strictly more expressive, cf. [8]. 8 If one would prove completeness in a more direct way, without relying on the alternative semantic characterization, one immediately takes the supplementation of M Θ Γ and proves the original truth lemma for that model. The general outline of such a proof will be analogous to our original proof for BL [∀] ∞ , but one has to go back and forth a number of times between M Θ Γ and its supplementation. 9 The positive is well-known, cf. [ Proof. It holds that: X ∈ N ∩ M (Λ, f) iff for every i ∈ I(M ), there is some Proof. Analogous to the proof for the previous lemma; however, in this case the X i can be taken to be finite, and hence, since also I(M ) is finite, there is a k ∈ N such that each X i has at most k elements.
f , BL ∞ , BL f }: BL + I is sound and strongly complete w.r.t. the class of intersective models. Moreover, it has the finite model property.
Proof. We first focus on BL Θ be maximal such that Θ ⊆ Γ and Γ is consistent. Let is finite whenever Θ is finite. In order to establish completeness and the finite model property, it suffices to prove the following: This gives us completeness and the finite model property for BL [∀] ∞ + I. For BL [∀] f + I, note first that we are working with a set Θ ⊆ L [∀] f , and thus M Θ ⊆ M f . Since K is a finite union of pooling profiles N ∈ M Θ , it follows that K ∈ M f . So we can apply (I) just as before. For the two logics without the universal modality, we have to adapt the proof in the same way as we did for BL ∞ and BL f (cf. Section 5.6).
f , BL ∞ , BL f }: BL + FI is sound and strongly complete w.r.t. the class of finite intersective models. Moreover, it has the finite model property.
1 ϕ is true. In contrast, (FI) and (I) fail on M ex , since it satisfies 1,1 ⊥ but does not satisfy 1 ⊥.

Regular Models
In the context of classical modal logic, regular modal logics are those obtained by requiring both closure under intersection and closure under supersets of the neighbourhood sets. These logics are standardly axiomatized by a combination of the aforementioned axioms (M) and (C) (or variants thereof), or by the single regularity axiom: Regular modal logics are very close to normal modal logics, in the sense that, when adding necessitation to the regular modal logic, we get a normal modal logic.
As for the case of intersection, we will distinguish between two notions of regularity. In the remainder, let a model M = W, N i i∈I , V be regular iff for all i ∈ I and all w ∈ W , N i (w) is closed under arbitrary intersections and under supersets. ∞ , all Λ ∈ MCS Θ Γ , and all f ∈ F Θ , the following are equivalent: We prove this by an induction on the complexity of ϕ. The base case and the induction step for ¬, ∨, and [∀] are safely left to the reader. For ϕ = M ψ, the equivalence of (ii) and (iii) follows from Proposition 1. The implication from (ii) to (i) follows immediately from the induction hypothesis and the fact that, for every i ∈ I and every world w ∈ W ,

Some Other Frame Conditions
In this subsection, we discuss a number of other frame conditions, showing that completeness and decidability results can be obtained for them by minor amendments to the proofs from preceding (sub)sections. We will gradually move from general to more restricted results. This at once illustrates the power and the limitations of our puzzle piece construction, for the metatheory of pooling modalities.

Definable Frame Conditions
Say a condition (C) on neighbourhood sets N i (w) is BL-definable iff there is some ϕ in the language of BL such that, for all models M = W, N i i∈I , V and all w ∈ W , N i (w) satisfies (C) if and only if M, w |= ϕ. In this case, we say that the formula ϕ defines condition (C). One very well-known example of a frame condition that is BL-definable is unit-containment, that W ∈ N i (w) for all w ∈ W . This frame condition is defined by the following well-known axiom: In the context of reasoning about possibly conflicting information (evidence, beliefs, norms, etc.), another noteworthy frame condition is (individual or joint) consistency of the neighbourhoods. Here the pooling modalities generate various non-equivalent options for defining frame conditions. First, one may require an individual neighbourhood set N i (w) not to generate any n-ary conflicts: there are no X 1 , . . . , X n ∈ N i (w) such that X 1 ∩. . .∩X n = ∅.
This frame condition is defined by the axiom ¬ M ⊥, where M is the pooling profile that puts M (i) = n and M (j) = 0 for all j = i. Alternatively, following Coalition Logic (cf. [8,Section 7.3]), one may require that distinct agents have jointly compatible neighbourhoods: for all i 1 , . . . , i n ∈ G, if X 1 ∈ N i 1 (w), . . ., and X n ∈ N i n (w), then X 1 ∩ . . . ∩ X n = ∅. This frame condition is defined by the formula ¬ M ⊥, where M (i) = 1 for all i ∈ G and M (j) = 0 for all j ∈ G. These variants are both covered by the general notion of M -consistency: and defined by the axiom (P M ): Other examples of definable conditions and formulas defining them are given in the second half of Table 3. Of course, not all combinations of definable frame conditions yield an interesting or even sensible logic. For instance, one cannot both have (N) and (NN), or (P) and (NP) on pains of triviality. Also, some (combinations of) axioms will imply others: e.g. if we have (P M ) for some M , and (N) for all i ∈ I(M ), then we can infer (P i ) for all i ∈ I(M ).
We now state a theorem that concerns any combination of such definable frame conditions. Proof. Soundness is routine, as usual. For strong completeness, we focus on the canonical models where the set Θ is a maximal consistent subset of the entire language of the logic in question-so e.g. L ∞ or L Θ = L f . In this case, every maximal consistent set Λ used in the construction will contain all formulas ϕ 1 , ϕ 2 , . . .. By the truth lemma, we know that at every world in these canonical models, each of ϕ 1 , ϕ 2 , . . . are true. Since these formulas define the respective frame conditions, we know that these canonical models satisfy (C 1 ), (C 2 ), . . ..
Theorem 15 is silent about the finite model property. This is slightly less easy to obtain. Let us first explain why, before we outline some strategies to fix this. By our construction, for infinite index sets I and finite Θ, I Θ will be a proper subset of I. (Recall that I Θ is the set of indexes that occur in some pooling profile, in some member of SF(Θ).) In view of Definition 10, this implies that for all i ∈ I\I Θ , and for all (Λ, f) ∈ W , N i (Λ, f) = ∅. This is so, even if our logic may e.g. have (N i ) as an axiom-simply because that formula is not a member of L Θ , and is hence also ignored in the construction of M Θ Γ . There are various ways one may fix our construction in order to obtain the finite model property for the mentioned extensions. First, in cases where the frame conditions are defined by a finite number of formulas, we may just include all those formulas in the set Θ, thus ensuring that they are "seen" in the construction of I Θ , L Θ . In other words: we can change those neighbourhood functions ad libitum, making sure we have the right frame conditions in the thus obtained model. This simple strategy allows us e.g. to prove the finite model property for the logic obtained by adding all instances of (N), for all i ∈ I, to BL

Reflexivity
Recall the reflection schema or truth schema T, that is familiar from normal modal logics: ϕ → ϕ. Call a neighbourhood function N reflexive iff, for every w ∈ W and for every X ∈ N(w), w ∈ X. A model M = W, N i i∈I , W is reflexive if and only if, for every i ∈ I, N i is reflexive.
Theorem 16. A sound and strongly complete axiomatization for the class of all reflexive (monotonic/intersective/regular) models is obtained by adding all instances of the following axiom schema to BL (BL + M/BL + I/ BL + R): Note that for monotonic, intersective, and regular models, our proofs basically consisted in showing that if we close the neighbourhood sets of the canonical model under supersets, intersections, resp. supersets and intersections, truth is preserved. Since each of those operations (and their combination) also preserve reflexivity of the neighbourhood functions, it can easily be inferred that all the canonical models constructed in Sections 6.1-6.3 are reflexive when the underlying logic contains (T). Importantly, one cannot get a complete axiomatization of reflexivity by just adding the axioms (T i ), i.e. i ϕ → ϕ to the base logic. To see this, note that all axioms M φ → φ are sound with respect to reflexive frames. The following example of a non-reflexive frame shows that these axioms do not logically follow from i ϕ → ϕ. We consider a simple case with I = {1}.
It is not easy to generalize the above theorem to classes of models where some, but not all i ∈ I are such that N i is reflexive. For instance, if we only require reflexivity of N 1 but not of N 2 , then {1,2} ϕ → ϕ is not valid. This implies that the reasoning in the first paragraph of our proof does not go through. The investigation of such "mixed" classes of models is left for future work.

Uniformity
A model M is uniform iff for all i ∈ I, for all w, w ∈ W , N i (w) = N i (w ). Uniform models are e.g. used in the study of evidence-based belief, cf. [1,7].
f }, a sound and strongly complete axiomatization for the class of all uniform (monotonic/intersective/regular) models is obtained by adding all instances of the following axiom schema to BL (BL + M/BL + I/BL + R): Moreover, the resulting logics all have the finite model property.
Proof. We only consider uniformity over the base logic; the argument for the monotonic, intersective, or regular models is analogous. It suffices to inspect our construction of M Θ Γ and check that in the presence of (U), this Note that we make essential use of the universal modality in order to axiomatize uniformity. In the absence of this modality, the frame condition of uniformity does have an impact. For instance, it makes all instances of the two following schemas valid: It is an open problem whether any such validities suffice to obtain a complete axiomatization of uniform models in L ∞ or L f . Table 3 provides an overview of the completeness results mentioned in this paper. As noted, the frame conditions in the second half of the table can be axiomatized for each of the agents independently; those of the first half are required to be valid for all the agents at once. For those first five frame conditions we also established the finite model property.

Overview of the Results
Taken together, these results show that on the one hand, our method for proving completeness is fairly powerful, allowing us to axiomatize a large class of systems. On the other hand our observations already pointed towards some of its limitations. For instance, upon inspection, it seems one cannot easily apply the canonical model in its present form to prove completeness of logics that satisfy the well-known (iterative) axioms of positive and negative introspection 11 : Likewise, the axiomatization of pooling modalities where only some, but not all the neighbourhood functions satisfy one of the conditions from the first half of Table 3 is an open problem. Note for instance that if we require N 1 (w) to be closed under supersets, this does not entail that also N {1,2} (w) satisfies these properties. Taking a more high-level perspective, the situation is essentially not much different from that in relational semantics. There is a standard method for proving completeness-i.e. via canonical models-, and there are more or less broadly applicable ways to adapt this method to specific cases, our puzzle construction being one among them. However, completeness is not to be expected in general, and with each new logic, new technical difficulties may arise.

Summary and Open Issues
The main contribution of this paper was threefold. First, we proved completeness for a class of logics that feature pooling modalities, considering four different formal languages. Second, we showed that a number of those logics also satisfy the finite model property. Third and perhaps most importantly, we introduced a novel method in proving our results, viz. the puzzle piece construction.
As pointed out in the last section, it remains to be seen how broadly applicable this method is, and thus what other frame conditions can be axiomatized using similar tools. Orthogonally, one may investigate alternative languages with (finitary or infinitary) pooling modalities, as noted in Section 3.4.
A final, more fundamental question is whether one can rephrase our method in terms of a two-step procedure, following common practice in modal logic: (i) show the logic to be complete with respect to a class of quasi-models; (ii) develop a general method for turning every quasi-model into a standard model of the logic. A natural notion of quasi-model would be obtained by combining our notion of a g-model (cf. Definition 8) with the following four constraints that reflect the axioms of the base logics: Step (ii) would then consist in showing that every g-model that satisfies axioms (C1)-(C4) is equivalent to a pooled g-model, i.e. one that satisfies the identity in Definition 6.
Acknowledgements. Open Access funding provided by Projekt DEAL. We are indebted to Eric Pacuit and Fengkui Ju for insightful discussions on the completeness proofs. We are also indebted to two anonymous referees for their incisive comments on an earlier version. Frederik Van De Putte's work on this paper was supported by the European Comission through a Marie Sk lodowska-Curie Fellowship (Grant Agreement ID: 795329) and by the Flemish Research Foundation (FWO-Vlaanderen Open Access. This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Appendix: Finitary Pooling
As explained in Section 3.4, our interpretation of ∞ as "arbitrary pointwise intersection" is crucial for the compactness of the logics that were studied in this paper. At the suggestion of a referee we now briefly discuss a noncompact but natural alternative.
Let The following definition should not be surprising in view of our informal reading of the * notation: Definition 12. Let X be a set of sets. Then * X :={X 1 ∩ . . . ∩ X n | X 1 , . . . , X n ∈ X , n ∈ N + }.
Once there, we can simply re-use Definitions 6 and 7 (cf. Section 2.3) to obtain a full-blown semantics for L [∀] * . As before, validity and semantic consequence are defined in the standard way. Let us call the resulting logic BL [∀] * . 12 We first show that this logic is not compact, by an argument that is entirely analogous to the one that illustrates the failure of compactness for PDL, cf. Section 3.4. Consider the set Θ = { 1 * p, ¬ 1 p, ¬ 1,1 p, ¬ 1,1,1 p, . . .}. Note that Θ is inconsistent. Indeed, if a model M verifies 1 * p at a world w, then there must be some n ∈ N such that, for some X 1 , . . . , X n ∈ N 1 (w), X 1 ∩ . . . ∩ X n = p M . However, this means that for some n ∈ N, M, w |= 1 n p. But that means at least one of the other members of Θ must be false.