首页 | 本学科首页   官方微博 | 高级检索  
     检索      


Proof analysis in intermediate logics
Authors:Roy Dyckhoff  Sara Negri
Institution:1. School of Computer Science, St. Andrews University, St. Andrews, Fife, KY16 9SX, Scotland
2. Department of Philosophy, University of Helsinki, P.O. Box 24, Unioninkatu 40A, 00014, Helsinki, Finland
Abstract:Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the G?del–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the explanation of the rules.
Keywords:
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号