Arnon Avron ; Ori Lahav - On Constructive Connectives and Systems

lmcs:967 - Logical Methods in Computer Science, December 25, 2010, Volume 6, Issue 4 - https://doi.org/10.2168/LMCS-6(4:12)2010
On Constructive Connectives and SystemsArticle

Authors: Arnon Avron ; Ori Lahav ORCID

    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.

    https://doi.org/10.2168/LMCS-6(4:12)2010
    Source: arXiv.org:1011.4384
    Volume: Volume 6, Issue 4
    Published on: December 25, 2010
    Imported on: June 28, 2010
    Keywords: Computer Science - Logic in Computer Science,F.4.1, I.2.3
    Licence: arXiv.org - Non-exclusive license to distribute

    Classifications

    Mathematics Subject Classification 20201
    Sources:
    • [1] zbMATH Open.

    6 Documents citing this article

    Share and export

    Consultation statistics

    This page has been seen 1833 times.
    This article's PDF has been downloaded 367 times.