Let <𝑛,𝑘> , <𝐵𝑛,𝑘> , and <𝐷𝑛,𝑘> be the Eulerian numbers in the types A, B, and D, respectively---that is, the number of permutations of n elements with k descents, the number of signed permutations (of n elements) with k type B descents, the number of even signed permutations (of n elements) with k type D descents. Let 𝑆𝑛(𝑡)=∑𝑛−1𝑘=0<𝑛,𝑘>𝑡𝑘 , 𝐵𝑛(𝑡)=∑𝑛𝑘=0<𝐵𝑛,𝑘>𝑡𝑘 , and 𝐷𝑛(𝑡)=∑𝑛𝑘=0<𝐷𝑛,𝑘>𝑡𝑘 . We give bijective proofs of the identity 𝐵𝑛(𝑡2)=(1+𝑡)𝑛+1𝑆𝑛(𝑡)−2𝑛𝑡𝑆𝑛(𝑡2) and of Stembridge's identity 𝐷𝑛(𝑡)=𝐵𝑛(𝑡)−𝑛2𝑛−1𝑡𝑆𝑛−1(𝑡) . These bijective proofs rely on a representation of signed permutations as paths. Using this representation we also establish a bijective correspondence between even signed permutations and pairs (𝑤,𝐸) with ([𝑛],𝐸) a threshold graph and 𝑤 a degree ordering of ([𝑛],𝐸) , which we use to obtain bijective proofs of enumerative results for threshold graphs.

It is often stated that Frobenius quantales are necessarily unital. By taking negation as a primitive operation, we can define Frobenius quantales that may not have a unit. We develop the elementary theory of these structures and show, in particular, how to define nuclei whose quotients are Frobenius quantales. This yields a phase semantics and a representation theorem via phase quantales. Important examples of these structures arise from Raney's notion of tight Galois connection: tight endomaps of a complete lattice always form a Girard quantale which is unital if and only if the lattice is completely distributive. We give a characterisation and an enumeration of tight endomaps of the diamond lattices Mn and exemplify the Frobenius structure on these maps. By means of phase semantics, we exhibit analogous examples built up from trace class operators on an infinite dimensional Hilbert space. Finally, we argue that units cannot be properly added to Frobenius quantales: every possible extention to a unital quantale fails to preserve negations.

The set of permutations on a finite set can be given the lattice structure known as the weak Bruhat order. This lattice structure is generalized to the set of words on a fixed alphabet Σ = x,y,z,..., where each letter has a fixed number of occurrences. These lattices are known as multinomial lattices and, when card(Σ) = 2, as lattices of lattice paths. By interpreting the letters x, y, z, . . . as axes, these words can be interpreted as discrete increasing paths on a grid of a d-dimensional cube, with d = card(Σ). We show how to extend this ordering to images of continuous monotone functions from the unit interval to a d-dimensional cube and prove that this ordering is a lattice, denoted by L(I^d). This construction relies on a few algebraic properties of the quantale of join- continuous functions from the unit interval of the reals to itself: it is cyclic ⋆-autonomous and it satisfies the mix rule. We investigate structural properties of these lattices, which are self-dual and not distributive. We characterize join-irreducible elements and show that these lattices are generated under infinite joins from their join-irreducible elements, they have no completely join-irreducible elements nor compact elements. We study then embeddings of the d- dimensional multinomial lattices into L(I^d). We show that these embeddings arise functorially from subdivisions of the unit interval and observe that L(I^d) is the Dedekind-MacNeille completion of the colimit of these embeddings. Yet, if we restrict to embeddings that take rational values and if d > 2, then every element of L(I^d) is only a join of meets of elements from the colimit of these embeddings.

Ruitenburg's Theorem says that every endomorphism f of a finitely generated free Heyting algebra is ultimately periodic if f fixes all the generators but one. More precisely, there is N ≥ 0 such that f N +2 = f N , thus the period equals 2. We give a semantic proof of this theorem, using duality techniques and bounded bisimulation ranks. By the same techniques, we tackle investigation of arbitrary endomorphisms between free algebras. We show that they are not, in general, ultimately periodic. Yet, when they are (e.g. in the case of locally finite subvarieties), the period can be explicitly bounded as function of the cardinality of the set of generators.

For a regular cardinal κ, a formula of the modal μ-calculus is κ-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of κ-directed sets. We define the fragment C_{aleph_1}(x) of the modal μ-calculus and prove that all the formulas in this fragment are aleph₁-continuous. For each formula φ(x) of the modal μ-calculus, we construct a formula ψ(x) C_{aleph_1}(x) such that φ(x) is κ-continuous, for some κ, if and only if φ(x) is equivalent to ψ(x). Consequently, we prove that (i) the problem whether a formula is κ-continuous for some κ is decidable, (ii) up to equivalence, there are only two fragments determined by continuity at some regular cardinal: the fragment C_{aleph_0}(x) studied by Fontaine and the fragment C_{aleph_1}(x). We apply our considerations to the problem of characterizing closure ordinals of formulas of the modal μ-calculus. An ordinal α is the closure ordinal of a formula φ(x) if its interpretation on every model converges to its least fixed-point in at most α steps and if there is a model where the convergence occurs exactly in α steps. We prove that ω₁, the least uncountable ordinal, is such a closure ordinal. Moreover we prove that closure ordinals are closed under ordinal sum. Thus, any formal expression built from 0, 1, ω, ω₁ by using the binary operator symbol + gives rise to a closure ordinal.

It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras---that is, the algebraic models of the Intuitionistic Propositional Calculus---always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the μ-calculus based on intuitionistic logic is trivial, every μ-formula being equivalent to a fixed-point free formula. We give in this paper an axiomatization of least and greatest fixed-points of formulas, and an algorithm to compute a fixed-point free formula equivalent to a given μ-formula. The axiomatization of the greatest fixed-point is simple. The axiomatization of the least fixed-point is more complex, in particular every monotone formula converges to its least fixed-point by Kleene's iteration in a finite number of steps, but there is no uniform upper bound on the number of iterations. We extract, out of the algorithm, upper bounds for such n, depending on the size of the formula. For some formulas, we show that these upper bounds are polynomial and optimal.

