The Semantics and Proof Theory of the Logic of Bunched ImplicationsSpringer Science & Business Media, 17 avr. 2013 - 290 pages This is a monograph about logic. Specifically, it presents the mathe matical theory of the logic of bunched implications, BI: I consider Bl's proof theory, model theory and computation theory. However, the mono graph is also about informatics in a sense which I explain. Specifically, it is about mathematical models of resources and logics for reasoning about resources. I begin with an introduction which presents my (background) view of logic from the point of view of informatics, paying particular attention to three logical topics which have arisen from the development of logic within informatics: • Resources as a basis for semantics; • Proof-search as a basis for reasoning; and • The theory of representation of object-logics in a meta-logic. The ensuing development represents a logical theory which draws upon the mathematical, philosophical and computational aspects of logic. Part I presents the logical theory of propositional BI, together with a computational interpretation. Part II presents a corresponding devel opment for predicate BI. In both parts, I develop proof-, model- and type-theoretic analyses. I also provide semantically-motivated compu tational perspectives, so beginning a mathematical theory of resources. I have not included any analysis, beyond conjecture, of properties such as decidability, finite models, games or complexity. I prefer to leave these matters to other occasions, perhaps in broader contexts. |
Table des matières
INTRODUCTION TO PART I | 3 |
NATURAL DEDUCTION FOR PROPOSITIONAL BI | 13 |
ALGEBRAIC TOPOLOGICAL CATEGORICAL | 33 |
KRIPKE SEMANTICS | 51 |
TOPOLOGICAL KRIPKE SEMANTICS | 67 |
PROPOSITIONAL BI AS A SEQUENT CALCULUS | 89 |
TOWARDS CLASSICAL PROPOSITIONAL BI | 97 |
BUNCHED LOGICAL RELATIONS | 107 |
The AAcalculus | 213 |
Context Joining | 219 |
Variable Sharing | 221 |
Equality | 223 |
The Propositionsastypes Correspondence | 225 |
Kripke Resource Semantics for A | 227 |
Kripke Resource Astructure | 228 |
Kripke Resource AAmodel | 234 |
THE SHARING INTERPRETATION I | 121 |
INTRODUCTION TO PART II | 147 |
THE SYNTAX OF PREDICATE BI | 157 |
NATURAL DEDUCTION SEQUENT CALCULUS | 163 |
KRIPKE SEMANTICS FOR PREDICATE BI | 179 |
TOPOLOGICAL KRIPKE SEMANTICS FOR PREDICATE BI | 201 |
Soundness and Completeness for predicate BI with | 202 |
RESOURCE SEMANTICS TYPE THEORY FIBRED CATEGORIES | 207 |
Logical Frameworks | 209 |
Soundness and Completeness | 243 |
A Class of Settheoretic Models | 253 |
Towards Systematic Substructural Type Theory | 257 |
THE SHARING INTERPRETATION II | 263 |
with References in RLF | 267 |
Bibliography | 271 |
283 | |
Autres éditions - Tout afficher
The Semantics and Proof Theory of the Logic of Bunched Implications David J. Pym Aucun aperçu disponible - 2010 |
The Semantics and Proof Theory of the Logic of Bunched Implications David J. Pym Aucun aperçu disponible - 2002 |
Expressions et termes fréquents
additive arrow axiom BI's bunch of variables bunched logic cartesian Chapter clauses closed structure combination conjunction connectives consider construction context corresponding defined definition denote dependent type theory Dereliction disjunction example exists extended fibred follows formulate function space functor functor categories Galmiche given Grothendieck Grothendieck topology implication induction hypothesis introduction rule intuitionistic logic Ishtiaq and Pym isomorphism judgement Kripke models Kripke resource Kripke semantics Lambek and Scott LEMMA logic programming logical framework maps meta-logic monoidal category monoidal closed multiplicative natural deduction notion O'Hearn and Pym predicate premisses preordered commutative monoid prime evaluation proof theory proofs in NBI Prop propositional provable quantifiers redex reduction relation sequent calculus sharing interpretation signature substructural logic symmetric monoidal tensor product theorem tion type theory worlds X)um XA-calculus ΓΕ ΓΕΦ ΓΗΣ ΔΕ Φι