On the Dynamic Logic of Agency and Action

We present a Hilbert style axiomatization and an equational theory for reasoning about actions and capabilities. We introduce two novel features in the language of propositional dynamic logic, converse as backwards modality and abstract processes specified by preconditions and effects, written as ${\varphi \Rightarrow \psi}$ and first explored in our recent paper (Hartonas, Log J IGPL Oxf Univ Press, 2012), where a Gentzen-style sequent calculus was introduced. The system has two very natural interpretations, one based on the familiar relational semantics and the other based on type semantics, where action terms are interpreted as types of actions (sets of binary relations). We show that the proof systems do not distinguish between the two kinds of semantics, by completeness arguments. Converse as backwards modality together with action types allow us to produce a new purely equational axiomatization of Dynamic Algebras, where iteration is axiomatized independently of box and where the fixpoint and Segerberg induction axioms are derivable. The system also includes capabilities operators and our results provide then a finitary Hilbert-style axiomatization and a decidable system for reasoning about agent capabilities, missing in the KARO framework.     

Order-Dual Relational Semantics for Non-distributive Propositional Logics: A General Framework

The contribution of this paper lies with providing a systematically specified and intuitive interpretation pattern and delineating a class of relational structures (frames) and models providing a natural interpretation of logical operators on an underlying propositional calculus of Positive Lattice Logic (the logic of bounded lattices) and subsequently proving a generic completeness theorem for the related class of logics, sometimes collectively referred to as (non-distributive) Generalized Galois Logics (GGL’s).     

Duality for Lattice-Ordered Algebras and for Normal Algebraizable Logics

Part I of this paper is developed in the tradition of Stone-type dualities, where we present a new topological representation for general lattices (influenced by and abstracting over both Goldblatt's [17] and Urquhart's [46]), identifying them as the lattices of stable compact-opens of their dual Stone spaces (stability refering to a closure operator on subsets). The representation is functorial and is extended to a full duality.In part II, we consider lattice-ordered algebras (lattices with additional operators), extending the Jónsson and Tarski representation results [30] for Boolean algebras with Operators. Our work can be seen as developing, and indeed completing, Dunn's project of gaggle theory [13, 14]. We consider general lattices (rather than Boolean algebras), with a broad class of operators, which we dubb normal, and which includes the Jónsson-Tarski additive operators. Representation of l-algebras is extended to full duality.In part III we discuss applications in logic of the framework developed. Specifically, logics with restricted structural rules give rise to lattices with normal operators (in our sense), such as the Full Lambek algebras (F L-algebras) studied by Ono in [36]. Our Stone-type representation results can be then used to obtain canonical constructions of Kripke frames for such systems, and to prove a duality of algebraic and Kripke semantics for such logics.