It is well-known that the weak Bruhat order on the symmetric group on a finite number n of letters is a lattice, denoted by P(n) and often called the permutohedron on n letters, of which the Tamari lattice A(n) is a lattice retract. The equational theory of a class of lattices is the set of all lattice identities satisfied by all members of that class. We know from earlier work that the equational theory of all P(n) is properly contained in the one of all A(n). We prove the following results. TheoremA. The equational theory of all P(n) and the one of all A(n) are both decidable. Theorem B. There exists a lattice identity that holds in all P(n), but that fails in a certain 3338-element lattice. TheoremC. The equational theory of all extended permutohedra, on arbitrary (possibly infinite) posets, is trivial. In order to prove Theorems A and B, we reduce the satisfaction of a given lattice identity in a Cambrian lattice of type A to a certain tiling problem on a finite chain. Theorem A then follows from Büchi's decidability theorem for the monadic second-order theory MSO of the successor function on the natural numbers. It can be extended to any class of Cambrian lattices of type A with MSO-definable set of orientations.

The natural join and the inner union operations combine relations in a database. Tropashko and Spight realized that these two operations are the meet and join operations in a class of lattices, known by now as the relational lattices. They proposed then lattice theory as an algebraic approach, alternative to the relational algebra, to the theory of databases. Litak et al. proposed an axiomatization in the signature extending the pure lattice signature with the header constant. They argued then that the quasiequational theory of relational lattices is undecidable in this extended signature. We refine this result by showing that the quasiequational theory of relational lattices in the pure lattice signature is undecidable as well. We obtain this result as a consequence of the following statement: it is undecidable whether a finite subdirectly-irreducible lattice can be embedded into a relational lattice. Our proof of this statement is a reduction from a similar problem for relation algebras and from the coverability problem of a frame by a universal product frame. As corollaries, we also obtain the following results: the quasiequational theory of relational lattices has no finite base; there is a quasiequation which holds in all the finite lattices but fails in an infinite relational lattice.

We establish a formal connection between algorithmic correspondence theory and certain dual characterization results for finite lattices, similar to Nation's characterization of a hierarchy of pseudovarieties of finite lattices, progressively generalizing finite distributive lattices. This formal connection is mediated through monotone modal logic. Indeed, we adapt the correspondence algorithm ALBA to the setting of monotone modal logic, and we use a certain duality-induced encoding of finite lattices as monotone neighbourhood frames to translate lattice terms into formulas in monotone modal logic.

For a closure space (P,f), the closures of open subsets of P, called the regular closed subsets, form an ortholattice Reg(P,f), extending the poset Clop(P,f) of all clopen subsets. If (P,f) is a finite convex geometry, then Reg(P,f) is pseudocomplemented. The Dedekind-MacNeille completion of the poset of regions of any central hyperplane arrangement can be obtained in this way, hence it is pseudocomplemented. The lattice Reg(P,f) carries a particularly interesting structure for special types of convex geometries, that we call closure spaces of semilattice type. For finite such closure spaces, (1) Reg(P,f) satisfies an infinite collection of stronger and stronger quasi-identities, weaker than both meet- and join-semidistributivity. Nevertheless it may fail semidistributivity. (2) If Reg(P,f) is semidistributive, then it is a bounded homomorphic image of a free lattice. (3) Clop(P,f) is a lattice iff every regular closed set is clopen. The extended permutohedron R(G) on a graph G, and the extended permutohedron Reg(S) on a join-semilattice S, are both defined as lattices of regular closed sets of suitable closure spaces. While the lattice of regular closed sets is, in the semilattice context, always the Dedekind Mac-Neille completion of the poset of clopen sets, this does not always hold in the graph context, although it always does so for finite block graphs and for cycles. Furthermore, both R(G) and Reg(S) are bounded homomorphic images of free lattices.

For a given transitive binary relation e on a set E, the transitive closures of open (i.e., co-transitive in e) sets, called the regular closed subsets, form an ortholattice Reg(e), the extended permutohedron on e. This construction, which contains the poset Clop(e) of all clopen sets, is a common generalization of known notions such as the generalized permutohedron on a partially ordered set on the one hand, and the bipartition lattice on a set on the other hand. We obtain a precise description of the completely join-irreducible (resp., completely meet-irreducible) elements of Reg(e) and the arrow relations between them. In particular, we prove that (1) Reg(e) is the Dedekind-MacNeille completion of the poset Clop(e); (2) Every open subset of e is a set-theoretic union of completely join-irreducible clopen subsets of e; (3) Clop(e) is a lattice iff every regular closed subset of e is clopen, iff e contains no ”square” configuration, iff Reg(e)=Clop(e); (4) If e is finite, then Reg(e) is pseudocomplemented iff it is semidistributive, iff it is a bounded homomorphic image of a free lattice, iff e is a disjoint sum of antisymmetric transitive relations and two-element full relations. We illustrate the strength of our results by proving that, for n greater than or equal to 3, the congruence lattice of the lattice Bip(n) of all bipartitions of an n-element set is obtained by adding a new top element to a Boolean lattice with n2^n-1 atoms. We also determine the factors of the minimal subdirect decomposition of Bip(n).

Grätzer asked in 1971 for a characterization of sublattices of Tamari lattices. 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 Tamari lattice is bounded (thus so are its sublattices). Geyer conjectured in 1994 that every finite bounded lattice embeds into some Tamari lattice. We disprove Geyer's conjecture, by introducing an infinite collection of lattice-theoretical identities that hold in every Tamari lattice, 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 a Tamari lattice 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.

A lattice L is spatial if every element of L is a join of completely join-irreducible elements of L ( points ), and strongly spatial if it is spatial and the minimal coverings of completely join-irreducible elements are well-behaved. Herrmann et al. proved in 1994 that every modular lattice can be embedded, within its variety, into an algebraic and spatial lattice. We extend this result to n -distributive lattices, for fixed n . We deduce that the variety of all n -distributive lattices is generated by its finite members, thus it has a decidable word problem for free lattices. This solves two problems stated by Huhn in 1985. We prove that every modular (resp., n -distributive) lattice embeds within its variety into some strongly spatial lattice. Every lattice which is either algebraic modular spatial or bi-algebraic is strongly spatial. We also construct a lattice that cannot be embedded, within its variety, into any algebraic and spatial lattice. This lattice has a least and a largest element, and it generates a locally finite variety of join-semidistributive lattices.

This paper exhibits a general and uniform method to prove completeness for certain modal fixpoint logics. Given a set Γ of modal formulas of the form γ(x,p₁,...,p_n), where x occurs only positively in γ, the language L_#(Γ) is obtained by adding to the language of polymodal logic a connective #_γ for each γinΓ. The term #_γ(φ₁,...,φ_n) is meant to be interpreted as the least fixed point of the functional interpretation of the term γ(x,φ₁,...,φ_n). We consider the following problem: given Γ, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language L_#(Γ) on Kripke frames. We prove two results that solve this problem. First, let K_#(Γ) be the logic obtained from the basic polymodal by adding a Kozen-Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective #_γ. Provided that each indexing formula γ satisfies the syntactic criterion of being untied in x, we prove this axiom system to be complete. Second, addressing the general case, we prove the soundness and completeness of an extension K⁺_#(Γ) of K_#(Γ). This extension is obtained via an effective procedure that, given an indexing formula γ as input, returns a finite set of axioms and derivation rules for #_γ, of size bounded by the length of γ. Thus the axiom system K⁺_#(Γ) is finite whenever Γ is finite.

