{'fraction_non_alphanumeric': 0.057907256311225924, 'fraction_numerical': 0.011791186024503159, 'mean_word_length': 4.055993792835898, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Uniform Interpolation in Coalgebraic Modal Logic

A logic has uniform interpolation if its formulas can be projected down to given subsignatures, preserving all logical consequences that do not mention the removed symbols; the weaker property of (Craig) interpolation allows the projected formula -- the interpolant -- to be different for each logical consequence of the original formula. These properties are of importance, e.g., in the modularization of logical theories. We study interpolation in the context of coalgebraic modal logics, i.e. modal logics axiomatized in rank 1, restricting for clarity to the case with finitely many modalities. Examples of such logics include the modal logics K and KD, neighbourhood logic and its monotone variant, finite-monoid-weighted logics, and coalition logic. We introduce a notion of one-step (uniform) interpolation, which refers only to a restricted logic without nesting of modalities, and show that a coalgebraic modal logic has uniform interpolation if it has one-step interpolation. Moreover, we identify preservation of finite surjective weak pullbacks as a sufficient, and in the monotone case necessary, condition for one-step interpolation. We thus prove or reprove uniform interpolation for most of the examples listed above.


Introduction
Given a logic with a notion of formula and signature (and featuring implication for simplicity), the Craig interpolation property requires that every valid implication φ → ψ has an interpolant, i.e. a formula ρ mentioning only the signature symbols that occur in both φ and ψ, such that both φ → ρ and ρ → ψ are valid. The stricter uniform interpolation property additionally demands that ρ can be made to depend only on φ and on the signature of ψ (or, yet stricter, on the shared symbols of φ and ψ), rather than also on ψ itself. Both Craig interpolation and uniform interpolation are useful in the structuring and modularization of logical theories for purposes of specification and automated deduction, e.g. in large ontologies [41,19]. Craig interpolation was originally proved for first-order logic [5] and later extended to many other systems, notably various modal logics including the basic modal logic K [8], as well as intuitionistic logic [9] and the µ-calculus [6]. Uniform interpolation is easily seen to hold for classical propositional logic but in fact fails for first-order predicate logic [16]. Intuitionistic logic [30], the basic modal logic K [10,40], and the modal µ-calculus [17] do have uniform interpolation, while it fails for the modal logics S4 [11] and K4 [2].
In this paper, we study interpolation and uniform interpolation in the context of predicatelifting style coalgebraic modal logic [26,34], equivalently, of modal logics that are axiomatized by rank-1 axioms [33,37]. Coalgebraic modal logic is a generic framework for modal logics whose semantics goes beyond the standard relational world, and e.g. includes probabilistic, game-based, neighbourhood-based, or weighted behaviour. It is parametrized over the choice of a type functor (in our setting, on the category of sets), whose coalgebras play the role of models. The name of the game in coalgebraic logic is to reduce properties of the full modal logic to properties of the one-step logic, which restricts to formulas with exactly one layer of modalities and is interpreted over very simple structures that essentially capture the collection of successors of a single state in a model. Following this paradigm, we identify a notion of one-step interpolation, and then establish that for a coalgebraic modal logic L with finitely many modalities, the following properties imply each other in sequence 1. the modalities are separating, i.e. support a Hennessy-Milner-style expressivity theorem [26,34] (implying that the type functor preserves finite sets), and the type functor preserves surjective finite weak pullbacks (which for finitary functors just means that the functor preserves surjective weak pullbacks); 2. L has one-step interpolation; 3. L has uniform interpolation. Here a pullback is called surjective if it consists of surjective maps. If the modalities of L are separating and monotone, then preservation of finite surjective weak pullbacks is in fact necessary for one-step interpolation.
As applications of this result, we obtain that neighbourhood logic (i.e. classical modal logic [3]), monotone modal (neighbourhood) logic [3], the relational modal logics K and KD, coalition logic [29], and logics of monoid-weighted transition systems for finite refinable commutative monoids (in particular for finite Abelian groups, even though the latter fail to admit monotone modalities) have uniform interpolation; for neighbourhood logic, coalition logic, and monoid-weighted logics, these results appear to be new.
Proofs are often omitted or only sketched; full proofs are in the appendix.

Related Work
Craig interpolation for monotone modal logic was first proved by Hansen and Kupke [14] and later improved to uniform interpolation by Santocanale and Venema [32]. Craig interpolation (but not uniform interpolation) for coalition logic was proved by Schröder and Pattinson using coalgebraic cutfree sequent systems [28]. Hansen, Kupke, and Pacuit [15] have proved Craig interpolation (but not uniform interpolation) for neighbourhood logic, using semantic methods. Uniform interpolation for coalgebraic modal logic with a generalized Moss modality based on a quasifunctorial lax lifting has been shown, for functors preserving finite sets, by Marti in his MSc thesis [20] (and in fact this result has been extended to coalgebraic modal fixpoint logics [21]). Logics based on diagonal-preserving lax liftings (even without assuming quasi-functoriality) satisfy an obvious variant of separation and thus support a generalized Hennessy-Milner theorem, and moreover can be translated into the language of monotone predicate liftings [20]. We leave it as an open problem to determine the relationship between quasifunctoriality and preservation of surjective weak pullbacks in presence of a separating set of monotone predicate liftings. We emphasize that our criteria for interpolation apply also to logics that fail to be separating or admit monotone modalities, hence cannot be phrased in terms of quasifunctorial lax liftings, notable examples of this type being coalition logic, neighbourhood logic, and logics of finite-Abelian-group-weighted transition systems.
In [27], the (coalgebraic) logic of exact covers was introduced; besides a generic Hennessy-Milner theorem and results on completeness and small models, a generic uniform interpolation theorem was claimed which implies that every rank-1 modal logic with finitely many (not necessarily monotone) modalities has uniform interpolation. We show by means of a counterexample that the latter claim is incorrect; our results help delineate in which cases it can be XX:3 salvaged.
This paper is an extended version of a previous conference publication [38].

Preliminaries
We assume basic familiarity with category theory (see [1] for an introduction). Throughout, we work over the category Set of sets and functions as the base category. Given a functor F ∶ Set → Set, an F-coalgebra is a pair X = (X, ξ) consisting of a set X (of states) and a function ξ ∶ X → FX. In the spirit of coalgebraic logic, we use such coalgebras as generic models of modal logics; e.g. Kripke frames can be seen as a coalgebras ξ ∶ X → PX for the powerset functor P, as they assign to each state x ∈ X a set ξ(x) ∈ P(X) of successor states. We will later see non-relational examples. We denote by Q the contravariant powerset functor, which acts on sets by taking powersets and on maps by taking preimage maps

Set Functors and Weak Pullbacks
The pullback of a cospan (f, and π 1 , π 2 are the projections to the components. An important property of set functors in the analysis of coalgebras is weak pullback preservation [31]. A set functor F preserves weak pullbacks, or weakly preserves pullbacks if it maps pullbacks to weak pullbacks (equivalently maps weak pullbacks to weak pullbacks), where a weak pullback is defined categorically like a pullback but requiring only existence, not uniqueness, of mediating morphisms. In an element-wise formulation, X for x ∈ X, y ∈ Y , then there exists p ∈ P (not necessarily unique) such that π 1 (p) = x, π 2 (p) = y. It well-known and easy to see that the identity functor, all constant functors, and the powerset functor preserve weak pullbacks and that the class of weak-pullback preserving functors is closed under products, coproducts, exponentiation with constants, functor composition, and taking finitary parts [31,39]. In particular, all generalized Kripke polynomial functors (built from powerset, finite powerset, constant functors, and identity by taking products, coproducts, and exponentiation with constants) preserve weak pullbacks. Some negative examples are as follows.
1. The Neighbourhood functor or double contravariant powerset functor N = QQ maps a set X to N X = QQX and a function f This functor does not preserve weak pullbacks [31].
2. A variant of the neighbourhood functor is the monotone neighbourhood functor denoted by M. Given an element α ∈ QQX we define Up(α) to be the set and we say that α is upwards closed if α = Up(α). The functor M is then given on sets X by MX = {α ∈ QQ(X) α upwards closed} and on maps Like N , M does not preserve weak pullbacks [14].
3. Another functor that does not preserve weak pullbacks is F 3 2 , defined as a subfunctor of the cubing functor X ↦ X 3 by

Coalgebraic Modal Logic
We briefly recall the syntax and semantics of coalgebraic modal logic. We fix a countable set V of propositional variables. The syntax of a coalgebraic modal logic L(Λ) is then determined by the choice a modal signature Λ consisting of modal operators with assigned arities: the set F(Λ) of (modal) Λ-formulas is defined by the grammar where v ∈ V and ♡ ∈ Λ is an n-ary modality (we deviate slightly from usual practice in coalgebraic modal logic by including propositional variables in the syntax rather then regarding them as nullary modalities; this is in order to facilitate the definition of interpolation). Other Boolean operators (⊺, ∨, →, ↔) are defined in the standard way. We write rk(φ) for the rank of φ, i.e. the maximal nesting depth of modal operators in φ.
As indicated above, the type of systems underlying the semantics of L(Λ) is then determined by the choice of a set functor F whose coalgebras play the role of frames. The interpretation of the modal operators is then defined in terms of predicate liftings for F: ▸ Definition 2.2 (Predicate liftings). An n-ary predicate lifting for F is a natural transformation By the Yoneda lemma, we have the following equivalent description of predicate liftings [34].
▸ Fact 2.3. The n-ary predicate liftings for F are in one-to-one correspondence with subsets of F(2 n ), where 2 = {⊺, }; for n = 1, such a subset U determines a predicate lifting λ by We then complete the semantic parametrization of L(Λ) by assigning to each n-ary modal operator ♡ ∈ Λ an n-ary predicate lifting ♡ for F. For readability, we mostly restrict the technical exposition to unary modalities from now on; the extension to finitary modalities is just a matter of adding indices.
▸ Definition 2.4. An F-model (X, ξ, τ ) consists of an F-coalgebra X = (X, ξ) and a valuation τ ∶ V → P(X) of the propositional variables. We then inductively define a satisfaction relation ⊧ between states of the model (X, ξ, τ ) and formulas of L(Λ) by x ⊩ v iff x ∈ τ (v), standard clauses for Boolean connectives, and As usual, we say that a formula φ is satisfiable if there exists a state x in some model such that x ⊧ φ, and valid if x ⊧ φ for every state x in every F-model. ▸ Example 2.5. 1. The modal logic K is captured coalgebraically by taking the powerset functor P as the type functor, Λ = { }, and

2.
Neighbourhood logic (or classical modal logic [3]) has Λ = {◻}, interpreted over the neighbourhood functor N (Example 2.1.1) by Monotone modal (neighbourhood) logic is captured in the same way, replacing N with the monotone neighbourhood functor M (Example 2.1.2).

XX:5
We fix the data F, Λ, ♡ of the logic L(Λ) from now on.
The One-Step Logic Given any set Z, we denote by Prop(Z) the set of propositional formulas over Z: and write Λ(Z) for the set of formulas ♡(z 1 , ⋯, z n ) where ♡ ∈ Λ has arity n and z 1 , ⋯, z n ∈ Z.
We then define a one-step formula over Z to be an element of Prop(Λ(Prop(Z))). Here, Z will often be a subset of V ; also, Z will sometimes be a subset of some powerset PX, in which case we will understand every element of PX to be interpreted as itself. In general, we interpret both propositional formulas and one-step formulas over Z w.r.t. P(X)-valuations τ ∶ Z → P(X) for some set X: We extend τ to propositional formulas using the Boolean algebra structure of PX, obtaining for φ ∈ Prop(Z) a subset φτ ∈ PX.
We write X ⊧ φτ if φτ = X. We then define the extension ψτ ∈ P(FX) of a one-step formula ψ ∈ Prop(Λ(Prop(Z))) recursively by the evident clauses for Boolean connectives, and When Z ⊆ P(X) and τ is just subset inclusion, the we omit τ from the notation, so ψ ∈ Prop(Λ(PX)) denotes both a one-step formula and its interpretation in P(FX).
We will need the following pieces of terminology and notation: For a map f ∶ X → Y , we write σ f for the substitution mapping A ∈ P(X) to f [A] (e.g. in one-step formulas of type Prop(Λ(P(X)))), and σ f − for the substitution Clearly, all sets of the form The f -invariant sets form a Boolean subalgebra of P(X).
▸ Definition 2.8. We denote by S(A) the set of atoms of a finite Boolean algebra A, i.e. its minimal non-bottom elements, and can A for the canonical isomorphism A → P(S(A)). Given a subalgebra A 0 of A, we have a canonical projection S(A) → S(A 0 ).
The following lemmas are straightforward consequences of naturality of predicate liftings:

Separation and Maximally Satisfiable Sets
The key condition ensuring that L(Λ) satisfies the Hennessy-Milner property, i.e. distinguishes non-bisimilar states, is separation [26,34]: ▸ Definition 2.11 (Separation). We say that Λ is separating if for each set X, the family of maps ( ♡ ♭ X ∶ FX → QQX = N X) ♡∈Λ is jointly injective.
We proceed to define the MSS-functor (for maximally one-step satisfiable sets) from F and Λ.
(A related functor using maximally one-step consistent sets has been used to show that every rank-1 modal logic has a coalgebraic semantics [37].) is one-step satisfiable if the intersection of the interpretations of the formulas in Φ is non-empty, and maximally one-step satisfiable if Φ is maximal among such sets. The MSS-functor M Λ F is given by M Λ F X being the set of maximally one-step satisfiable subsets of Prop(Λ(PX)), and The following lemma allows us to identify F with its MSS-functor whenever Λ is separating.

Surjective Weak Pullbacks
We proceed to introduce the key semantic interpolation criterion, preservation of surjective weak pullbacks. We record explicitly: Of course, every functor that preserves weak pullbacks also preserves surjective weak pullbacks, e.g. the (finite or unrestricted) powerset functor, and more generally all Kripke polynomial functors. Two negative examples are as follows.
▸ Example 3.3. 1. The neighbourhood functor N fails to preserve finite surjective weak pullbacks. To see this, consider the pullback of the following functions as in [31]. Let We proceed to see examples that fail to preserve weak pullbacks but do preserve surjective weak pullbacks.

XX:7
The Monotone Neighbourhood Functor The monotone neighbourhood functor M does not preserve all weak pullbacks (Example 2.1.2). However: ▸ Proposition 3.4. The monotone neighbourhood functor M preserves surjective weak pullbacks.
The proof is facilitated by the following fact: ▸ Lemma and Definition 3.5 (Compatibility). Let be a surjective pullback, and let ] ∈ α 2 and symmetrically.

Monoid-weighted Functors
Given a commutative monoid M (which we write additively), the monoid-weighted functor S M is defined by taking S M X to be the set of finitely supported functions X → M (i.e. functions that vanish almost everywhere), and ▸ Definition 3.6 (Refinability).
. . , a n , b 1 , . . . , b k ∈ M , n, k ≥ 1, then there exists an n × k-matrix over M with row sums a i and column sums b j .
As shown by Gumm and Schröder [13], S M preserves weak kernel pairs iff M is refinable. In fact, refinability already ensures preservation of all weak surjective pullbacks: Given that a) weak pullback preserving finitary functors are known to admit separating sets of monotone predicate liftings [18], and b) the monotone neighbourhood functor itself preserves surjective weak pullbacks but not all weak pullbacks, it is tempting to conjecture that preservation of surjective weak pullbacks is already sufficient for existence of a separating set of monotone predicate liftings. This is not true, however: ▸ Proposition 3.9. Let M be refinable. Then S M has a separating set of monotone predicate liftings iff M is positive.

