On Constructive Connectives and Systems

TL;DR

This paper develops a framework for non-strict single-conclusion sequent systems, introduces a non-deterministic Kripke semantics, and provides criteria for cut-elimination and constructive connectives.

Contribution

It introduces a general semantics and coherence criterion for strong cut-elimination in non-strict sequent systems, advancing the understanding of constructive connectives.

Findings

Established a non-deterministic Kripke-style semantics.

Provided a coherence criterion for cut-elimination.

Characterized constructive connectives syntactically and semantically.

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.