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)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Harmony and Autonomy in Classical Logic.Stephen Read - 2000 - Journal of Philosophical Logic 29 (2):123-154.
Subformula and Separation Properties in Natural Deduction Via Small Kripke Models.Peter Milne - 2010 - Review of Symbolic Logic 3 (2):175-227.
Intuitionistic Logic and Elementary Rules.L. Humberstone & D. Makinson - 2011 - Mind 120 (480):1035-1051.
Verification, Falsification, and the Logic of Enquiry.Peter Milne - 1991 - Erkenntnis 34 (1):23 - 54.
On the Role of Implication in Formal Logic.Jonathan P. Seldin - 2000 - Journal of Symbolic Logic 65 (3):1076-1114.
Classical Harmony: Rules of Inference and the Meaning of the Logical Constants.Peter Milne - 1994 - Synthese 100 (1):49 - 94.
Added to index2009-08-17
Total downloads4 ( #645,265 of 2,172,024 )
Recent downloads (6 months)0
How can I increase my downloads?