Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Bibliography
L. E. J. Brouwer, Collected Works, A. Heyting (ed.), North-Holland, 1974; rev. Bull. A.M.S. 83 (1977), 86–93.
C. Cellucci, ‘Un connettivo per la logica intuizionista’, Matematiche 29 (1974), 274–290.
M. Dummett, Elements of Intuitionism, Oxford University Press, 1977.
C. Goad, ‘Monadic Infinitary Propositional Logic: a Special Operator’, Reports on Mathematical Logic 10 (1978), 43–50.
C. Jockusch, ‘Ramsey’s Theorem and Recursion Theory’, J. Symbolic Logic 37 (1972), 268–280.
H. J. Keisler, ‘Logic With the Quantifier “There Exist Uncountably Many”,’ Ann. Math. Logic 1 (1970), 1–93.
G. Kreisel and J.-L. Krivine, Elements of Mathematical Logic, North-Holland, 1971.
P. Lindstrom, ‘On Extensions of Elementary Logic’, Theoria 35 (1969), 1–11.
D. A. Martin, ‘Borel Determinacy’, Ann. Math. (2) 102 (1975), 363–371.
J. Paris and L. Harrington, ‘A Mathematical Incompleteness in Peano Arithmetic’, in Handbook of Mathematical Logic, J. Barwise (ed.), North-Holland, 1977, pp. 1133–1142.
D. Prawitz, ‘Meaning and Proofs: On the Conflict Between Classical and Intuitionistic Logic’, Theoria 43 (1977), 2–40.
A. S. Troelstra, Choice Sequences. A Chapter of Intuitionistic Mathematics, Oxford University Press, 1977.
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.
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.
D. P. McCullough, ‘Logical Connectives for Intuitionistic Propositional Logic’, J. Symbolic Logic 36 (1971), 15–20.
J. Zucker, The Adequacy Problem for Inferential Logic, Preprint 37, Dept. of Mathematics, University of Utrecht, 1976.
PS (added July 1980): Further information on the operator in Example 2 of 111(a) will appear in [17] and [18]. By [17], has no basis in (⇁, ⋀, ⋁, →, o) under very general conditions on the range of propositions considered. In contrast, by [18], 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 [17], his work is incomparable with [18] since KS is an implicit restriction on the species considered, requiring them to be enumerable (by certain lawlike functions).
G. Kreisel, ‘Monadic Operators Defined by Means of Propositional Quantification in Intuitionistic Logic’ Reports on Mathematical Logic 12 (1980).
A. S. Troelstra, On a Second Order Propositional Operator Intuitionistic Logic, Studia logica, to appear.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1981 D. Reidel Publishing Company
About this chapter
Cite this chapter
Kreisel, G. (1981). Constructivist Approaches to Logic. In: Agazzi, E. (eds) Modern Logic — A Survey. Synthese Library, vol 149. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-9056-2_5
Download citation
DOI: https://doi.org/10.1007/978-94-009-9056-2_5
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-009-9058-6
Online ISBN: 978-94-009-9056-2
eBook Packages: Springer Book Archive