We address the problem of finding nice labellings for event structures of degree 3. We develop a minimum theory by which we prove that the labelling number of an event structure of degree 3 is bounded by a linear function of the height. The main theorem we present in this paper states that event structures of degree 3 whose causality order is a tree have a nice labelling with 3 colors. Finally, we exemplify how to use this theorem to construct upper bounds for the labelling number of other event structures of degree 3.

Parity games are combinatorial representations of closed Boolean μ-terms. By adding to them draw positions, they have been organized by Arnold and one of the authors into a μ-calculus. As done by Berwanger et al. for the propositional modal μ-calculus, it is possible to classify parity games into levels of hierarchy according to the number of fixed-point variables. We ask whether this hierarchy collapses w.r.t. the standard interpretation of the games μ-calculus into the class of all complete lattices. We answer this question negatively by providing, for each n >= 1, a parity game G_n with these properties: it unravels to a μ-term built up with n fixed-point variables, it is semantically equivalent to no game with strictly less than n-2 fixed-point variables.

Motivated by the nice labeling problem for event structures, we study the topological properties of the associated graphs. For each n >=0, we exhibit a graph G_n that cannot occur on an antichain as a subgraph of the graph of an event structure of degree n. The clique complexes of the graphs G_n are disks (n even) and spheres (n odd) in increasing dimensions. We strengthen the result for event structure of degree 3: cycles of length greater than 3 do not occur on antichains as subgraphs. This amount to saying that the clique complex of the graph of an event structure of degree 3 is acyclic.

For L a finite lattice, let C(L) denote the set of pairs γ= (γ₀,γ₁) such that γ₀ is a lower cover of γ₁ and order it as follows: γ<=δ iff γ₀ <= δ₀, γ₁ <=δ₁, but γ₁ <=δ₀ does not hold. Let C(L,γ) denote the connected component of γ in this poset. Our main result states that C(L,γ) is a semidistributive lattice if L is semidistributive, and that C(L,γ) is a bounded lattice if L is bounded. Let S_n be the permutohedron on n letters and T_n be the associahedron on n+1 letters. Explicit computations show that C(S_n,α) = S_n-1 and C(T_n,α) = T_n-1, up to isomorphism, whenever α is an atom. These results are consequences of new characterizations of finite join semidistributive and finite lower bounded lattices: (i) a finite lattice is join semidistributive if and only if the projection sending γin C(L) to γ₀ inL creates pullbacks, (ii) a finite join semidistributive lattice is lower bounded if and only if it has a strict facet labelling. Strict facet labellings, as defined here, are generalization of the tools used by Barbut et al. to prove that lattices of Coxeter groups are bounded.

A μ-algebra is a model of a first order theory that is an extension of the theory of bounded lattices, that comes with pairs of terms (f,μ_x.f) where μ_x.f is axiomatized as the least prefixed point of f, whose axioms are equations or equational implications. Standard μ-algebras are complete meaning that their lattice reduct is a complete lattice. We prove that any non trivial quasivariety of μ-algebras contains a μ-algebra that has no embedding into a complete μ-algebra. We focus then on modal μ-algebras, i.e. algebraic models of the propositional modal μ-calculus. We prove that free modal μ-algebras satisfy a condition -- reminiscent of Whitman's condition for free lattices -- which allows us to prove that (i) modal operators are adjoints on free modal μ-algebras, (ii) least prefixed points of Σ₁-operations satisfy the constructive relation μ_x.f = _{n >=0} fⁿ(). These properties imply the following statement: the MacNeille-Dedekind completion of a free modal μ-algebra is a complete modal μ-algebra and moreover the canonical embedding preserves all the operations in the class Comp(Σ₁,Π₁) of the fixed point alternation hierarchy.

We study the congruence lattices of the multinomial lattices L(v) introduced by Bennett and Birkhoff. Our main motivation is to investigate Parikh equivalence relations that model concurrent computation. We accomplish this goal by providing an explicit description of the join dependency relation between two join irreducible elements and of its reflexive transitive closure. The explicit description emphasizes several properties and makes it possible to separate the equational theories of multinomial lattices by their dimensions. In their covering of non modular varieties Jipsen and Rose define a sequence of equations SD_n(/\), for n >=0. Our main result sounds as follows: if v = (v₁,...,v_n) belongs to Nⁿ and v_i > 0 for i = 1,...,n, then the multinomial lattice L(v) satisfies SD_n-1(/\) and fails SD_n-2(/\).

A classical result by Rabin states that if a set of trees and its complement are both Büchi definable in the monadic second order logic, then these sets are weakly definable. In the language of μ-calculi, this theorem asserts the equality between the complexity classes Σ₂ /\ Π₂ and Comp(Σ₁,Π₁) of the alternation-depth hierarchy of the μ-calculus of tree languages. It becomes natural to ask whether at higher levels of the hierarchy the ambiguous classes Σ_{n + 1} /\Π_{n + 1} and the composition classes Comp(Σ_n,Π_n) are equal, and for which μ-calculi. A first result of this paper is that the alternation-depth hierarchy of the games μ-calculus -- whose canonical interpretation is the class of all complete lattices -- enjoys this property. Explicitly, every parity game which is equivalent both to a game in Σ_{n + 1} and to a game in Π_{n + 1} is also equivalent to a game obtained by composing games in Σ_n and Π_n. A second result is that the alternation-depth hierarchy of the μ-calculus of tree languages does not enjoy the property. Taking into account that any Büchi definable set is recognized by a nondeterministic Büchi automaton, we generalize Rabin's result in terms of the following separation theorem: if two disjoint languages are recognized by nondeterministic Π_{n+ 1} automata, then there exists a third language recognized by an alternating automata in Comp(Σ_n,Π_n) containing one and disjoint with the other. Finally, we lift the results obtained for the μ-calculus of tree languages to the propositional modal μ-calculus: ambiguous classes do not coincide with composition classes, but a separation theorem is established for disjunctive formulas.

We investigate the reasons for which the existence of certain right adjoints implies the existence of some final coalgebras, and vice-versa. In particular we prove and discuss the following theorem which has been partially available in the literature: let F G be a pair of adjoint functors, and suppose that an initial algebra F(X) of the functor H(Y) = X + F(Y) exists; then a right adjoint G(X) to F(X) exists if and only if a final coalgebra HG(X) of the functor K(Y) = X ×G(Y) exists. Motivated by the problem of understanding the structures that arise from initial algebras, we show the following: if F is a left adjoint with a certain commutativity property, then an initial algebra of H(Y) = X + F(Y) generates a subcategory of functors with inductive types where the functorial composition is constrained to be a Cartesian product.

