Topological semantics of provability logic is well-known since the work of Harold Simmons and Leo Esakia in the 1970s. The diamond modality can be interpreted as a topological derivative operator acting on a scattered topological space. Although quite natural and complete, this semantics has not been much used in the study of provability logics because of the more convenient Kripke semantics. The situation turns out to be different for the polymodal provability logic GLP that has been applied to proof-theoretic analysis of Peano arithmetic. GLP is known to be incomplete w.r.t.\ any class of Kripke frames. We study natural topological models of GLP where modalities correspond to derivative operators on a polytopological space $(X,\tau_0,\tau_1,\dots)$. We call such a space \emph{GLP-space} if, for all $n$, topologies $\tau_n$ are scattered, $\tau_n\subseteq \tau_{n+1}$, and $d_n(A)$ is open in $\tau_{n+1}$, for any $A\subseteq X$. Here $d_n(A)$ denotes the set of limit points of $A$ w.r.t.\ topology $\tau_n$. GLP-spaces are exactly the spaces validating all the axioms of GLP. We show that GLP is complete w.r.t.\ the class of GLP-spaces (joint work with David Gabelaia). On the other hand, completeness w.r.t.\ natural ordinal GLP-spaces turns out to be dependent on large cardinal axioms of set theory and various facts on reflecting stationary sets. In particular, it is consistent (relative to ZFC) that GLP is incomplete. However, under the assumption of large cardinal axioms one can establish at least some partial completeness results. Under the assumption V=L we show that the bimodal fragment of GLP is complete w.r.t.\ the cardinal $\aleph_\omega$ (taken with the interval topology and the club filter topology).

This talk will review Leo Esakia's main contributions to intuitionistic and modal logics. It will also have biographical sketches of Leo Esakia, and will discuss his influence on several generations of Georgian (and non-Georgian) mathematicians, as well as his main mathematical interests, most of which are central to the TACL conference series.

One of the focal points of research at Leo Esakia's logic group in Tbilisi has been the topological interpretations of modal diamond first put forth my McKinsey and Tarski in the 1940s. In this talk I will survey this research area and report some recent results obtained by Leo Esakia, his students and colleagues. I will try to delineate the main trends, methods and constructions, as well as the remaining open problems in this line of research.

In this talk I will review recent results obtained by the Esakia school on intuitionistic modalities, which are motivated by topological, algebraic and categorical considerations. The resulting modalities arise on the lattices of open sets of topological spaces as coderivative operators (duals of the topological derivative). I will discuss algebraic properties of such operators arising from various classes of topological spaces.

Homotopy type theory refers to a new interpretation of Martin-Löf's system of intensional, constructive type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. In parallel, Vladimir Voevodsky (IAS) has recently proposed a comprehensive, computational foundation for mathematics based on this homotopical interpretation of type theory. The Univalent Foundations Program posits a new ``univalence axiom" relating propositional equality on the universe with homotopy equivalence of small types. The program is currently being implemented with the help of the automated proof assistant Coq. This talk will survey some of these recent developments.

Substructural logics are generalizations of classical and intuitionistic logic and they include among others relevance, many-valued, and linear logic. Their algebraic semantics are classes of residuated lattices, examples of which include Boolean algebras, Heyting algebras, lattice-ordered groups, ideal lattices of rings, and relation algebras. Residuated frames provide relational, Kripke-style, semantics for substructural logics. They differ from Kripke frames for modal and intuitionistic logic in that they are not based on distributive logics (so two sets of worlds need to be considered) and in that the accessibility relation is ternary. The apparent complexity of the structure does not allow direct combinatorial manipulation of the frames as in modal and intuitionistic logic. However, the generality of residuated frames essentially encompasses proof theory, and proof-theoretic tools can be extended and applied to residuated frames yielding results on both logic and algebra. Moreover, they provide a way to organize and generalize proof-theoretic systems (from sequents to hypersequents and beyond) in view of a hierarchy of formulas. We will first survey the above in a historically inaccurate but pedagogically instructive and very accessible way, showing how they can all be derived in a natural fashion from simple algebraic properties of residuated lattices. Having obtained a deep and fundamental algebraic understanding of the substructural hierarchy and of residuated frames, we will show how to relativize the hierarchy to the involutive and to the distributive cases and we will obtain two new applications of the theory. (Partly based on joint work with A. Ciabattoni and K. Terui, and with P. Jipsen)

Why do so many representation problems in algebra, enjoying positive solutions in the finite case, have counterexamples of minimal cardinality either aleph 0, aleph 1, aleph 2 and no other cardinality? By a representation problem, we mean that we are given two functors with the same codomain, and we compare there range. We also assume that the involved categories are equipped with a notion of ``cardinality''. Examples of such representation problems cover various fields of mathematics. Here are a few examples, among many: (1) Every (at most) countable Boolean algebra is generated by a chain, but not every Boolean algebra is generated by a chain. (2) Every dimension group with at most aleph 1 elements is isomorphic to K0(R) for some (von Neumann) regular ring R (G.A. Elliott 1976 for the countable case, then K.R. Goodearl and D.E. Handelman 1986), but there is a dimension group with aleph 2 elements which is not isomorphic to K0(R) for any regular ring R (F. Wehrung, 1998). (3) Every distributive algebraic lattice with at most aleph 1 compact elements is isomorphic to the congruence lattice of some lattice (A.P. Huhn, 1989), but not every distributive algebraic lattice is isomorphic to the congruence lattice of some lattice (F. Wehrung 2007); the minimal number of compact elements in a counterexample is aleph 2 (Růžička, 2008). J. Tůma and F. Wehrung introduced in 2002 a particular case of the kind of representation problem considered above, concentrated in the notion of critical point between two varieties of (universal) algebras. The critical point is related to the following statement: (*) For each algebra in the first variety there is an algebra in the second variety with the same congruence lattice. If (*) does not hold for two varieties, the critical point is the minimal number of compact congruences of a counterexample. For example, the critical point between the variety of all lattices and the variety of all groups is aleph 2 (P. Růžička, J. Tůma, and F. Wehrung, 2007). The critical point between variety of all majority algebras and the variety of all lattices is aleph 2 (M. Ploščica, 2009). In this talk we shall study the case where both varieties are locally finite, and the second variety satisfies a "smallness" condition, which turn out to be satisfied if the variety is finitely generated and congruence-modular. Under this conditions either (*) is satisfied, or the critical point is at most aleph 2. We shall also show that in the case of varieties of lattices, the local finiteness assumption can be dropped modulo a rather weak assumption on the simple members of the second variety, moreover, under that assumption, the containment between two congruence classes can occur only for the obvious reason (namely, the first variety is contained in either the second variety or its dual variety).

