Completeness-via-canonicity in coalgebraic logics

File Description SizeFormat 
Dahlqvist-FPH-2015-PhD-Thesis.pdfThesis1.68 MBAdobe PDFView/Open
Title: Completeness-via-canonicity in coalgebraic logics
Authors: Fredrik Paul Herbert, Dahlqvist
Item Type: Thesis or dissertation
Abstract: This thesis aims to provide a suite of techniques to generate completeness re- sults for coalgebraic logics with axioms of arbitrary rank. We have chosen to investigate the possibility to generalize what is arguably one of the most suc- cessful methods to prove completeness results in ‘classical’ modal logic, namely completeness-via-canonicity. This technique is particularly well-suited to a coal- gebraic generalization because of its clean and abstract algebraic formalism. In the case of classical modal logic, it can be summarized in two steps, first it isolates the purely algebraic problem of canonicity, i.e. of determining when a variety of boolean Algebras with Operators (BAOs) is closed under canonical extension (i.e. canonical). Secondly, it connects the notion of canonical vari- eties to that of canonical models to explicitly build models, thereby proving completeness. The classical algebraic theory of canonicity is geared towards normal logics, or, in algebraic terms, BAOs (or generalizations thereof). Most coalgebraic log- ics are not normal, and we thus develop the algebraic theory of canonicity for Boolean Algebra with Expansions (BAEs), or more generally for Distributive Lattice Expansions (DLEs). We present new results about a class of expan- sions defined by weaker preservation properties than meet or join preservation, namely (anti)-k-additive and (anti-)k-multiplicative expansions. We show how canonical and Sahlqvist equations can be built from such operations. In order to connect the theory of canonicity in DLEs and BAEs to coalgebraic logic, we choose to work in the abstract formulation of coalgebraic logic. An abstract coalgebraic logic is defined by a functor L : BA → BA, and we can heuristically separate these logics in two classes. In the first class the functor L is relatively simple, and in particular can be interpreted as defining a BAE. This class includes the predicate lifting style of coalgebraic logics. In the second class the functor L can be very complicated and the whole theory requires a different approach. This class includes the nabla style of coalgebraic logics. For simple functors, we develop results on strong completeness and then prove strong completeness-via-canonicity in the presence of canonical frame con- ditions for strongly complete abstract coalgebraic logics. In particular we show coalgebraic completeness-via-canonicity for Graded Modal Logic, Intuitionistic Logic, the distributive full Lambek calculus, and the logic of trees of arbitrary branching degrees defined by the List functor. These results are to the best of our knowledge, new. For a complex functor L we use an indirect approach via the notion of functor presentation. This allows us to represent L as the quotient of a much simpler polynomial functor. Polynomial functors define BAEs and can thus be treated as objects in the first class of functors, in particular we can apply all the above mentioned techniques to the logics defined by such functors. We develop techniques that ensure that results obtained for the simple presenting logic can be transferred back to the complicated presented logic. We can then prove strong-completeness-via-canonicity in the presence of canonical frame conditions for coalgebraic logics which do not define a BAE, such as the nabla coalgebraic logics.
Content Version: Open Access
Issue Date: Mar-2015
Date Awarded: Oct-2015
URI: http://hdl.handle.net/10044/1/27689
Supervisor: Hodkinson, Ian
Sponsor/Funder: Engineering and Physical Sciences Research Council
Department: Department of Computing
Publisher: Imperial College London
Qualification Level: Doctoral
Qualification Name: Doctor of Philosophy (PhD)
Appears in Collections:Computing PhD theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commonsx