XX:8 Uniform Interpolation in Monotone Coalgebraic Modal Logic
That is, every commutative monoid that is refinable but not positive gives rise to a monoidweighted functor that preserves surjective weak pullbacks but does not admit a separating set of monotone predicate liftings. One class of such commutative monoids are the non-trivial Abelian groups: they clearly fail to be positive, and are easily seen to be refinable [13].

One-Step Interpolation
We proceed to develop our notion of one-step interpolation, and its relationship to preservation of surjective weak pullbacks. From here on, we assume throughout that the modal signature Λ is finite.
It is in fact not hard to see that under our running assumptions, these two notions coincide, so refer to them just as one-step interpolation: Proof. 'Only if' is trivial. For 'if', the assumption implies that, given data as in Definition 4.1, In any logic supporting the requisite propositional connectives, the set of formulas φ having a uniform interpolant is easily seen to be closed under disjunction, and similarly the set of pairs of formulas φ, ψ such that an interpolant between φ and ψ exists is closed under disjunction in φ and under conjunction in ψ. When establishing (one-step) uniform interpolation for φ, or (one-step) interpolation between φ and ψ, we can therefore assume that φ is a conjunctive clause over modalized formulas and that ψ is a disjunctive clause over modalized formulas.
Our first positive example is neighbourhood logic: ▸ Example 4.4. Neighbourhood logic has one-step interpolation (and hence, by Lemma 4.2, uniform one-step interpolation). To see this, let A 1 , A 2 be interpolable Boolean subalgebras of P(X), let φ be a conjunctive clause over Λ(A 1 ), and let ψ be a disjunctive clause over Λ(A 2 ) such that FX ⊧ φ → ψ (this case suffices by Remark 4.3). We can assume w.l.o.g. that FX ⊧ ¬φ and FX ⊧ ψ. Then FX ⊧ φ → ψ implies that φ contains a conjunct ◻ A and ψ a disjunct ◻ B, with representing either nothing or negation, such that A = B. Then ◻ A interpolates between φ and ψ.
Preservation of surjective weak pullbacks is sufficient for uniform one-step interpolation: Proof. Let A 0 ⊆ A 1 be finite Boolean subalgebras of PX, and let φ ∈ Prop(Λ(A 1 )). We show that Again by Lemma 2.9, we thus have t ∈ F(S(A 1 )) such that t ⊧ (φ ∧ θ)can A1 . Let A be the Boolean subalgebra of PX generated by A 1 ∪ A 2 . Then the diagram The proof relies on invariant sets, and uses the following lemma: ▸ Lemma 4.7. Let f ∶ X → Y be surjective, let A denote the subalgebra of P(X) consisting of the f -invariant sets, and let φ ∈ Prop(Λ(A)). (1). As indicated in Section 2, we can identify F with its MSS functor, i.e. we assume that FX consists of maximally satisfiable subsets Φ ⊆ Prop(Λ(P(X))). In this reading, we are given Φ 1 ∈ FX and Φ 2 ∈ FY such that Ff (Φ 1 ) = Fg(Φ 2 ), which by a straightforward generalization of Lemma 3.5 means that Φ 1 and Φ 2 are compatible, i.e.
and symmetrically. We have to show that there exists Φ ∈ FR such that F π 1 (Φ) = Φ 1 and and correspondingly for Φ 2 . In (2), '⇒' is sufficient, because the logic has negation. That is, we have to show that the set

