Premium
Cut‐Elimination Theorem for the Logic of Constant Domains
Author(s) -
Kashima Ryo,
Shimura Tatsuya
Publication year - 1994
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19940400203
Subject(s) - mathematics , intuitionistic logic , intermediate logic , axiom , discrete mathematics , constant (computer programming) , many valued logic , minimal logic , calculus (dental) , pure mathematics , linear logic , multimodal logic , zeroth order logic , computer science , description logic , theoretical computer science , medicine , geometry , dentistry , programming language
The logic CD is an intermediate logic (stronger than intuitionistic logic and weaker than classical logic) which exactly corresponds to the Kripke models with constant domains. It is known that the logic CD has a Gentzen‐type formulation called LD (which is same as LK except that (→) and (⊃–) rules are replaced by the corresponding intuitionistic rules) and that the cut‐elimination theorem does not hold for LD . In this paper we present a modification of LD and prove the cut‐elimination theorem for it. Moreover we prove a “weak” version of cut‐elimination theorem for LD , saying that all “cuts” except some special forms can be eliminated from a proof in LD . From these cut‐elimination theorems we obtain some corollaries on syntactical properties of CD : fragments collapsing into intuitionistic logic. Harrop disjunction and existence properties, and a fact on the number of logical symbols in the axiom of CD . Mathematics Subject Classification : 03B55. 03F05.