Quasi-metrics are just like metrics, except you don't require the distance from x to y to be the same as from y to x: think of distance as measuring the effort it takes to go from x to y, and comparing climbing up and down a mountain. I'll show that several classic results in the theory of metric spaces transfer to quasi-metric spaces---with some complications. And I'd like to mention some of the results that please me most: 1. Completeness splits into two notions, a strong one (Smyth completeness) and a weak one (Yoneda completeness, due to Rutten, Bonsangue, and van Breugel), but both can be characterized elegantly through the notion of formal balls, as shown by Kostanek-Waszkiewicz and by Romaguera-Vallero, both in 2010. My contribution here will be in a simpler presentation of the Romaguera-Vallero Theorem, using Erné's notion of c-space and sobriety (equivalently, the domain-theoretic notion of abstract bases, and rounded ideal completion). 2. The space of probability distributions on a quasi-metric space is itself quasi-metric, and I'll mention a quasi-metric form of the Kantorovitch-Rubinstein theorem, itself an infinite version of linear programming duality. 3. Generalizing the Kantorovitch-Hutchinson metric, one can compare states from infinite-state 2 player turn-based stochastic games, in such a way that close states yield close values of the (min-, max-) expected payoff. This is called a simulation distance. 4. There is a simple modal logic, interpreted on the latter games, which characterizes similarity, and simulation distances. I only have a modest contribution in Item 1. Items 2 and 3 are from one of my papers at FOSSACS'08. Item 4 is new.

Solving equations has long featured as a main item in the mathematician's agenda, at the very least since Diophantus' {\it Arithmetica} appeared. Unification is the modern version of the quest for general solutions to systems of equations within a class of domains. If the class in question is equationally definable, one speaks of unification modulo an equational theory. A straightforward universal-algebraic reformulation shows that, in this case, one is really concerned with solving equations in a given variety of algebras. A tight connection between unification problems in a variety and finitely presented projective objects in the variety was established by Ghilardi in 1997. When coupled with Gabriel's and Ulmer's 1971 categorial abstraction of finitely presentable object, Ghilardi's work extends the scope of the theory of unification to all locally small categories. What tools do we have to understand the structure of the set of solutions to a unification problem in such general contexts, or even just in varieties of algebras? I argue that key insights can usually be gained by dualising the problem --- provided, of course, that an efficient description of the dual category is available. I support this claim with selected examples where such a description is known, including Boolean algebras, distributive lattices, rings, and MV-algebras. (The featured talk by Luca Spada discusses unification for MV-algebras in greater detail.) Through these case studies, an interesting pattern begins to emerge. Stepping from syntax to semantics through the looking-glass provided by a duality theory allows to develop an analogy between the structure of the set of solutions to a unification problem, and such homotopy-theoretic notions as the universal covering space of a sufficiently connected topological space. I discuss some preliminary results indicating that this analogy may indeed be fruitful.