Uniform Interpolation
We now relate one-step interpolation to interpolation for the full logic. Recall from Section 2.2 that we work in a language with propositional variables. Given a set V 0 ⊆ V of propositional variables, we write F(Λ, V 0 ) for the set of Λ-formulas mentioning only propositional atoms from V 0 , and put For a state x in some model, we put (eliding the model, which will always be clear from the context). Since Λ is assumed to be finite, we have ▸ Lemma 5.1. For finite V 0 , F n (Λ, V 0 ) is finite up to logical equivalence.
We do not currently know whether one-step interpolation in the strong sense of Definition 4.1 is necessary for L(Λ) to have interpolation. However, a weaker version of one-step interpolation is necessary:

▸ Lemma 5.3. If L(Λ) has interpolation, then the one-step logic Prop(Λ(Prop(V ))) has interpolation.
This can be used to disprove interpolation in some examples (contradicting [27] as indicated in the introduction): ▸ Example 5.4. Let N ∨ be the subfunctor of the neighbourhood functor N defined by and interpret the modality ◻ over N ∨ like over N . Take V 1 = {p, q}, V 2 = {r, p}. Then the implication ¬ ◻ (p ∨ q) → ◻(¬p ∨ r) is valid but has no interpolant in Prop({◻}(Prop{p})).
As to sufficiency, we have ▸ Theorem 5.5. If L(Λ) has one-step interpolation then L(Λ) has uniform interpolation.

