Hostname: page-component-cd9895bd7-7cvxr Total loading time: 0 Render date: 2024-12-27T02:09:46.151Z Has data issue: false hasContentIssue false
  • English
  • Français

Intuitionistic sets and ordinals

Published online by Cambridge University Press:  12 March 2014

Paul Taylor
Paul Taylor*
Affiliation:
Department of Computing, Imperial College, London SW7 2BZ, England, E-mail: [email protected]
*
Department of Computer Science, Queen Mary and Westfield College, University of London, London E1 4NS, England, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Transitive extensional well founded relations provide an intuitionistic notion of ordinals which admits transfinite induction. However these ordinals are not directed and their successor operation is poorly behaved, leading to problems of functoriality.

We show how to make the successor monotone by introducing plumpness, which strengthens transitivity. This clarifies the traditional development of successors and unions, making it intuitionistic; even the (classical) proof of trichotomy is made simpler. The definition is, however, recursive, and, as their name suggests, the plump ordinals grow very rapidly.

Directedness must be defined hereditarily. It is orthogonal to the other four conditions, and the lower powerdomain construction is shown to be the universal way of imposing it.

We treat ordinals as order-types, and develop a corresponding set theory similar to Osius' transitive set objects. This presents Mostowski's theorem as a reflection of categories, and set-theoretic union is a corollary of the adjoint functor theorem. Mostowski's theorem and the rank for some of the notions of ordinal are formulated and proved without the axiom of replacement, but this seems to be unavoidable for the plump rank.

The comparison between sets and toposes is developed as far as the identification of replacement with completeness, and there are some suggestions for further work in this area.

Each notion of set or ordinal defines a free algebra for one of the theories discussed by Joyal and Moerdijk, namely joins of a family of arities together with an operation s satisfying conditions such as x ≤ sx, monotonicity or s(x ∨ y) ≤ sx ∨ sy.

