Let's talk about duality. Duality is a mathematical technique that allows us to have two different perspectives on the same class of structures.

Often one of these perspectives is geometrical, whereas the other perspective is logical. The mother of all dualities, stone duality, is a duality between Boolean algebras and certain topological spaces that we now know as stone spaces.

Subsequently, we've seen dualities between distributive lattices and what is now known as priestly spaces, and also hating algebras and so-called Isarchaeo spaces. In the context of modal logic, duality allows us to connect the algebraic semantics and the frame semantics of the given logic.

This is well known and established for descriptive frames on the one side and Boolean algebras with operators on the other side, and it's also been developed for positive modal algebras and so-called A-plus spaces. The last two are specifically interesting because, as it turns out, these two dualities

naturally arise as duality between algebras on the one side describing the algebraic aspect, and color algebras that describe the spaces or frames on the other side. One observation, however, is that a duality between modal hating algebras and modal

Intuitunistic spaces hasn't so far been established as an instance of a more general algebra-co-algebra duality until now. To see why, let's look at an example. We take the simplest Intuitunistic modal logic, where we just add a box to the language of

propositional logic, and we stipulate that box distributes over finite meets. This logic is interpreted in box frames, which are Intuitunistic cryptic frames, that are equipped with an extra relation to interpret the box modality. In the literature, one sees that this relation is required to satisfy a

compatibility condition, mainly to ensure that the interpretation of formulae is persistent. The interpretation itself is mostly standard in that Intuitunistic connectives are interpreted as in the underlying Intuitunistic cryptic frame, and X makes the formula box phi true

if phi holds in all relational successes of X. To put this into a co-algebraic setting, we need a category and a functor on this category. F co-algebras are then pairs X comma gamma, where gamma is amorphism from X to FX.

We can then model box frames as co-algebras on the category of posets for the upper power set functor. The upper power set functor takes a poset and maps it to the poset of its upsets, ordered by reverse inclusion. This allows us to go back and forth between box frames and

co-algebras for the upper power set functor, where one direction from box frames to co-algebras goes via defining the structure map to map every state to its relational successes. So far, this looks quite promising.

However, not all is well when we look at morphisms. Co-algebromorphisms are morphisms between the object part, that is the X and Y part of co-algebras that make the expected diagram commute. In particular, in our example, morphisms live in the category of posets.

That means that they're monotone maps. As a consequence, these morphisms do not preserve the interpretation of logical connectives because monotone maps don't preserve hating implication. To repair this, one could take bounded morphisms instead, that is,

morphisms between intuitunistic Kripke frames. But then the co-algebra structure map gamma would also need to be a bounded morphism, which means that we would lose the correspondence with box frames. What we want here is that morphisms between structures are bounded

morphisms, whereas the structure maps themselves are just monotone maps. One way to achieve this is by using die-algebras. Given a pair of functors G and F from a category C to a category D, a GF-die-algebra is just a map gamma from GX to FX or an object X of the category C.

Die-algebromorphisms are just C-morphisms between the object part that again make the expected diagram commute. This now allows us to separate out the category of posets into the category

pos of posets with monotone morphisms and the category Krip of intuitunistic Kripke frames and bounded morphisms. And we can have box frames and their morphisms as die-algebras for a pair of functors. One functor is just the inclusion of Kripke frames into posets.

And the other functor is the upper power set functor that we've already seen, but now conceive as a functor that maps an intuitunistic Kripke frame to a poset.

Interestingly, the same also works for hating algebras with operators that constitute the algebraic semantics of intuitunistic modal logics. Hating algebras with operators are just ordinary hating algebras with an additional operator that we write as box, which preserves finite meets.

Morphisms between hating algebras with operators preserve this new operator as well as all propositional connectives. Hating algebras with operators also arise as a category of die-algebras for a pair of functors. One of the functors is just the inclusion J of hating

algebras into distributive lattices, and the other one N maps a hating algebra A to the distributive lattice generated by all boxed elements of A modded out by the axioms that stipulate that box preserves finite meets. If we do this, we see immediately that the category of hating

algebras with operators is isomorphic to the category of die-algebras for the functors N and J. So we've seen that box frames arise as die-algebras for a pair of

functors. We've seen that hating algebras with operators arise as a pair of functors, and moreover, we see that one of these functors is an inclusion. That's going to be the starting point of what comes next.

Logics for die-algebras can then be modeled in a similar way to logics for co-algebras. One approach there is to start with a dual junction between a category of spaces that we write as C and a category of

algebras. For example, spaces could be posets and algebras could be distributive lattices. Frames are then described by a functor T on the category of spaces, so T could be the upper powerset functor, and the logic is given by a functor L on the category of algebras together

with a natural transformation rho of type LP to PT that defines the interpretation. For die-algebras, we simply add two subcategories to the picture, C' and A' of C and A respectively, with inclusions I and J.

In our running example, C' could be the category of intuitunistic Cripky frames viewed as a subcategory of the category of posets, and A', the category of hating algebras, a subcategory of the category of distributive lattices. We also assume a

dual junction between C and A that restricts to the chosen subcategories, but we don't need to require that the restriction is again a dual junction. Frames are then defined by a functor T from C' to C,

for example the upper powerset functor that is sending a Cripky frame to a poset. Similarly, a logic is given by a functor L from A' to A, and we could for instance map a hating algebra A to the distributive