Proof (Sketch).
Induction on the rank, proving the stronger claim that the rank of the uniform interpolant of φ is at most rk(φ). Let φ ∈ L n (Λ, V 1 ), and let V 0 ⊆ V 1 . We claim that (by Lemma 5.1, effectively a finite formula) is a uniform V 0 -interpolant for φ. The proof reduces straightforwardly to showing that, given ψ ∈ F(Λ, Using a minor variation of standard model constructions in coalgebraic modal logic [33,36,24], we can assume that C, D are finite dags in which all states have a well-defined height (distance from any initial state in a supporting Kripke frame), with x 0 and y 0 being initial states whose depth (length of the longest path starting at x 0 and y 0 , respectively) equals the rank of the relevant formulas, and in which every state x of height n − k in C is uniquely determined (among the states of height n − k) by Th k V1 (x), correspondingly for y ∈ D and Th k V2 (x). Moreover, we can assume that the models are canonical, i.e. every maximally satisfiable subset of F k (Λ, V 1 ) is indeed satisfied at a unique state of height n − k of C, as by Lemma 5.1, there are only finitely many such sets; correspondingly for D and F k (Λ, V 2 ).
We now construct a model E = (Z, γ, τ ) of φ ∧ ψ as follows. We put denoting the first part by Z 0 and the second by Z 1 , and their height-k levels by Z k 0 , Z k 1 , Z k , respectively. Note that (x 0 , y 0 ) ∈ Z 0 . It is straightforward to define the valuation τ on Z. Moreover, we define a coalgebra structure γ ∶ Z → FZ such that γ(z) ∈ FZ k+1 for z ∈ Z k . We put γ(y) = ζ(y) ∈ FZ 1 ⊆ FZ for y ∈ Z 1 (using preservation of inclusions by F), and on states (x, y) ∈ Z 0 of maximal height n by γ(x, y) = ζ(y). On the rest of Z 0 we define γ by a coherence requirement: By construction of Z, we have a well-defined a pseudo-satisfaction relation ⊧ 0 on Z given by For i = 0, 1, 2, let A i be the Boolean subalgebra of PZ k+1 0 of sets of the formρ ∩ Z k+1 0 for ρ ∈ F n−k−1 (Λ, V i ). Then, of course, A 1 ∩ A 2 ⊆ A 0 , and by induction, A 1 , A 2 are interpolable. We define φ 0 ∈ Prop(Λ(A 1 )) and ψ 0 ∈ Prop(Λ(A 2 )) by By applying Lemma 4.2 and forming the uniform A 0 -interpolant i(φ 0 ) of φ 0 , and showing satisfiability of i(φ 0 ) ∧ ψ 0 , one can show that a coherent γ exists. Then, we have by induction on ρ ∈ F n (Λ, V 1 ) ∪ F rk(ψ) (Λ, V 2 ) that z ⊧ E ρ iff z ⊧ 0 ρ for ht(z) = k and rk(ρ) ≤ n − k; so in particular z 0 = (x 0 , y 0 ) ⊧ φ and z 0 ⊧ ψ, as required. ◂ ▸ Remark 5.6. Canonical models in the sense of the above proof sketch in fact bear a strong resemblance to models based on the stages of the final sequence of functors of the type P(V i ) × F, i = 0, 1 (e.g. [25]). This indicates in particular that the proof may eventually be made to bear a relationship, via duality, with Ghilardi's method of graded modal algebras [10].
As indicated in the introduction, our results can be summed up as follows: We note that if Λ is finite and separating, then F preserves finite sets. As indicated above, we suspect but cannot currently prove that 5 implies 2, which would make items 2-5 equivalent. From Theorem 5.7, we obtain uniform interpolation for the following concrete logics: ▸ Example 5.8. 1. Whenever F preserves weak pullbacks and Λ is finite and separating, then L(Λ) has uniform interpolation. This case is covered already in [20], see Remark 5.9.
In particular, we obtain that the modal logics K and KD have uniform interpolation, thus reproving previous results [10,40].

2.
Since the monotone neighbourhood functor preserves surjective weak pullbacks (Section 3), we obtain that monotone modal logic has uniform interpolation, again reproving a previous result [32].

3.
If M is a finite refinable monoid, then the monoid-weighted functor S M (Section 3) preserves surjective weak pullbacks, so that any rank-1 modal logic that is expressive (i.e. separating) for S M has uniform interpolation, such as the logic with modalities [m] for m ∈ M , interpreted by the predicate lifting given by [m] X (A) = {µ ∈ S M ∑ x∈A µ(x) = m}. This holds in particular when M is a finite Abelian group, in which case S M does not have a separating set of monotone predicate liftings so that this case is not covered by existing generic results [20]. If we take M = Z nZ, then the modalities [m] described above are modulo-constraints as found in Presburger modal logic [7]: [m]φ says that the number of successors of the current state (counting multiplicities) equals m modulo n.

Neighbourhood logic fails to preserve surjective weak pullbacks (Example 3.3) but does
have one-step interpolation (Example 4.4), so we obtain that neighbourhood logic has uniform interpolation. 5. One-step interpolation has been proved, in slightly different terms, for coalition logic [28], so that our results improve the known interpolation result for coalition logic [28] to uniform interpolation.
▸ Remark 5.9. We conclude with a more detailed discussion of the relationship between our results and results on the logic of quasi-functorial lax liftings. Glossing over the ramifications of the axiomatics, a diagonal-preserving lax lifting L for a set functor T [22] extends T to act also on relations, satisfying monotonicity w.r.t. inclusion of relations, preservation of relational converse and diagonal relations, and lax preservation of composition (LR ○ LS ⊆ L(R ○ S)). The monotone neighbourhood functor and its polyadic variants have diagonal-preserving lax liftings, and diagonal-preserving lax liftings are easily seen to be inherited along products and subfunctors, so that every functor that has a separating set of monotone predicate liftings has a diagonal-preserving lax lifting. Conversely, every finitary functor that has a diagonal-preserving lax lifting has a separating set of monotone predicate liftings, the so-called Moss liftings [20]. A lax lifting induces a modal logic with a slightly non-standard modality ∇ that generalizes Moss' modality for weak-pullback-preserving functors [23]; for functors that preserve finite sets, the ∇-modality and the predicate-lifting based modalities are however mutually intertranslatable [20], essentially by dint of the fact that both are separating. Summing up, for a functor that preserves finite sets, a diagonal-preserving lax lifting exists iff a separating (finite) set of monotone predicate lifting exists, and the induced logics are essentially the same.
Marti [20] shows that the logic of a diagonal-preserving lax lifting L for T has uniform interpolation if T preserves finite sets and L is quasifunctorial, i.e. satisfies LS○LR = L(S○R)∩ (dom(LR) × rg(LS)) where dom(LR) = {t ∃t. (s, t) ∈ LR} and rg(LS) = {t ∃s. (s, t) ∈ LS}. We recall again that our reduction of uniform interpolation to one-step interpolation holds also in cases where either separation or monotonicity fails, such as coalition logic / alternating-time logic and neighbourhood logic, respectively. Also, we have seen examples (Abelian-groupweighted functors) where there is no monotone separating set of predicate liftings but we nevertheless obtain uniform interpolation from preservation of surjective weak pullbacks.

Conclusions
We have given sufficient criteria for a rank-1 modal logic (with finitely many modalities), i.e. a coalgebraic modal logic, to have uniform interpolation: In the general case, we have established a reduction to the one-step logic; and in the case where the modalities are separating, we have given a simple semantic criterion, namely preservation of (finite) surjective weak pullbacks, which in the monotone case is in fact also necessary for one-step interpolation. We have thus reproved uniform interpolation for the relational modal logics K and KD and for monotone (neighbourhood) modal logic, and newly established uniform interpolation for coalition logic, neighbourhood logic (i.e. classical modal logic), and various logics of finite-monoid-weighted transition systems. All proofs are entirely semantic; we leave a proof-theoretic treatment, in generalization of tentative results based on cut-free sequent systems [28], for future work.
In particular, such a treatment will hopefully lead to practically feasible algorithms for the computation of interpolants. Another open question is how our results relate to definability of bisimulation quantifiers.

A Omitted Proofs
Proof of Lemma 2.9 We note that for A ∈ A, can A (A) = {U ∈ S(A) U ⊆ A}.
We have a map p ∶ X → S(A) that maps x ∈ X to the unique atom U ∈ S(A) such that x ∈ U . We show more generally that for the interpretations of φ and φcan A , φ = (Fp) −1 φcan A . We use induction over φ, with trivial Boolean steps. For the modal case, we note that for A ∈ A, A = p −1 [can A (A)]; the claim then follows by naturality of predicate liftings. ◂

Proof of Lemma 2.10
We note that the canonical projection f ∶ S( We prove the claim by induction over φ, with trivial Boolean steps. For the modal case, we note that for A ∈ A 0 , can A1 (A) = f −1 [can A0 (A)]. The claim follows by naturality of predicate liftings. ◂

Proof of Lemma 2.13
Define the natural transformation η ∶ F → M Λ F by η X (t) = {φ ∈ Prop(Λ(P(X))) t ⊧ φ}, i.e., t ∈ FX is mapped to its theory in M Λ F (X). Given a set X, η X is surjective by satisfiability of sets in M Λ F (X), and injective since Λ is separating and each t ∈ FX is uniquely determined by the set {φ ∈ Λ(P(X)) t ⊧ φ}. Hence F and M Λ F are naturally isomorphic. ◂

Proof of Lemma 3.2
We prove only the claim for surjective pullbacks. So let P X Y Z π2 π1 f g be a surjective pullback, and let s ∈ FX, t ∈ FY such that Ff (s) = Fg(t). We have to show that there exists u ∈ FZ such that Fπ 1 (u) = s and Fπ 2 (iu) = t. Since F is finitary (and we assume that F preserves inclusions), there exist finite subsets X 0 ⊆ X, Y 0 ⊆ Y such that s ∈ FX 0 ⊆ FX, t ∈ FY 0 ⊆ FY . Since f and g are surjective, we can moreover ensure, by suitably where we abuse f, g, π 1 , π 2 to denote their restrictions) is a finite surjective pullback, hence weakly preserved by F; it follows that u ∈ FP 0 ⊆ FP exists as required. be a surjective pullback, and let α 1 ∈ MX, α 2 ∈ MY such that Mf (α 1 ) = Mg(α 2 ). We put and claim that Mπ 1 (β) = α 1 and Mπ 2 (β) = α 2 . By symmetry, it suffices to prove Mπ 1 (β) = α 1 . Here, '⊇' is clear by construction of β; we prove '⊆'. We distinguish the following cases for U ∈ Mπ 1 (β): ] by the pullback property. The other direction is symmetric.

