Canonical Constructive Systems ⋆

Abstract

We define the notions of a canonical inference rule and a canonical system in the framework of single-conclusion Gentzen-type systems (or, equivalently, natural deduction systems), and prove that such a canonical system is non-trivial iff it is coherent (where coherence is a constructive condition). Next we develop a general non-deterministic Kripke-style semantics for such systems, and show that every constructive canonical system (i.e. coherent canonical single-conclusion system) induces a class of non-deterministic Kripke-style frames for which it is strongly sound and complete. We use this non-deterministic semantics to show that all constructive canonical systems admit a strong form of the cut-elimination theorem. We also use it for providing a decision procedure for every such system. These results identify a large family of basic constructive connectives, each having both a proof-theoretical characterization in terms of a coherent set of canonical rules, as well as a semantic characterization using non-deterministic frames. The family includes the standard intuitionistic connectives, together with many other independent connectives

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,221

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

Analytics

Added to PP
2009-02-19

Downloads
4 (#1,420,104)

6 months
0

Historical graph of downloads

Sorry, there are not enough data points to plot this chart.
How can I increase my downloads?

Author's Profile

Arnon Avron
Tel Aviv University

Citations of this work

Transitive primal infon logic.Carlos Cotrini & Yuri Gurevich - 2013 - Review of Symbolic Logic 6 (2):281-304.

Add more citations

References found in this work

No references found.

Add more references