Propositional lax logic (Q1368378)

The authors investigate the use of a special intuitionistic modal logic with several applications to the performance evaluation of computer hardware. The logic contains a single modal operator enjoying aspects of ``possibility'' and ``necessity''. Several formal properties of the logic are well developed. E.g., (1) a cut-elimination theorem for the usual Gentzen-style sequent presentation of the logic, (2) a major Deduction Theorem, (3) the completeness of the logic with respect to Kripke constraint models, and (4) the finite model property for the logic relative to the class of constraint models. Early examples of mention of a similar modal operator by \textit{H. B. Curry} [A theory of formal deducibility (Notre Dame Math. Lectures, Volume 6) (1950; Zbl 0041.34807)] have come a long way!