Proof of Lemma 3.7
It only remains to show 'if'; by Lemma 3.2, it suffices to show preservation of finite weak surjective pullbacks. It is easy to see that refinability is exactly the condition that ensures that S M maps non-empty binary products to weak pullbacks. Now S M is generally additive [4], i.e. maps finite coproducts to products. Since every finite set is a coproduct of singletons, every finite surjective pullback is a sum of non-empty finite products. Thus, S M maps finite surjective pullbacks to products of weak pullbacks, which are again weak pullbacks. ◂

Proof of Lemma 3.9
'If': If M is refinable and positive, then S M preserves all weak pullbacks [13] and hence has a separating set of monotone predicate liftings [18].
We can understand the elements of S M (X) as formal linear combinations over X with coefficients from M . Recall that a monotone n-ary predicate lifting λ for S M is equivalently determined by a subset of S M (2 n ) that is closed under the relation ≲ given by taking t ≲ s if t, s can be written as linear combinations . . , n in the pointwise ordering on 2 n [34]. Now let X be a set with at least two distinct elements x ≠ y. We show that ax, ay ∈ S M X are indistinguishable under n-ary monotone predicate liftings by showing that for any f ∶ X → 2 n , we have T f (ax) ≲ T f (ay) ≲ T f (ax). Namely: Writing n ∈ 2 n for the n-tuple ( , . . . , ), we have T f (ax) = af (x) = af (x) + a n + b n ≲ af (x) + af (y) + bf (x) = af (y) = T f (ay), and analogously T f (ay) ≲ T f (ax). ◂

