Axioms of a Local Set Theory

Question

So this one’s from J.L. Bell’s Toposes and Local Set Theories. Taking a look at the axioms, I’m struggling to see why any sequent of the form$\emptyset$:t would be of much use... Take the axiom of “Unity” for example... what good does it do to have “the set of all$\emptyset$ such that x of type 1 equals a term of type 1” as an axiom? If the set of all$\emptyset$ is empty, then how is a supposedly “empty” set displaying “qualities” in such a sense? What am I missing here?

Answer 1

A sequent with an empty set of premises is something that's true without any additional assumptions.

The axiom of unity is saying that all terms of type $\mathbf 1$ are equal to the canonical term of type $\mathbf 1$, that is, $*$. And this is true without any assumptions. (A more modern treatment would probably put $x_{\mathbf 1}$ as a premise: $x: \mathbf 1 \vdash x = *$).

The axioms of products say that the $i$th projection of a tuple is the $i$th term of the tuple, and that any element in a product is equal to the tuple of its projections. (Again, most treatments I've seen would put variables in the premises). Other than the variables, no premises are needed.