ellucci, C., Existential instantiation and normalization in sequent natural deduction, Annals of Pure and Applied Logic 58 111–148. A sequent conclusion natural deduction system is introduced in which classical logic is treated per se, not as a special case of intuitionistic logic. The system includes an existential instantiation rule and involves restrictions on the discharge rules. Contrary to the standard formula conclusion natural deduction systems for classical logic, its normal derivations satisfy both the subformula property and the separation property and (...) allow to establish a version of the midsequent theorem and Herbrand's theorem. (shrink)

The concept of “necessity of thought” plays a central role in Dag Prawitz’s essay “Logical Consequence from a Constructivist Point of View” (Prawitz 2005). The theme is later developed in various articles devoted to the notion of valid inference (Prawitz, 2009, forthcoming a, forthcoming b). In section 1 I explain how the notion of necessity of thought emerges from Prawitz’s analysis of logical consequence. I try to expound Prawitz’s views concerning the necessity of thought in sections 2, 3 and 4. (...) In sections 5 and 6 I discuss some problems arising with regard to Prawitz’s views. (shrink)