Past exam of the mathematics course of the University of Cambridge / 2013 / iii / Paper 74 / 5

For each object $X$, characteristic maps identify $\mathcal{E}(X,\Omega )$ with $\mathrm{Sub}(X)$. These subobject posets carry a natural Heyting algebra structure. Truth and falsity classify $X$ and the empty subobject. Intersections define $\wedge$, unions define $\vee$, and implication is characterized byThese operations commute with pullback, giving arrows on $\Omega$ and the internal Heyting algebra of truth values. Concretely, the order relation on $\Omega$ is the subobject where $p\wedge q=p$; its characteristic map is implication. Negation is $p\Rightarrow \perp$.

If $U\hookrightarrow 1$ has truth value $u:1\to \Omega$, its quasi-closed local operator isThis is double negation relative to the bottom value $u$. In the Heyting algebra interval $[u,1]$, relative implication is inherited and relative negation is $N_u(p)=p\Rightarrow u$. Also $N_u(p)=N_u(p\vee u)$. Therefore the displayed map is the composite of adjoining $u$ and relative double negation. It is inflationary, idempotent, fixes truth and preserves binary meets, so it is a Lawvere-Tierney topology. Its value at bottom is $u$.

The truth values of its sheaf topos are the fixed elements $p=q(U)(p)$. They have bottom $u$, inherited meet and join $q(U)(p\vee r)$. Their relative negation is $N_u(p)$, which is again fixed because $N_u^3=N_u$. The relative double-negation law holds on every fixed element, andThus every subobject in the sheaf topos has a complement: every quasi-closed subtopos is Boolean. This identifies its internal logic, not merely the global truth-value lattice.

Now work in $\mathcal{E}/\Omega$. The arrow $\top :1\hookrightarrow \Omega$ is a subterminal object there; internally it supplies a freely varying generic truth value $u$. Let $a_q$ be sheafification for a local operator for its quasi-closed topology, and let $\pi :\mathcal{E}/\Omega \to \mathcal{E}$ be the slice geometric morphism. The composite $h$ has inverse image $h^{\ast }=a_q{\pi }^{\ast }$.

To prove surjectivity, take any mono $S\hookrightarrow X$ in $\mathcal{E}$, classified by $p:X\to \Omega$. Its pullback along $\pi$ has predicate $p(x)$, independent of the generic $u$. If $h^{\ast }$ sends the mono to an isomorphism, it is $q$-dense in the slice, sofor all $(x,u)$. Pull back this identity along the graph $x\mapsto (x,p(x))$. Substituting $u=p(x)$ gives $q_{p(x)}(p(x))=p(x)$, and therefore $p(x)=1$. Thus the original mono was already invertible.

For parallel arrows $r,s:X\rightrightarrows Y$, equality of their inverse images makes the inverse image of their equalizer invertible. The preceding mono argument makes the equalizer invertible and hence $r=s$. Therefore $h^{\ast }$ is faithful, and the composite is a surjective geometric morphism. A fixed double-negation subtopos can erase information; allowing the generic relative bottom is what detects every original predicate.

For the completeness consequence, let $\mathbb{T}$ be coherent and use its classifying topos with the generic model. Its conservative syntactic interpretation makes an underivable coherent sequent fail as a subobject inclusion. Pulling this model into the Boolean cover constructed above preserves coherent formulas and still refutes that inclusion, because the inverse image is faithful and reflects containment. In the Boolean topos, the difference between antecedent and consequent is a nonzero complemented subobject. Slicing over that difference gives a nondegenerate Boolean topos with a global tuple satisfying the antecedent and the negation of the consequent.

Classical first-order deduction is sound in a Boolean topos. Hence $\mathbb{T}$ together with constants for that tuple, the antecedent and the negated consequent is classically consistent: a proof of contradiction would hold in the nondegenerate sliced model. The ordinary Henkin construction supplies a set model of this consistent theory. Briefly, extend it by witness constants, complete it to a maximal consistent theory, form the term structure modulo provable equality, and prove the truth lemma by induction on formulas. For possibly empty sorts use the standard encoding by sort predicates and functional graph relations, without asserting sort inhabitance; the constants for the chosen tuple assert only the needed witnesses. The resulting set model is a countermodel to the original sequent.

Consequently a coherent sequent valid in every set-valued model of a coherent theory is derivable in coherent logic. The Boolean cover supplies the crucial passage from the generic intuitionistic countermodel to consistency with classical negation; the final set-model step uses ordinary first-order completeness via its Henkin proof, rather than an assumption that every Boolean topos has points.