|New foundations for imperative logic IV: Natural deduction|
Peter B. M. Vranas
Sentential Pure Imperative Logic (SPIL) deals with arguments from imperative premises
to imperative conclusions (i.e., pure imperative arguments) that do not contain quantifiers or modal operators. I introduce a formal language and a natural deduction system for SPIL. I provide the formal language with a semantics, and I prove that the natural deduction system is sound and complete with respect to that semantics.