Presheaf Truth Values and Heyting Negation

The big idea

In a presheaf, information at different stages must agree with restriction maps. A subobject of the terminal presheaf selects either the empty set or the singleton at each stage, but not every raw selection is compatible. The valid subobjects form an ordered lattice of global truth values. Negation is not necessarily stagewise complement; it is the largest valid truth value whose meet with the original value is bottom.

Worked example

Take two stages, broad \(B\) restricting to narrow \(N\), with a singleton at each stage. The four raw pairs of subsets are

\[ (\varnothing,\varnothing),\quad (\varnothing,\{\}),\quad (\{\},\varnothing),\quad (\{\},\{\}). \]

The third pair is invalid: a selected broad-stage element restricts to \(*\), which is missing at the narrow stage. The three valid values form a chain \(0<L<1\).

Negation is the largest disjoint valid value. Thus \(\neg0=1\), while \(\neg L=0\) and \(\neg1=0\). Consequently \(L\lor\neg L=L\ne1\), so excluded middle fails inside this finite logic.

How children may show it

A learner may enumerate a compatibility table, draw the three-element lattice, or calculate meet and join stage by stage before checking validity. Keeping the stage order fixed prevents silent reversals.

Common mix-up

The forbidden raw pair is often used as a classical-looking complement. Ask whether its selected broad element restricts into the selected narrow subset. Internal negation must remain a valid subpresheaf.

Try it together

List the three valid values in a chain and build full meet, join, and negation tables. Test excluded middle and double-negation elimination on each value, identifying exactly which middle value supplies the counterexample.