Modern Logic — A Survey pp 67-91 | Cite as

# Constructivist Approaches to Logic

## 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.

## Keywords

Constructivist Approach Classical Logic Intuitionistic Logic Constructive Proof Choice Sequence## Preview

Unable to display preview. Download preview PDF.

## Bibliography

- [1]L. E. J. Brouwer,
*Collected Works*, A. Heyting (ed.), North-Holland, 1974; rev.*Bull. A.M.S*.**83**(1977), 86–93.Google Scholar - [2]C. Cellucci, ‘Un connettivo per la logica intuizionista’,
*Matematiche***29**(1974), 274–290.Google Scholar - [3]M. Dummett,
*Elements of Intuitionism*, Oxford University Press, 1977.Google Scholar - [4]C. Goad, ‘Monadic Infinitary Propositional Logic: a Special Operator’,
*Reports on Mathematical Logic***10**(1978), 43–50.Google Scholar - [5]C. Jockusch, ‘Ramsey’s Theorem and Recursion Theory’,
*J. Symbolic Logic***37**(1972), 268–280.CrossRefGoogle Scholar - [6]H. J. Keisler, ‘Logic With the Quantifier “There Exist Uncountably Many”,’
*Ann. Math. Logic***1**(1970), 1–93.CrossRefGoogle Scholar - [7]G. Kreisel and J.-L. Krivine,
*Elements of Mathematical Logic*, North-Holland, 1971.Google Scholar - [8]
- [9]
- [10]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.CrossRefGoogle Scholar - [11]D. Prawitz, ‘Meaning and Proofs: On the Conflict Between Classical and Intuitionistic Logic’,
*Theoria***43**(1977), 2–40.CrossRefGoogle Scholar - [12]A. S. Troelstra,
*Choice Sequences. A Chapter of Intuitionistic Mathematics*, Oxford University Press, 1977.Google Scholar - [13]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 - [14]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*v*alid for predicates A not depending on choice sequences.Google Scholar - [15]D. P. McCullough, ‘Logical Connectives for Intuitionistic Propositional Logic’,
*J. Symbolic Logic***36**(1971), 15–20.CrossRefGoogle Scholar - [16]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 [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).Google Scholar - [17]G. Kreisel, ‘Monadic Operators Defined by Means of Propositional Quantification in Intuitionistic Logic’
*Reports on Mathematical Logic***12**(1980).Google Scholar - [18]A. S. Troelstra, On a Second Order Propositional Operator Intuitionistic Logic,
*Studia logica*, to appear.Google Scholar