Name
Abstract | ||
|---|---|---|
A canonical (propositional) Gentzen-type system is a system in which every rule has the subformula property, it introduces exactly one occurrence of a connective, and it imposes no restrictions on the contexts of its applications. A larger class of Gentzen-type systems which is also extensively in use is that of quasi-canonical systems. In such systems a special role is given to a unary connective \(\lnot \) of the language (usually, but not necessarily, interpreted as negation). Accordingly, each application of a logical rule in such systems introduces either a formula of the form \(\diamond (\psi _1,\ldots ,\psi _n)\), or of the form \(\lnot \diamond (\psi _1,\ldots ,\psi _n)\), and all the active formulas of its premises belong to the set \(\{\psi _1,\ldots ,\psi _n,\lnot \psi _1,\ldots ,\lnot \psi _n\}\). In this paper we investigate the whole class of quasi-canonical systems. We provide a constructive coherence criterion for such systems, and show that a quasi-canonical system is coherent iff it is analytic iff it has a characteristic non-deterministic matrix (Nmatrix) which is based on some subset of the set of the four truth-values which are used in the famous Dunn–Belnap four-valued (deterministic) matrix for information processing. In addition, we determine when a quasi-canonical system admits (strong) cut-elimination. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1007/s11229-018-02045-0 | Synthese |
Keywords | DocType | Volume |
Gentzen-type systems, Quasi-canonical systems, Non-deterministic matrices, Coherence, Negation | Journal | 198 |
Issue | ISSN | Citations |
22-S | 1573-0964 | 0 |
PageRank | References | Authors |
0.34 | 4 | 1 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Arnon Avron | 1 | 1292 | 147.65 |