Embedding Constructive K into Intuitionistic K
Kurt Ranalter · Electronic Notes in Theoretical Computer Science · 2010
We investigate an embedding of CK natural deduction proofs into IK natural deduction proofs. CK and IK can both be regarded as intuitionistic analogs of the basic classical modal logic K. Since, in general, the proof theory of these logics is given by means of quite different techniques the embedding can be considered as an attempt to reconcile these two approaches. Further, we show that the embedding naturally extends to the case of CS4 and IS4, and propose a framework that allows one to obtain a modular approach for all the intermediate systems.