Set types and local set theories

set theory

Another of the most fundamental concepts of modern mathematics is the notion of set or class. Class theory arose out of Frege's foundation for mathematics in Grundgesetze and in Principia along similar lines. Even before 1900 Cantor was creating a rich naive set theory which was axiomatized in 1908 by Zermelo and improved by Skolem and Fraenkel into modern day axiomatic set theories such as ZF ([11]) and BG ([51]) and Bourbaki's set theory ([16]).

We could formulate a full blown axiomatic set theory based on the type Set. But the type theory of section 3 is an alternative into which ZF can be encoded ([1]). So instead we pursue a much more modest treatment of sets along the lines of Principia's classes. In Principia, given a propositional function $\phi \hat{x}$ whose range of significance is the type A, we can form the class $\hat{x}(\phi x)$ of those elements of A satisfying $\phi$. We write this as $\{ x\!:\!A\, \vert\,\phi(x)\}$. We call this a set typeset type or a classclass. Given two classes $\alpha, \beta$ we can form the usual combinations of union, $\alpha \cup \beta$, intersection, $\alpha \cap \beta$, complement, $\bar{\alpha}$, universal class, A, and empty class, $\phi$.

The typing judgment associated with a set type is what one would expect. Suppose A is a type and $P \in A \rightarrow Prop$, then

$\bar{H} \vdash a \in \{x\!:\!A\:\vert\:P(x)\}\ \ \mbox{by}\ \ setR$

$\bar{H} \vdash a \in A$

$\ \ \bar{H} \vdash P(a)$

The rule for using an assumption about set membership is

$\bar{H}, y : \{x\!:\!A\:\vert\:P(x)\} \vdash G\ \ \ by\ setL$

$\bar{H}, y\!:\!A,\ P(y) \vdash G$

As with the other rules, we can choose to name the assumption P(y)by using the justification by $setL\ new\ u$. In Nuprl there is the option to ``hide'' the proof of P(y). This hidden version is the default in Nuprl. A hypothesis is hidden to prevent the proof object from being used in computations. This is necessary because the set membership rule, setR, does not keep track of the proof P(a); so the constructive elimination rule is

$\bar{H}, y\!:\!\left\{x\!:\!A\:\vert\:P(x)\right\}, \bar{J} \vdash G\ \ \mbox{by}\ \ IsetL, new\ u$

$\bar{H}, y\!:\!A, \left[u\!:\!P(y)\right], \bar{J} \vdash G$.

In local set theories, the concept of the power set, ${\cal P}(A)$ is introduced (c.f. [10,78]). This type collects all sets built over A and Prop. If A is a type, then ${\cal P}(A)$ is a type.

In order to express rules about this type, we need to treat the judgments $A \in Type$ and $P \in A \rightarrow Prop$ in the rules. Thus far we have expressed these judgments only implicitly, not as explicit goals, in part because Type and $A \rightarrow Prop$ are not types themselves, but ``large types.'' However, it makes sense to write a rule such as

5(160,80)[l] $\bar{H} \vdash \left\{ x\!:\!A\:\vert\:P(x)\right\} \in P(A)$
$\ \ \ \ \bar{H} \vdash A \in Type$
$\ \ \ \ \bar{H} \vdash P \in A \rightarrow Prop$

We can also imagine the rule

5(350,50) $\bar{H}, X\!:\!{\cal P}(A) \vdash \exists P\!:\!A\rightarrow Prop. \left(X = \{x\!:\!A\:\vert\: P(x)\}\ \mbox{in}\ {\cal P}(A)\right).$

This introduces the large type, $(A \rightarrow Prop)$ into the type position. Treating this concept precisely requires that we consider explicit rules for Type and Prop, especially their stratification as Type_i and Prop_i. We defer these ideas until section 3.4.

Let us note at this point that the notion of Prop and set types be at the heart of topos theorytopos theory as explained in [10]. Essentially, the subobject classifiersubobject classifier, $\Omega$ and $T\!:\!1 \rightarrow \Omega$, of topos theory is an (impredicative) notion of Prop and the subtype of true propositions. The notion of a pullbackpullback is used to define subtypes of a type A by ``pulling back'' a characteristic function $P\!:\!A \rightarrow Prop$ and the truth arrow $T\!:\!1 \rightarrow Prop$ to get the domain of P, $\{x\!:\!A\:\vert\:P(x)\}$. A topostopos is essentially a category with Cartesian products (n-ary) a subobject classifier and power objects. In other words, it is an abstraction of a type theory which has Prop, a collection of true propositions, subtypes and a power type, ${\cal P}(A)$ for each type. The notion of a Grothendieck topos Grothendieck topos (c.f. [10,78]) is essentially a predicative version of this concept. It can be defined in Martin-Löf type theory and in Nuprl, but that is beyond the scope of these notes. (However, see section .)