Effectus theory is a new branch of categorical logic that aims to capture the essentials of quantum logic, with probabilistic and Boolean logic as special cases. Predicates in effectus theory are not subobjects having a Heyting algebra structure, like in topos theory, but `characteristic' functions, forming effect algebras. Such effect algebras are algebraic models of quantitative logic, in which double negation holds. Effects in quantum theory and fuzzy predicates in probability theory form examples of effect algebras. This text is an account of the basics of effectus theory. It includes the fundamental duality between states and effects, with the associated Born rule for validity of an effect (predicate) in a particular state. A basic result says that effectuses can be described equivalently in both `total' and `partial' form. So-called `commutative' and `Boolean' effectuses are distinguished, for probabilistic and classical models. It is shown how these Boolean effectuses are essentially extensive categories. A large part of the theory is devoted to the logical notions of comprehension and quotient, which are described abstractly as right adjoint to truth, and as left adjoint to falisity, respectively. It is illustrated how comprehension and quotients are closely related to measurement. The paper closes with a section on `non-commutative' effectus theory, where the appropriate formalisation is not entirely clear yet.

Abstract Ruitenburg’s Theorem says that every endomorphismfof a finitely generated free Heyting algebra is ultimately periodic ifffixes all the generators but one. More precisely, there isN≥ 0 such thatfN+2=fN, 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 of 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.

It follows from known results in the 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. In the first part of this article, we give 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. The axiomatization yields a decision procedure for the μ-calculus based on propositional intuitionistic logic. The second part of the article deals with closure ordinals of monotone polynomials on Heyting algebras and of intuitionistic monotone formulas; these are the least numbers of iterations needed for a polynomial/formula to converge to its least fixed-point. Mirroring the elimination procedure, we show how to compute upper bounds for closure ordinals of arbitrary intuitionistic formulas. For some classes of formulas, we provide tighter upper bounds that, in some cases, we prove exact.

For a regular cardinal $\kappa$, a formula of the modal $\mu$-calculus is $\kappa$-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of $\kappa$-directed sets. We define the fragment $C_{\aleph_1}(x)$ of the modal $\mu$-calculus and prove that all the formulas in this fragment are $\aleph_1$-continuous. For each formula $\phi(x)$ of the modal $\mu$-calculus, we construct a formula $\psi(x) \in C_{\aleph_1 }(x)$ such that $\phi(x)$ is $\kappa$-continuous, for some $\kappa$, if and only if $\phi(x)$ is equivalent to $\psi(x)$. Consequently, we prove that (i) the problem whether a formula is $\kappa$-continuous for some $\kappa$ 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 $\mu$-calculus. An ordinal $\alpha$ is the closure ordinal of a formula $\phi(x)$ if its interpretation on every model converges to its least fixed-point in at most $\alpha$ steps and if there is a model where the convergence occurs exactly in $\alpha$ steps. We prove that $\omega_1$, 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, $\omega$, $\omega_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 [25] 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 [17, 23] 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 interpretations in some relational lattice. We achieve this goal by showing that if an inclusion $$t \le 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.

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.

One of the authors introduced in [Santocanale, FoSSaCS, 2002] 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 [Santocanale, FoSSaCS, 2002] 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 mu-bicomplete categories in [Santocanale, ITA, 2002]). 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 mu-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 define the class of algebraic models of /spl mu/-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 /spl mu/-algebras, i.e. Lindenbaum algebras of the propositional modal /spl mu/-calculus. We prove the following fact: the MacNeille-Dedekind completion of a free modal /spl mu/-algebra is a complete modal algebra, hence a modal /spl mu/-algebra (i.e. an algebraic model of the propositional modal /spl mu/-calculus). The canonical embedding of the free modal /spl mu/-algebra into its Dedekind-MacNeille completion preserves the interpretation of all the terms in the class Comp(/spl Sigma//sub 1//spl Pi//sub 1/) 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 /spl mu/-calculus.