Finally we discuss the fixed point theorem for a monotone endofunction s of a poset with least element and directed joins. This may be proved under each of a variety of additional hypotheses. We explain why it is unlikely that any notion of ordinal obeying the induction scheme for arbitrary predicates will prove the pure result.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 61 , Issue 3 , September 1996 , pp. 705 - 744
Copyright
Copyright © Association for Symbolic Logic 1996

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]Aczel, Peter, Non-well-founded sets, CSLI Lecture Notes 14, Center for the Study of Language and Information, Stanford University, Stanford, California, 1988.Google Scholar
[2]Bell, John, Toposes and local set theories: an introduction, Clarendon Press, Oxford, 1988.Google Scholar
[3]Burali-Forti, Cesare, Una questione sui numeri transfiniti, Rendiconti del Circolo Matematico di Palermo, vol. 11 (1897), pp. 154–164; English translation, A question on tranfinite numbers and on well-ordered classes, in [32], pp. 104–111.CrossRefGoogle Scholar
[4]Cantor, Georg, Über unendliche, lineare Punktmannigfaltigkeiten, Mathematische Annalen, vol. 21 (1883), pp. 546–591.CrossRefGoogle Scholar
[5]Conway, John, On numbers and games, Academic Press, New York, 1976.Google Scholar
[6]Fraenkel, Abraham, Über die Grundlagen der Cantor-Zermeloschen Mengenlehre, Mathematische Annalen, vol. 86 (1922), pp. 230–237.CrossRefGoogle Scholar
[7]Friedman, Harvey and Scedrov, Andre, The lack of definable witnesses and provably total functions in intuitionistic set theories, Advances in Mathematics, vol. 57 (1985), pp. 1–13.CrossRefGoogle Scholar
[8]Girard, Jean-Yves, logic. Part I: Dilators, Annals of Mathematical Logic, vol. 21 (1981), pp. 75–219.CrossRefGoogle Scholar
[9]Gödel, Kurt, The consistency of the axiom of choice and the continuum hypothesis, Proceedings of the National Academy of Sciences of the United States of America, vol. 24 (1938), pp. 556–557; reprinted in his The consistency of the continuum hypothesis, Annals of Mathematics Studies, vol. 3, Princeton University Press, Princeton, New Jersey, 1940.CrossRefGoogle ScholarPubMed
[10]Grayson, Robin, Heyting valued modelsfor intuitionistic set theory, in Fourman, Michael P., Mulvey, Chris J., and Scott, Dana S., editors, Applications of sheaves, Lecture Notes in Mathematics, vol. 753, Springer-Verlag, Berlin, 1977, pp. 402–414.CrossRefGoogle Scholar
[11]Hartogs, Friedrich, Über das Problem der Wohlordnung, Mathematische Annalen, vol. 76 (1915), pp. 436–443.CrossRefGoogle Scholar
[12]Hyland, Martin and Pitts, Andrew, The theory of constructions: Categorical semantics and topostheoretic models, in Gray, John and Scedrov, Andre, editors, Categories in computer science and logic, Contemporary Mathematics, vol. 92, American Mathematical Society, Providence, Rhode Island, 1989, pp. 137–199.CrossRefGoogle Scholar
[13]Johnstone, Peter, Topos theory, Academic Press, London, 1977.Google Scholar
[14]Johnstone, Peter and Vickers, Steven, Preframe presentations present, in Carboni, Aurelio, Pedicchio, Cristina, and Rosolini, Giuseppe, editors, Category theory — Proceedings, Como, 1990, Lecture Notes in Mathematics, vol. 1488, Springer-Verlag, Berlin, 1991, pp. 193–212.Google Scholar
[15]Joyal, André and Moerdijk, Ieke, Algebraic Set Theory, London Mathematical Society Lecture Note Series, no. 220, Cambridge University Press, Cambridge, 1995.CrossRefGoogle Scholar
[16]Knuth, Donald E., Surreal numbers, Addison-Wesley, Reading, Massachusetts, 1974.Google Scholar
[17]Lambek, Jim and Scott, Philip, Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, Cambridge, 1986.Google Scholar
[18]Lawvere, William, An elementary theory of the category of sets, Proceedings of the National Academy of Sciences of the United States of America, vol. 52 (1964), pp. 1506–1511.CrossRefGoogle ScholarPubMed
[19]Mathias, Adrian, The ignorance of Bourbaki, Mathematical Intelligencer, vol. 14 (1992) no. 3, pp. 4–13.CrossRefGoogle Scholar
[19a]Mirimanoff, Dimitry, Les antinomies de Russell et de Burali-Forti et le probléme fondamental de la théorie des ensembles, and Remarques sur la théorie des ensembles et les antinomies cantoriennes. I, L'Enseignement Mathématique, vol. 19 (1917), pp. 37–52, 209–217.Google Scholar
[20]Montague, Richard, Well founded relations; generalisations of principles of induction and recursion, Bulletin of the American Mathematical Society, vol 61 (1955), p. 442.Google Scholar
[20a]Moore, Gregory H., Zermelo's axiom of choice, Springer-Verlag, Berlin, 1982.CrossRefGoogle Scholar
[21]Mostowski, Andrzej, An undecidable arithmetical statement, Fundamenta Mathematica, vol. 36 (1949), pp. 143–164.CrossRefGoogle Scholar
[22]Osius, Gerhard, Categorical set theory: a characterisation of the category of sets, Journal of Pure and Applied Algebra, vol. 4 (1974), pp. 79–119.CrossRefGoogle Scholar
[23]Pitts, Andrew, A co-induction principle for recursively defined domains, Theoretical Computer Science, vol. 124 (1994), pp. 195–219.CrossRefGoogle Scholar
[24]Pitts, Andrew and Taylor, Paul, A note on Russell's paradox in locally cartesian closed categories, Studia Logica, vol. 48 (1989), pp. 377–387.CrossRefGoogle Scholar
[25]Powell, William, Extending Gödel's negative interpretation to ZF, this Journal, vol. 40 (1975), pp. 221–229.Google Scholar
[26]Skolem, Thoralf, Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre, in Matematikerkongressen i Helsingfors den 4–7 Juli 1922, Den Funfe Skandinaviska Matematikenkongressen, Rodogörelse, Akademiska Bokhandeln, Helsinki, 1922, pp. 217–232; English translation, Some remarks on axiomatised set theory, in [32], pp. 290–301.Google Scholar
[27]Tarski, Alfred, A lattice-theoretic fixed point theorem and its applications, Pacific Journal of Mathematics, vol. 5 (1955), pp. 285–309.CrossRefGoogle Scholar
[28]Taylor, Paul, Quantitative domains, groupoids and linear logic, in Pitt, Davidet al., editors, Category theory and computer science 3, Lecture Notes in Computer Science, vol. 389, Springer-Verlag, Berlin, 1989, pp. 155–181.CrossRefGoogle Scholar
[29]Taylor, Paul, The fixed point property in synthetic domain theory, in Kahn, Gilles, editor, Logic in computer science 6, IEEE Computer Society Press, Washington, D.C., 1991, pp. 152–160.Google Scholar
[30]Taylor, Paul, Practical foundations, Cambridge University Press, Cambridge (in preparation).Google Scholar
[31]Taylor, Paul, Towards a unified theory of induction, Work in progress, to be presented at Logical Foundations of Mathematics, Computer Science and Physics—Kurt Gödel's Legacy (Gödel '96), Brno, 08 1996. Available from the Hypatia Electronic Library, http://hypatia.dcs.qmw.ac.uk.Google Scholar
[32]van Heijenoort, Jan, From Frege to Gödel: a source book in mathematical logic, 1879–1931, Harvard University Press, Cambridge, Massachusetts, 1967.Google Scholar
[33]Vermeulen, Japie, A note on iterative arguments in a topos, Mathematical Proceedings of the Cambridge Philosophical Society, vol. 111 (1992), pp. 57–62.CrossRefGoogle Scholar
[34]von Neumann, John, Zur Einführung der transfiniten Zahlen, Acta Litterarum ac Scientiarum Regiae Universitatis Hungaricae Franscisco-Josephinae, Section Scientiarum Mathematicarum, vol. 1 (1923), pp. 199–208; English translation, On the introduction of transfinite numbers, in [32], pp. 346–354.Google Scholar
[35]Zermelo, Ernst, Neuer Beweis für die Möglichkeit einer Wohlordnung, Mathematische Annalen, vol. 65 (1908), pp. 107–128; English translation, New proof that every set can be well ordered, in [32], pp. 183–198.CrossRefGoogle Scholar
[36]Zermelo, Ernst, Untersuchungen über die Grundlagen der Mengenlehre. I, Mathematische Annalen, vol. 59 (1908), pp. 261–281; English translation, Investigations in the foundations of set theory. I, in [32], pp. 199–215.CrossRefGoogle Scholar