We propose a method to axiomatize by equations the least prefixed point of an order preserving function. We discuss its domain of application and show that the Boolean μ-calculus has a complete equational axiomatization. The method relies on the existence of a "closed structure" and its relationship to the equational axiomatization of Action Logic is made explicit. The implication operation of a closed structure is not monotonic in one of its variables; we show that the existence of such a term that does not preserve the order is an essential condition for defining by equations the least prefixed point. We stress the interplay between closed structures and fixed point operators by showing that the theory of Boolean modal μ-algebras is not a conservative extension of the theory of modal μ-algebras. The latter is shown to lack the finite model property.

For an arbitrary category, we consider the least class of functors containing the projections and closed under finite products, finite coproducts, parameterized initial algebras and parameterized final coalgebras, i.e. the class of functors that are definable by μ-terms. We call the category μ-bicomplete if every μ-term defines a functor. We provide concrete examples of such categories and explicitly characterize this class of functors for the category of sets and functions. This goal is achieved through parity games: we associate to each game an algebraic expression and turn the game into a term of a categorical theory. We show that μ-terms and parity games are equivalent, meaning that they define the same property of being μ-bicomplete. Finally, the interpretation of a parity game in the category of sets is shown to be the set of deterministic winning strategies for a chosen player.

A μ-lattice is a lattice with the property that every unary polynomial has both a least and a greatest fix-point. In this paper we define the quasivariety of μ-lattices and, for a given partially ordered set P, we construct a μ-lattice J_P whose elements are equivalence classes of games in a preordered class J(P). We prove that the μ-lattice J_P is free over the ordered set P and that the order relation of J_P is decidable if the order relation of P is decidable. By means of this characterization of free μ-lattices we infer that the class of complete lattices generates the quasivariety of μ-lattices.

The alternation hierarchy problem asks whether every μ-term φ, that is, a term built up also using a least fixed point constructor as well as a greatest fixed point constructor, is equivalent to a μ-term where the number of nested fixed points of a different type is bounded by a constant independent of φ. In this paper we give a proof that the alternation hierarchy for the theory of μ-lattices is strict, meaning that such a constant does not exist if μ-terms are built up from the basic lattice operations and are interpreted as expected. The proof relies on the explicit characterization of free μ-lattices by means of games and strategies.

All the binomial lattices embed into Q(I), the complete lattice of sup-preserving endomaps of the unit interval---whose elements can be seen as continuous monotone paths from (0,0) to (1,1). This lattice is completely distributive. We give a general description of the complete congruences of completely distributive lattices by means of an interior operator on the collection of closed subsets of an associated topological space. In particular, we show that these form a frame. We give a description of this frame for the unit interval lattice, showing that it is not a Boolean algebra nor a (co)spatial frame. For Q(I), we give a geometrical interpretation of these congruences by means of directed homotopies.

For a functor Q from a category C to the category Pos of ordered sets and order-preserving functions, we study liftings of various kind of structures from the base category to the total category ∫ Q. That lifting a monoidal structure corresponds to giving some lax natural transformation making Q almost monoidal, might be part of folklore in category theory. We rely on and generalize the tools supporting this correspondence so to provide exact conditions for lifting symmetric monoidal closed and star-autonomous structures. A corollary of these characterizations is that, if Q factors as a monoidal functor through SLatt, the category of complete lattices and sup-preserving functions, then ∫ Q is always symmetric monoidal closed. In this case, we also provide a method, based on the double negation nucleus from quantale theory, to turn ∫ Q into a star-autonomous category. The theory developed, originally motivated from the categories Q-Set of Schalk and de Paiva, yields a wide generalization of Hyland and Schalk construction of star-autonomous categories by means of orthogonality structures.

It is known that the quantale of sup-preserving maps from a complete lattice to itself is a Frobenius quantale if and only if the lattice is completely distributive. Since completely distributive lattices are the nuclear objects in the autonomous category of complete lattices and sup-preserving maps, we study the above statement in a categorical setting. We introduce the notion of Frobenius structure in an arbitrary autonomous category, generalizing that of Frobenius quantale. We prove that the monoid of endomorphisms of a nuclear object has a Frobenius structure. If the environment category is star-autonomous and has epi-mono factorizations, a variant of this theorem allows to develop an abstract phase semantics and to generalise the previous statement. Conversely, we argue that, in a star-autonomous category where the monoidal unit is a dualizing object, if the monoid of endomorphisms of an object has a Frobenius structure and the monoidal unit embeds into this object as a retract, then the object is nuclear.

We consider skew metrics (equivalently, transitive relations that are tournaments, linear orderings) valued in Sugihara semigroups on autodual chains. We prove that, for odd chains and chains without a unit, skew metrics classify certain tree-like structures that we call perfect augmented plane towers. When the chain is finite and has cardinality 2K + 1, skew metrics on a set X give rise to perfect rooted plane trees of height K whose frontier is a linear preorder of X. Any linear ordering on X gives rise to an ordering on the set of its skew metrics valued in an arbitrary involutive residuated lattice Q. If Q satisfies the mix rule, then this poset is most often a lattice. We study this lattice for X = {1,...,n} and Q the Sugihara monoid on the chain of cardinality 2K + 1. We give a combinatorial model of this lattice by de- scribing its covers as moves on a space of words coding perfect augmented plane trees. Using the combinatorial model, we develop enumerative considerations on this lattice.

Let n,k, n,k, and n,k be the Eulerian numberss in the types A, B, D, respectively---that is, number of permutations of n elements with k descents, the number of signed permutations (of n elements) with k type B descents, the number of even signed permutations (of n elements) with k type D descents. Let S_n(t) = _{k = 0}^n-1 n,k^k and B_n(t) = _{k = 0}ⁿ nkt^k, and D_n(t) = _{k = 0}ⁿ nkt^k. We give bijective proofs of the identity B_n(t²) = (1+t)ⁿ⁺¹S_n(t) - 2ⁿtS_n(t²) and of Stembridge's identity D_n(t) = B_n(t) - n2^n-1tS_n-1(t). These bijective proofs rely on a representation of signed permutations as paths. Using the same representation we establish a bijective correspondence between even signed permutations and pairs (w,E) with ([n], E) a threeshold graph and w a degree ordering of ([n], E).

