Hostname: page-component-848d4c4894-4hhp2 Total loading time: 0 Render date: 2024-05-05T19:01:30.396Z Has data issue: false hasContentIssue false

Extending Gödel's negative interpretation to ZF

Published online by Cambridge University Press:  12 March 2014

William C. Powell*
Affiliation:
Suny at Buffalo, Amherst, New York 14226

Extract

In [5] Gödel interpreted Peano arithmetic in Heyting arithmetic. In [8, p. 153], and [7, p. 344, (iii)], Kreisel observed that Gödel's interpretation extended to second order arithmetic. In [11] (see [4, p. 92] for a correction) and [10] Myhill extended the interpretation to type theory. We will show that Gödel's negative interpretation can be extended to Zermelo-Fraenkel set theory. We consider a set theory T formulated in the minimal predicate calculus, which in the presence of the full law of excluded middle is the same as the classical theory of Zermelo and Fraenkel. Then, following Myhill, we define an inner model S in which the axioms of Zermelo-Fraenkel set theory are true.

More generally we show that any class X that is (i) transitive in the negative sense, ∀xXyx ¬ ¬ xX, (ii) contained in the class St = {x: ∀u(¬ ¬ uxux)} of stable sets, and (iii) closed in the sense that ∀x(xX ∼ ∼ xX), is a standard model of Zermelo-Fraenkel set theory. The class S is simply the ⊆-least such class, and, hence, could be defined by S = ⋂{X: ∀x(x ⊆ ∼ ∼ X→ ∼ ∼ xX)}. However, since we can only conservatively extend T to a class theory with Δ01-comprehension, but not with Δ11-comprehension, we will give a Δ01-definition of S within T.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1975

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]Friedman, H., Some applications of Kleene's methods for intuitionistic systems, Cambridge Summer School in Mathematical Logic, Springer Lecture Notes, vol. 337 (1974), pp. 113170.CrossRefGoogle Scholar
[2]Friedman, H., The consistency of classical set theory relative to a set theory with intuitionistic logic, this Journal, vol. 38 (1973), pp. 315319.Google Scholar
[3]Goodman, N. D. and Myhill, J., The axiom of choice and the law of excluded middle, Bulletin of the American Mathematical Society (submitted).Google Scholar
[4]Goodman, N. D. and Myhill, J., The formalization of Bishop's constructive mathematics, Toposes, algebraic geometry and logic, Springer Lecture Notes, vol. 274 (1972), pp. 8396.CrossRefGoogle Scholar
[5]Gödel, K., Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines mathematische Kolloquium (for 1931–32, pub. 1933), pp. 3438.Google Scholar
[6]Heyting, A., Infinitistic methods from a finite point of view, Infinitistic methods, Warsaw, pp. 185192.Google Scholar
[7]Kreisel, G., A survey of proof theory, this Journal, vol. 33 (1968), pp. 321388.Google Scholar
[8]Kreisel, G., Functions, ordinals, species, Logic, Methodology and the Philosophy of Science III, North-Holland, Amsterdam, 1968, pp. 143158.Google Scholar
[9]Myhill, J., Constructive set theory, this Journal, vol. 40 (1975) (to appear).Google Scholar
[10]Myhill, J., Embedding classical type theory in intuitionistic logic, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 19 (1973), pp. 9396.CrossRefGoogle Scholar
[11]Myhill, J., Embedding classical type theory in ‘intuitionistic’ type theory, Proceedings of Symposia in Pure Mathematics, Part I (Scott, D., Editor), vol. 13, Part I, American Mathematical Society, Providence, R.I., pp. 267270.Google Scholar
[12]Myhill, J., Some properties of intuitionistic Zermelo-Fraenkel set theory, Cambridge Summer School in Mathematical Logic, Springer Lecture Notes, vol. 337 (1974), pp. 206231.CrossRefGoogle Scholar
[13]Powell, W., A completeness theorem for Zermelo-Fraenkel set theory, this Journal (accepted).Google Scholar
[14]Powell, W., Heyting-valued models (in preparation).Google Scholar
[15]Smorynski, C., Applications of Kripke models, Metamathematical investigations of intuitionistic arithmetic and analysis (Troelstra, A.S., Editor), Springer Lecture Notes, vol. 344 (1973), pp. 324391.CrossRefGoogle Scholar