{'fraction_non_alphanumeric': 0.06303586073212555, 'fraction_numerical': 0.00852406868957976, 'mean_word_length': 3.7074754328497894, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 58, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Canonicity results for mu-calculi: an algorithmic approach

We investigate the canonicity of inequalities of the intuitionistic mu-calculus. The notion of canonicity in the presence of fixed point operators is not entirely straightforward. In the algebraic setting of canonical extensions we examine both the usual notion of canonicity and what we will call tame canonicity. This latter concept has previously been investigated for the classical mu-calculus by Bezhanishvili and Hodkinson. Our approach is in the spirit of Sahlqvist theory. That is, we identify syntactically-defined classes of inequalities, namely the restricted inductive and tame inductive inequalities, which are, respectively, canonical or tame canonical. Our approach is to use an algorithm which processes inequalities with the aim of eliminating propositional variables. The algorithm we introduce is closely related to the algorithms ALBA and mu-ALBA studied by Conradie, Palmigiano, et al. It is based on a calculus of rewrite rules, the soundness of which rests upon the way in which algebras embed into their canonical extensions and the order-theoretic properties of the latter. We show that the algorithm succeeds on every restricted inductive inequality by means of a so-called proper run, and that this is sufficient to guarantee their canonicity. Likewise, we are able to show that the algorithm succeeds on every tame inductive inequality by means of a so-called tame run. In turn, this guarantees their tame canonicity.


Introduction
The modal mu-calculus was defined in 1983 by Kozen [11] and is obtained by adding the least and greatest fixed point operators to the basic modal logic. An overview of the modal mu-calculus can be found in the chapter by Bradfield and Stirling [4]. Canonical models and completeness results for the finitary and infinitary logics defined by Kozen were obtained by Ambler et al. [1]. In our algebraic canonicity proofs we will build on the definitions of modal mu-algebras from [1]. The correspondence and completeness of logics with fixed point operators has been the subject of recent studies by Bezhanishvili and Hodkinson [3] and Conradie et al. [5]. Both of these works aim to develop a Sahlqvist-like theory for their respective fixed point settings.
Sahlqvist theory, first developed in 1975 [12], is one of the most important and powerful ideas in the study of modal and related logics. The theory consists of two parts: canonicity and correspondence. The Sahlqvist formulas are a recursively defined class of modal formulas with a particular syntactic shape. Any modal logic axiomatized by Sahlqvist formulas is strongly complete (via canonicity) with respect to its class of Kripke frames, and the latter is moreover guaranteed to be an elementary class. This last fact, that the class of frames can be characterized by first-order conditions, is the correspondence aspect of Sahlqvist theory. This Sahlqviststyle approach of describing a class of formulas of a certain syntactic shape for which correspondence and completeness results can be proved, has been extensively developed by van Benthem [13,14] and others. The so-called Sahlqvist-van Benthem algorithm is used to find the first-order condition that corresponds to a given Sahlqvist formula. Various generalizations of the Sahlqvist class exist, including the inductive formulas, introduced by Goranko and Vakarelov [10].
The work in [3] looks at both correspondence and a certain type of canonicity for the classical mu-calculus. They define Sahlqvist fixed point formulas: a syntactic class which allows for limited use of fixed point operators. A modified version of canonicity is proved for these Sahlqvist fixed point formulas. (We also note the related algebraic work on preservation of Sahlqvist fixed point equations under MacNeille completions by Bezhanishvili and Hodkinson [2].) In contrast to the work on Sahlqvist fixed point formulas in [3], [5] examines correspondence only, and, using an algorithmic approach, obtains results for a broader class of formulas in the setting of bi-intuitionistic mu-calculus. The correspondence results are achieved by examining validity on the complex algebras dual to Kripke frames. The algorithmic approach of [5] builds on work by Conradie and Palmigiano [6] on canonicity and correspondence for distributive modal logic.
In this paper we will make use of purely algebraic and order-theoretic techniques. This approach has proved fruitful in obtaining completeness results for many non-classical logics.
We prove two different canonicity results for two classes of intuitionistic mu-formulas. We show that the members of a certain class of intuitionistic mu-formulas are canonical, in the sense of [3]; that is, they are preserved under certain modified canonical extensions. We refer to this modified form of canonicity (described in detail in Section 3) as tame canonicity. We also define a second class of formulas for which the usual notion of canonicity holds. However, in this second case we do not get completeness of the logics defined by the canonical mu-formulas. This lack of completeness is explained in more detail in Section 3.
Our methods use a variation of the algorithm ALBA (Ackermann Lemma Based Algorithm) developed in [6]. The key step in our algorithm µ * -ALBA is the elimination of propositional variables via an Ackermannstyle rule. We define tame and proper runs of our algorithm and show that all mu-inequalities that can be successfully processed by these runs are, respectively, tame canonical or canonical.
In Section 2 we define the languages in which we operate and establish the algebraic setting for the interpretation of these languages. Section 3 summarizes our canonicity results and outlines the method for achieving these results. The syntactic classes of inequalities for which we obtain our canonicity results are defined in Section 4; the examples in this section will assist the reader in getting to grips with the rather technical syntactic definitions. The algorithm µ * -ALBA is presented in Section 5. The soundness of most of the rules of µ * -ALBA follows easily from properties of the interpreting algebras. However, the proofs of the fixed point approximation rules and the Ackermann rules require more intricate algebraic manipulations. These proofs are given in Section 7 and Section 8 respectively. Some technical lemmas required for the proofs in Section 8 are given in Appendix 11. Section 6 describes a syntactically defined class of formulas, the term functions of which satisfy the order-theoretic conditions required by the fixed point approximation rules. Section 9 demonstrates the tame canonicity of mu-inequalities on which a tame run of our algorithm succeeds and also shows the canonicity of mu-inequalities on which a proper run of µ * -ALBA succeeds. In Section 10 we prove that the members of the two different syntactic classes defined in Section 4 are, respectively, tame canonical and canonical. To end the paper, in Section 11 we present two examples of the algorithm at work.

Language and interpretation
In this section we collect the essential details of the syntax and semantics we will be using. We have opted to work in an intuitionistic rather than classical setting for two reasons: firstly, it allows us to carefully disentangle the order theoretic properties of connectives which make our approach tick, in a way that would seem unnecessary and pedantic if, e.g., classical negation was available; secondly, this added generality comes at very little extra cost. Since the focus of this paper is canonicity, we will work almost exclusively with algebraic semantics, which in this case takes the form of bi-Heyting algebras with additional modal operators. The relational semantics can be given, as usual, by intuitionistic Kripke frames with additional relations for interpreting the modalities, see e.g., [15] and [7]. such that (A, ∧, ∨, →, −, , ⊥) is a bi-Heyting algebra and and preserve finite meets and joins, respectively. We observe that → and − satisfy the inequalities The completely join-irreducible elements and completely meet-irreducible elements of a complete lattice will play a very important role in our algorithmic approach.
Definition 2.1. Let C be a complete lattice. Then (i) j ∈ C is completely join-irreducible if for any X ⊆ C, if j = X then j = x for some x ∈ X; (ii) m ∈ C is completely meet-irreducible if for any Y ⊆ C, if m = Y then m = y for some y ∈ Y; (iii) j ∈ C is completely join-prime if for any X ⊆ C, if j ≤ X then j ≤ x for some x ∈ X; (iv) m ∈ C is completely meet-prime if for any Y ⊆ C, if m ≥ Y, then m ≥ y for some y ∈ Y.
A perfect lattice is a complete lattice in which the completely join-irreducible elements are join-dense (i.e., every element is a join of join-irreducibles), and the completely meet-irreducible elements are meet-dense (i.e., every element is a meet of meet-irreducibles). A perfect distributive lattice is a perfect lattice that is also completely distributive, i.e., arbitrary meets distribute over arbitrary joins and vice versa. In this case the completely join-irreducible (completely meet-irreducible) elements coincide with the completely join-prime (completely meet-prime) elements. (In general, a completely join-prime (completely meet-prime) element of a complete lattice is completely join-irreducible (completely meet-irreducible) but not vice versa.) A bi-Heyting algebra is perfect if its lattice reduct is a perfect distributive lattice. If follows that in a perfect bi-Heyting algebra A, for any S ⊆ A, we have that S → a = s∈S (s → a), a → S = s∈S (a → s), S − a = s∈S (s − a) and a − S = s∈S (a − s). A perfect modal bi-Heyting algebra is a modal bi-Heyting algebra the bi-Heyting reduct of which is a perfect bi-Heyting algebra, and moreover such that and preserve arbitrary meets and joins, respectively. The latter property allows us to add to any perfect modal bi-Heyting algebra the adjoint operations and uniquely defined by the inequalities: The canonical extension. Let A be a bounded distributive lattice with additional operations, in particular, A could be a modal bi-Heyting algebra. The canonical extension of A, defined by Gehrke and Harding [8] and denoted A δ , is a perfect bounded distributive lattice which, up to an isomorphism fixing A, is the unique extension in which A is dense and compact: density every element of A δ can be written both as a join of meets and as a meet of joins of elements from A.
compactness for all S , T ⊆ A, if S ≤ T then S ≤ T for some finite S ⊆ S and T ⊆ T .
Additional operations on A can be extended to A δ in a standard way. For more details the reader is referred to the appendix.
Languages and their interpretations. Let PROP, FVAR, PHVAR, NOM and CNOM be disjoint sets of propositional variables, fixed point variables, placeholder variables, nominals and co-nominals, respectively. Formulas in the basic language L of modal bi-Heyting algebras are defined recursively by where p ∈ PROP and X ∈ FVAR. We identify the language with its set of formulas/terms. Formulas in the extended language L + are defined by where p ∈ PROP, X ∈ FVAR, j ∈ NOM and m ∈ CNOM. Placeholder variables from PHVAR, denoted x, y, z, will be used as generic variables which can take on the roles of propositional and fixed point variables. They will also be used to enhance the clarity of the exposition when dealing with substitution instances of formulas.
On perfect modal bi-Heyting algebras and are interpreted as the right and left adjoints of and , respectively. Elements of NOM (CNOM) are interpreted as elements of J ∞ (A δ ) (M ∞ (A δ )). We now describe two extensions of L obtained by adding fixed point operators. The distinction between the two extensions will become clear when we define their interpretations on distributive lattices with operators.
We define L 1 to be the set of terms which extends L by allowing terms µx.t(x) and νx.t(x) where t ∈ L 1 , x ∈ FVAR and t(x) is positive in x. The second extension is denoted L 2 and extends L by allowing construction of the terms µ 2 x.t(x) and ν 2 x.t(x) where t ∈ L 2 , x ∈ FVAR and t(x) is positive in x.
Suppose that a ∈ A is a pre-fixed point of t, that is, t(a, a 1 , . . . , a n−1 ) ≤ a. We will prove by transfinite induction that t α (⊥, a 1 , . . . , a n−1 ) ≤ a for all ordinals α.
The importance of Lemma 2.2 is that if we are interpreting formulas/terms on a mu-algebra of the second kind the interpretations of terms with the two different fixed point binders will agree. That is, µX.ϕ(X) = µ 2 X.ϕ(X) and νX.ψ(X) = ν 2 X.ψ(X).
An L + formula is pure if it contains no ordinary (propositional) variables but only, possibly, nominals and co-nominals. A formula of L 1 (respectively L + 1 , L 2 , L + 2 , L * , L + * ) is an L 1 -sentence if it contains no free fixed point variables (and similarly for L + 1 , L 2 , L + 2 , L * , L + * ). The reason for using µ * and ν * in formulas/terms is so that the interpretation does not change when moving between A and A δ .
Quasi-inequalities, assignments, validity. An assignment on A sends propositional variables to elements of A and is extended to formulas of L 1 , L 2 and L * in the usual way, where these are defined. An assignment on A δ sends propositional variables to elements of A δ , nominals into J ∞ (A δ ) and co-nominals into M ∞ (A δ ) and extends to all formulas of L + * , L + 1 and L + 2 . An admissible assignment on A δ is an assignment which takes all propositional variables to elements of A. An L + -inequality α ≤ β is admissibly valid on A δ , denoted A δ | = A α ≤ β, if it holds under all admissible assignments.
A quasi-inequality of L 1 (resp., L + 1 , L 2 , L + 2 , L * , L + * ) is an expression of the form A quasi-inequality is (admissibly) valid in an algebra if it is satisfied by every (admissible) assignment.
Signed generation trees To any formula/term in L + 1 and L + * we assign two signed generation trees. That is, for ϕ ∈ L we consider two trees +ϕ and −ϕ. The generation tree is constructed as usual, beginning at the root with the main connective and then branching out into n-nodes at each n-ary connective. Each leaf is either a propositional variable, a fixed point variable, or a constant. Each node is signed as follows: • the root node of +ϕ is signed + and the root node of −ϕ is signed −; • if a node is ∨, ∧, , , , or assign the same sign to its successor nodes; • if a node is →, assign the opposite sign to its left successor, and the same sign to its right successor; • if a node is −, assign the same sign to its left successor, and the opposite sign to its right successor; • if a node is µx.ϕ(x), µ * x.ϕ(x), νx.ϕ(x) or ν * x.ϕ(x) (with every free occurrence of x in the positive generation tree of ϕ labelled positively) then assign the same sign to the successor node.
A node in a signed generation tree is said to be positive if it is signed "+" and negative if it is signed "−". Examples of signed generation trees can be found in Figure 2 and Figure 3.
Order types We will often be using formulas in n variables and hence use x to denote n-tuple of variables. An order-type over n ∈ N is an n-tuple ∈ {1, ∂} n . Given an order-type , its opposite order type, denoted ∂ , is given by ∂ i = 1 ⇔ i = ∂ for 1 ≤ i ≤ n. We will also use the symbol τ to denote an order type over n. When we define the Approximation Rules in Section 5 it will be useful to write 1 and ∂ for and ⊥ respectively. Similarly we will write ⊥ 1 and ⊥ ∂ for ⊥ and respectively.
For both order types and tuples of variables, we will use the symbol ⊕ to denote concatenation.
Join-and meet-irreducible elements in products Let A be a perfect lattice and τ and order type over n. It is not difficult to prove that in the product A n every join-irreducible element j is an n-tuple such that ( j) k ∈ J ∞ (A) for some 1 ≤ k ≤ n and ( j) i = ⊥ for all i k. Dually, every completely meet-irreducible element in the product A n is an n-tuple m such that (m) k ∈ M ∞ (A) for some 1 ≤ k ≤ n and (m) i = for all i k. This characterization of J ∞ (A n ) and M ∞ (A n ) can be generalized to the case of J ∞ (A τ ) and M ∞ (A τ ): every join-irreducible element j ∈ J ∞ (A τ ) is an n-tuple such that, for some 1 ≤ k ≤ n, Let A be a perfect lattice and let τ be an order type over n. The notation j τ i will denote a nominal if τ i = 1 and a co-nominal if τ i = ∂. Dually, n τ i denotes a co-nominal if τ i = 1 and a nominal if τ i = ∂.
Accordingly, we will use the notation j τ i to denote an n-tuple in which the i-th component is j τ i and, for all k i, the k-th component is ⊥ τ k . Accordingly, such tuples range over the subset of J ∞ (A τ ) in which the i-th

Canonicity results
In this section we highlight and explain the main results of this paper and describe our methodology in broad strokes. Our approach goes via a "U-shaped argument" (see Figure 1), a generic version of which we now outline.
Going down the left-hand arm of the diagram, the first bi-implication is given by the fact that validity in A coincides with admissible validity in A δ , modulo certain provisions regarding the fixed point binders. In the richer setting of A δ we can now interpret the extended language L + * where equivalences involving the adjoints and as well as nominals and co-nominals are available. The aim is now to transform the inequality into a set of pure (quasi-)inequalities, denoted pure(α ≤ β) in Figure 1. This is done by means of an algorithm, µ * -ALBA, based on a calculus of rewrite rules which are presented in Section 5. The fact that admissible and ordinary validity coincide for pure inequalities is the linchpin for the transition from validity in A (simulated as admissible validity in A δ ) to validity in A δ . This justifies the bi-implication forming the base of the "U".
We progress up the right-hand arm of the 'U' by reversing the rewrite rules applied when coming down the left-hand side. The equivalences are justified by the fact that these rules preserve validity on perfect algebras. (The last statement needs to be qualified somewhat to accommodate fixed point binders, as will be specified in Section 9.) We observe that the equivalences on the right-hand arm of Figure 1 justifies the first-order frame definability of α ≤ β, which is the topic of [5]. Indeed, the fact that α ≤ β is equivalent on perfect algebras (or, dually, relational structures) to a set of pure quasi-inequalities guarantees first-order definability since the absence of propositional variables in pure(α ≤ β) means that all quantification ranges over first-order definable subsets of the dual relational structure of A δ .
As we now explain, the notion of canonicity of a formula in the presence of fixed points admits some variation. If ϕ is a formula without fixed point binders, then the term function ϕ A δ extends the term function ϕ A , i.e., they agree on arguments from A. This is something which is usually of crucial importance in proving that an equation is canonical. As soon as we add fixed point binders this extension property fails. Indeed, (ϕ(X)) A δ can have more pre-fixed points in A δ than (ϕ(X)) A has in A, and so (µX.ϕ(X)) A δ would generally be smaller than (µX.ϕ(X)) A . This phenomenon creates significant obstacles for standard canonicity arguments.
One possible remedy to regain the extension property, is to insist that only pre-fixed points from the smaller algebra A be considered in calculating (µX.ϕ(X)) A δ , i.e., rather calculating (µ * X.ϕ(X)) A δ . This leads to the first notion of canonicity that we will examine. This is the notion described by Bezhanishvili and Hodkinson [3], and used by them to obtain completeness results for some axiomatic extensions of the basic (classical) mu-calculus with respect to certain types of general frames. We will refer to this as tame canonicity. In tame canonicity, all fixed point binders µ and ν in inequalities are replaced by the binders µ * and ν * and interpreted as such in the canonical extension. Proving that an L 1 -inequality is tame canonical is proving that A | = ϕ ≤ ψ if and only if A δ | = ϕ * ≤ ψ * where A is mu-algebra of the first kind. (Further explanation regarding the use of µ * and ν * is given at the end of Section 7.) Using our algorithmic approach we are able to prove tame canonicity for what we call tame inductive muinequalities. This is a smaller class than that for which correspondence results were shown in [5] but extends the Sahlqvist mu-inequalities of [3] when projected to the classical case.
The second type of canonicity which we investigate is essentially the usual notion of canonicity and thus we simply refer to this as canonicity. That is, for A a mu-algebra of the second kind, if A | = ϕ ≤ ψ, then A δ | = ϕ ≤ ψ. (Note the additional assumption that A is of the second kind.) Our method of proof is as follows: we first show that A | = ϕ ≤ ψ if and only if A δ | = A ϕ * ≤ ψ * and then that this implies A δ | = ϕ ≤ ψ. However, we are not able to show the converse, i.e., that We will call the syntactically specified class of formulas for which we can prove canonicity the restricted inductive mu-inequalities. This class is again a restriction of the class for which correspondence results were shown in [5], but it is a generalization of the inductive inequalities from [6].
From a logical perspective, one of the main motivations for proving canonicity results is to obtain relational completeness results for axiomatic extension of logics -if we have a general algebraic completeness result any non-theorem is refuted on an algebra of the logic and, if the axioms are preserved under canonical extensions, we can transfer this refutation to a relational structure obtained as the dual of the perfect algebra which is the canonical extension. Unfortunately this does not work in the setting of the mu-calculus, since generally it will not be true that Hence refutations will not necessarily be preserved when taking canonical extensions.
The proof of the tame canonicity of the tame inductive mu-inequalities and the proof of the canonicity of the restricted inductive mu-inequalities is concluded in Section 10. The proof is a two-step process, beginning in Section 9. There it is shown that whenever a tame run of µ * -ALBA succeeds on a mu-inequality ϕ ≤ ψ, we have that ϕ ≤ ψ is tame canonical. It is also shown that whenever a proper run succeeds on a mu-inequality α ≤ β, then α ≤ β will be canonical. Section 10 then completes the overall result by showing that for every tame inductive mu-inequality (respectively, a restricted inductive mu-inequality), there exists a tame (respectively, proper) run of µ * -ALBA which succeeds on that inequality.

Syntactic classes
In this section we introduce two new syntactically defined classes of mu-inequalities. Both will be subclasses of the recursive mu-inequalities introduced in [5], and therefore the members of both classes will all have first-order frame correspondents.
The reason we concern ourselves with inequalities is because certain fragments (for example, distributive modal logic [9]) do not have an implication in the language. In the absence of an implication, modal sequents of the form ϕ ⇒ ψ are used to capture the logic. When using the algebraic semantics, the interpretation of inequality ϕ ≤ ψ is used as the interpretation of the sequent ϕ ⇒ ψ.
For any L 1 -sentence ϕ(p 1 , . . . p n ), any order-type over n, and any 1 ≤ i ≤ n, an -critical node in a signed generation tree of ϕ is a (leaf) node +p i with i = 1, or −p i with i = ∂. An -critical branch in the tree is a branch terminating in an -critical node. The intuition, which will be built upon later, is that variable occurrences corresponding to -critical nodes are to be solved for, according to .
In the signed generation tree of a L 1 -sentence ϕ(p 1 , . . . p n ) a live branch is a branch ending in a (signed) propositional variable. In particular, all critical branches are live. It follows that a branch is not live iff it ends in a propositional constant ( or ⊥) or in a fixed point variable.
For every L 1 -sentence ϕ(p 1 , . . . p n ), and every order-type , we say that +ϕ (resp. −ϕ) agrees with , and write (+ϕ) (resp. (−ϕ)), if every leaf node in the signed generation tree of +ϕ (resp. −ϕ) which is labelled with a propositional variable is -critical. In other words, (+ϕ) (resp. (−ϕ)) means that all propositional variable occurrences corresponding to leaves of +ϕ (resp. −ϕ) are to be solved for according to . We will also make use of the sub-tree relation γ ≺ ϕ, which extends to signed generation trees, and we will write (γ) ≺ * ϕ to indicate that γ, regarded as a sub-(signed generation) tree of * ϕ, agrees with .

Outer Skeleton (P 3 )
Inner Skeleton (P 2 ) PIA (P 1 ) ∆-adjoints Binders Binders While reading the following definition, the reader might find it useful to refer to Example 4.3 for an illustration of the concepts being introduced.  A branch in a signed generation tree * ϕ, for * ∈ {+, −}, ending in a propositional variable is an -good branch if, apart from the leaf, it is the concatenation of three paths P 1 , P 2 , and P 3 , each of which may possibly be of length 0, such that P 1 is a path from the leaf consisting only of PIA-nodes, P 2 consists only of inner skeletonnodes, and P 3 consists only of outer skeleton-nodes and, moreover, it satisfies conditions (GB1), (GB2) and (GB3), below.
(GB1) The formula corresponding to the uppermost node on P 1 is a mu-sentence.
(GB3) For every SLR-node in P 2 of the form γ β or β γ, where β is the side where the branch lies, γ is a mu-sentence and ∂ (γ) ≺ * ϕ (see above for this notation). Unravelling the condition ∂ (γ) ≺ * ϕ specifically to the L 1 -signature (expanded with • and ), we obtain: As promised, the example below illustrates the concept of an -good branch.
are given in Figure 2. Taking to be the order type with p = 1 and q = ∂ there are two -critical branches, with -good branches indicated for an order type with p = 1 and q = ∂.
namely the one ending in +p and the one ending in −q. These are both -good. Indeed, they can correctly be split into P 1 , P 2 and P 3 paths as indicated in the figure. Let us verify that the branch ending in +p moreover satisfies (GB1), (GB2) and (GB3): the formula ( q ∨ p) corresponding to the uppermost P 1 node is a mu-sentence as it contains no fixed point variables, so (GB1) holds. The only SRR-node on P 1 is +∨ and we must check that it satisfies (GB2): here the role of γ is played by q which, firstly, is a mu-sentence; secondly, the only occurring propositional variable is q which occurs positively while There are no SLR nodes in P 2 , so (GB3) holds vacuously.
Turning our attention to the branch ending in −q: the formula ((q → ⊥) ∧ (p → ⊥)) corresponding to the uppermost P 1 node is a mu-sentence, and hence (GB1) is satisfied. There is one SLR-node, namely − →, which verifies (GB3) as the formula playing the role of γ is the constant sentence ⊥. Similarly, there is one SRR-node, + →, which satisfies (GB2) as, in this instance, formula playing the role of γ is again the constant sentence ⊥.
Our main interest is in -good branches satisfying some of the additional properties in the following definition.
Definition 4.4. Let ϕ(p 1 , . . . , p n ) be a formula in the propositional variables p 1 , . . . , p n , let be an order type on {1, . . . , n} and < Ω a strict partial order on the variables p 1 , . . . p n . An -good branch may satisfy one or more of the following properties: (NB-PIA) P 1 contains no fixed point binders.
(NL) For every SLR-node in P 2 of the form γ β or β γ, where β is the side where the branch lies, the signed generation tree of γ contains no live branches. Unravelling this condition specifically to the L-signature, we obtain: , then +γ contains no live branches.
(Ω-CONF) For every SRR-node in P 1 of the form γ β or β γ, where β is the side where the branch lies: p j < Ω p i for every p j occurring in γ, where p i is the propositional variable labelling the leaf of the branch.
1. Since there is overlap between the signed connectives in the columns of Table 1, the borders between the P 1 , P 2 and P 3 parts of a good branch need not be uniquely determined. For strategic reasons, to be discussed below, it is preferable make P 3 as long as possible at the cost of P 2 and, in turn, make P 2 as long as possible at the cost of P 1 .  An inequality ϕ ≤ ψ is -recursive (resp., (Ω, )-inductive, restricted (Ω, )-inductive, tame (Ω, )-inductive) if +ϕ and −ψ are both -recursive (resp., (Ω, )-inductive, restricted (Ω, )-inductive, tame (Ω, )-inductive).
The corresponding classes of inequalities will be referred to as the recursive (resp., inductive, restricted inductive, tame inductive) mu-inequalities, or the recursive (resp., inductive, restricted inductive, tame inductive) mu-formulas, if the inequality signs have been replaced with implications.
Remark 4.7. If we were to interpret L 1 formulas classically, the tame inductive formulas would include the Sahlqvist fixed point formulas of [3,Definition 5.1]. In this setting the tame inductive formulas are, for example, slightly more liberal in terms of what they allow to play the role of a 'boxed atom' (see Example 4.10, below). Figure 2.
From the generation trees we can now see that this is a restricted (Ω, )-inductive inequality for such that p = 1 and q = ∂ and Ω such that q < Ω p. Indeed, given this , there are two -critical branches: the one ending in +p and the one ending in −q. In Example 4.3 we verified that these branches are -good. It is straightforward to check that the branch ending in +p also satisfies (NB-PIA) and (NL). We need to check that the SRR node +∨ satisfies (Ω-CONF): in this case q plays the role of γ, and indeed ∂ (+ q) and q < Ω p. Now considering the branch ending in −q: it is easy to check that is satisfies (NB-PIA) and (NL). To check that is satisfies (Ω-CONF) we need to consider the SRR-node + →, but here the role of γ is played by +⊥, so clearly ∂ (γ).
The inequality is not (Ω , )-inductive for any other order type or dependency order Ω . Indeed, we cannot have q = 1, as the branch ending in +q cannot be correctly divided in P 1 , P 2 and P 3 parts due the presence of + in the scope of + , and is therefore not good. Also we cannot have p = q , since in that case there would be a binder in one of the trees the occurrence of which is not on a critical branch, violating Definition 4.6.3(b). So since is the only possible order type, the configuration + ( q ∨ p) and (Ω-CONF) dictate that Ω is the only possible dependency order.
. This is valid at a point w in a frame iff all point reachable from w are reachable from one another. The corresponding and for no other order type) and any strict partial order Ω. Note that it is not restricted inductive nor tame inductive, since binders occur on both critical and non-critical branches for every possible choice of .
and Ω = ∅), as can be seen from the generation trees in Figure 3. Moreover, the corresponding implication it is not a Sahlqvist fixed point formula in the sense of [3, Definition 5.1], as that definition (and the classical definition of Sahlqvist formulas) would not allow the configuration ( ⊥ ∨ p) where p is a variable to be solved for. It is not tame (Ω, )-inductive for any with p = ∂ or q = ∂, as in such cases the binder µ would appear on an -critical branch. Finally note that this inequality is not restricted inductive. Indeed, since the definition of restricted (Ω, )inductive inequalities requires all binders to occur on critical branches, the −µ would have to be on a critical branch, but then it would have to be on the P 1 part of that branch (according to the definition of good branches), yet (NB-PIA) prohibits this for restricted (Ω, )-inductive inequalities.
The relationships between the different classes of inequalities or, equivalently, formulas, under consideration are illustrated in the diagram below. The inclusions follow from the definitions. Each of the regions is nonempty: that regions A, B and F are non-empty follows from Examples 4.9, 4.8 and 4.10, respectively. Region C contains the inductive formulas which are not Sahlqvist and which contain no fixed point binders, e.g., the Frege axiom (p → (q → r)) → ((p → q) → (p → r)) (see [6,Examples 3.16 and 7.5]). Region D contains the binder free (intuitionistic) Sahlqvist formulas, e.g., p → p, while the Sahlqvist mu-formulas which do contain binders are found in region D, e.g., The algorithm µ-ALBA was introduced in [5, Section 1]. Here we present a variant called µ * -ALBA, and which is a restricted version of µ-ALBA. The goal of our algorithm is to eliminate propositional variables from inequalities, while maintaining admissible validity. The purpose of this is to make the transition from admissible validity to validity in the argument for canonicity, as outlined in Section 3. Before formally stating the rules which can be applied at each stage of the algorithm, we outline its general strategy. The final stage of the algorithm, where the actual elimination of propositional variables takes place, is the application of the two Ackermann rules. There are very specific syntactic requirements of the quasi-inequalities which can be used as input for the right and left Ackermann rules, (RA) and (LA). The steps before this final elimination stage are used to get the original inequality into the correct 'shape' so that the Ackermann rules can be applied.
• Preprocessing: operations are distributed according to the signed generation trees (see below), inequalities are split where possible with (∨LA) and (∧RA), and simple propositional variable elimination takes place using (⊥) and ( ). Preprocessing may split the original inequality into a number of inequalities, on each of which we proceed separately.
• Conversion of fixed point binders: all occurrences of µX.ϕ(X) are converted to µ * X.ϕ(X) and all occurrences of νX.ψ(X) are converted to ν * X.ψ(X). We emphasize that this step is required in both tame and proper runs of µ * -ALBA (see below).
• First approximation: an inequality is converted by (FA) into a quasi-inequality consisting of an implication with two inequalities in the antecedent, and one inequality in the consequent. The inequality in the consequent contains no propositional variables and thus all steps after this point are aimed only at eliminating propositional variables from the two inequalities in the antecedent.
• Residuation, adjunction and approximation rules: these rules prepare the antecedents of quasi-inequalities for the application of the Ackermann rules. The residuation and adjunction rules are straightforward applications of properties of the operations on perfect algebras. The approximation rules are more intricate in their formulation. The approximation rules for fixed point binders are the crucial link which enables us to apply this algorithmic approach to the mu-calculus. When dealing with inductive inequalities, a winning strategy (see Section 10) dictating the order in which these various rules are to be applied is determined by the way in which each critical branch is divided into its P 1 , P 2 and P 3 parts as described in the previous section.
• Ackermann rules: the rules (RA) and (LA) are applied to the quasi-inequalities in the final step to eliminate the propositional variables.
Before we introduce the rules of our algorithm we comment briefly on their presentation. Let ϕ and ψ be two L 1 -terms. Then ϕ ≤ ψ is an L 1 -inequality. We use the symbols & and ⇒, interpreted as conjunction and implication, respectively, to combine L-inequalities into quasi-inequalities. To show canonicity of an inequality, we must show that the validity of the inequality is preserved when we move from interpreting it in an algebra A to interpreting it in the canonical extension A δ . The algorithm µ * -ALBA restructures the inequality into an equivalent quasi-inequality (or sometimes a set of quasi-inequalities).
As mentioned in the introduction, when formulas from the extended language L + are interpreted in A δ , an assignment V will have V(NOM) ⊆ J ∞ (A δ ) and V(CNOM) ⊆ M ∞ (A δ ). Given an assignment V, we call V a p-variant (or, potentially a j-variant or m-variant) of V if V agrees with V on all elements of PROP ∪ NOM ∪ CNOM except possibly at p (respectively, at j or m). We denote this by writing V ∼ p V. From this point on we will use the same V to denote both the assignment V : PROP ∪ NOM ∪ CNOM → A δ and the assignment V : L + → A δ .
Preprocessing Given an inequality ϕ ≤ ψ, consider the positive generation tree of ϕ and the negative generation tree of ψ and apply the following transformations exhaustively: 1. distribute positive occurrences of and ∧ over positive occurrences of ∨; 2. distribute negative occurrences of and ∨ over negative occurrences of ∧; 3. apply the splitting rules rules (∨LA) and (∧RA); 4. apply the monotone variable elimination rules ( ) and (⊥).
In (⊥) we require that α is negative and β is positive in p, while for ( ) we require that γ is positive and χ is negative in p.
First approximation rule This is the same as for µ-ALBA, viz.: The rule (FA) takes an inequality from L * (or L 1 ) and replaces it with a quasi-inequality from L + (L + 1 ). The soundness of (FA) follows from the set J ∞ (A δ ) (the interpretation of the nominals of L + ) being join-dense in A δ , and from M ∞ (A δ ) (the interpretation of the co-nominals of L + ) being meet-dense in A δ (see the base case in the proof of Proposition 9.1).
Residuation rules These rules are the same as the corresponding group for µ-ALBA. The soundness and invertibility of the residuation rules follows from the facts that ∨ and ∧ are, respectively, the right residual of − and the left residual of →.
Adjunction rules The equivalent validity of the formulas above and below the line in (∨LA) and (∧RA) follows from the fact that ∨ is a left adjoint and ∧ a right adjoint of the diagonal map a → (a, a). The rules ( LA) and ( RA) are justified by being the left adjoint of , and being the right adjoint of .
Approximation rules These four rules have the requirement that the nominals and co-nominals introduced by them need to be fresh, i.e., do not occur in the derivation thus far. The justification of all four rules uses the join-primeness of elements of J ∞ (A δ ) and the meet-primeness of elements of M ∞ (A δ ) (see the example of (→Appr) in Proposition 9.1).
We will usually refer to the above group of approximation rules as the ordinary approximation rules in order to distinguish them from the fixed point binder approximation rules that follow.
Approximation rules for fixed point binders Our next two rules are used to extract propositional variables that occur within the scope of a fixed point binder. Let ψ be an (n + 1)-ary term function, and suppose that there exists an order type τ over n such that ψ(x, X) is completely -preserving in (x, X) ∈ C τ × C where C is any perfect mu-algebra of the second kind. Then (subject to the conditions listed below) we will be able to define two rules: (µ τ -A-R) and (ν τ -A-R). We refer the reader to the definitions at the end of Section 2 regarding order types and join-irreducible elements to assist in the reading of these two rules.
where 1. in each rule, the variables x ∈ PHVAR do not occur in any formula in ψ or in ϕ; 2. all propositional variables and free fixed point variables in ψ(x, X) and ϕ(x, X) are among x and X.
3. in (µ τ -A-R) the associated term function of ψ(x, X) is completely -preserving in (x, X) ∈ C τ × C, for any perfect modal bi-Heyting algebra C; in particular we require that ψ(x, X) is positive (negative) in x i if τ i = 1 (τ i = ∂); 4. in (ν τ -A-R) the associated term function of ϕ(x, X) is completely -preserving in (x, X) ∈ C τ × C, for any perfect modal bi-Heyting algebra C; in particular we require that ϕ(x, Note that the difference between these rules and the more general rules, (µ τ -A) and (ν τ -A) (see [5, Section 2.3]), is the absence of the additional tuple, z, of place holder variables in ϕ and ψ. This ensures that, in applications of the rule, the resulting inequalities i ≤ µX.ψ(j i τ /x, X) and νX.ϕ(n i τ /x, X) ≤ m are pure -a fact which will be needed in Section 10 to justify the applicability of the Ackermann-rules, when we prove that µ * -ALBA successfully purifies all restricted and tame inductive mu-inequalities.
Note that (µ τ -A-R) and (ν τ -A-R) are the only rules which can result in the overall quasi-inequality becoming a set of quasi-inequalities. This happens as a result of the introduction of the disjunction n i=1 . Given the way we have set up µ * -ALBA, when the rule is applied, the inequality i ≤ µ * X.ψ(ϕ/x, X) will occur in the antecedent of an implication as part of a conjunction of inequalities. Once the disjunction n i=1 is introduced, this will be distributed over the conjunctions and the implications, producing a set of n quasi-inequalities.
The first inequality from the antecedent gives us the term function ψ(x, y, X) = x ∨ ( ⊥ − y) ∨ X which is -preserving in (x, y, X) for the order type τ = (1, ∂). That is, ψ(x, y, X) is order-preserving as a map from C τ × C. A tuple j τ 1 has the form (j, ) and a tuple j τ 2 has the form (⊥, n). Let ϕ = (p, q). The rule (µ τ -A-R) gives us the following: This can be further simplified and written as: Ackermann rules The Ackermann rules are used for the crucial task of eliminating propositional variables from quasi-inequalities. Before we define these rules we need to introduce some terminology and definitions. Let ϕ ∈ L + 1 or ϕ ∈ L + * . We say that ϕ is positive (negative) in a variable p if in the generation tree +ϕ all p-nodes are signed +(−). An inequality ϕ ≤ ψ is positive (negative) in a variable p if ϕ is negative (positive) in p and ψ is positive (negative) in p.
The syntactically open formulas ϕ and syntactically closed formulas ψ are defined by simultaneous mutual recursion as follows: where p ∈ PROP, i ∈ NOM, and m ∈ CNOM.
The syntactically almost open formulas and syntactically almost closed formulas are defined by adding, respectively, µ * X.ϕ and ν * X.ψ to the recursions above.
Informally, an L + * -term is syntactically almost open if, in it, all occurrences of nominals and are negative, while all occurrences of co-nominals and are positive. If, in addition, all occurrences of µ * are negative and all occurrences of ν * positive, the term is syntactically open. Similarly, an L + * -term is syntactically almost closed if, in it, all occurrences of nominals and are positive, while all occurrences of co-nominals and are negative. If, in addition, all occurrences of µ * are positive and all occurrences of ν * are negative, the term is syntactically closed.
Given these definitions we are now able to define our restricted versions of the Ackermann rules: subject to the restrictions that the α i are p-free and syntactically closed, the β j are positive in p and syntactically closed, while the γ j are negative in p and syntactically open.
subject to the restrictions that the α i are p-free and syntactically open, the β j are positive in p and syntactically open, while the γ j are negative in p and syntactically closed.
A tame run of µ * -ALBA is one during which there are no applications of either (µ τ -A-R) or (ν τ -A-R). By contrast, a proper run of µ * -ALBA is one during which all occurrences of fixed point binders are handled by (µ τ -A-R) and (ν τ -A-R). We say that a run of the algorithm µ * -ALBA succeeds if all propositional variables are eliminated from the input inequality, ϕ ≤ ψ, and we denote the resulting set of pure quasi-inequalities by pure(ϕ * ≤ ψ * ). An inequality on which some run of µ * -ALBA succeeds is called a µ * -ALBA inequality.

Syntactic conditions for meet and join preservation: inner formulas
In the formulation of the approximation rules (µ τ -A-R) and (ν τ -A-R) we required the term functions ψ(x, X) and ϕ(x, X) to be, respectively, completely and -preserving as maps from A τ × A to A. The inner formulas (introduced in [5, Section 4]) are a syntactically specified classes of formulas, the term functions of which satisfy these properties. Being an inner formula is thus an effectively checkable sufficient condition for the applicability of the rules (µ τ -A-R) and (ν τ -A-R).
Definition 6.1. Let y, z ⊆ PHVAR and X ⊆ FVAR be tuples of variables which are pairwise different in the union of the their underlying sets. Let τ be an order-type on x = y ⊕ X. The τand τ-(x, z)-inner formulas ((x, z)-IF τ and (x, z)-IF τ ), the free variables of which are contained in (x, z), are given by the following simultaneous recursion (for the sake of readability, the parameters x and z are omitted): where 1. τ i = 1 in the base of the recursion, 2. π is π(z) ∈ L * (specifically, π(z) contains none of the variables in x or X), 3. ϕ = ϕ (y ⊕ X , z) and ψ = ψ (y ⊕ X , z) are IF τ and IF τ , respectively, with X = X ⊕ Y and τ = τ ⊕ 1, 4. ψ c ∈ (x, z)-IF τ ∂ and ϕ c ∈ (x, z)-IF τ ∂ .

All other formulas have their free variables among (x, z).
The key fact about (x, z)-IF τ and (x, z)-IF τ formulas is the following:
For our purposes then, the most important consequence of this lemma is the fact that (ν τ -A-R) and (µ τ -A-R) are respectively applicable to formulas of the form ψ(ϕ/x, γ/z) and ϕ(ψ/x, γ/z), where ψ(x, z) is IF τ , ψ(x, z) is IF τ and the γ are constant L + * sentences. In particular, (ν τ -A-R) and (µ τ -A-R) are applicable to formulas ψ(ϕ/x) and ϕ(ψ/x), where ψ(x, z) is IF τ and ψ(x, z) is IF τ with z the empty tuple.

Soundness of the fixed point approximation rules
Before we prove the soundness of the Approximation Rules (µ τ -A-R) and (ν τ -A-R), we require some lemmas regarding preservation properties of operations.
Lemma 7.1. Let L be a complete lattice. If f : L m × L → L is completely join-preserving, then the function f (x 1 , . . . , x m , ⊥) : L m → L is completely join-preserving.
We note that this result would also hold if we replaced ⊥ with any a ∈ L, so long as S is non-empty. To accommodate the case that S = ∅, we must have a = ⊥.
Lemma 7.2. Let A be a mu-algebra of the second kind and let τ be an order type over n. Let τ be the order type over n+1 defined by τ = τ⊕{1}. Suppose f : A n+1 → A is an L * term function such that f A δ : (A δ ) τ → A δ is completely -preserving. By the assumption that A is of the second kind, µ 2 x. f (a 1 , a 2 , . . . , a n , x) exists in A for all a 1 , a 2 , . . . a n ∈ A.
Proof. We have the following sequence of equalities: The equivalence of (1) and (2), as well as (5) and (6), follows from the fact that all of the arguments of f A δ are in A. The equivalence of (2) and (3) is the definition of how µx.ϕ(x) is interpreted, and the equivalence of (3) and (4) follows from the fact that A is a mu-algebra of the second kind. By induction on α we will show that ( f A δ ) α ( S , ⊥) = { ( f A δ ) α (s, ⊥) | s ∈ S } and this will be sufficient to prove the overall result.
The second equivalence follows from Lemma 7.1.
• Successor ordinals: • Limit ordinals: Before demonstrating that the Approximation Rule is sound we should point out that this rule is only ever applied to a quasi-inequality that is the result of an application of the First Approximation Rule (FA). That is, (µ τ -A-R) and (ν τ -A-R) are each applied to an inequality which forms part of the antecedent of an implication. When demonstrating the soundness of the rule (µ τ -A-R) it is therefore sufficient to show that the inequality above the line and the inequality below the line are valid under assignments which agree everywhere except at some nominal which does not occur in the consequent of the quasi-inequality. Proposition 7.3. (Soundness of (µ τ -A-R)) Let C be a mu-algebra of the second kind. Let ψ(x, X) and ϕ be terms in L * , with ψ(x, X) completely -preserving in (x, X) ∈ (C δ ) τ × C δ for an order type τ. Let V be an admissible assignment on C δ .
Then C δ , V | = i ≤ µ * X.ψ(ϕ/x, X) if and only if there exists i (1 ≤ i ≤ n) and a j τ i -variant V of V such that Proof. Suppose that C δ , V | = i ≤ µ * X.ψ(ϕ/x, X) for some admissible assignment V. By Lemma 7.2 we have that the term function µ * X.ψ(x, X) is completely -preserving in (C δ ) τ . At this point we will not distinguish between formulas and their interpretations under V. Since C δ is a perfect modal bi-Heyting algebra we have that ϕ is completely join-irreducible and hence completely join-prime we have that there exists j 0 ∈ J ∞ ((C δ ) τ ) with j 0 ≤ ϕ such that V(i) ≤ µ * X.ψ( j 0 , X). Recall from the end of Section 2 that j 0 is ⊥ τ i at every 1 ≤ i ≤ n except at one coordinate, say k. There we have ( j 0 ) k ∈ J ∞ ((C δ ) τ k ) and also ( j 0 ) k ≤ τ k ϕ k . Let j 0 be some nominal for which µ * X.ψ(ϕ/x, X) is j 0 -free. Now let V be the j 0 -variant of V such that V (j 0 ) = ( j 0 ) k .
For the converse, suppose that there exists i ∈ {1, . . . , n} and j τ i such that C δ , V | = i ≤ µ * X.ψ(j i τ /x, X) and C δ , V | = j τ i ≤ τ i ϕ i where V is an admissible j τ i -variant of V. Let us consider the n-tuple j i τ . Given k i, if τ k = 1, then the k-th coordinate of j i τ is ⊥ and hence (j i τ ) k ≤ ϕ k . Again for k i, if τ k = ∂, then the k-th coordinate of j i τ is and thus (j i τ ) k ≤ ∂ ϕ k . Thus we have for all k that (j i τ ) k ≤ τ k ϕ k . The fact that i ≤ µ * X.ψ(ϕ/x, X) follows from the fact that ψ is completely join-preserving (and hence monotone) in x ∈ (C δ ) τ . Thus we have V (i) ≤ V (µ * X.ψ(j i τ /x, X)) ≤ V (µ * X.ψ(ϕ/x, X)) and hence C δ , V | = i ≤ µ * X.ψ(ϕ/x, X).
The statements and proofs of Lemma 7.1, Lemma 7.2 and Proposition 7.3 can easily be dualised and hence we can prove the soundness of the rule (ν τ -A-R).
The reason that we need to use µ * and ν * in the rules (µ τ -A-R) and (ν τ -A-R), respectively, is shown by the proof of Lemma 7.2. If we were to use µx. (1), we would then have only (1) ≤ (2) (as A ⊆ A δ ). Thus if we formulated (µ τ -A-R) and Lemma 7.2 with µ instead of µ * , we would not have the equality in Lemma 7.2 and thus would not be able to show the invariance of admissible validity under (µ τ -A-R).

Soundness of the Ackermann rules
In this section we prove the soundness of the Ackermann rules, (RA) and (LA). Once we have shown the soundness of (RA) and (LA), we will be able, in the next section, to prove Proposition 9.1. This proposition declares the soundness of µ * -ALBA derivations with respect to admissible validity.
We will need the next two technical lemmas, the proofs of which will make extensive use of the algebraic results presented in the appendix. Our strategy closely follows that in [6]. However, we work algebraically whereas [6] proceeds in the setting of general frames. Moreover, we need to accommodate fixed point binders which are absent in [6].
Fix a modal bi-Heyting algebra A of the first kind. The set of open elements of A δ , denoted O(A δ ), is defined as { S | S ⊆ A}, i.e., as all those elements of A δ that can be obtained as arbitrary joins of elements of A. Dually, the set of closed elements of A δ , denoted K(A δ ), is defined as { S | S ⊆ A}, i.e., as all those elements of A δ that can be obtained as arbitrary meets of elements of A. The intention behind the definition of syntactically open and closed L + * formulas is that admissible assignments will always interpret them as open and closed elements of A δ , respectively.
Proof. We proceed by simultaneous structural induction on ϕ and ψ. We show (1). Assume that ϕ(p, q, i, m) is positive in p and ψ(p, q, i, m) is negative in p. As they do not impact the overall result, we will omit the parameters q, i and m and simply write ϕ(p) and ψ(p) for ϕ(p, q, i, m) and ψ(p, q, i, m) respectively. The base cases are when ϕ is of the form , ⊥, p, q (where q is a propositional variable different from p), or ϕ = i, and when ψ is of the form , ⊥, q (where q is a propositional variable different from p), or ψ = m. The ϕ cannot be a co-nominal m since ϕ is syntactically closed but m syntactically open. Similarly ψ cannot be p or a nominal i since ψ must be negative in p and any occurrence of a nominal must be negative. Now clearly , ⊥, q are all interpreted as clopen elements of A δ , as is p. Furthermore, the claims follow for ϕ any nominal i and ψ any co-nominal m since If ϕ(p) = ϕ 1 (p) ∧ ϕ 2 (p) or ϕ(p) = ϕ 1 (p) ∨ ϕ 2 (p) then both ϕ 1 (p) and ϕ 2 (p) must be syntactically closed and positive in p. Thus by the inductive hypothesis we have that ϕ 1 (k) ∈ K(A δ ) and ϕ 2 (k) ∈ K(A δ ) and both their meet and join are in K(A δ ) as this is closed under the lattice operations.
We note that there cannot be occurrences of µ or ν in either ϕ(p) or ψ(p). If ϕ(p) is of the form µ * X.ϕ 1 (p, X), If ϕ(p) = ϕ 1 (p) − ϕ 2 (p) then ϕ 1 (p) is syntactically closed and positive in p and ϕ 2 (p) is syntactically open and negative in p. By the inductive hypothesis, ϕ 1 (k) ∈ K(A δ ) and ϕ 2 (k) ∈ O(A δ ). Now by Lemma .11 (4) we If ψ(p) = ψ 1 (p) → ψ 2 (p) then ψ 1 (p) is syntactically closed and positive in p while ϕ 2 (p) is syntactically open and negative in p. By the inductive hypothesis we have ψ 1 (k) ∈ K(A δ ) and ψ 2 (k) ∈ O(A δ ). Using Lemma .11(3) we see that Now we look at the cases for the unary connectives. We note that ϕ cannot be of the form ϕ 1 as this is not syntactically closed. Likewise, ψ cannot be of the form ψ 1 as this is not syntactically open.
The base cases of the induction for ϕ are when ϕ is of the form , ⊥, p, a propositional variable q other than p, or i. The base cases for ψ are those when ψ is of the form , ⊥, a propositional variable q other than p, or m. In each case the claim is trivially true.
Thus when ϕ(p) = ϕ 1 (p) ∧ ϕ 2 (p) the claim follows by the inductive hypothesis and the associativity of the meet operation, and when ψ(p) = ψ 1 (p) ∨ ψ 2 (p) the claim follows by the inductive hypothesis and the associativity of the join operation. Now suppose that ϕ(p) = ϕ 1 (p) ∨ ϕ 2 (p). By the inductive hypothesis, For the reverse inequality, suppose that x ∈ J ∞ (A δ ) and x ϕ( D). This implies that Hence there exists d 1 , d 2 ∈ D such that x ϕ 1 (d 1 ) and x ϕ 2 (d 2 ). Since D is down-directed, there exists d 3 ∈ D such that d 3 ≤ d 1 and d 3 ≤ d 2 . Since ϕ 1 and ϕ 2 are monotone we have that ϕ 1 (d 3 ) ≤ ϕ 1 (d 1 ) and ϕ 2 (d 3 ) ≤ ϕ 2 (d 2 ). This implies that x ϕ 1 (d 3 ) and x ϕ 2 (d 3 ). By Lemma .3(3), ϕ 1 (d 3 ) ≤ κ(x) and ϕ 2 (d 3 ) ≤ κ(x) and so ϕ 1 (d 3 . If ψ(p) = ψ 1 (p) ∧ ψ 2 (p) then by the inductive hypothesis, . This implies that there exist d 1 , d 2 ∈ D such that ψ 1 (d 1 ) κ(x) and ψ 2 (d 2 ) κ(x). Now by Lemma .3(3) we have x ≤ ψ 1 (d 1 ) and x ≤ ψ 2 (d 2 ). Furthermore, by the downdirectedness of D, there exists d 3 ∈ D such that d 3 ≤ d 1 , d 2 . Since ψ 1 and ψ 2 are antitone in p we have that x ≤ ψ 1 (d 3 ) and x ≤ ψ 2 (d 3 ). This gives us that Suppose ϕ(p) = µ * X.ϕ 1 (p, X) where ϕ 1 (p) is closed and positive in p. For each d ∈ D we have { a ∈ A | ϕ 1 (d, a) ≤ a } ⊆ { a ∈ A | ϕ 1 ( D, a) ≤ a } and hence It follows that ϕ 1 (d 1 ∧ . . . ∧ d n , a) ≤ a and since D is down-directed, there exists d a ∈ D such that d a is a lower bound for If ψ(p) is of the form ν * X.ψ 1 (p, X) then ψ 1 (p) must be open and negative in p. Now and hence a ≤ ψ 1 (d a , a). Now a ≤ ν * X.ψ 1 (d a , X) and so If ϕ(p) is of the form ϕ 1 (p) for ∈ { , , }, then ϕ 1 (p) must be syntactically closed and positive in p. By the inductive hypothesis, ϕ 1 ( D) = { ϕ 1 (d) | d ∈ D }. By Lemma 8.1(1a) we have that ϕ 1 (d) ∈ K(A δ ) for all d ∈ D. As ϕ 1 is monotone, and since D is down-directed, we have that { ϕ 1 (d) | d ∈ D } is a down-directed subset of K(A δ ). Thus we can use the fact that is -preserving, Lemma .8(2), and Lemma .10(2) to conclude that is of the form ψ 1 (p) for ∈ { , , }, then ψ 1 (p) must be syntactically open and negative in p. By the inductive hypothesis, ψ 1 ( D) = d∈D ψ 1 (d). By Lemma 8.1(1b), each ψ 1 (d) ∈ O(A δ ). Since D is down-directed, we have that { ψ 1 (d) | d ∈ D } is an up-directed set of open elements. We apply the fact that is -preserving, Lemma .8(2), and Lemma .10(2) to conclude that ψ( If ϕ(p) is of the form ϕ 1 (p) − ϕ 2 (p) then ϕ 1 (p) is syntactically closed and positive in p, and ϕ 2 (p) is syntactically open and negative in p. By the inductive hypothesis we have ϕ( Since D is down-directed, there exists f such that f ≤ d and f ≤ e. This gives us ϕ 1 ( f ) ≤ ϕ 1 (d) and ϕ 2 (e) ≤ ϕ 2 ( f ). By the fact that − is order-preserving in its first argument and order-reversing in its second argument, we get that If ψ(p) is of the form ψ 1 (p) → ψ 2 (p) then ψ 1 (p) is syntactically closed and positive in p and ψ 2 (p) is syntactically open and negative in p. By the inductive hypothesis we have Again, { ψ 1 (d) | d ∈ D } is a down-directed subset of K(A δ ) and { ψ 2 (e) | e ∈ D } is an up-directed subset of O(A δ ). We apply Lemma .10(4) to get ψ( D) = { ψ 1 (d) → ψ 2 (e) | d, e ∈ D }. It is then clear that Since D is down-directed, for any d, e ∈ D, there exists a lower bound f for d, e. Now ψ 1 ( f ) ≤ ψ 2 (d) and ψ 2 (e) ≤ ψ 2 ( f ) and so We are now ready to prove the Ackermann lemmas which will justify the rules (RA) and (LA).
Lemma 8.3 (Righthanded Ackermann lemma for mu-algebras). Let A be a mu-algebra of the first kind. Let α(q, i, n), β(p, q, i, n) and γ(p, q, i, n) be L + * -formulas such that (i) α(q, i, n) is syntactically closed and does not contain any occurrences of p, (ii) β(p, q, i, n) is syntactically closed and positive in p, and (iii) γ(p, q, i, n) is syntactically open and negative in p.
Then for any b ∈ A, c ∈ J ∞ (A δ ) and d ∈ M ∞ (A δ ), the following are equivalent 1. there exists a ∈ A such that α(b, c, d) ≤ a and β(a, b, c, d) ≤ γ(a, b, c, d), Proof. For the implication from top to bottom, it suffices to appeal to the monotonicity of β in p and the antitonicity of γ in p.
For the sake of the converse implication, assume that β (α(b, c, d) Since β is syntactically closed and positive in p, and γ is syntactically open and negative in p, we may apply By Lemma 8.1, β(u, b, c, d) is closed and γ(u, b, c, d) is open for each u ∈ A. Hence, by compactness, for some u 1 , . . . , u m ∈ A with α(b, c, d) ≤ u i for 1 ≤ i ≤ m, and some u 1 , . . . , u n ∈ A with α(b, c, d) ≤ u j for all 1 ≤ j ≤ n. Let a = u 1 ∧ · · · ∧ u m ∧ u 1 ∧ · · · ∧ u n . Then α(b, c, d) ≤ a ∈ A. By the monotonicity of β in p, the antitonicity of γ in p, and (7), it follows that β(a, b, c, d) ≤ γ(a, b, c, d).

Canonicity of µ * -ALBA inequalities
We now have all of the machinery in place to prove that admissible validity for an inequality ϕ * ≤ ψ * is preserved under any number of applications of rules from µ * -ALBA. This will be crucial in showing both canonicity and tame canonicity for classes of inequalities on which the algorithm succeeds. In this section we will assume that each of the inequalities that we are working with has already undergone preprocessing (see Section 5). The fact that both admissible validity and ordinary validity is preserved throughout the preprocessing stage is straightforward to prove. Proposition 9.1. (Soundness of µ * -ALBA rules w.r.t. admissible validity) Let A be a mu-algebra of the second kind, and ϕ ≤ ψ an L 1 -inequality. Let FA(ϕ * ≤ ψ * ) := ∀i∀m(i ≤ ϕ * & ψ * ≤ m ⇒ i ≤ m) and let { QIneq k | 1 ≤ k ≤ n } be a set of quasi-inequalities obtained from FA(ϕ * ≤ ψ * ) through the application of µ * -ALBA rules.
Proof. We proceed by induction on the number of rule applications. For the base case, suppose that there are no applications of rules to FA(ϕ * ≤ ψ * ). Assume A δ | = A ϕ * ≤ ψ * . Let V be an admissible assignment such that V(i) ≤ V(ϕ * ) and V(ψ * ) ≤ V(m). By assumption we have that V(ϕ * ) ≤ V(ψ * ) and hence by transitivity we have Let V be any admissible assignment. We need to show that V(ϕ * ) ≤ V(ψ * ). By the join-density of J ∞ (A δ ) and the meet-density of M ∞ (A δ ), it is sufficient to show that for every i ∈ J ∞ (A δ ) and be a set of quasi-inequalities obtained from Q 1 via a single rule application. (To be clear, Q 2 is the same as Q 1 except for the quasi-inequality QIneq m ∈ Q 1 which has been changed via the single rule application.) We now cover the various possible cases for the (k+1)-th rule application that gives us { QIneq m j | 1 ≤ j ≤ } from QIneq m . The cases of the residuation and adjunction rules are clear from the properties of the residuals and adjoints.
We prove the case of (→Appr). Let V be an admissible assignment such that V(χ → ϕ) ≤ V(m). We Since → is completely join-reversing in its first coordinate and completely meet-preserving in its second coordinate, we get { j → n | j ≤ V(χ), V(ϕ) ≤ n } ≤ V(m). As V(m) ∈ M ∞ (A δ ) and hence completely meet-prime, there must exist j 0 ∈ J ∞ (A δ ) with j 0 ≤ V(χ) and n 0 ∈ M ∞ (A δ ) with V(ϕ) ≤ n 0 such that j 0 → n 0 ≤ V(m). Now choose j ∈ NOM, n ∈ CNOM such that χ → ϕ ≤ m is (j, n)-free and construct a (j, n)-variant V of V such that V (j) = j 0 and V (n) = n 0 . The opposite direction only requires the observation that → is order-reversing in the first coordinate and order-preserving in the second coordinate.
The soundness and invertibility of the remaining ordinary approximation rules will follow using properties of canonical extension A δ , especially the join-density and join-primeness of J ∞ (A δ ) and the meet-density and meet-primeness of M ∞ (A δ ).
The case of the rule application being that of the Approximation Rules (µ τ -A-R) and (ν τ -A-R) follows from Proposition 7.3. We observe that these are the only rules which could possibly result in > 1.
The case for the Ackermann rules (RA) and (LA) follow from Lemmas 8.3 and 8.4, respectively.
Proof. The only part of the proof of Proposition 9.1 above that requires A to be a mu-algebra of the second kind is the case of (µ τ -A-R) and (ν τ -A-R). Those cases rely on Proposition 7.3, which is proved using Lemma 7.2. Figure 4: The proof of tame canonicity for L 1 -inequalities on which a tame run of µ * -ALBA succeeds.
The proof of that lemma requires A be of the second kind. The soundness and invertibility of the remaining rules are proved exactly as in Proposition 9.1 and do not require A to be of the second kind.
In order to complete the right-hand side of the U-shaped argument, we need to know that the rules can be 'undone' when using arbitrary assignments on the algebras that are the canonical extensions of mu-algebras of the first kind. Proposition 9.3. Let A be a mu-algebra of the first kind. For any L 1 -inequality ϕ ≤ ψ on which a tame run of µ * -ALBA succeeds, we have that Proof. Since pure(ϕ * ≤ ψ * ) is the result of a successful tame run of µ * -ALBA, we know that pure(ϕ * ≤ ψ * ) is a single quasi-inequality obtained via some finite number of rule applications from µ * -ALBA, not including (µ τ -A-R) or (ν τ -A-R). Not including (RA) and (LA), the soundness and invertibility of each of the rules under arbitrary (i.e., not necessarily admissible) assignments is clear from the fact that the admissibility of the assignments was not used in any of the proofs in Proposition 9.1.
When working on perfect algebras, the Ackermann lemmas are easy to prove, and depend only on the monotonicity and antitonicity of the formulas involved. For (RA), the direction from top to bottom can be proved using only the fact that β is positive in p and γ is negative in p. The direction from bottom to top can be shown by taking V to be the p-variant of V such that V (p) = V(α).
Theorem 9.4. (Tame Canonicity) All L 1 -inequalities on which a tame run of µ * -ALBA succeeds are tame canonical.
Proof. Suppose that a tame run of µ * -ALBA succeeds on the inequality ϕ ≤ ψ. Then we have the following sequence of equivalences: The equivalence of (9) and (10) follows from the fact that the admissible validity of formulas without µ or ν on A δ will agree with ordinary admissible validity of formulas without µ or ν. For formulas with µ or ν, the definition of µ * and ν * assures that the interpretation of such formulas will be identical on A and A δ . For the equivalence of (10) and (11) we use Corollary 9.2. The equivalence of (11) and (12) follows from the fact that pure(ϕ * ≤ ψ * ) contains no propositional variables and hence that its admissible validity and validity coincide. The final equivalence is the statement of Proposition 9.3.
The next two lemmas and the proposition which follows are needed to convert formulas of the form µ * X.ϕ(X) back to µX.ϕ(X). The first of the lemmas is proved in [5].
If G is completely join-preserving, then µy.G(−, y) : M → L is defined everywhere on M and is completely join-preserving.
Lemma 9.6. Let A be a mu-algebra of the second kind and let τ be an order type over n. Let ψ(x, X) ∈ L 1 such that ψ(x, X) is completely -preserving in (x, . Thus by the assumption, V(i) ≤ V(m).
Proof. The set of quasi-inequalities pure(ϕ * ≤ ψ * ) is obtained through a finite number of rule applications of µ * -ALBA. As detailed by Proposition 9.3, all of the residuation, adjunction, ordinary approximation and Ackermann rules can be reversed while preserving validity on A δ . Suppose that at some stage during the proper run of µ * -ALBA, the inequality i ≤ µ * X.ψ(ϕ/x, X) is converted into We are now ready to present the final canonicity result.
Theorem 9.8. (Canonicity) Let A be a mu-algebra of the second kind and let ϕ ≤ ψ be an L 1 -inequality on which a proper run of µ * -ALBA succeeds. If A | = ϕ ≤ ψ then A δ | = ϕ ≤ ψ.
Proof. The proof is similar to that of Theorem 9.4.
The equivalence of (14) and (15) follows as for Theorem 9.4. For the equivalence of (15) and (16) we apply the inductive argument from Proposition 9.1. The equivalence of (16) and (17) follows from the fact that pure(ϕ * ≤ ψ * ) contains no propositional variables and hence admissible validity and validity coincide for it. The final implication is the statement of Proposition 9.7.
Lastly, we make an observation regarding mu-inequalities with no occurrences of fixed point binders. If ϕ ≤ ψ does not contain any fixed point binders, and a tame run of µ * -ALBA succeeds on ϕ ≤ ψ, then ϕ ≤ ψ will be tame canonical. That is, A | = ϕ ≤ ψ if and only if A δ | = ϕ * ≤ ψ * . However, we have that ϕ = ϕ * and ψ = ψ * and so A | = ϕ ≤ ψ if and only if A δ | = ϕ ≤ ψ. Likewise, if a proper run of µ * -ALBA succeeds on α ≤ β where this mu-inequality has no occurrences of fixed point binders, Proposition 9.3 can be applied to show the converse of (21) ⇒ (22) in Theorem 9.8 and hence A | = α ≤ β if and only if A δ | = α ≤ β.

Canonicity of the restricted and tame inductive mu-inequalities
In this section we argue that µ * -ALBA successfully purifies all restricted inductive mu-inequalities by means of proper runs, and all tame inductive mu-inequalities by means of tame runs. Once we have established these claims, the next theorem will then follow from Theorems 9.4 and 9.8: Theorem 10.1. All restricted inductive mu-inequalities are canonical and all tame inductive mu-inequalities are tame canonical.
As far as tame inductive inequalities are concerned, the proof is almost verbatim the same as in [6, Section 10.1]. Indeed, tame inductive inequalities are just (a subset of the) inductive inequalities from the language of intuitionistic modal logic with some fixed point binders 'along for the ride' on the non-critical branches. Thus the binders never need to be handled by the algorithm, so the runs are guaranteed to be tame and exactly the same strategy employed in [6] is sufficient. The only point that needs to be checked is that the side conditions of the Ackermann rules pertaining to syntactic openness and closure are met when these rules need to be applied. This follows from the next two lemmas: Lemma 10.2. If µ * -ALBA is applied to any L 1 -inequality then, during the whole run, every inequality in every antecedent of every produced quasi-inequality is either pure, or has a syntactically almost closed left-hand side and a syntactically almost open right-hand side. Consequently, if a non-pure inequality contains no fixed point binders it has a syntactically closed left-hand side and a syntactically open right-hand side.
Proof. The proof is by induction on the application of the rules of µ * -ALBA. Suppose µ * -ALBA is run on an L 1 -inequality. As discussed above, preprocessing turns this into a finite number of inequalities η ≤ β. Starring and first approximation produce (i ≤ η * & β * ≤ m) ⇒ i ≤ m. We claim that i ≤ η * and β * ≤ m satisfy the statement of the lemma. Indeed, i and m are, respectively, syntactically closed and open. As η * , β * ∈ L * , they do not contain any nominals, co-nominals, or , and are therefore both syntactically almost open and syntactically almost closed.
The induction now proceeds by showing that the desired properties are invariant under the application of the rules of µ * -ALBA. The most interesting cases are those for (µ τ -A-R) and (ν τ -A-R). We verify (µ τ -A-R). Applied to an inequality i ≤ µ * X.ψ(ϕ/x, X, γ/z), the rule (µ τ -A-R) produces a disjunction of inequalities of the form i ≤ µ * X.ψ(j i τ /x, X, γ/z) and j τ i ≤ τ i ϕ i . Since the γ are constant sentences, the first of these inequalities is pure.
If τ i = 1, the second inequality is j ≤ ϕ i where j is syntactically closed and ϕ i is syntactically almost open since it occurs positively as a subformula of the syntactically almost open formula µ * X.ψ(ϕ/x, X, γ/z). On the other hand, if τ i = ∂, the second inequality is ϕ i ≤ n where n is syntactically open and ϕ i is syntactically almost closed since it occurs negatively as a subformula of the syntactically almost open formula µ * X.ψ(ϕ/x, X, γ/z).
Lemma 10.3. If µ * -ALBA is applied to any tame inductive L 1 inequality, then, during the whole run, every inequality in every antecedent of every quasi-inequality is either pure or has a left-hand side (resp., right-hand side) in which all occurrences of µ * are positive (resp., negative) and all occurrences of ν * are negative (resp., positive).
Proof. Preprocessing turns any tame inductive L 1 inequality into a finite number of tame inductive inequalities η ≤ β. By the definition of tame inductive inequalities, the only occurrences of binder nodes in +η and −β are +ν and −µ. Thus starring and first approximation yields a quasi-inequality where in η * (resp., β * ) all occurrences of all occurrences of µ * are negative (resp., positive) and all occurrences ν * are positive (resp., negative). Thus this quasi-inequality satisfies the claim of the lemma. It is now sufficient to show that these conditions are invariant under the application of all µ * -ALBA rules. For the sake of the adjunction rules, note that all occurrences of binders are untouched and left on the same sides of inequalities. The residuation rules move subformulas across the inequality but with an accompanying change in polarity, and the same consideration also deals with the Ackermann rules. The fixed point approximation rules (µ τ -A-R) and (ν τ -A-R) are not applied, since tame inductive inequalities contain no binders on critical branches. The cases for the other approximation rules are easy to verify -let us look explicitly only at (→Appr). By assumption, in the premise χ → ϕ ≤ m, all occurrences of µ * are positive and all occurrences of ν * are negative. Thus, in j → n ≤ m & j ≤ χ & ϕ ≤ m, the conclusion of the rule, the inequality j → n is pure, the righthand side of j ≤ χ contains µ * only negatively and ν * only positively, while the lefthand side of ϕ ≤ m contains µ * only positively and ν * only negatively. Now that we have established Theorem 10.1 for tame inductive mu-inequalities, we will focus on the restricted inductive mu-inequalities for the remainder of this section. In [5,Section 9] it was proven that µ-ALBA successfully purifies all recursive mu-inequalities. The restricted inductive mu-inequalities form a subclass of these, but µ * -ALBA is also a restricted version of µ-ALBA. Consequently our argument will follow that in [5] very closely, but we will be at pains to show how the constraints built into the restricted inductive muinequalities allow us to still succeed with the restricted resources of µ * -ALBA. The reader might find it useful to refer to Example 11.1 while reading the following argument.
Let η ≤ β be an (Ω, )-inductive inequality. We proceed as in ALBA and preprocess this inequality by applying splitting and ( ) and (⊥) exhaustively. This might produce multiple inequalities, on each of which we proceed separately. On each such inequality, denoted again η ≤ β, we proceed to first approximation, which yields the following quasi-inequality: Because its consequent is always pure, we only concentrate on its antecedent. Since the outer skeletons of β and η are built exactly as the outer part of an inductive modal formula, the ordinary approximation rules can be applied so as to surface the inner skeleton. So we can equivalently rewrite i ≤ η & β ≤ m as the conjunction of a set of inequalities which, whenever they contain critical variables in the scope of fixed point binders occurring as skeleton nodes, are of the form i ≤ µX.ψ (p) and νX.ϕ (p) ≤ m, where µX.ψ (p) and νX.ϕ (p) are sentences. (For the critical branches which do not contain such fixed point binders, we further proceed by exhaustively applying the approximation rules as in ALBA in order to surface the PIA parts.) In what follows, we call a generation tree non-trivially restricted (Ω, )-inductive if it is restricted (Ω, )inductive and contains at least one -critical branch. (20) is of the form i ≤ µX.ψ(ϕ/y, X, γ/z), where µX.ψ(y, X, z) is an (y, z)-IF τ formula for some order-type τ over y, and the γ are constant sentences; 2. the inequality νX.ϕ ≤ m in (20) is of the form νX.ϕ(ψ/y, X, γ/z) ≤ m, where νX.ϕ(y, X, z) is an (y, z)-IF τ formula for some order-type τ over y, and the γ are constant sentences.
Proof. Notice that preprocessing, first approximation and ordinary approximation rules do not involve fixed points. Hence a proof very similar to that of [6, Lemma 10.6] proves that +µX.ψ and −νX.ϕ are non-trivially restricted (Ω, )-inductive. Hence the statement immediately follows from Lemma 10.5 below.

2.
Let ϕ be such that −ϕ is non-trivially restricted (Ω, )-inductive, and the P 3 -paths of all critical branches are of length 0. Then ϕ is of the form ϕ(ψ/y, X, γ/z) where ϕ(x, z) is an (x, z)-IF τ formula, for x = y ⊕ X and some order-type τ over x, the ϕ are sentences and the γ are constant sentences. Moreover, if y = (y 1 , . . . , y n ) then, for each Proof. The proof is virtually identical to that of [5, Lemma 9.2] and [5, Remark 9.3], the only difference being that we need to ensure that the γ are constant, i.e., contain no propositional variables. We will do so by appealing to the condition (NL) at the appropriate point. The proof is by simultaneous induction on the skeleton depths of +ψ and −ϕ , where the skeleton depth of an -recursive (or inductive) generation tree * ξ, with * ∈ {+, −}, is the maximum length of the P 2 parts of -critical branches in * ξ.
Consider the base case when the skeleton depth of +ψ is 0, i.e., the critical branches consist only of PIA nodes. Then, by (GB1), ψ is a sentence. Hence we let ψ = x 1 which is IF τ with τ = (1), ϕ 1 = ψ (which is -PIA and a sentence). Moreover, (vacuously) all γ are constant sentences.
Proposition 10.4 implies that the approximation rules (µ τ -A-R) and (ν τ -A-R) can be applied to the inequalities (20), respectively. 2 In addition to this, we can assume w.l.o.g. that every inequality sitting in an antecedents of any quasi-inequality produced by these rule applications and containing a critical branch is of the form j ≤ ϕ or ψ ≤ n, where +ϕ and −ψ are non-trivially (Ω, )-PIA (i.e., non-trivially (Ω, )-inductive with all critical branches consisting only of PIA-nodes, i.e., of P 1 -nodes) and, by (NB-PIA) and (GB1) ϕ and ψ are sentences containing no binders, i.e., they are formulas of L. In other words ϕ and ψ are (Ω, )-inductive formulas of intuitionistic modal logic. This means that we can proceed as in ALBA to eliminate all propositional variables from the quasi-inequality. However, before the Ackermann rules can be applied we need to be sure that their side conditions are met. This is guaranteed by the following considerations: after the application of the approximation rules (µ τ -A-R) and (ν τ -A-R), all fixed point binders in the current quasi-inequalities occur only in pure inequalities of the form i ≤ µ * X.ψ(j i /x, X, γ/z) and ν * X.ϕ(n i /x, X, γ/z) ≤ m. The only inequalities involved in the application of an Ackermann rule are non-pure, and therefore cannot contain any fixed point binders. So by Lemma 10.2 above, their left hand sides will be syntactically closed and their right and sides syntactically open, as desired.
In summary: In dealing with the outer skeleton we proceed as in ALBA. The inner skeleton is processed as in µ-ALBA, but with the applicability of the restricted approximation rules (µ τ -A-R) and (ν τ -A-R) guaranteed by Proposition 10.4 via Lemma 10.5. This proposition and lemma are provable thanks to the condition (NL). The condition (NB-PIA) ensures that the PIA parts contain no fixed point binders or fixed point variables and can hence be treated as in ALBA, without the need of the adjunction rules for µ and ν used in µ-ALBA. Next, the condition (Ω-CONF) guarantees that we are working with inductive rather than recursive inequalities, and hence that the ordinary (non-recursive) Ackermann rule can be used to eliminate the propositional variables. Lastly, the requirement that every occurrence of a binder is on an -critical branch (Definition 4.6) guarantees that every binder must have one of the approximation rules (µ τ -A-R) and (ν τ -A-R) applied to it, i.e., that the run of the algorithm is proper.
Thus the PIA parts have been surfaced and the quasi-inequality has been transformed into: We now proceed to apply adjunction and residuation rules to get the quasi-inequality into the right shape for the application of the Ackermann rules. Applying ( RA), (∨RR) and (∧RA) produces Now applying (→RA) and then (∧LR) to l ≤ q → ⊥ transforms it into q ≤ l → ⊥. This yields the following quasi-inequality, which has now been solved for +p and −q and is therefore ready for the application of the right and lefthanded Ackermann rules (RA) and (LA) to eliminate p and q, respectively:

Now applying (LA) gives
and then applying (RA) gives the pure quasi-inequality Example 11.2. Consider the tame inductive inequality ( ⊥∨ p)∧ q ≤ µY.( (p∧q)∧ Y) from Example 4.10. Preprocessing distributes and ∧ over ∨ in the antecedent producing ( ⊥ ∧ q) ∨ ( p ∧ q) ≤ µY.( (p ∧ q) ∧ Y), to which we can apply (∨LA) to split into two inequalities: ( ⊥ ∧ q) ≤ µY.( (p ∧ q) ∧ Y) and ( p ∧ q) ≤ µY.( (p ∧ q) ∧ Y). As p appears only positively in the first, we may eliminate it by applying the (⊥) rule to obtain ( ⊥ ∧ q) ≤ µY.( (⊥ ∧ q) ∧ Y). The algorithm µ * -ALBA now proceeds separately on these two inequalities. We will describe this process only for the second one, the execution on the first being very similar but less interesting. Starring and first approximation transforms the second inequality into the quasi-inequality Applying (∧RA) to i ≤ p ∧ q produces i ≤ p and i ≤ q. To the first of these we apply ( Appr) to produce i ≤ j and j ≤ p, while ( RA) turns the second into i ≤ q. Thus we have the quasi-inequality This is now ready for the Ackermann rule (RA) to be applied twice to eliminate both p and q, producing Appendix: Algebraic properties of additional operations on perfect distributive lattices Let C be a perfect distributive lattice. The map κ : J ∞ (C) → M ∞ (C) is defined as by κ(x) = (C \↑x). This map is an order isomorphism between J ∞ (C) and M ∞ (C) with κ −1 defined for m ∈ M ∞ (C) by κ −1 (m) = (C \ ↓m). Note that if C is an atomic Boolean algebra, then κ is simply the negation ¬.
The results at the end of this section are algebraic versions of results presented in Appendix A of [6]. We acknowledge that some of these results have been shown independently by Zhao [16].