TR-2004003: Intuitionistic Logic with Classical Atoms
Hidenori Kurokawa · CUNY Academic Works (City University of New York) · 2004
In this paper, we define a Hilbert-style axiom system IPC CA that conservatively extends intuitionistic propositional logic (IPC) by adding new classical atoms for which the law of excluded middle (LEM) holds.We establish completeness of IPC CA with respect to an appropriate class of Kripke models.We show that IPC CA is a conservative extension of both classical propositional logic (CPC) and also IPC.We further investigate the disjunction property in IPC CA .In particular, we show that the disjunction property holds for every formula A ∨ B if either A or B does not contain classical atoms. 1