On Constructive Connectives and Systems
Logic in Computer Science
2015-07-01 v2
Abstract
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 non-deterministic 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.
Cite
@article{arxiv.1011.4384,
title = {On Constructive Connectives and Systems},
author = {Arnon Avron and Ori Lahav},
journal= {arXiv preprint arXiv:1011.4384},
year = {2015}
}