Hiroakira Ono on Substructural Logics

Preface
Contents
Editors and Contributors
A Scientific Autobiography
1 My Early Days
2 A Start in Academic Life
3 Going into the Outside World
4 A New Beginning
5 Stepping Forward
6 A Few More Words
Part I Expository and Survey Chapters
Universal Algebraic Methods for Non-classical Logics
1 Introduction
2 Basic Concepts and Results
3 Terms and Term Operations
4 Permutability of Congruences
5 Variants of Distributivity
6 Abelian Algebras
7 Filtered Products
8 Definable Principal Congruences
9 Controlling Irreducible Algebras
10 Some Finite Basis Theorems
11 Lattices of Subvarieties
12 Maltsev Conditions
13 Categorical Equivalence
References
Abstract Algebraic Logic
1 Introduction
2 Some Preliminary Issues
3 Bare Algebraizability
3.1 The Equational Consequence Relative to a Class of Algebras
3.2 Translating Formulas into Equations
3.3 Translating Equations into Formulas
3.4 Putting It All Together
4 The Origins of Algebraizability: The Lindenbaum–Tarski Process
4.1 The Process for Classical Logic
4.2 The Process for Algebraizable Logics
4.3 The Universal Lindenbaum–Tarski Process: matrix semantics
4.4 Algebraizability and Matrix Semantics: Definability
4.5 Implicative Logics
5 Modes of Algebraizability, and Non-algebraizability
6 Beyond Algebraizability
6.1 The Leibniz Hierarchy
6.2 The General Definition of the Algebraic Counterpart of a Logic
6.3 The Frege Hierarchy
7 Exploiting Algebraizability: Bridge Theorems and Transfer Theorems
8 Algebraizability at a More Abstract Level
References
Topological Duality and Algebraic Completions
1 Introduction
2 Completions
2.1 Join- and Meet-Completions
2.2 Δ-Completions
3 Extensions of Maps
3.1 Extension of Residuated Families of Maps
4 Canonicity
4.1 Canonicity for LOs
4.2 Canonicity of Axioms from Substructural Logic
4.3 Class Operators and Finitely Generated Varieties
5 Connections with Topological Duality
6 Concluding Remarks
References
An Algebraic Glimpse at Bunched Implications and Separation Logic
1 Introduction
2 Logic and Algebra
2.1 Algebras
2.2 Congruences
2.3 Logic
3 Concrete Models: Standard Models of BI
3.1 Generalized PPMs
3.2 Intuitionistic Versus Classical Resource Models
3.3 Resource Allocation and Generalized Effect Algebras
3.4 Resource Separation, Memory and the Heap Model
3.5 Ambient Logic, Trees and Semistructured Data
3.6 Costs, Logic Programming and Petri Nets
4 Essentially Noncommutative Models
4.1 Weakening Relations and Relation Algebras
4.2 Language Models
5 Subvarieties of GBI-algebras and InGBI-Algebras
6 Semantics via Duality
6.1 Semantics and Duality for Heyting Algebras
6.2 Semantics and Duality for GBI-Algebras
7 Decidability Issues
7.1 Positive Decidability Results
7.2 Subvarieties with Undecidable Equational Theory
7.3 Undecidability of Quasi-Equational Theories
8 A Glimpse at Proof Theory
9 (B)BI and Separation Logic
9.1 Basic Ideas of Floyd-Hoare Logic(s)
9.2 Heap(let)s, Allocation and Separation
9.3 Local Axioms, Global Specifications and the Frame Rule
10 Proof Theory and Decidability for Fragments of SL
10.1 Sketch of a Proof System for SL
10.2 Decidability Revisited
11 Bi-Abduction: The Main Issue of SL Proof Theory
11.1 Abduction and Bi-Abduction Algebraically
11.2 Bi-Abduction in Separation Logic
12 Applications and Later Developments
12.1 Competing Formalisms
12.2 Tools
12.3 Concurrency and Algebraic Aspects
References
Part II Special Topics
Recognizability in Residuated Lattices
1 Introduction
2 Background and Motivation
3 Residuation, Residuated Lattices, and Modules over Residuated Lattices
4 Recognizable Elements in Residuated Lattices
5 Regular Elements and Boolean-Recognizability
References
Finite Embeddability Property for Residuated Lattices via Regular Languages
1 Introduction
2 Finite Embeddability Property
3 Regular Languages and Syntactic Congruences
4 Residuated Lattices Induced by a Collection of Languages
5 Analytic Identities and Corresponding Rules
6 Finite Embeddability Property
7 Applications
7.1 Integral Residuated Lattices
7.2 Knotted Residuated Lattices
7.3 Disproving the FEP
References
Cover Systems for the Modalities of Linear Logic
1 Introduction
2 Modalities on Residuated Lattices
3 Cover Systems
4 Residuated Cover Systems
5 Modal FL-Cover Systems
6 Representation of Modal FL-Algebras
7 Kripke-Type Semantics
8 Negation and Orthogonality
9 Classical/Grishin Algebras
References
A Negative Solution to Ono's Problem P52: Existence and Disjunction Properties in Intermediate Predicate Logics
1 Introduction
2 Preliminaries
2.1 Intermediate and Super-Intuitionistic Logics
2.2 Kripke Semantics
2.3 Algebraic Semantics
3 Intermediate Predicate Logics with EP but Lacking DP
4 Z-normality + EP Imply DP
5 Concluding Remarks
References
Conservative Expansions of Substructural Logics
1 Foreword
2 Introduction
3 Preliminaries
4 Adding Δ and Other Algebraic Operators
4.1 Adding Δ
4.2 Δ-expansions with Special Propositional Operators
5 Expansions with Δ and with Propositional Quantifiers with Applications to Craig's Interpolation Property
5.1 Adding Propositional Quantifiers
5.2 Craig's Interpolation Property
6 Adding Propositional Quantifiers to Δ-core Fuzzy Logics with the Finite Model Property
6.1 Algebraizable Expansions of MTL with Propositional Quantifiers
6.2 Conservative Δ-expansions of Semilinear Logics and Craig's Interpolation Property
7 Expansions of QFLΔ
7.1 Some Definitional Expansions
7.2 Induction
7.3 Expansions by Recursion and Łukasiewicz Logic
7.4 An Alternative Way to Introduce a Product in MV-Algebras
7.5 Failure of the Finite Model Property for QFLΔ(oplus,cdot)
8 Conclusions
References
Bibliography
A.1 Books
A.2 Edited Special Issues and Books
A.3 Papers