Bell 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?

  • $\begingroup$ @SCappella yes empty set $\endgroup$ – mizejonathan17 2 days ago

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.