Constructivist Approaches to Logic
The first part of this paper recalls contributions of general philosophical interest which have been made by foundational research, and lists some specific contributions of this sort made by constructivist foundations; in particular, to the history of ideas, and to the correction of wide-spread convictions. The second part goes into the heuristic value of developing constructivist foundations systematically, and into the conflict between the (naive) requirement of (i) solving a problem by means of constructive operations, and the additional (sophisticated) requirement of establishing (i) by a constructive proof. The third part contains some new results on constructive propositional logic (also of interest to specialists in the subject), which illustrate pedagogic uses of constructivist foundations; in particular, for understanding phenomena in advanced model-theoretic socalled classical logic, in connection with functional and deductive completeness, or with extending the domain of definition of familiar operations.
KeywordsConstructivist Approach Classical Logic Intuitionistic Logic Constructive Proof Choice Sequence
Unable to display preview. Download preview PDF.
- L. E. J. Brouwer, Collected Works, A. Heyting (ed.), North-Holland, 1974; rev. Bull. A.M.S. 83 (1977), 86–93.Google Scholar
- C. Cellucci, ‘Un connettivo per la logica intuizionista’, Matematiche 29 (1974), 274–290.Google Scholar
- M. Dummett, Elements of Intuitionism, Oxford University Press, 1977.Google Scholar
- C. Goad, ‘Monadic Infinitary Propositional Logic: a Special Operator’, Reports on Mathematical Logic 10 (1978), 43–50.Google Scholar
- G. Kreisel and J.-L. Krivine, Elements of Mathematical Logic, North-Holland, 1971.Google Scholar
- A. S. Troelstra, Choice Sequences. A Chapter of Intuitionistic Mathematics, Oxford University Press, 1977.Google Scholar
- D. M. Gabbay, ‘On Some New Intuitionistic Propositional Connectives’, Studia Logica 36 (1977), 127–139. This paper could not be discussed in the body of Part Ilia because I received a reprint only after the present article was typed. Like Si in Ilia, the new operators are defined in the language of second-order propositional logic. But, in contrast to Ilia, the various meanings of ‘new’ are somewhat unorthodox (and not shown to be insensitive to the exact ranges of the propositional quantifiers, for example, by means of suitable ‘basis’ results). Specificially, by the mixed bag of conditions (l)–(6) on pp. 127–128, in Theorem A (of §1) ‘new’ does not mean demonstrably indefinable in Heyting’s system (⇁, ∧, ∨, →), but rather the consistency of assuming such indeflnability. In Theorem 3 (of § 2), where the ‘new’ (monadic) operator F is given in (c) of Def. 2.3 on p. 137, and the set of axioms T (given in the Cor. 27 on p. 138!) is valid by deductive completeness, F cannot be proved to be different from True (by use of T): in fact, ⇁⇁ ∀pF is asserted. Perhaps more conclusive indefinability results can be obtained from Gabbay’s paper by attention to the pitfalls just mention ed “Added in proof: cf. also the review in Zentralblatt f. Math”. 363 (1978), 17, No. 0 2027.Google Scholar
- H. Luckhardt, ‘Über das Markov-Prinzip II’ Archiv f. math. Logik 18 (1977), 147–157. In effect, this paper discusses the question whether [∀x(A ∨ ⇁A) ∧ ⇁⇁ ∃xA] → ∃xA is valid for predicates A not depending on choice sequences.Google Scholar
- J. Zucker, The Adequacy Problem for Inferential Logic, Preprint 37, Dept. of Mathematics, University of Utrecht, 1976.Google Scholar
- PS (added July 1980): Further information on the operator in Example 2 of 111(a) will appear in  and . By , has no basis in (⇁, ⋀, ⋁, →, o) under very general conditions on the range of propositions considered. In contrast, by , the validity of ∀p[(⇁⇁ p)] ↔ (p)] even for propositions about projections of lawless sequences, can depend sensitively on the kind of projection (or, similarly, in the case of classical topological models: on connectedness properties of the topological space) considered. There is also unpublished work by Luckhardt on propositions involving (species of) both lawless and lawlike sequences, but required to satisfy Kripke’s schema KS. Contrary to first impressions, for example, in § 3 of the PS to , his work is incomparable with  since KS is an implicit restriction on the species considered, requiring them to be enumerable (by certain lawlike functions).Google Scholar
- G. Kreisel, ‘Monadic Operators Defined by Means of Propositional Quantification in Intuitionistic Logic’ Reports on Mathematical Logic 12 (1980).Google Scholar
- A. S. Troelstra, On a Second Order Propositional Operator Intuitionistic Logic, Studia logica, to appear.Google Scholar