On Constructive Connectives and Systems

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

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Arnon Avron, Ori Lahav
• Keywords: Canonical Inference Rules, CORR 2010, Education, Nondeterministic Kripke-style Semantics, Single-conclusion Sequent Systems