It is argued in (Eklund et al., 2018) that the quantale [L,L] of sup-preserving endomaps of a complete lattice L is a Girard quantale exactly when L is completely distributive. We have argued in (Santocanale, 2020) that this Girard quantale structure arises from the dual quantale of inf-preserving endomaps of L via Raney's transforms and extends to a Girard quantaloid structure on the full subcategory of SLatt (the category of complete lattices and sup-preserving maps) whose objects are the completely distributive lattices. It is the goal of this talk to illustrate further this connection between the quantale structure, Raney's transforms, and complete distributivity. Raney's transforms are indeed mix maps in the isomix category SLatt and most of the theory can be developed relying on naturality of these maps. We complete then the remarks on cyclic elements of [L,L] developed in (Santocanale, 2020) by investigating its dualizing elements. We argue that if [L,L] has the structure a Frobenius quantale, that is, if it has a dualizing element, not necessarily a cyclic one, then L is once more completely distributive. It follows then from a general statement on involutive residuated lattices that there is a bijection between dualizing elements of [L,L] and automorphisms of L. Finally, we also argue that if L is finite and [L,L] is autodual, then L is distributive.

Let L be a complete lattice and let Q(L) be the unital quantale of join-continuous endo-functions of L. We prove the following result: Q(L) is an involutive (that is, non-commutative cyclic ⋆-autonomous) quantale if and only if L is a completely distributive lattice. If this is the case, then the dual tensor operation corresponds, via Raney's transforms, to composition in the (dual) quantale of meet-continuous endo-functions of L. Let sLatt be the category of sup-lattices and join-continuous functions and let cdLatt be the full subcategory of sLatt whose objects are the completely distributive lattices. We argue that (i) cdLatt is itself an involutive quantaloid, and therefore it is the largest full-subcategory of sLatt with this property; (ii) cdLatt is closed under the monoidal operations of sLatt and therefore it is ⋆-autonomous. Consequently, if Q(L) is involutive, then it is completely distributive as well.

The set of discrete lattice paths from (0, 0) to (n, n) with North and East steps (i.e. words w ∈ { x, y }* such that |w| x = |w| y = n) has a canonical monoid structure inherited from the bijection with the set of join-continuous maps from the chain 0, 1, ..., n to itself. We explicitly describe this monoid structure and, relying on a general characterization of idempotent join-continuous maps from a complete lattice to itself, we characterize idempotent paths as upper zigzag paths. We argue that these paths are counted by the odd Fibonacci numbers. Our method yields a geometric/combinatorial proof of counting results, due to Howie and to Laradji and Umar, for idempotents in monoids of monotone endomaps on finite chains.

The set of permutations on a finite set can be given a lattice structure (known as the weak Bruhat order). The lattice structure is generalized to the set of words on a fixed alphabet Σ= {x,y,z,...}, where each letter has a fixed number of occurrences (these lattices are known as multinomial lattices and, in dimension 2, as lattices of lattice paths). By interpreting the letters x,y,z,... as axes, these words can be interpreted as discrete increasing paths on a grid of a d-dimensional cube, where d = card(Σ). We show in this paper how to extend this order to images of continuous monotone paths images of monotone functions from the unit interval to a d-dimensional cube. The key tool used to realize this construction is the quantale L_V(I) of join-continuos functions from the unit interval to itself; the construction relies on a few algebraic properties of this quantale: it is star-autonomous and it satisfies the mix rule. We begin developing a structural theory of these lattices by characterizing join-irreducible elements, and by proving these lattices are generated from their join-irreducible elements under infinite joins.

For a given intuitionistic propositional formula A and a propositional variable x occurring in it, define the infinite sequence of formulae { A_i | i≥1} by letting A_1 be A and A_i+1 be A(A_i/x). Ruitenburg's Theorem says that the sequence { A_i } (modulo logical equivalence) is ultimately periodic with period 2, i.e. there is N ≥ 0 such that A_{N+2} ↔ A_N is provable in intuitionistic propositional calculus. We give a semantic proof of this theorem, using duality techniques and bounded bisimulations ranks.

The natural join and the inner union operations combine relations of a database. Tropashko and Spight realized that these two operations are the meet and join operations in a class of lattices, known by now as the relational lattices. They proposed then lattice theory as an algebraic approach to the theory of databases, alternative to the relational algebra. Previous works proved that the quasiequational theory of these lattices—that is, the set of definite Horn sentences valid in all the relational lattices—is undecidable, even when the signature is restricted to the pure lattice signature. We prove here that the equational theory of relational lattices is decidable. That, is we provide an algorithm to decide if two lattice theoretic terms t, s are made equal under all intepretations in some relational lattice. We achieve this goal by showing that if an inclusion t ≤ s fails in any of these lattices, then it fails in a relational lattice whose size is bound by a triple exponential function of the sizes of t and s.

For a regular cardinal κ, a formula of the modal μ-calculus is κ-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of κ-directed sets. We define the fragment C_{aleph_1}(x) of the modal μ-calculus and prove that all the formulas in this fragment are aleph₁-continuous. For each formula φ(x) of the modal μ-calculus, we construct a formula ψ(x) C_{aleph_1}(x) such that φ(x) is κ-continuous, for some κ, if and only if φ(x) is equivalent to ψ(x). Consequently, we prove that (i) the problem whether a formula is κ-continuous for some κ is decidable, (ii) up to equivalence, there are only two fragments determined by continuity at some regular cardinal: the fragment C_{aleph_0}(x) studied by Fontaine and the fragment C_{aleph_1}(x). We apply our considerations to the problem of characterizing closure ordinals of formulas of the modal μ-calculus. An ordinal α is the closure ordinal of a formula φ(x) if its interpretation on every model converges to its least fixed-point in at most α steps and if there is a model where the convergence occurs exactly in α steps. We prove that ω₁, the least uncountable ordinal, is such a closure ordinal. Moreover we prove that closure ordinals are closed under ordinal sum. Thus, any formal expression built from 0, 1, ω, ω₁ by using the binary operator symbol + gives rise to a closure ordinal.

The natural join and the inner union operations combine relations of a database. Tropashko and Spight realized that these two operations are the meet and join operations in a class of lattices, known by now as the relational lattices. They proposed then lattice theory as an algebraic approach to the theory of databases alternative to the relational algebra. Litak et al. proposed an axiomatization of relational lattices over the signature that extends the pure lattice signature with a constant and argued that the quasiequational theory of relational lattices over this extended signature is undecidable. We prove in this paper that embeddability is undecidable for relational lattices. More precisely, it is undecidable whether a finite subdirectly-irreducible lattice can be embedded into a relational lattice. Our proof is a reduction from the coverability problem of a multimodal frame by a universal product frame and, indirectly, from the representability problem for relation algebras. As corollaries we obtain the following results: the quasiequational theory of relational lattices over the pure lattice signature is undecidable and has no finite base; there is a quasiequation over the pure lattice signature which holds in all the finite relational lattices but fails in an infinite relational lattice.