Abstract: Quantales are ordered algebras which can be thought of as pointfree noncommutative topologies. In recent years, their connections have been studied with fundamental notions in noncommutative geometry such as groupoids and C*-algebras, in the framework of a research program aimed at establishing noncommutative counterparts of the Gelfand-Naimark duality. In this framework, groupoids play the role of noncommutative spaces. The setting of (unital involutive) quantales corresponding to étale groupoids has been very well understood: a bijective correspondence has been defined by Pedro Resende between localic étale groupoids and inverse quantale frames. We present an equivalent but independent way of defining this correspondence for topological étale groupoids, and we extend this bijective correspondence to a setting of non-étale groupoids, the quantale counterpart of which is given by the axiomatically defined SGF-quantales. Dropping the étale restriction allows this theory to be extended to interesting families of groupoids, such as those arising as equivalence relations induced by group actions with fixed points. Quantales can also be understood as algebraic models for the logical theory of binary relations on an intuitionistic base. As such, they are akin to relation algebras, the representation theory of which has been studied by Jónsson and Tarski in the `B side' of their more famous paper on Boolean algebras with operators. Interestingly, Jónsson and Tarski's representation theorems embed relation algebras into those relation algebras arising as `complex algebras' of groupoids. We establish the quantale-theoretic counterparts of these results: we give a purely algebraic characterization of those quantales arising as `complex algebras' of groupoids, show that every SGF-quantale can be optimally embedded into one of these; finally, we characterize the unital involutive quantales which arise as `complex algebras' of equivalence relations (seen as groupoids). [PR11b] A. Palmigiano, R. Re, Relational representation of groupoid quantales, to appear in Order, DOI 10.1007/s11083-011-9227-z. [PR11a] A. Palmigiano, R. Re, Groupoid quantales: a non-étale setting, Journal of Pure and Applied Algebra, 215: 8 (2011), 1945-1957.

After revisiting the basic ideas of Krivine's classical realizability we give an algebraic reformulation of the basic ingredients by identifying the notion of an Abstract Krivine Structure (aks). Such structures may be understood as an extension of combinatory logic by stacks (i.e continuations) and control operators. We prove that in a precise sense Cohen forcing is the commutative case of classical realizability. Further, we show how classical realizability over an arbitrary aks gives rise to a ``classical realizability tripos'' this way subsuming Krivine's highly original work in more traditional terms, namely the categorical account of realizability as originated by Martin Hyland's work in the early 1980s. Finally, we sketch how to build forcing models on top of classical realizability and how such a 2 step construction can be understood as a single classical realizability construction. This is a necessary requirement for building classical models of ZF validating stronger and stronger choice principles.

The aim of my paper will be to review the idea of a dependently sorted logic and the notion of a type setup for dependently sorted logic and introduce the notion of a generalised type setup.

Languages and families of binary relations are standard interpretations of Kleene algebras. It is known that the equational theories of these interpretations coincide. We investigate the identities valid in these interpretations when we expand the signature of Kleene algebras with the meet operation. In both cases meet is interpreted as intersection. We show that there are more identities valid in language algebras than in relational algebras (exactly three more in some sense). We also look at the picture when we exclude the identity from the signature. We prove that in this case the equational theories of the two kinds of interpretations coincide again.

We present an abstract unifying framework for interpreting Stone-type dualities; several known dualities are seen to be instances of just one topos-theoretic phenomenon, and new dualities are introduced. In fact, infinitely many new dualities between preordered structures and locales or topological spaces can be generated through our topos-theoretic machinery in a uniform way. We then apply our topos-theoretic interpretation to obtain results connecting properties of preorders and properties of the corresponding locales or topological spaces, and we establish adjunctions between various kinds of categories as natural applications of our general methodology.

We present a Sahlqvist theorem for non-distributive modal logics, i.e., logics with algebraic semantics based on arbitrary lattices with operators. We identify the appropriate extension of the Sahlqvist and inductive inequalities to this more general setting. The proof of the canonicity and elementarity of these inequalities takes the shape of an algorithm (called ND-ALBA) which tries to eliminate variables from the inequality replacing them, if possible, with special variables ranging only over the completely join- and meet-irreducible elements of perfect lattices. These special elements are the states and the co-states of the relational structure which is dual to the perfect lattice, and of which the given perfect lattice is the ``complex algebra''. It can be shown that ND-ALBA is correct and that all inequalities on which it terminates successfully are elementary and canonical.

In this paper we describe a generalization of the notion of canonical extension of distributive lattices to coherent categories. We start by discussing earlier work on this topic by Magnan & Reyes and Butz, which both point to Makkai's topos of types construction as the natural categorical generalization of canonical extension. Thereafter we will give an alternative description of this topos of types, using the correspondence between coherent categories and polyadic distributive lattices.

In this paper, we propose a new approach to topological duality theory for arbitrary lattices, which uses the canonical extension as the prime source.

The semantics of recursion is usually described by fixed points of functions, functors, or other constructors. Least fixed points of monotone or continuous functions on cpo's or complete lattices have been widely used to give semantics to functional programs and various programming logics such as the $\mu$-calculus.The parameterized least fixed point operation $^\dagger$, in conjunction with function composition and the cartesian operations (or Lawvere theory operations) and the binary supremum operation satisfies several nontrivial equations, such as the well-known De Bakker-Scott-Bekic equation. One would naturally like to have a complete description of all valid (in)equations in the form of a system of axioms. Our aim in this paper is to provide such complete descriptions.

We present a generalization of Permutative logic (PL) which is a non-commutative variant of Linear logic suggested by some topological investigations on the geometry of linear proofs. The original logical status based on a variety-presentation framework is simplified by extending the notion of q-permutation to the one of pq-permutation. Whereas PL is limited to orientable structures, we characterize the whole range of topological surfaces, orientable as well as non-orientable. The system we obtain is a surface calculus that enjoys both cut elimination and focussing properties and comes with a natural phase semantics whenever explicit context is considered.

If a subvariety of BL is generated by a set of stanard BL-algebras, then it is generated by a finite set of standard BL-algebras.

The problems considered in this paper originate in recent applications of large scale ontologies in medicine and other life sciences. The profile OWL2EL of the OWL2 Web Ontology Language, used for this purpose, is based on the description logic EL. The syntactic terms of EL, called concepts, are interpreted as sets in first-order relational models. From a modal logic point of view, concepts are modal formulas constructed from propositional variables and the constants for top and bottom using conjunction and diamonds. An EL-theory is a set of inclusions (or implications) between such concepts, and the main reasoning problem in applications of EL in life sciences is to decide whether an EL-theory entails a concept inclusion when interpreted over a class of relational structures satisfying certain constraints on its binary relations. Standard constraints in OWL2EL are transitivity and reflexivity, for which reasoning in EL is Ptime-complete, as well as symmetry and functionality, for which reasoning is ExpTime-complete. As in modal logic, apart from reasoning over relational models, one can try to develop a purely syntactical reasoning machinery using a calculus. In other words, we can define a more general algebraic semantics for EL: the underlying algebras are bounded meet-semilattices with monotone operators (SLOs, for short), constraints are given by equational theories of SLOs, and the reasoning problem is validity of quasi-equations in such equational theories. The resulting more general entailment problem is not necessarily complete with respect to the `intended' relational semantics. This paper presents our initial results in an attempt to clarify which equational theories of SLOs are complete in this sense and which are not. We also prove that the completeness problem -given a finitely axiomatised equational theory of SLOs, decide whether it is complete with respect to the relational semantics- is algorithmically undecidable, which establishes a principle limitation regarding possible answers to our research question.

We show that the unification type of Lukasiewicz (infinite-valued propositional) logic and of its equivalent algebraic semantics, the variety of MV-algebras, is nullary. The proof rests upon Ghilardi's algebraic characterisation of unification types in terms of projective objects, recent progress by Cabrer and Mundici in the investigation of projective MV-algebras, the categorical duality between finitely presented MV-algebras and rational polyhedra, and, finally, a homotopy-theoretic argument that exploits lifts of continuous maps to the universal covering space of the circle.

