UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC

DOI10.1017/BSL.2023.14MaRDI QIDQ6170504zbMATH OpenFDO

Authors G. A. Kavvos, Daniel Gratzer

Publication date 10 August 2023

Published in The Bulletin of Symbolic Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2211.06217

zbMATH Keywords

Curry-Howardmodal logicmodal type theorymultimodal logicproofs for modal logic

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40) Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Structure of proofs (03F07)

Abstract: We present a proof system for a multimodal logic, based on our previous work on a multimodal Martin-Loef 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.

Recommendations

• A systematic proof theory for several modal logics
• A modal provability logic of explicit and implicit proofs
• scientific article; zbMATH DE number 6863660
• Proof nets for the multimodal Lambek calculus
• scientific article; zbMATH DE number 4195937
• Modal multilattice logic
• A general proof certification framework for modal logic
• A multimodal logic for reasoning about complementarity
• ON DEFINABILITY IN MULTIMODAL LOGIC
• scientific article; zbMATH DE number 3845548

Cites work

• A judgmental reconstruction of modal logic
• A modal analysis of staged computation
• Adjoint logic with a 2-category of modes
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory
• Dual-context calculi for modal logic
• Dynamic epistemic logic
• Fitch-style modal lambda calculi
• scientific article; zbMATH DE number 5761737 (Why is no real title available?)
• scientific article; zbMATH DE number 3950781 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1078585 (Why is no real title available?)
• scientific article; zbMATH DE number 2079022 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 755666 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 822489 (Why is no real title available?)
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• Lectures on the Curry-Howard isomorphism
• Many-dimensional modal logics: theory and applications
• Modal and temporal properties of processes
• Modal dependent type theory and dependent right adjoints
• Modal logic
• Modalities and multimodalities. With the assistance and collaboration of Juliana Bueno-Soler.
• Modalities and Parametric Adjoints
• Multimodal dependent type theory
• Multimodal dependent type theory
• Practical foundations for programming languages
• Temporal logics in computer science. Finite-state systems

This page was built for publication: UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6170504)