Title
Canonical Signed Calculi, Non-deterministic Matrices and Cut-Elimination
Abstract
Canonical propositional Gentzen-type calculi are a natural class of systems which in addition to the standard axioms and structural rules have only logical rules where exactly one occurrence of a connective is introduced and no other connective is mentioned. Cut-elimination in such systems is fully characterized by a syntactic constructive criterion of coherence. In this paper we extend the theory of canonical systems to the considerably more general class of signed calculi . We show that the extended criterion of coherence fully characterizes only analytic cut-elimination in such calculi, while for characterizing strong and standard cut-elimination a stronger criterion of density is required. Modular semantics based on non-deterministic matrices are provided for every coherent canonical signed calculus.
Year
DOI
Venue
2009
10.1007/978-3-540-92687-0_3
LFCS
Keywords
Field
DocType
analytic cut-elimination,stronger criterion,signed calculus,canonical system,coherent canonical,standard axiom,natural class,general class,non-deterministic matrices,syntactic constructive criterion,extended criterion
Atomic formula,Analytic proof,Discrete mathematics,Combinatorics,Algebra,Matrix (mathematics),Axiom,Constructive,Natural class,Sequent calculus,Coherence (physics),Mathematics
Conference
Volume
ISSN
Citations 
5407
0302-9743
4
PageRank 
References 
Authors
0.52
9
2
Name
Order
Citations
PageRank
Arnon Avron11292147.65
Anna Zamansky224543.38