Unique Existence In Local Set Theories

Question

I am working through Toposes and Local Set Theories by Bell. I would like to know the proof of this expression from page 82:

$$(\exists ! w)\alpha, \alpha(w/true),\alpha \vdash w = true $$

I would like the proof to be based on local set theory/ Mitchell–Bénabou language (i.e., the internal language of a topos).

Any help would be much appreciated.

Answer 1

This may be a bit tedious so let me give you an outline (references are from Bell):

1. Expand the definition of $\exists!$ $$\exists w.(\alpha\wedge \forall u.\alpha(w/u)\to w=u),\alpha(w/true),\alpha\vdash w=true$$

2. Use proposition 3.7.3 to eliminate the existential on the left and introduce a fresh variable $v$, $$\alpha(w/v)\wedge\forall u.\alpha(w/u)\to v=u,\alpha(w/true),\alpha\vdash w=true$$

3. Use proposition 3.3.1 to eliminate the conjunction on the left $$\alpha(w/v),\forall u.\alpha(w/u)\to v=u,\alpha(w/true),\alpha\vdash w=true$$

4. Use proposition 3.4.7 to eliminate the universal on the left and substitute $u/true$ $$\alpha(w/v),\alpha(w/true)\to v=true,\alpha(w/true),\alpha\vdash w=true$$

5. But we can also use 3.4.7 to eliminate the universal on the left and substitute $u/w$ $$\alpha(w/v),\alpha(w/w)\to v=w,\alpha(w/true),\alpha\vdash w=true$$

6. Putting these together, (noticing that we don't even need $\alpha(w/v)$, and also that $\alpha(w/w) = \alpha$), we obtain

$$\alpha\to v = w, \alpha(w/true)\to v = true,\alpha(w/true),\alpha\vdash w = true$$

The result then follows by applying transitivity (and a few applications of modus ponens/cut).