The natural join and the inner union combine in different ways tables of a relational database. Tropashko observed that these two operations are the meet and join in a class of lattices---called the relational lattices---and proposed lattice theory as an alternative algebraic approach to databases. Aiming at query optimization, Litak et al. initiated the study of the equational theory of these lattices. We carry on with this project, making use of the duality theory developed by us. The contributions of this paper are as follows. Let A be a set of column's names and D be a set of cell values; we characterize the dual space of the relational lattice R(D,A) by means of a generalized ultrametric space, whose elements are the functions from A to D, with the P(A)-valued distance being the Hamming one but lifted to subsets of A. We use the dual space to present an equational axiomatization of these lattices that reflects the combinatorial properties of these generalized ultrametric spaces: symmetry and pairwise completeness. Finally, we argue that these equations correspond to combinatorial properties of the dual spaces of lattices, in a technical sense analogous of correspondence theory in modal logic. In particular, this leads an exact characterization of the finite lattices satisfying these equations.

It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras---that is, the algebraic models of the Intuitionistic Propositional Calculus---always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the μ-calculus based on intuitionistic logic is trivial, every μ-formula being equivalent to a fixed-point free formula. We give in this paper an axiomatization of least and greatest fixed-points of formulas, and an algorithm to compute a fixed-point free formula equivalent to a given μ-formula. The axiomatization of the greatest fixed-point is simple. The axiomatization of the least fixed-point is more complex, in particular every monotone formula converges to its least fixed-point by Kleene's iteration in a finite number of steps, but there is no uniform upper bound on the number of iterations. We extract, out of the algorithm, upper bounds for such n, depending on the size of the formula. For some formulas, we show that these upper bounds are polynomial and optimal.

The varieties of lattices D_n, n >=0, were introduced in [Nation90] and studied later in [Semenova05]. These varieties might be considered as generalizations of the variety of distributive lattices which, as a matter of fact, coincides with D₀. It is well known that least and greatest fixed-points of terms are definable on distributive lattices; this is an immediate consequence of the fact that the equation φ²() = φ() holds on distributive lattices, for any lattice term φ(x). In this paper we propose a generalization of this fact by showing that the identity φ^{n + 2}(x) = φ^{n +1}(x) holds in D_n, for any lattice term φ(x) and for x in ,. Moreover, we prove that the equations φ^{n + 1}(x) = φⁿ(x), x = ,, might not hold in the variety D_n nor in the variety D_n D_n^op, where D_n^op is the variety containing the lattices L^op, for L inD_n.

One of the authors introduced in [31] a calculus of circular proofs for studying the computability arising from the following categorical operations: finite products, finite coproducts, initial algebras, final coalgebras. The calculus presented [31] is cut-free; even if sound and complete for provability, it lacked an important property for the semantics of proofs, namely fullness w.r.t. the class of intended categorical models (called μ-bicomplete categories)). In this paper we fix this problem by adding the cut rule to the calculus and by modifying accordingly the syntactical constraint ensuring soundness of proofs. The enhanced proof system fully represents arrows of the canonical model (a free μ-bicomplete category). We also describe a cut-elimination procedure as a a model of computation arising from the above mentioned categorical operations. The procedure constructs a cut-free proof-tree with possibly infinite branches out of a finite circular proof with cuts.

We reconstruct the syntax and semantics of monotone modal logic, in the style of Moss' coalgebraic logic. To that aim, we replace the box and diamond with a modality nabla which takes a finite collection of finite sets of formulas as its argument. The semantics of this modality in monotone neighborhood models is defined in terms of a version of relation lifting that is appropriate for this setting. We prove that the standard modal language and our r -based one are effectively equi-expressive, meaning that there are effective translations in both directions. We prove and discuss some algebraic laws that govern the interaction of nabla with the Boolean operations. These laws enable us to rewrite each formula into a special kind of disjunctive normal form that we call transparent. For such transparent formulas it is relatively easy to define the bisimulation quantifiers that one may associate with our notion of relation lifting. This allows us to prove the main result of the paper, viz., that monotone modal logic enjoys the property of uniform interpolation.

The word problem for categories with free products and coproducts (sums), SP-categories, is directly related to the problem of determining the equivalence of certain processes. Indeed, the maps in these categories may be directly interpreted as processes which communicate by two-way channels. The maps of an SP-category may also be viewed as a proof theory for a simple logic with a game theoretic intepretation. The cut-elimination procedure for this logic determines equality only up to certain permuting conversions. As the equality classes under these permuting conversions are finite, it is easy to see that equality between cut-free terms (even in the presence of the additive units) is decidable. Unfortunately, this does not yield a tractable decision algorithm as these equivalence classes can contain exponentially many terms. However, the rather special properties of these free categories -- and, thus, of two-way communication -- allow one to devise a tractable algorithm for equality. We show that, restricted to cut-free terms s,t : X --> A, the decision procedure runs in time polynomial on |X||A|, the product of the sizes of the domain and codomain type.

Parity games are combinatorial representations of closed Boolean μ-terms. By adding to them draw positions, they have been organized by Arnold and one of the authors into a μ-calculus. As done by Berwanger et al. for the propositional modal μ-calculus, it is possible to classify parity games into levels of hierarchy according to the number of fixed-point variables. We ask whether this hierarchy collapses w.r.t. the standard interpretation of the games μ-calculus into the class of all complete lattices. We answer this question negatively by providing, for each n >= 1, a parity game G_n with these properties: it unravels to a μ-term built up with n fixed-point variables, it is semantically equivalent to no game with strictly less than n-2 fixed-point variables.

An event structures is a mathematical model of a concurrent process. It consists of a set of local events ordered by a causality relation and separated by a conflict relation. A global state, or configuration, is an order ideal whose elements are pairwise not in conflict. Configurations, ordered by subset inclusion, form a poset whose Hasse diagram codes the state-transition graph of the process. By labelling edges, the state-transition graph can be enriched with the structure of a deterministic concurrent automaton on some alphabet. The nice labelling problem asks to minimize the cardinality of the alphabet. In this talk we shall first introduce the nice labelling problem and show how it translates to a graph coloring problem. We shall then survey on the problem and present the results that are available to us nowadays. Thus we shall The survey will also be the occasion to point out new perspectives, open problems, and research paths.

