Title
Cut elimination in the presence of axioms
Abstract
A way is found to add axioms to sequent calculi that maintains the eliminability of cut, through the representation of axioms as rules of inference of a suitable form. By this method, the structural analysis of proofs is extended from pure logic to free-variable theories, covering all classical theories, and a wide class of constructive theories. All results are proved for systems in which also the rules of weakening and contraction can be eliminated. Applications include a system of predicate logic with equality in which also cuts on the equality axioms are eliminated.
Year
DOI
Venue
1998
10.2307/420956
BULLETIN OF SYMBOLIC LOGIC
Keywords
Field
DocType
structure analysis
Discrete mathematics,Axiom,Mathematics
Journal
Volume
Issue
ISSN
4
4
1079-8986
Citations 
PageRank 
References 
42
4.81
1
Authors
2
Name
Order
Citations
PageRank
Sara Negri128024.76
Jan Von Plato219429.54