On Constructive Connectives and Systems

Canonical inference rules and canonical systems are defined in the frameworkof non-strict single-conclusion sequent systems, in which the succeedents ofsequents can be empty. Important properties of this framework are investigated,and a general non-deterministic Kripke-style semantics is provided. Thisgeneral semantics is then used to provide a constructive (and very natural),sufficient and necessary coherence criterion for the validity of the strongcut-elimination theorem in such a system. These results suggest new syntacticand semantic characterizations of basic constructive connectives