Intuitionistic set theory

Thesis

We describe the formal system of higher—order intuitionistic logic with power types and (impredicative) comprehension which provides the basis for our "set theory"; this is adapted from the system of FOURMAN (D.Phil. Thesis, Oxford 1974), and such theories are equivalent to the notion of a topos. We interpret the basic concepts of sets, relations and functions; we consider relations of equality, apartness and order, and develop some of the intuitionistic theory of complete Heyting algebras (cHa's). We give the semantical definitions which make sheaves over a cHa into a model for the formal system. We give a unified description of the Dedekind reals and Baire space as the spaces of models of geometric propositional theories, from which follows the usual characterisation of them as they appear in sheaf models.

We investigate some notions from topology, adapting classical definitions and proofs where possible, and using sheaf models as counterexamples, especially for the Cauchy and Dedekind reals. Topologies are given by "open" sets as "closed" ones are unsuitable; strong forms of the basic separation principles arise in the presence of an apartness relation.

Well—founded relations are those satisfying the principle of induction, and well—orderings act as the unique representatives of their "ranks". This class of well-orderings has good closure properties, but they need not be linearly ordered nor have Cantor normal forms; the Hartogs' number of an infinite set forms a regular limit well-ordering. We consider some notions of cardinality, in particular the many possible notions of finiteness. For sets with apartness different ones arise; we characterise strongly the sense in which real polynomials have "finitely many" roots.

Authors: Grayson, RJ

• DOI: 10.5287/ora-azgxayaor
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English