Constructivist Approaches to Logic

  • G. Kreisel
Part of the Synthese Library book series (SYLI, volume 149)


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.


Constructivist Approach Classical Logic Intuitionistic Logic Constructive Proof Choice Sequence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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. [2]
    C. Cellucci, ‘Un connettivo per la logica intuizionista’, Matematiche 29 (1974), 274–290.Google Scholar
  3. [3]
    M. Dummett, Elements of Intuitionism, Oxford University Press, 1977.Google Scholar
  4. [4]
    C. Goad, ‘Monadic Infinitary Propositional Logic: a Special Operator’, Reports on Mathematical Logic 10 (1978), 43–50.Google Scholar
  5. [5]
    C. Jockusch, ‘Ramsey’s Theorem and Recursion Theory’, J. Symbolic Logic 37 (1972), 268–280.CrossRefGoogle Scholar
  6. [6]
    H. J. Keisler, ‘Logic With the Quantifier “There Exist Uncountably Many”,’ Ann. Math. Logic 1 (1970), 1–93.CrossRefGoogle Scholar
  7. [7]
    G. Kreisel and J.-L. Krivine, Elements of Mathematical Logic, North-Holland, 1971.Google Scholar
  8. [8]
    P. Lindstrom, ‘On Extensions of Elementary Logic’, Theoria 35 (1969), 1–11.CrossRefGoogle Scholar
  9. [9]
    D. A. Martin, ‘Borel Determinacy’, Ann. Math. (2) 102 (1975), 363–371.CrossRefGoogle Scholar
  10. [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. [11]
    D. Prawitz, ‘Meaning and Proofs: On the Conflict Between Classical and Intuitionistic Logic’, Theoria 43 (1977), 2–40.CrossRefGoogle Scholar
  12. [12]
    A. S. Troelstra, Choice Sequences. A Chapter of Intuitionistic Mathematics, Oxford University Press, 1977.Google Scholar
  13. [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. [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 valid for predicates A not depending on choice sequences.Google Scholar
  15. [15]
    D. P. McCullough, ‘Logical Connectives for Intuitionistic Propositional Logic’, J. Symbolic Logic 36 (1971), 15–20.CrossRefGoogle Scholar
  16. [16]
    J. Zucker, The Adequacy Problem for Inferential Logic, Preprint 37, Dept. of Mathematics, University of Utrecht, 1976.Google Scholar
  17. 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
  18. [17]
    G. Kreisel, ‘Monadic Operators Defined by Means of Propositional Quantification in Intuitionistic Logic’ Reports on Mathematical Logic 12 (1980).Google Scholar
  19. [18]
    A. S. Troelstra, On a Second Order Propositional Operator Intuitionistic Logic, Studia logica, to appear.Google Scholar

Copyright information

© D. Reidel Publishing Company 1981

Authors and Affiliations

  • G. Kreisel
    • 1
  1. 1.Stanford UniversityUSA

Personalised recommendations