| Summary: | <p>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.</p>
<p>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.</p>
<p>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.</p>
|
|---|