From Indexed Lax Logic to Intuitionistic Logic
Deepak Garg, Michael Carl Tschantz · 2008
We present translations from a logic with indexed lax modalities to first-order intuitionistic logic and intuitionistic linear logic. These translations rely on a continuation passing style encoding for the lax modalities. We show that our translations preserve provability of formulas. 1 This author was partially sponsored by the Air Force Research Laboratory under grant no. FA87500720028.