Hostname: page-component-8448b6f56d-xtgtn Total loading time: 0 Render date: 2024-04-23T20:57:38.977Z Has data issue: false hasContentIssue false
  • English
  • Français

Combinator realizability of a constructive Morse set theory

Published online by Cambridge University Press:  12 March 2014

John Staples
John Staples*
Affiliation:
Australian National University, Canberra, Act 2600, Australia
Get access Rights & Permissions [Opens in a new window]

Extract

A constructive version of Morse set theory is given, based on Heyting's predicate calculus and with countable rather than full choice. An elaboration of the method of [5] is used to show that the theory is combinator-realizable in the sense defined there. The proof depends on the assumption of the syntactic consistency of the theory.

The method is introduced by first treating a subtheory without countable choice of foundation.

It is intended that the work can be read either classically or constructively, though whether the word constructive is correctly used as a description of either the theory or the metatheory is of course a matter of opinion.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 39 , Issue 2 , June 1974 , pp. 226 - 234
Copyright
Copyright © Association for Symbolic Logic 1974

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] Barendregt, Henk, Combinatory logic and the axiom of choice, Indagationes Mathematicae, vol. 35 (1973), pp. 205–221.Google Scholar
[2] Friedman, H., Some applications of Kleene's methods for intuitionistic systems, Cambridge Summer School in Mathematical Logic (Mathias, A. R. D. and Rogers, H., Editors, Springer, 1973, pp. 113–170.Google Scholar
[3] Kelley, J. L., General topology, van Nostrand, New York, 1955.Google Scholar
[4] Myhill, John, Some properties of intuitionistic Zermelo-Freankel set theory, Cambridge Summer School in Mathematical Logic (Mathias, A. R. D. and Rogers, H., Editor), Springer, Berlin, 1973, pp. 206–231.Google Scholar
[5] Staples, John, Combinator realizability of constructive finite type analysis, Cambridge Summer School in Mathematical Logic (Mathias, A. R. D. and Rogers, H., Editors), Springer, Berlin, 1973, pp. 253–273.Google Scholar