David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
In natural deduction classical logic is commonly formulated by adding a rule such as Double Negation Elimination (DNE) or Classical Reductio ad Absurdum (CRA) to a set of introduction and elimination rules sufficient for intuitionist first-order logic with conjunction, disjunction, implication, negation and the universal and existential quantifiers all taken as primitive. The natural deduction formulation of intuitionist logic, coming from Gentzen, has nice properties:— (i) the separation property: an intuitionistically valid inference is derivable using only the introduction and elimination rules governing the connectives and/or quantifiers that occur in the premises (if any) and conclusion; (ii) the (strict) subformula property: more narrowly, there is a derivation of any intuitionistically valid inference that employs only subformulas of the formulas occurring in premises (if any) and conclusion. (Every formula is, of course, a subformula of itself.).
|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
No citations found.
Similar books and articles
Ross Thomas Brady (2010). Free Semantics. Journal of Philosophical Logic 39 (5):511 - 529.
Jonathan P. Seldin (2000). On the Role of Implication in Formal Logic. Journal of Symbolic Logic 65 (3):1076-1114.
Sara Negri (2002). Varieties of Linear Calculi. Journal of Philosophical Logic 31 (6):569-590.
Peter Milne (1991). Verification, Falsification, and the Logic of Enquiry. Erkenntnis 34 (1):23 - 54.
L. Humberstone & D. Makinson (2012). Intuitionistic Logic and Elementary Rules. Mind 120 (480):1035-1051.
Hartley Slater (2008). Harmonising Natural Deduction. Synthese 163 (2):187 - 198.
Peter Milne (2010). Subformula and Separation Properties in Natural Deduction Via Small Kripke Models. Review of Symbolic Logic 3 (2):175-227.
Stephen Read (2000). Harmony and Autonomy in Classical Logic. Journal of Philosophical Logic 29 (2):123-154.
Peter Milne (1994). Classical Harmony: Rules of Inference and the Meaning of the Logical Constants. Synthese 100 (1):49 - 94.
Added to index2009-08-17
Total downloads4 ( #530,072 of 1,789,836 )
Recent downloads (6 months)0
How can I increase my downloads?