Grätzer asked in 1971 for a characterization of sublattices of Tamari lattices (associahedra). A natural candidate was coined by McKenzie in 1972 with the notion of a bounded homomorphic image of a free lattice--in short, bounded lattice. Urquhart proved in 1978 that every associahedron is bounded (thus so are its sublattices). Geyer conjectured in 1994 that every finite bounded lattice embeds into some associahedron. We disprove Geyer's conjecture, by introducing an infinite collection of lattice-theoretical identities that hold in every associahedron, but not in every finite bounded lattice. Among those finite counterexamples, there are the permutohedron on four letters P(4), and in fact two of its subdirectly irreducible retracts, which are Cambrian lattices of type A. For natural numbers m and n, we denote by B(m,n) the (bounded) lattice obtained by doubling a join of m atoms in an (m+n)-atom Boolean lattice. We prove that B(m,n) embeds into an associahedron iff min{m,n} <= 1, and that B(m,n) embeds into a permutohedron iff min{m,n} <= 2. In particular, B(3,3) cannot be embedded into any permutohedron. Nevertheless we prove that B(3,3) is a homomorphic image of a sublattice of the permutohedron on 12 letters.

Closure system on a finite set is a unifying concept in logic programming, relational data bases and knowledge systems. It can also be presented in the terms of finite lattices, and the tools of economic description of a finite lattice have long existed in lattice theory. We present this approach by describing the so-called D-basis and introducing the concept of ordered direct basis of an implicational system. The direct basis of a closure operator, or an implicational system, is the set of implications that allows one to compute the closure of arbitrary set by a single application of each implication. This property is preserved by D-basis at the cost of following a prescribed order in which implications will be applied. In particular, this allows us to optimize the forward chaining procedure in logic programming that uses the Horn fragment of propositional logic. We show that one can extract the D-basis from any direct unit basis S in time polynomial of |S|, and it takes only linear time of the size of D-basis to put it into a proper order. We find examples of closure systems on 6-element set whose canonical basis of Guiques-Duquenne is not ordered direct.

A convex geometry is a closure space with the anti-exchange axiom. For several types of algebraic convex geometries we describe when they are order scattered, in terms of obstructions to the semilattice of compact elements. The connection to topological scatterdness is established in convex geometries of relatively convex sets.

The logic CSL (first introduced by Sheremet, Tishkovsky, Wolter and Zakharyaschev in 2005) allows one to reason about distance comparison within a modal language. The logic can express assertions of the kind "A is closer/more similar to B than to C" and has a natural application to spatial reasoning, generalizing the well known S4u. The semantics of CSL is defined in terms of models based on different classes of distance spaces. In this paper we do a quick survey of the properties of CSL, as well as its axiomatizations. We then propose an alternative semantics, based on preferential spaces similar to the ones used for some conditional logics, closer to the traditional modal semantics. We show that this semantics always have the small model property, and briefly discuss some remaining open problems.

We address the problem of combining logics along general translations by introducing techniques from abstract homotopy theory. We replace the usual colimit constructions by homotopy colimits, which subsume the former in good cases and have better properties in general. We show that a variety of settings for abstract logic falls under the framework of ABC cofibration categories which allow easy calculation of homotopy colimits and recognizing metaproperties of combined logics from their constituent logics, as it works for usual fibring. Finally we address further homotopical perspectives on abstract logic.

Extending concept lattices to protoconcept algebras and semiconcept algebras, [Herrmann et al 2000] and [Wille 2000] introduced negations in conceptual structures based on formal contexts such as double Boolean algebras. These algebras have attracted interest for their theoretical merits - basic representations have been obtained [Herrmann et al 2000 ; Wille 2000] - and their practical relevance - applications in the field of knowledge representation have been developed [Priss 2006 ; Stumme 2002]. This interest motivated [Vormbrock 2007] to attack the word problem (WP) in protoconcept algebras and to demonstrate that given terms s,t, if s=t is not valid in all protoconcept algebras then there exists a finite protoconcept algebra in which s=t is not valid. Nevertheless, the upper bound on the size of the finite protoconcept algebra given in [Vormbrock 2007] is not elementary. Switching over to semiconcept algebras, our aim is to prove that the WP in semiconcept algebras is PSPACE-complete.

In this paper we give a topology over a set of knowledge states, providing a possible description of Learning in the Limit in the sense of Gold, both monotonic and non-monotonic. We want to explore the possibility of a quite general description of the original Gold's approach, by giving a topology over a set of individual we call \answers", a topology which is directly motivated by the concept of learning. The topology we have in mind is an extension of Scott's topology, akin to Lawson topology but more general than it.

We define Sahlqvist fixed point formulas and present completeness and correspondence results for modal fixed point logics axiomatized by these formulas for LFP-definable classes of general mu-frames. We also define modal mu*-algebras and show that Sahlqvist fixed point formulas are preserved under completions of conjugated modal mu*-algebras.

We present new results in theory of the pseudo hoops. Namely, we show that any pseudo hoop satisfy Riesz decomposition property, we introduce new visualization of structures and finally we characterize a class of normal valued basic pseudohoops as an equational theory.

In this paper we present a procedure that given a unification problem in the equational theory of Distributive Lattice or Kleene algebras it determines if it is unitary, finitary or nullary.

