期刊
JOURNAL OF LOGIC AND COMPUTATION
卷 -, 期 -, 页码 -出版社
OXFORD UNIV PRESS
DOI: 10.1093/logcom/exad065
关键词
Logic; proof theory; model theory; semantics; modal logic; intuitionistic logic
This paper presents a comprehensive programme for decomposing proof systems of non-classical logics into proof systems of other logics using an algebra of constraints. By enriching simpler proof systems with constraints, proof systems for target logics can be recovered. The aim is to provide a tool for uniform and modular treatment of proof theory and establish a bridge between semantics logics and their proof theory.
We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof system for a target logic by enriching a proof system for another, typically simpler, logic with an algebra of constraints that act as correctness conditions on the latter to capture the former; e.g. one may use Boolean algebra to give constraints in a sequent calculus for classical propositional logic to produce a sequent calculus for intuitionistic propositional logic. The idea behind such forms of decomposition is to obtain a tool for uniform and modular treatment of proof theory and to provide a bridge between semantics logics and their proof theory. The paper discusses the theoretical background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics: including, a uniform treatment of modular and cut-free proof systems for a large class of propositional logics; a general criterion for a novel approach to soundness and completeness of a logic with respect to a model-theoretic semantics; and a case study deriving a model-theoretic semantics from a proof-theoretic specification of a logic.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据