Entanglement is a complexity measure of directed graphs that origins in fixed point theory. This measure has shown its use in designing efficient algorithms to verify logical properties of transition systems. We are interested in the problem of deciding whether a graph has entanglement at most k. As this measure is defined by means of games, game theoretic ideas naturally lead to design polynomial algorithms that, for fixed k, decide the problem. Known characterizations of directed graphs of entanglement at most 1 lead, for k = 1, to design even faster algorithms. In this paper we present an explicit characterization of undirected graphs of entanglement at most 2. With such a characterization at hand, we devise a linear time algorithm to decide whether an undirected graph has this property.

Given a set Γ of modal formulas of the form γ(x,p), where x occurs positively in γ, the language L_#(Γ) is obtained by adding to the language of polymodal logic connectives #_γ, γin Γ. Each term #_γ is meant to be interpreted as the least fixed point of the functional interpretation of the term γ(x). Given such a Γ, we construct an axiom system K_#(Γ) which is sound and complete w.r.t. the concrete interpretation of the language L_#(Γ) on Kripke frames. If Γ is finite, then K_#(Γ) is a finite set of axioms and inference rules.

We address the problem of finding nice labellings for event structures of degree 3. We develop a minimum theory by which we prove that the labelling number of an event structure of degree 3 is bounded by a linear function of the height. The main theorem we present in this paper states that event structures of degree 3 whose causality order is a tree have a nice labelling with 3 colors. Finally, we exemplify how to use this theorem to construct upper bounds for the labelling number of other event structures of degree 3.

We define the class of algebraic models of μ-calculi and study whether every such model can be embedded into a model which is a complete lattice. We show that this is false in the general case and focus then on free modal μ-algebras, i.e. Lindenbaum algebras of the propositional modal μ-calculus. We prove the following fact: the MacNeille-Dedekind completion of a free modal μ-algebra is a complete modal algebra, hence a modal μ-algebra (i.e. an algebraic model of the propositional modal μ-calculus). The canonical embedding of the free modal μ-algebra into its Dedekind-MacNeille completion preserves the interpretation of all the terms in the class Comp(Σ₁,Π₁) of the alternation-depth hierarchy. The proof uses algebraic techniques only and does not directly rely on previous work on the completeness of the modal μ-calculus.

We introduce a new method (derived from model theoretic general combination procedures in automated deduction) for proving fusion decidability in modal systems. We apply it to show fusion decidability in case not only the boolean connectives, but also a universal modality and nominals are shared symbols.

We prove that every finitary polynomial endofunctor of a category C has a final coalgebra, provided that C is locally Cartesian closed, it has finite coproducts and is an extensive category, it has a natural number object.

Every parity game is a combinatorial representation of a closed Boolean μ-term. When interpreted in a distributive lattice every Boolean μ-term is equivalent to a fixed-point free term. The alternation-depth hierarchy is therefore trivial in this case. This is not the case for non distributive lattices, as the second author has shown that the alternation-depth hierarchy is infinite. In this paper we show that the alternation-depth hierarchy of the games μ-calculus, with its interpretation in the class of all complete lattices, has a nice characterization of ambiguous classes: every parity game which is equivalent both to a game in Σ_{n + 1} and to a game in Π_{n + 1} is also equivalent to a game obtained by composing games in Σ_n and Π_n.

We survey on the ongoing research that relates the combinatorics of parity games to the algebra of categories with finite products, finite coproducts, initial algebras and final coalgebras of definable functors, i.e. μ-bicomplete categories. We argue that parity games with a given starting position play the role of terms for the theory of μ-bicomplete categories. We show that the interpretation of a parity game in the category of sets and functions is the set of deterministic winning strategies for one player in the game. We discuss bounded memory communication strategies between two parity games and their computational significance. We describe how an attempt to formalize them within the algebra of μ-bicomplete categories leads to develop a calculus of proofs that are allowed to contain cycles.

We present a calculus of “circular proofs”: the graph underlying a proof is not a finite tree but instead it is allowed to contain a certain amount of cycles. The main challenge in developing a theory for the calculus is to define the semantics of proofs, since the usual method by induction on the structure is not available. We solve this problem by associating to each proof a system of equations -- defining relations among undetermined arrows of an arbitrary category with finite products and coproducts as well as constructible initial algebras and final coalgebras -- and by proving that this system admits always a unique solution.

We show how to axiomatize by equations the least prefixed point of an order preserving function and discuss the domain of application of the proposed method. Thus, we generalize the well known equational axiomatization of Propositional Dynamic Logic to a complete equational axiomatization of the Boolean Modal μ-Calculus. We show on the other hand that the existence of a term which does not preserve the order is an essential condition for the least prefixed point to be definable by equations.

A presentation is a triple X,<=,M with X,<= a finite poset and M : X ((X)) -- these data being subject to additional constraints. Given a presentation we can define closed subsets of X, whence a finite lattice. Given a finite lattice L, we can define its presentation: X is the set of join-irreducible elements of L, <= is the restriction of the order to join-irreducible elements, and M(x) is the set of minimal join-covers of x. Morphisms of presentations can be defined as some zig-zag relations. Our main result is: the category of presentations is dually equivalent to the category of finite lattice. The two constructions described above are the object part of contravariant functors giving rise to the duality. We think of presentations as semantic domains for lattice terms and formulas of substructural logics. Relying on previous work by Nation and Semenova, we show that some equational properties of finite lattices correspond to first order properties of presentations. Namely, for each finite tree T, we construct an equation e_T that holds in a finite lattice if and only its presentation does not have some a shape from T. We illustrate further use of these semantics within the theory of fixed points over finite lattices: we generalize, in a non-trivial way, the well known fact that least fixed points on distributive lattice terms can be eliminated.

We prove that every finitary polynomial endofunctor of a category C has a final coalgebra if C is locally Cartesian closed, has finite disjoint coproducts and a natural number object. More generally, we prove that the category of coalgebras for such an endofunctor has all finite limits.