Algebraic axiomatization of the classical propositional calculus is provided via Boolean algebras, i.e. bounded distributive lattices with complementation. However, not every reasoning may be described by means of the classical two-valued logic. In particular, two important cases can be men- tioned. At first, it is the logic of quantum mechanics where the logical law of excluded middle fails. This caused that, contrary to the classical logic, the induced lattice need not be distributive although the negation is still a com- plementation. In 1940's, G. Birkhoff and J. von Neumann found out that the appropriate algebraic tool for axiomatizing this logic are orthomodular lattices. Another important class of non-classical logics having numerous applications are many-valued logics. In particular, the Lukasiewicz many-valued logic is of interest due to the fact that it is a fuzzy logic which is applied in numerous technical devices (e.g. fuzzy regulators, fuzzy control systems etc.). It was recognized by C. C. Chang in the 1950's that the appropri- ate tool for axiomatizing many-valued Lukasiewicz logics are the so-called MV-algebras. The mentioned examples of non-classical logics motivated us to find a basic tool which is common to all of them. As we have already mentioned, the logic of quantum mechanics is axiomatized by a lattice which is complemented but not necessarily distributive. It turns out that MV-algebras induce bounded lattices which are distributive and the logical connective negation is realized by an antitone involution which need not be a comple- mentation. Hence, it is natural to search for a common algebraic structure among non necessarily distributive bounded lattices equipped with an anti- tone involution. Having a bounded lattice L, for every element a of L the interval [a; 1] is called a section. We say that L is endowed by section antitone involutions if for every a of L there exists an antitone involution on [a; 1]. Hence, there exist so many antitone involutions as many elements the lattice L has. It is easy to check that if L is an orthomodular lattice then L has section antitone involutions. Now we turn our attention to MV-algebras. The induced lattice L(A) is distributive and the mapping x to neg x + a is an antitone involution on the section [a; 1] (which need not be a complementation). Comparing the induced lattice of an MV-algebra with an orthomodular lattice, we can see that both of them are lattices with section antitone invo- lutions which differ in the properties that these involutions are complementations but the lattice need not be distributive in the first case but the lattice is distributive and the involutions need not be complementations in the second case. We conclude that the common base of algebraic axiomatization of the logic of quantum mechanics as well as of many-valued Lukasiewicz logic are bounded lattices with section antitone involutions. Although these lattices are very useful tools for computations, a formal disadvantage is that they are not of the same type since the number of unary operations (section antitone involutions) depends on the number of elements of the lattice. To avoid this difficulty, we introduce the concept of basic algebra.

The concept of a relatively pseudocomplemented directoid was introduced recently by the first author. It was shown that the class of relatively pseudocomplemented directoids forms a variety whose axiom system contains seven identities. Our aim is three-fold. First we show that these identities are not independent and their independent subset is presented. Second, we modify the adjointness property known for relatively pseudocomplemented semilattices in the way which is suitable for relatively pseudocomplemented directoids. Hence, they can also be considered as residuated structures in a rather modified version. We also get two important congruence properties, namely congruence distributivity and 3-permutability valid in the variety V of relatively pseudocomplemented directoids. Then we show some basic results connected with subdirect irreducibility in V. Finally, we show another way how to introduce pseudocomplementation on directoids via relative pseudocomplementation.

In this talk, we will present the generalized Jónsson–Tarski duality between Vietors coalgebras and modal algebras over stably locally compact spaces and the corresponding frames by general Stone duality. We also build the canonical representation concretely as the final Vietoris coalgebra and extend the duality to Vietoris polynomial functors.

Presheaf semantics [Osius, 1975, Fourman and Scott, 1979, Mac Lane and Moerdijk, 1992] is one of the most natural semantics for intuitionistic predicate logic. Although completeness for this semantics is known, it is usually obtained indirectly, e.g. via categorical equivalences with omega-models as in [Troelstra and Van Dalen, 1988], while a direct completeness proof seems to be absent in the literature. We describe a simple canonical model construction which allows us to prove completeness in a direct way. Moreover (unlike, for instance, the completeness proofs known for Kripke semantics) the proof presented here is totally constructive.

This paper is a contribution to the theory of substructural logics. We introduce the notions of (MP)-based} and almost (MP)-based} logics (w.r.t. a special set of formulae D), which leads to an alternative proof of the well-known forms of the local deduction theorems for prominent substructural logics (FL, FLe, FLew, etc.). Roughly speaking, we decompose the proof of the local deduction theorem into the trivial part, which works almost classically, and the non-trivial part of determining with respect to which set (if any) the logic is almost (MP)-based. We can also show connection of (almost) (MP)-based condition and the proof by cases properties for generalized disjunctions and the description of (deductive) filters generated by some elements of a given algebra. In order to provide as general theory as possible, i.e., to cover more logics than the usual Ono's definition of substructural logics (i.e. axiomatic extensions of the logic of pointed residuated lattices) we propose a more general notion of substructural logic based on a very weak system lacking not only structural rules, but also associativity of multiplicative conjunction, and consider all its (even non-axiomatic) extensions, expansions (by new connectives), and well-behaved fragments thereof. This defines a wide family of logical systems containing pretty much all prominent substructural logics.

We describe a uniform construction of finitely generated free algebras for classes of algebras axiomatized by quasi-equations of rank 0,1.

Augmented posets and (Z1,Z2)-complete posets are two different approaches to the classification of posets with specified joins and meets. The main purpose of this talk is to reveal the relations between these approaches. In particular, it is pointed out that spatiality and sobriety in one of these approaches are closely linked with the corresponding notions in another approach. In addition to this, we will formulate a Stone-type duality for (Z1,Z2)-complete posets, and derive it from an analogous duality, proven by Banaschewski and Bruns, for augmented posets.

We give a finite axiomatisation to representable ordered domain algebras and show that finite algebras are representable on finite bases.