Proof of Lemma 4.2
'Only if' is trivial; we prove 'if'. So let φ ∈ Prop(Λ(Prop(V 1 ))), and let V 0 ⊆ V 1 . We put effectively a finite formula because Λ is finite and Prop preserves finite sets up to logical equivalence, and claim that

Proof of Lemma 4.6
Let P X Y Z π1 π2 f g be a finite surjective pullback. As indicated in Section 2, we can identify F with its MSS functor, i.e. we assume that FX consists of maximally satisfiable subsets Φ ⊆ Prop(Λ(P(X))).

Proof of Lemma 4.7
Induction over φ, with trivial Boolean steps. For the modal step, i.e. by the above for atoms of the form ♡f −1 [B], note that Ff is also surjective, and for t ∈ FX, where the last equality is by surjectivity. ◂

Proof of Lemma 5.3
Let φ ∈ Prop(Λ(Prop(V 1 ))) and ψ ∈ Prop(Λ(Prop(V 2 ))) such that ⊧ φ → ψ. Since L(Λ) has propositional variables, we can see φ and ψ as formulas in F(Λ), so φ and ψ have an We proceed to show that we can modify θ to obtain an interpolant in Prop(Λ(Prop(V 1 ∩ V 2 ))). We begin by eliminating occurrences of propositional variables at the top level of θ, i.e. outside the scope of modal operators. Let θ ′ arise from θ by replacing all such occurrences with ⊺. Then, of course, θ ′ ∈ F(Λ, V 1 ∩ V 2 ). Moreover, we still have ⊧ φ → θ ′ : Let x be a state in a coalgebraic model C such that C, x ⊧ φ; we have to show C, x ⊧ θ ′ . Since coalgebraic modal logic has the tree model property [35], we can assume that C is a tree. Under this assumption, we can change the valuation of all propositional variables at x to ⊺ without affecting satisfaction of φ, obtaining C ′ such that C ′ , x ⊧ φ. Then C ′ , x ⊧ θ, which by the choice of valuation at x implies C ′ , x ⊧ θ ′ . Since θ ′ does not contain propositional variables at the top level and C is tree-shaped, it follows that C, x ⊧ θ ′ . The proof that ⊧ θ ′ → ψ is entirely analogous.
Informally speaking, V 0 and σ represent the parts of θ that stick out of rank 1. Now let y be a state in some coalgebraic model D, and define σ ′ ∶ V 0 → 2 by Then θ ′ ∶= θ 0 σ ′ is rank 1 and mentions only variables in V 1 ∩ V 2 ; we claim that it interpolates between φ and ψ. Again, we prove only that ⊧ φ → θ ′ . So let x be a state in a coalgebraic model C such that C, x ⊧ φ; we have to show C, x ⊧ θ ′ . As above, we can assume that C is tree-shaped. We now construct a coalgebraic model C ′ by replacing every successor state of x and the associated subtree (according to the supporting Kripke frame of C) with a copy of y and D, keeping however the original valuation for the propositional variables. Then C and C ′ satisfy the same rank-1 formulas, (4) in particular C ′ , x ⊧ φ and therefore C ′ , x ⊧ θ. By the definition of σ ′ it follows that C ′ , x ⊧ θ ′ , and since θ ′ is rank 1, this implies C, x ⊧ θ ′ , again by (4). ◂

