Article contents
Sentences of type theory: the only sentences preserved under isomorphisms1,2
Published online by Cambridge University Press: 12 March 2014
Extract
Sometimes it is said that mathematics talks only about truths that are invariant under isomorphisms. Thus, a syntactical characterization of sentences preserved under isomorphisms seems to be important to understand what mathematics is.
The importance of such sentences is underlined, for instance, by Bourbaki's requirement in [1, Chapter IV] that all axioms for mathematical structures satisfy the condition of being what they call transportable, that is, preserved under isomorphisms. In [2, §1], a formalization of Bourbaki's notion of mathematical structure and of the notion of transportable sentence was given and discussed. We adopt here, as in [2], Bourbaki's terminology, and call a sentence φ transportable if φ is true in a structure E if and only if φ is true in any structure F isomorphic to E.
An alternative formulation for Bourbaki's notion of structure is offered in [2, §3], which is also intended as a formalization of Suppes' notion of set-theoretical predicate, as formulated, for instance, in [3]. It is this alternative formulation that we adopt here.
In [2, p. 106], it was conjectured that a set-theoretical sentence is transportable if and only if it is equivalent to a sentence of type theory. One direction of the conjecture is obvious, namely, that any sentence of type theory is transportable. It is also clear that there are sentences of set theory which are not transportable. The main purpose of the present paper is to prove the rest of the conjecture. That is, we prove here that any transportable set-theoretical sentence is equivalent to a sentence of type theory.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1991
Footnotes
Research for this paper was partially supported by FONDECYT-Chile Grant # 89033 and DIUC Grant # 89041. We thank the referee for several suggestions to improve the presentation of the paper.
After completing the proof of the main theorem of the paper, the authors received from Jeff Paris a sketch of the proof, by a different method, of the same theorem (Theorem 2.1), without including constants of higher types in the language. It is possible that his proof may also be extended to the case with constants.
References
REFERENCES
- 5
- Cited by