A Permutation-free Calculus for Lax Logic
Jacob M. Howe · Kent Academic Repository (University of Kent) · 2007
this paper the same `permutation-free' techniques used to develop MJ are applied to Lax Logic, giving a `permutation-free' calculus for Lax Logic. As our starting point we take the above cited papers of Fairtlough & Mendler and of Benton, Bierman & de Paiva. 2 Natural Deduction