We have investigated axioms related to linear negation in the context of intuitionistic generalization of complete semantics for Distributive Linear Logic presented in [GM]. We show that internal monoids in the monoidal category of bimodules between partially ordered sets provide a complete semantics for Linear Logic based on intuitionism. The basic framework is a set with a partial order and a ternary relation which satisfies compatibility conditions with the order, as also shown in [AD]. We give concrete examples of such structures: one of them is suggested by an immediate generalization to intuitionism of the quantale of all relations over a set; another universe can be obtained by putting together all the individuals of a monoid in presheaves. The analysis in this context of axioms ruling linear negation has followed the suggestion in [Yet]: condition of being a dualizing element and condition of being a cyclic element have been analyzed separately. Since the starting point of our work has been the observation that groupoids are models not only for linear logic, but also for classical linear logic when a proper choice of linear false is done, we have investigated also syntactic conditions which are always valid in these particular universes. These are a non-contradiction principle which merges cartesian conjunction with linear negation and true, and De Morgan laws of complement with respect to linear conjunction and disjunction. In the classical case the non contradiction principle is equivalent to take as linear false the complement of unity. This choice leads in groupoids to satisfy De Morgan laws which are however not derivable; which is proved by construction of counterexamples. Quantifiers elimination by means of properties of the free algebra of lower sets has been the general method followed in the analysis from syntax to semantics. A second part of the work has confronted the opposite problem: given semantic conditions we show that, from their truth in the canonical model of prime filters, equivalent syntactic conditions are found. In this case an analogous way of eliminating quantifiers over prime filters needs the extensive use of Extension/Exclusion Lemma which requires the axiom of choice. Beside the problem of extending a theory in which a syntactic condition holds to a complete one, there is the research of syntactic equivalents to interesting semantic conditions. [AD] G. Allwein - J.M. Dunn, Kripke Models for Linear Logic, The Journal of Symbolic Logic, Volume 58, Number 2, (1993), pp. 514-545; [GM] S. Ghilardi - G. Meloni, Modal logics with n-ary connectives, Zeitschr.f.math.Logik und Grundlagen d.Math., Bd. 36, S.193-215 (1990); [Yet] D.N. Yetter, Quantales and (noncommutative) linear logic, The Journal of Symbolic Logic, Volume 55, Number 1, (1990), pp. 41-64;

If f(y) is an order preserving endofunction of a closed ordered monoid, then the two inequations align* f(g(x))x & <=g(x) & g(f(x) x) & <=x align* determine an order preserving endofunction g(x) as μ_y.(f(y) x), the parameterized least prefixed point of f(y) x. This observation is the core of a method to axiomatize by equations the least prefixed point. When this method is applied to the propositional Boolean modal μ-calculus, it shows that Kozen's axiomatization can be turned into an equivalent equational axiomatization that is complete with respect to Kripke frames by Walukiewicz's theorem. Being able to equationally axiomatize the propositional Boolean modal μ-calculus implies that its algebraic models form a variety of algebras, in the usual sense. We call these models modal μ-algebras. The main characteristic that distinguishes a variety from a quasivariety -- i.e. a class of models that can be axiomatized by equational implications -- is that such a class is closed under homomorphic images defined from congruences. Thus, in a variety of algebras, there is always a bijection between quotients of an algebra (categorically, strong epimorphisms) and congruences on the algebra. Modal μ-algebras are therefore closed under homomorphic images; we have investigated congruences of modal μ-algebras and found a characterization suitable for algebraic computations. In this talk we will present this characterization and illustrate its use by lifting some classical results from modal logic and modal algebras to the setting of modal μ-algebras. The characterization of congruences can also be exploited in the context of verification of systems, as these results can be reformulated in a logical framework. For example, it could be useful to analyze a restricted class of transition systems where given subsets of states are known to satisfy a finite number of algebraic relations. Some propositions of the modal μ-calculus could hold true in these models, and it would be desirable to know whether their truth is a consequence of Kozen's axiomatization and of those algebraic relations. This is a particular instance of a common problem in logic: is a proposition derivable from a finite set of propositions that are assumed as axioms? Among the results that we present is a deduction theorem for the propositional Boolean modal μ-calculus; this theorem allows to reduce derivability from a finite set of axioms to derivability from no axioms. As the latter problem is well known to be decidable for the modal μ-calculus, then derivability from a finite set of propositions becomes decidable as well.

We present a calculus of proofs, the intended models of which are categories with finite products and coproducts, initial algebras and final coalgebras of functors that are recursively constructible out of these operations, that is, μ-bicomplete categories. The calculus satisfies the cut elimination and its main characteristic is that the underlying graph of a proof is allowed to contain a certain amount of cycles. To each proof of the calculus we associate a system of equations which has a meaning in every μ-bicomplete category. We prove that this system admits always a unique solution, and by means of this theorem we define the semantics of the calculus

The alternation hierarchy problem asks whether every μ-term, that is a term built up using also a least fixed point constructor as well as a greatest fixed point constructor, is equivalent to a μ-term where the number of nested fixed point of a different type is bounded by a fixed number.In this paper we give a proof that the alternation hierarchy for the theory of μ -lattices is strict, meaning that such number does not exist if μ-terms are built up from the basic lattice operations and are interpreted as expected. The proof relies on the explicit characterization of free μ-lattices by means of games and strategies

A μ-lattice is a lattice with the property that every unary polynomial has both a least and a greatest fix-point. In this paper we define the quasivariety of μ-lattices and, for a given partially ordered set P, we construct a μ-lattice J_P whose elements are equivalence classes of games in a preordered class J(P). We prove that the μ-lattice J_P is free over the ordered set P and that the order relation of J_P is decidable if the order relation of P is decidable. By means of this characterization of free μ-lattices we infer that the class of complete lattices generates the quasivariety of μ-lattices

Un code est essentiellement la base d'un sous-monoïde libre d'un monoïde libre (l'ensemble de tous les mots sur un alphabet). Un code est circulaire si l'image (par l'inclusion) d'un mot primitif est primitif et si les images inverses de deux mots conjugues sont conjugues. Il existe une sous-classe de codes circulaires, celle des codes uniformément synchrones. Un résultat bien connu nous dit qu'un code circulaire fini est toujours uniformément synchrone. Cependant la preuve contenue dans l'ouvrage classique sur la théorie des codes utilise des outils raffines de la théorie de la reconnaissance des codes par des représentations non ambiguës sur de monoïdes de relations. Cet expose donnera une petite introduction à la théorie et procédera à la preuve de ce résultat de façon "simple", à l'aide de calculs sur les mots seulement.

Un μ-treillis est un treillis L avec la propriété que tout polynôme avec coefficients dans L possède à la fois un plus petit point préfixe et un plus grand point postfixe. Dans ce travail nous définissons la quasivariété des μ-treillis et, pour un ensemble partiellement ordonné P, nous construisons un μ-treillis J_P dont les éléments sont des classes d'équivalence de jeux appartenants à une classe préordonnée J(P). Nous montrons que le μ-treillis J_P est libre sur l'ensemble ordonné P et que la relation d'ordre de J_P est décidable si la relation d'ordre de P est décidable. À l'aide de cette caractérisation nous montrons que la variété équationelle des μ-treillis est engendrée par la classe des treillis complets.

Nous souhaitons illustrer comment la notion de structure, algébrique et d'ordre, peut être un guide fructuex dans l'étude de sujets importants de l'informatique tels que les processus concurrents et les logiques modales et temporales pour la vérification des systèmes informatiques.