David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Philosophical Logic 25 (6):581 - 596 (1996)
Let ⊢ be the ordinary deduction relation of classical first-order logic. We provide an "analytic" subrelation ⊢a of ⊢ which for propositional logic is defined by the usual "containment" criterion Γ ⊢a φ iff Γ⊢φ and Atom(φ) ⊆ Atom(Γ), whereas for predicate logic, ⊢a is defined by the extended criterion Γ⊢aφ iff Γ⊢aφ and Atom(φ) ⊆' Atom(Γ), where Atom(φ) ⊆' Atom(Γ) means that every atomic formula occurring in φ "essentially occurs" also in Γ. If Γ, φ are quantifier-free, then the notions "occurs" and "essentially occurs" for atoms between Γ and φ coincide. If ⊢ is formalized by Gentzen's calculus of sequents, then we show that ⊢a is axiomatizable by a proper fragment of analytic inference rules. This is mainly due to cut elimination. By "analytic inference rule" we understand here a rule r such that, if the sequent over the line is analytic, then so is the sequent under the line. We also discuss the notion of semantic relevance as contrasted to the previous syntactic one. We show that when introducing semantic sequents as axioms, i.e. when extending the pure logical axioms and rules by mathematical ones, the property of syntactic relevance is lost, since cut elimination no longer holds. We conclude that no purely syntactic notion of analytic deduction can ever replace successfully the complex semantico-syntactic deduction we already possess
|Keywords||analytic inference rule analytic deduction Gentzen sequent calculus cut-free proof|
|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
No citations found.
Similar books and articles
Janusz Czelakowski (1986). Local Deductions Theorems. Studia Logica 45 (4):377 - 391.
Andrzej Indrzejczak (2003). A Labelled Natural Deduction System for Linear Temporal Logic. Studia Logica 75 (3):345 - 376.
Torben BraÜner (2005). Natural Deduction for First-Order Hybrid Logic. Journal of Logic, Language and Information 14 (2):173-198.
Francis Jeffry Pelletier (1999). A Brief History of Natural Deduction. History and Philosophy of Logic 20 (1):1-31.
Greg Restall & Francesco Paoli (2005). The Geometry of Non-Distributive Logics. Journal of Symbolic Logic 70 (4):1108 - 1126.
Gerhard Schurz (1991). Relevant Deduction. Erkenntnis 35 (1-3):391 - 437.
Raymond M. Smullyan (1965). Analytic Natural Deduction. Journal of Symbolic Logic 30 (2):123-139.
Janusz Czelakowski (1985). Algebraic Aspects of Deduction Theorems. Studia Logica 44 (4):369 - 387.
Yannis Delmas-Rigoutsos (1997). A Double Deduction System for Quantum Logic Based on Natural Deduction. Journal of Philosophical Logic 26 (1):57-67.
Dag Prawitz (1965/2006). Natural Deduction: A Proof-Theoretical Study. Dover Publications.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads2 ( #345,268 of 1,098,889 )
Recent downloads (6 months)2 ( #174,745 of 1,098,889 )
How can I increase my downloads?