Hostname: page-component-cd9895bd7-fscjk Total loading time: 0 Render date: 2024-12-25T02:08:40.272Z Has data issue: false hasContentIssue false
  • English
  • Français

On the quantificational logic of intuitionistic set theory

Published online by Cambridge University Press:  24 October 2008

Harvey M. Friedman  and
Andrej Ščedrov
Harvey M. Friedman
Affiliation:
Department of Mathematics, Ohio State University, Columbus, OH 43210, U.S.A.
Andrej Ščedrov
Affiliation:
Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104, U.S.A.
Get access Rights & Permissions [Opens in a new window]

Extract

Formal propositional logic describing the laws of constructive (intuitionistic) reasoning was first proposed in 1930 by Heyting. It is obtained from classical pro-positional calculus by deleting the Law of Excluded Middle, and it is usually referred to as Heyting's (intuitionistic) propositional calculus ([9], §§23, 19) (we write HPP in short). Formal logic involving predicates and quantifiers based on HPP is called Heyting's (intuitionistic) predicate calculus ([9], §§31, 19) (we write HPR in short).

Type
Research Article
Information
Mathematical Proceedings of the Cambridge Philosophical Society , Volume 99 , Issue 1 , January 1986 , pp. 5 - 10
Copyright
Copyright © Cambridge Philosophical Society 1986

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Fourman, M. P.. Sheaf models for set theory. J. Pure Appl. Algebra 19 (1980), 91–101.Google Scholar
[2]Fourman, M. P. and Scott, D. S.. Sheaves and logic. In Applications of sheaves, ed. Fourman, M. P., Mulvey, C. J. and Scott, D. S., Lecture Notes in Math. vol. 753 (Springer-Verlag, 1979), 302–401.Google Scholar
[3]Friedman, H.. Some applications of Kleene's methods for intuitionistic systems. In Cambridge Summer School in mathematical logic 1971, ed. Mathias, A. R. D. and Rogers, H. Jr, Lecture Notes in Math. vol. 337 (Springer-Verlag, 1973), 113–170.Google Scholar
[4]Friedman, H. and ŠČedrov, A.. Arithmetic transfinite induction and recursive well-orderings. Advances in Math., 56 (1985), 283–294.Google Scholar
[5]Grayson, R.. Heyting-valued models for intuitionistic set theory. In Applications of sheaves, ed. Fourman, M. P., Mulvey, C. J. and Scott, D. S., Lecture Notes in Math. vol. 753 (Springer-Verlag, 1979), 402–414.Google Scholar
[6]Jech, T. J.. Set theory (Academic Press, 1978).Google Scholar
[7]Johnstone, P. T.. Topos theory (Academic Press, 1977).Google Scholar
[8]de Jongh, D. H. J.. The maximality of intuitionistic predicate calculus with respect to Heyting's arithmetic (abstract). J. Symbolic Logic 35 (1970), 606.Google Scholar
[9]Kleene, S. C.. Introduction to metamathematics (Wolters-Noordhoff & North-Holland, 1974).Google Scholar
[10]Leivant, D.. Absoluteness in intuitionistic logic. Mathematical Centre Tract, no. 73 (Amsterdam, 1979).Google Scholar
[11]Moerdijk, I.. Some topological spaces which are universal for intuitionistic predicate logic. Proc. Kon. Nederl. Akad. Wetensch., Ser. A, 85 (2) (1982), 227–235.Google Scholar
[12]Smoryński, C.. Applications of Kripke models. In Metamathematical investigation of intuitionistic arithmetic and analysis, ed. Troelstra, A. S., Lecture Notes in Math. vol. 344 (Springer-Verlag, 1973), 324–388.Google Scholar