We show that given a finite, transitive and reflexive Kripke frame and w in W, the property of being simulated by w (i.e., lying on the image of a literal-preserving relation satisfying the `forth' condition of bisimulation) is modally undefinable within the class of S4 Kripke models. Note the contrast to the fact that lying in the image of w under a bisimulation is definable in the standard modal language even over the class of K4 models. We then propose a minor extension of the language adding a sequent operator (`tangle') which can be interpreted over Kripke models as well as over topological spaces. Over finite Kripke models it indicates the existence of clusters satisfying a specified set of formulas, very similar to an operator introduced by Dawar and Otto. In the extended language L+, being simulated by a point on a finite S4 model becomes definable over the class of all topological models. As a consequence of this we obtain the result that any class of finite S4 models over finitely many propositional variables which is closed under simulability is also definable in L+, as well as Boolean combinations of these classes. From this it follows that the mu-calculus interpreted over any such class of models is decidable.

Pseudoeffect algebras are partial algebraic structures which are non-commutative generalizations of effect algebras. The main result of the paper is a characterization of lattice pseudoeffect algebras in terms of so-called pseudo Sasaki algebras. In contrast to pseudoeffect algebras, pseudo Sasaki algebras are total algebras. They are obtained as a generalization of Sasaki algebras, which in turn characterize lattice effect algebras. Moreover, it is shown that lattice pseudoeffect algebras are a special case of double CI-posets, which are algebraic structures with two pairs of residuated operations, and which can be considered as generalizations of residuated posets. For instance, a lattice ordered pseudoeffect algebra, regarded as a double CI-poset, becomes a residuated poset if and only if it is a pseudo MV-algebra. It is also shown that an arbitrary pseudoeffect algebra can be described as a special case of conditional double CI-poset, in which case the two pairs of residuated operations are only partially defined.

The theory of canonical exensions is an important tool in algebraic logic. We discuss several universal properties of canonical extensions, which relate them to domain theory and topological algebra. In particular, we show that the canonical extension of a lattice can be given a dcpo presentation, and that canonical extensions have universal properties with respect to profinite and certain Boolean topological lattice-based algebras.

The work we present here was motivated by recent results obtained for lattice-based algebras in finitely generated varieties. Those results reconcile canonical, natural and profinite extensions of the algebras. They were obtained by several authors such as Gehrke and Harding, for canonical extensions, Harding, for profinite limits, and Davey, Gouveia, Haviar and Priestley, for natural extensions. We apply some of those results to join-semilattices with 0 to show how their canonical extensions can be obtained from their profinite extensions.

A description of finitely generated free algebras over the variety of Solovay algebras, as well as over its pyramid locally finite subvarieties is given. Particulary we highlight the free algebra with one free variable.

In analogy to the situation for continuous lattices which were introduced by Dana Scott as precisely the injective T0 spaces via the (nowadays called) Scott topology, we study those metric spaces which correspond to injective T0 approach spaces and characterise them as precisely the continuous lattices equipped with an unitary and associative [0,infty]-action. This result is achieved by a detailed analysis of the notion of cocompleteness for approach spaces.

In analogy to the situation for ordered compact Hausdorff spaces which are precisely the stably compact spaces, we introduce the notion of metric compact Hausdorff spaces as triple (X,d,c), where d is a metric on X and c is a convergence relation of a compact Hausdorff space. Then we show that they correspond to the class of approach spaces, stably compact approach spaces, which are sober, +-exponentiable and stable.

The aim of our talk is to characterize non-associative BL-algebras by the language of quantum structures.

The graphical games of Delande and Miller and Hirschowitz have been used in proof search and provability. This work obtains a first proof theoretical result using them. We define games for Multiplicative Linear Logic with units (MLL) over a set A of atomic propositions. We then construct a category of plays G(A), using a new method based on (i) a category P containing plays as particular morphisms, (ii) a stack (a weak variant of sheaves) of plays, with amalgamation in the stack implementing parallel composition, (iii) a factorisation system on P, which we use to implement hiding. We finally prove that G(A) is the free split *-autonomous category over A.

The implicative-group (the partially-ordered (lattice-ordered) implicative-group) is a term equivalent definition of the group (the partially-ordered (lattice-ordered) group, respectively). We study the normal filters/ideals and the compatible deductive systems, the representability of some of the involved algebras and we establish other ``vertical" connections between the group level and the algebras of logic level.

For any two logics over S4, if one of them is not tabular and another is not maximal, then the power of the lattice of their extensions is continuum.

Commutative partially ordered monoids will be referred to as uninorms. Our aim is to investigate involutive uninorms. Our main question is the following: in an involutive FLe-algebra, how far its uninorm (or its algebraic structure, in general) is determined by its “local behavior”, i.e., its underlying t-norm and t-conorm. An answer to this question is presented for a particular case on [0,1] with t = f, which will illustrate our background idea. It says that the uninorm is determined uniquely by any of them, i.e., either by the t-norm or by the t-conorm. In fact, the t-norm and the t-conorm are determined by each other, in this case. Then, a natural question is how far we can extend this, and when the uninorm is determined uniquely? Our main goal is to give an answer to this question: Uniqueness is guaranteed and moreover, the uninorm is represented by the twin-rotation construction whenever the algebra is conic. To have a closer look at the situation, then we consider involutive FLe-algebras which are finite and linearly ordered. As a byproduct it follows that the logic IUL extended by the axiom t ↔ f does not have the finite model property.

In this paper we define a bi-topological space on an interval of ordinals that is sound and complete for the closed fragment of GLB. This result sharply contrasts the existence of topological ordinal spaces for full GLB which is known to be independent of ZFC.

In this short paper we give an algorithmic criterion of modal definability of a Horn formula in terms of its graph. As a consequence we obtain that every modal logic axiomatized by a single Horn formula is Kripke complete.

The Craig interpolation property (CIP) and other related properties are considered in the case of the logics from NEXT(KTB), where KTB is the so-called Brouwerian modal logic. It is proven that n-transitive logics (with n>1) have (CIP). On the other hand, an uncountable family of logics without (CIP) is constructed. The logics are determined by wheel-frames.

Every frame with a given open subframe extends to a stably supported quantale.

We present two refinements of the classical Stone duality between generalized Boolean algebras and locally compact Boolean spaces to dualities between left-handed skew Boolean algebras and étale spaces over locally compact Boolean spaces. We also apply our results to construct a series of adjunctions between the category of generalized Boolean algebras and the category of left-handed skew Boolean algebras.

We study divisible and n-potent pseudo-BCK-algebras that are the residuation subreducts of integral residuated lattices.

We prove Finite Embeddability Property (FEP) of the class of residuated groupoids with modal operators，satisfying standard S4-axioms (4, T), and distributive lattice operations. The key tool is an interpolation lemma adapted to S4-systems.

In this paper, we start studying epistemic updates using the standard toolkit of duality theory. We focus on public announcements, which are the simplest epistemic actions, and hence on single-agent (but the results straightforwardly extend to the multi-agent setting). Public Announcement Logic (PAL) without the common knowledge operator. As is well known, the epistemic action of publicly announcing a given proposition is semantically represented as a process of relativization of the model encoding the current epistemic setup of the given agents; from the given model to its submodel relativized to the announced proposition. We give the dual characterization of the corresponding submodel-injection map, as a certain pseudo-quotient map between the complex algebras respectively associated with the given model and with its relativized submodel. As is well known, these complex algebras are complete atomic BAOs (Boolean algebras with operators). The dual characterization we provide naturally generalizes to much wider classes of algebras, which include, but are not limited to, arbitrary BAOs and arbitrary modal expansions of Heyting algebras (HAOs). In this way, we access the benefits and the wider scope of applications given by a point-free, intuitionistic theory of epistemic updates. As an application of this dual characterization, we axiomatize the intuitionistic analogue of PAL, which we refer to as IPAL, and prove soundness and completeness of IPAL w.r.t. both algebraic and relational models.

Extensions of the Johansson minimal logic are investigated. Representation theorems for well-composed logics with the Graig interpolation property CIP, restricted interpolation property IPR and projective Beth property PBP are stated. It is proved that PBP is equivalent to IPR for any well-composed logic, and there are only finitely many well-composed logics with CIP, IPR or PBP.

The present work provides the first steps of a project of considering categories of logical systems satisfying simultaneously certain natural requirements such as: (i) If they represent the majority part of the usual logical systems; (ii) If they have good categorial properties (e.g., if they are a complete and/or cocomplete category, if they are accessible categories); (iii) If they allow a natural notion of algebraizable logical system (as in the concept of Blok-Pigozzi algebraizable logic or Czelakowski's proto-algebraizability; (iv) If they provide a satisfactory treatment of the identity problem of logical systems (when logics can be considered "the same"?).

Based on the concept of structure dualizability, we extend the theory of natural dualities so as to encompass Jonsson-Tarski's topological and Kupke-Kurz-Venema's coalgebraic dualities for (all) modal algebras, and Esakia duality for (all) Heyting algebras. Since natural duality theory is closely related to many-valued logics, we also provide applications of our theory to modal and intuitionistic many-valued logics.

In this talk, we are concerend with dualities between set-theoretic, point-based spaces (e.g., topological space, convexity space, and measurable space) and algebraic, point-free spaces (e.g., frame, continuous lattice, and sigma-complete Boolean algebra). We first develop a moderately general theory of dual adjunctions between them, then apply it to the case of Scott's continuous lattices (seen as point-free convex structures) and convexity spaces, and analyze in detail the resulting dual adjunction between them to obtain deeper insights that cannot be derived from a neat, general theory. In the process, we exploit the concrete-categorical concepts of a functor-structured category and topological axioms in it.

We give a categorical axiomatization of cut elimination in classical logic, interpreting proofs in a hyperdoctrine-like ca.tegory in which the fibres are Fuhrmann and Pym's classical categories: categories enriched with a partial order structure interpreting cut-elimination in propositional classical logic.

The admissible rules of a quasivariety may be understood as the quasiequations that hold in its free algebra on countably many generators, and the quasivariety is said to be structurally complete if it is generated as a quasivariety by this free algebra. Similarly, multiple-conclusion rules are implications between finite sets of equations that are admissible if a corresponding universal formula holds in the free algebra on countably many generators, and the quasivariety is said to be universally complete if generated as a universal class by this free algebra. Examples will be provided of interesting admissible rules and quasivarieties that are or fail to be structurally complete or universally complete. Moreover, necessary and sufficient embedding conditions are given for a quasivariety generated by a finite algebra to be structurally complete and universally complete.

We discuss an algebraic aspect of logic KM. Introducing enrichment of elements of a Heyting algebra to make the latter a KM-algebra, we prove that every element of an initial Heyting algebra can be enriched uniquely up to isomorphism. This work is an attempt in progress to give an algebraic proof of Kuznetsov's theorem that intuitionistic propositional logic and KM are deductively equipollent.

Generalizations of Boolean algebras as carriers of probability measures are (lattice) effect algebras. They are a common generalization of MV-algebras and orthomodular lattices. In the present paper, we continue the study of homogeneous effect algebras. This class of effect algebras includes orthoalgebras, lattice ordered effect algebras and effect algebras satisfying the Riesz decomposition property. It was proved that every homogeneous effect algebra is a union of its blocks, which are defined as maximal sub-effect algebras satisfying the Riesz decomposition property. J. Tkadlec introduced the so-called property (W+) as a common generalization of orthocomplete and lattice effect algebras. The aim of our paper is to show that every block of an Archimedean homogeneous effect algebra satisfying the property (W+) is lattice ordered. Therefore, any Archimedean homogeneous effect algebra satisfying the property (W+) is covered by MV-algebras. As a corollary, this yields that every block of a homogeneous orthocomplete effect algebra is lattice ordered. As a by-product of our study we extend the results on sharp and meager elements into the realm of Archimedean homogeneous effect algebras satisfying the property (W+).

We develop a theory of proof nets for propositional classical logic where the usual "axiom link" structure is defined by maps in the free Frobenius category on one generator. We give a correctness criterion for two different sequent calculi and we discuss the issue of cut elimination.

The Reiterman isomorphism is extended onto the family of all polymeric categories. This will provide an important step for the proof of algebraicity of all varieties.

We solve two problems concerning the compact congruences of an algebra.

We develop a Priestley-style duality theory for bilattices and some related algebras. This topic has already been investigated by Mobasher et al., but only from an abstract category-theoretic point of view. Here instead we are interested in a concrete study of the topological spaces that correspond to the these algebraic structures.

We introduce the concept of MV-topology, an MV-algebra-based generalization of general topology to fuzzy subsets, and we prove a proper extension of Stone duality to, respectively, semisimple MV-algebras and a suitable category of MV-topologies.

Lattices of multipermutations L(v), v in N^d, generalize the weak Bruhat order on permutations. For d_0 fixed, lattices L(v) with v in N^d_0 form a directed system, and can be glued into their colimit. We give an explicit description of the Dedekind-MacNeille completion of this colimit, for each d >= 2.

We present a new area in model theory, which concerns ultrafilter extensions of arbitrary models. Given a model $\mathfrak A=(X,F,\ldots,P,\ldots)$, it extends to a model $\scc\mathfrak A=(\scc X,\tilde F,\ldots,\tilde P,\ldots)$ (of the same language), where the underlying set $\scc X$ consists of all ultrafilters over $X$ and carries the standard compact Hausdorff topology. The extension lifts various relationships between models. Continuous extensions of homomorphisms of $\mathfrak A$ into $\mathfrak B$ are homomorphisms of $\scc\mathfrak A$ into $\scc\mathfrak B$. Moreover, whenever a model $\mathfrak C$ carries a compact Hausdorff topology which is compatible with its structure (like the topology and the structure of $\scc\mathfrak A$), then continuous extensions of homomorphisms of $\mathfrak A$ into $\mathfrak C$ are homomorphisms of $\scc\mathfrak A$ into $\mathfrak C$. Thus the construction provides a direct generalization of the Stone--Cech (or Wallman) compactification. These facts about homomorphisms remain true also for embeddings and other relationships between models. The construction, together with the mentioned basic results, appeared very recently in [1]. It has however some precursors. Ultrafilter extensions of semigroups are known from 70s and used as a powerful tool in number theory, algebra, topological dynamics, and ergodic theory, see [2, 3]. Other sources of close constructions were semantics of modal logic and universal algebra, see [4, 5]. We discuss connections with these earlier constructions. Further, we present several new (yet unpublished) results from [6, 7]. Certain ultrafilters form submodels. Given any infinite cardinal $\kappa$, $\kappa$-complete ultrafilters form a submodel of $\scc\mathfrak A$, and under certain conditions $\kappa$-uniform ultrafilters form a closed submodel. In some particular cases ultrafilter extensions can be elementary. In general however the equational theory of $\scc\mathfrak A$ is quite different from the equational theory of $\mathfrak A$. We describe identities that are preserved under ultrafilter extensions. Finally we consider some applications of these results in algebra. References [1] D. I. Saveliev. Ultrafilter Extensions of Models. Lecture Notes in AICS, Springer, 6521 (2011), 162--177. [2] J. Berglund, H. Junghenn, and P. Milnes. Analysis on Semigroups. Wiley, N.Y., 1989. [3] N. Hindman, D. Strauss. Algebra in the Stone--Cech Compactification. W. de Gruyter, Berlin--N.Y., 1998. [4] R. Goldblatt. Varieties of Complex Algebras. Annals of Pure and Applied Logic, 44 (1989), 173--242. [5] V. Goranko. Filter and Ultrafilter Extensions of Structures: Universal-algebraic Aspects. Manuscript, 2007. [6] D. I. Saveliev. On Hindman Sets. Manuscript, 2008. [7] D. I. Saveliev. On Identities Stable under Ultrafilter Extensions. In progress.

We consider propositional normal unimodal pretransitive logics, i.e., logics with expressible `transitive' modality. There is a long-standing open problem about the finite model property (fmp) and decidability of pretransitive logics, in particular --for the logics K^m_n=K+ \Box^m p -> \Box^n p, n>m>1. A pretransitive logic L has the fmp or is decidable, only if these properties hold for the logic L.Sym, which is the extension of L with the symmetry axiom for `transitive' modality: like S5 can be embedded into S4, L.Sym can be embedded into L. We show that for all n>m>0, the logics K^m_n.Sym have the fmp.

We study products of propositional modal logics in hybrid modal languages, with nominals referring to the second component. These hybrid products correspond to fragments of modal predicate logics (with nominals corresponding to individual constants). The main result is completeness theorem for hybrid products applicable to many cases when axiomatizing of usual products is difficult.

We study morphisms of quantum triads.

This talk shows that a concrete category is fibre-small and topological if and only if it is concretely isomorphic to a subcategory of some category Top(T) of categorically-algebraic topological structures that is definable by topological co-axioms in Top(T).

We introduce the multi-modal logic KD4+KD4. As a main result we prove that in derived set interpretation of modalities KD4+KD4 is the modal logic of bi-topological rational plane Q x Q with horizontal and vertical topologies.

Finiteness spaces were introduced by Ehrhard as a model of linear logic, which relied on a finitess property of the standard relational interpretation and allowed to reformulate Girard's quantitative semantics in a simple, linear algebraic setting. We review recent results obtained in a joint work with Christine Tasson, providing a very simple and generic construction of finiteness spaces: basically, one can transport a finiteness structure along any relation mapping finite sets to finite sets. Moreover, this construction is functorial under mild hypotheses, satisfied by the interpretations of all the positive connectives of linear logic. Recalling that the definition of finiteness spaces follows a standard orthogonality technique, fitting in the categorical framework established by Hyland and Schalk, the question of the possible generalization of transport to a wider setting is quite natural. We argue that the features of transport do not stand on the same level as the orthogonality category construction; rather, they provide a simpler and more direct characterization of the obtained structure, in a webbed setting.

We introduce a goal-oriented graphical calculus for relational inclusions. It reduces establishing a relational inclusion to establishing that a graph constructed from it has empty extension. This sound and complete calculus is conceptually simpler and easier to use than the usual ones.