David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Bulletin of Symbolic Logic 4 (4):418-435 (1998)
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
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
Jeremy Avigad, Edward Dean & John Mumma (2009). A Formal System for Euclid's Elements. Review of Symbolic Logic 2 (4):700--768.
Paolo Maffezioli, Alberto Naibo & Sara Negri (2013). The Church–Fitch Knowability Paradox in the Light of Structural Proof Theory. Synthese 190 (14):2677-2716.
Andrew Arana (2009). On Formally Measuring and Eliminating Extraneous Notions in Proofs. Philosophia Mathematica 17 (2):208–219.
Sara Negri (2011). Proof Theory for Modal Logic. Philosophy Compass 6 (8):523-538.
Raul Hakli & Sara Negri (2011). Reasoning About Collectively Accepted Group Beliefs. Journal of Philosophical Logic 40 (4):531-555.
Similar books and articles
Arnon Avron & Anna Zamansky, A Triple Correspondence in Canonical Calculi: Strong Cut-Elimination, Coherence, and Non-Deterministic Semantics.
Gilles Dowek & Benjamin Werner (2003). Proof Normalization Modulo. Journal of Symbolic Logic 68 (4):1289-1316.
Sara Negri & Jan von Plato (2001). Sequent Calculus in Natural Deduction Style. Journal of Symbolic Logic 66 (4):1803-1816.
Roy Dyckhoff & Sara Negri (2000). Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic. Journal of Symbolic Logic 65 (4):1499-1518.
Anna Zamansky & Arnon Avron (2006). Cut-Elimination and Quantification in Canonical Systems. Studia Logica 82 (1):157 - 176.
Carlo Cellucci (2000). Analytic Cut Trees. Logic Journal of the Igpl 8 (6):733-750.
Kai Brünnler (2006). Cut Elimination Inside a Deep Inference System for Classical Predicate Logic. Studia Logica 82 (1):51 - 71.
Jan Plato Sara Negrvoni (1998). Cut Elimination in the Presence of Axioms. Bulletin of Symbolic Logic 4 (4).
Added to index2009-01-28
Total downloads13 ( #179,414 of 1,700,224 )
Recent downloads (6 months)4 ( #161,079 of 1,700,224 )
How can I increase my downloads?