A weak intuitionistic propositional logic with purely constructive implication (Q1102265)

By weakening the intuitionistic implication, two subsystems WLJ and SI of the sequent calculus LJ for intuitionistic logic are defined. The cut- elimination theorems for WLJ and SI are given and the corresponding constructive semantics is described. An interpretation of the system SI by means of modal operators and classical implication is considered, where a weak modal system WM is obtained. In the end of the paper, the Kripke models for WM are presented and the completeness theorem is proved.