Mathematical Logic Quarterly 40 (2):153-172 (1994)

The logic CD is an intermediate 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 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.
Keywords Intermediate logic  Logic with constant domains  Cut‐elimination
Categories (categorize this paper)
DOI 10.1002/malq.19940400203
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 59,677
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Intuitionistic Logic, Model Theory and Forcing.Melvin Fitting - 1969 - Amsterdam: North-Holland Pub. Co..
Semantical Investigations in Heyting's Intuitionistic Logic.Dov M. Gabbay - 1986 - Journal of Symbolic Logic 51 (3):824-824.
Intuitionistic Logic Model Theory and Forcing.F. R. Drake - 1971 - Journal of Symbolic Logic 36 (1):166-167.
Proof Theory.Gaisi Takeuti - 1975 - Elsevier.
Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.

Add more references

Citations of this work BETA

Nested Sequents for Intuitionistic Logics.Melvin Fitting - 2014 - Notre Dame Journal of Formal Logic 55 (1):41-61.

Add more citations

Similar books and articles

Linear Kripke Frames and Gödel Logics.Arnold Beckmann & Norbert Preining - 2007 - Journal of Symbolic Logic 72 (1):26 - 44.
Directed Frames.Giovanna Corsi & Silvio Ghilardi - 1989 - Archive for Mathematical Logic 29 (1):53-67.
Cut Elimination for Propositional Dynamic Logic Without.Robert A. Bull - 1992 - Mathematical Logic Quarterly 38 (1):85-100.
On the Proof Theory of the Intermediate Logic MH.Jonathan P. Seldin - 1986 - Journal of Symbolic Logic 51 (3):626-647.


Added to PP index

Total views
19 ( #547,592 of 2,432,203 )

Recent downloads (6 months)
1 ( #467,285 of 2,432,203 )

How can I increase my downloads?


My notes