lattice generated by all boxed elements of A modulo the pertinent axioms. The last ingredient is a natural transformation rho of type LP' to PT. For the semantics, we assume an initial L, J

di-algebra that plays the role of syntax modular axioms, i.e. something like the Lindenbaum-Tarski algebra. We start with a given di-algebra gamma, where gamma maps Ix to Tx, and dualize this to P-gamma, which maps PTx to Pix.

Precomposition with rho at x then gives us the complex algebra of x, gamma, which is a di-algebra for the functors L and J. The assumed initiality of the Lindenbaum-Tarski di-algebra

then defines the interpretation. As a side remark, we just state that we can define both the functor L that defines the logic and the transformation rho that defines the semantics in terms of predicate liftings and axioms.

In our running example of box frames, we just need to define the natural transformation rho that determines the interpretation of the logic. In the definition, A is an upset and we map box A to the collection of all upsets that are contained in A.

The semantics is then the usual one where the interpretation of box phi are all those states where all relational successes satisfy the formula phi. This quotient is taken in the category of distributive

lattices so our logic can only contain axioms with connectives in the category in with distributive This quotient is taken in the category of distributive lattices so the axioms of our logic can only contain

distributive lattice connectives. Soundness of our setup is automatic by construction so let's have a look at completeness or rather the contraposition of completeness. Any two non-equivalent

formulae must be semantically distinguishable. This means that if we take any two distinct elements of the Linde-Beltarsky algebra, we need to find a die algebra on which they differ. And this is indeed our definition of completeness. The source of the

defining the interpretations is jointly monic. In instances what we'll find is that the source is jointly monic simply because we find one single monomorphism among all the interpretation maps. To establish completeness we're going to use general

frames. General frames are basically just standard frames together with a bunch of admissible predicates. In our die algebraic setting this means that we have a die algebra plus a sub object which for all intents and purposes we can think of as a sub algebra of

predicates over this given die algebra. So this sub object must have the property that we can make it into an LJ die algebra which means we need to be able to close it under the syntax such that this maps into the complex algebra gamma star

of our given die algebra X comma gamma. The filling that defines the algebra structure will be unique if the inclusion functor J reserves monos. If this is the case we can define a functor that we write upper plus that maps

general frames to L comma J die algebras. One thing that is not terribly deep is that if this functor has a section on objects we automatically get completeness. If we have such a section we have a general frame X comma gamma comma A such that

upper plusing this gives the initial die algebra psi that defines the syntax. But then the sub object A of predicates is equal to the set or of the object of formulae modulo equivalence and this

embeds into P prime X i.e. the algebra of all predicates. What we then see is that the induced map is necessarily the theory map and it is monic by construction. Therefore we get completeness. The question is now of course under

what conditions a section exists. One sufficient condition is the existence of a right inverse of a certain natural transformation that we've written as rho flat. If we were just dealing

with an adjunction and not an adjunction and two inclusions rho flat would be the adjoint mate of the natural transformation rho that defines the interpretation of a logic. If we look very closely at the diagram we see that the rightmost unit does not live in the right category. That means we have

to impose a very minor requirement that this unit actually restricts to amorphism in the chosen subcategory. In our running example of box frames it's not difficult to define a section of rho flat

so that completeness for box frames follows. Let's have a look at a different example and that is intuitunistic monotone modal logic. That is, we have intuitunistic propositional logic plus a box operator and we stipulate that

box is a monotone operator. The algebraic semantics for this logic is given by hating algebras with a monotone operator and they also arise as a category of di-algebras for a pair of functors M and J. J is the inclusion of hating

algebras into distributive lattices as before and M maps a hating algebra to the free distributive lattice generated by boxing all elements of the hating algebra and morning out by monotonicity. On the frame side we have a poset

X equipped with a collection of neighborhoods N of X for each X. These neighborhoods are required to be upsets and upclosed under inclusion. Moreover we require that the neighborhood functor N is compatible with the poset order.

These also arise as di-algebras for a pair of functors I and W where I is the inclusion of intuitunistic Cripky frames into posets and W takes a poset to upclosed collections of upclosed sets

ordered by inclusion. The interpretation of this logic is given by a natural transformation row of type M after upsets to upsets after W which is defined by mapping box A where A is an upset to the collection of all neighborhoods

that contain A as an element. To understand the type of row flat recall that we start out with the junction between distributive lattices and posets and one part of this junction is the prime filter functor. In the slide PF' is the restriction

of the prime filter functor to the category of hating algebras. With these preliminaries the type of row flat is W after prime filters prime to prime filters after M. A right inverse of row flat can be constructed with the

help of the prime filter lemma so that completeness also follows. There's a bunch of things that we haven't told you about but you can find them in the paper. We have more examples such as conditional intuitunistic logic and modal bi-intuitunistic logic.

We also have a couple more results concerning prime filter extensions and expressivity. Then there's also a bunch of things that we haven't told you because we simply don't know. One class of questions is which intuitunistic modal logics

we can capture in our framework. We would like to develop it further to be able to capture modal logics in the style of Fisher-Servey, Potkin and Stirling and Simpson and we would also like to be able to treat a larger class of base logics such as relevance logic or sub-intuitunistic

logic. For example, implicational meat semi-lattices. The question about examples that we can capture in our framework naturally leads to questions such as definability and star quest because the examples that we've

mentioned above require a slightly different set of axioms that we would like to be able to treat uniformly. And finally, one question is whether we can do away with the requirement that one of our functors in the definition of di-algebras is an inclusion.