Under Lock and Key: A Proof System for a Multimodal Logic

&
Bulletin of Symbolic Logic 29 (2):264-293 (2023)
  Copy   BIBTEX

Abstract

We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-Löf type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e., a small 2-category. The logic is extended to a lambda calculus, establishing a Curry–Howard correspondence.

Categories

Keywords

Reprint years

DOI

10.1017/bsl.2023.14

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,168

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Dual tableau for a multimodal logic for order of magnitude qualitative reasoning with bidirectional negligibility.Joanna Golińska-Pilarek & Emilio Munoz-Velasco - 2009 - International Journal of Computer Mathematics 86 (10-11):1707–1718.
A multimodal logic for closeness.A. Burrieza, E. Muñoz-Velasco & M. Ojeda-Aciego - 2017 - Journal of Applied Non-Classical Logics 27 (3):225-237.
Predicate Modal Logics Do Not Mix Very Well.Olivier Gasquet - 1998 - Mathematical Logic Quarterly 44 (1):45-49.
Kripke semantics and proof systems for combining intuitionistic logic and classical logic.Chuck Liang & Dale Miller - 2013 - Annals of Pure and Applied Logic 164 (2):86-111.
Goal-Driven Reasoning in First-Order Logic.Claes Strannegård - 2006 - In Björn Haglund & Helge Malmgren (eds.), Kvantifikator för en Dag. Essays dedicated to Dag Westerståhl on his sixtieth birthday. Philosophical Communications.
A Cut-free Proof System for Bounded Metric Temporal Logic Over a Dense Time Domain.Franco Montagna, G. Michele Pinna & Elisa B. P. Tiezzi - 2000 - Mathematical Logic Quarterly 46 (2):171-182.
On the proof of Solovay's theorem.Dick Jongh, Marc Jumelet & Franco Montagna - 1991 - Studia Logica 50 (1):51 - 69.
Proof nets for the multimodal Lambek calculus.Richard Moot & Quintijn Puite - 2002 - Studia Logica 71 (3):415-442.
On the proof of Solovay's theorem.Dick de Jongh, Marc Jumelet & Franco Montagna - 1991 - Studia Logica 50 (1):51-69.
Quantified Multimodal Logics in Simple Type Theory.Christoph Benzmüller & Lawrence C. Paulson - 2013 - Logica Universalis 7 (1):7-20.
A Simplified System Of Sentential Logic.Michael Goodman - 2011 - Annales Philosophici 2:35-40.
A proof–theoretic study of the correspondence of hybrid logic and classical logic.H. Kushida & M. Okada - 2006 - Journal of Logic, Language and Information 16 (1):35-61.
Deriving polarity effects.Raffaella Bernardi - unknown
Implicit proofs.Jan Krajíček - 2004 - Journal of Symbolic Logic 69 (2):387-397.
Implicit Proofs.Jan Krajíček - 2004 - Journal of Symbolic Logic 69 (2):387 - 397.

Analytics

Added to PP
2023-04-22

Downloads
14 (#993,927)

6 months
4 (#796,773)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references