Hostname: page-component-78c5997874-dh8gc Total loading time: 0 Render date: 2024-11-16T16:17:00.308Z Has data issue: false hasContentIssue false
  • English
  • Français

General models and extensionality

Published online by Cambridge University Press:  12 March 2014

Peter B. Andrews
Peter B. Andrews*
Affiliation:
Carnegie-Mellon University, Pittsburgh, Pennsylvania 15213
Get access Rights & Permissions [Opens in a new window]

Extract

It is well known that equality is definable in type theory. Thus, in the language of [2], the equality relation between elements of type α is definable as , i.e., xα = yα iff every set which contains xα also contains yα. However, in a nonstandard model of type theory, the sets may be so sparse that the wff above does not denote the true equality relation. We shall use this observation to construct a general model in the sense of [2] in which the Axiom of Extensionality is not valid. Thus Theorem 2 of [2] is technically incorrect. However, it is easy to remedy the situation by slightly modifying the definition of general model.

Our construction will show that the Axiom Schema of Extensionality is independent even if one takes as an axiom schema.

We shall assume familiarity with, and use the notation of, [2] and §§2–3 of [1].

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 37 , Issue 2 , June 1972 , pp. 395 - 397
Copyright
Copyright © Association for Symbolic Logic 1972

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

BIBLIOGRAPHY

[1]Andrews, Peter B., General models, descriptions, and choice in type theory, this Journal, vol. 37 (1972), pp. 385–394.Google Scholar
[2]Henkin, Leon, Completeness in the theory of types, this Journal, vol. 15 (1950), pp. 81–91.Google Scholar