Cut‐Elimination Theorem for the Logic of Constant Domains
Ryo Kashima, Tatsuya Shimura · Mathematical logic quarterly · 1994
Abstract 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.