Details for Example 5.4
We use liberally that the rule a ∨ b ◻ a ∨ ◻b is one-step cutfree complete for the logic of N ∨ [36], i.e. every valid clause over {◻}(Prop(V )) must contain ◻φ and ◻ψ such that φ ∨ ψ is valid. Assume that an interpolant in Prop({◻}(Prop({p})) exists. Then by the same argument as in Lemma 4.2, the formula χ obtained as the essentially finite conjunction of all clauses ρ over {◻}(Prop({p})) such that ◻(p ∨ q) ∨ ρ is (one-step) valid is also an interpolant. In the definition of χ, we can clearly omit clauses ρ that are themselves valid. Then the only way that ◻(p ∨ q) ∨ ρ is valid is that ρ contains (and then w.l.o.g. equals) a literal ◻(θ) with θ ∈ Prop({p}) such that (p ∨ q) ∨ θ is valid. Up to logical equivalence, θ is one of ⊺, , p, ¬p; validity of (p ∨ q) ∨ θ leaves only θ = ¬p. But ◻(¬p) → ◻(¬p ∨ r) is not valid. ◂
Using a minor variation of standard model constructions in coalgebraic modal logic [33,36,24], we can assume that both these models are finite dags in which all states have a well-defined height (distance from any initial state in a smallest supporting Kripke frame, which exists because the models are finite), with x 0 and y 0 being initial states whose depth (length of the longest path starting at x 0 and y 0 , respectively) equals the rank of the relevant formulas, and in which every state x of height n − k in C is uniquely determined (among the states of height n − k) by Th k V1 (x), correspondingly for y ∈ D and Th k V2 (x). Moreover, we can assume that the models are canonical, i.e. every maximally satisfiable subset of F k (Λ, V 1 ) is indeed satisfied at a unique state of height n − k of C, as by Lemma 5.1, there are only finitely many such sets; correspondingly for D and F k (Λ, V 2 ).
By construction, states z ∈ Z have a well-defined height ht(z). We define a V 1 ∪ V 2valuation θ on Z by which is well-defined by construction of Z 0 . Moreover, we define a coalgebra structure γ ∶ Z → FZ such that γ(z) ∈ FZ k+1 for z ∈ Z k . We put γ(y) = ζ(y) ∈ FZ 1 ⊆ FZ for y ∈ Z 1 (using preservation of inclusions by F), and on states (x, y) ∈ Z 0 of maximal height n by γ(x, y) = ζ(y).
On the rest of Z 0 we define γ by a coherence requirement: we define a pseudo-satisfaction relation ⊧ 0 between states in Z of height k and F(Λ, V 1 )-formulas of rank at most n − k, as well as states in Z of height k and F(Λ, V 2 )-formulas of rank at most rk(ψ) − k. by This is well-defined by construction of Z 0 . For a formula ρ ∈ F n (Λ, V 1 ) ∪ F rk(ψ) (Λ, V 2 ), we then have the pseudo-extensionρ ⊆ Z defined bŷ ρ = {z ∈ Z rk(ρ) ≤ n − ht(z), z ⊧ 0 ρ}.