Boolean Toposes, Forcing, and the Independence¶
Job: develop the Boolean / two-valued toposes, the Cohen forcing / independence of CH, the Solovay Boolean-valued, and the LEM / intuitionistic — with the \(\mathbf{Sh}(\mathbb{P},\neg\neg)\) / CH as the worked example.
Core¶
The Boolean and the two-valued¶
| Boolean / \(\neg\neg\) / two-valued | Description |
|---|---|
| Boolean topos | \(\Omega\) the Boolean, \(\neg\neg=\mathrm{id}\) (the category theory / categorical logic) |
| Two-valued | \(\mathrm{Hom}(1,\Omega)=\{\bot,\top\}\) (the category theory) |
The forcing and the Cohen¶
| Cohen / \(\mathbb{P}\) / \(\neg\neg\) / forcing | Description |
|---|---|
| Cohen forcing | \(\mathbb{P}\) the poset, \(\mathbf{Sh}(\mathbb{P},\neg\neg)\) the Boolean topos (the category theory) |
| Forcing / topos | the topos the forcing (the category theory) |
The independence and the CH¶
| Independence / CH / Solovay / Boolean-valued | Description |
|---|---|
| Independence of CH | the CH the independent (the Cohen / the Boolean topos) |
| Solovay | the Boolean-valued model (the category theory) |
The LEM and the intuitionistic¶
| LEM / Boolean / intuitionistic | Description |
|---|---|
| LEM | \(\neg\neg=\mathrm{id}\) the Boolean (the LEM) |
| Intuitionistic | the Heyting, \(\neg\neg\ne\mathrm{id}\) (the category theory) |
See it¶
Cohen forcing \(\mathbf{Sh}(\mathbb{P},\neg\neg)\) the Boolean topos and the independence of CH. The Cohen: the \(\mathbb{P}\) the forcing poset, the \(\mathbf{Sh}(\mathbb{P},\neg\neg)\) the Boolean topos (the \(\neg\neg\) the double-negation, the Boolean, the category theory / categorical logic). The CH: the \(\mathbf{Sh}(\mathbb{P},\neg\neg)\) the internal \(\mathbf{Set}\) the \(\neg\) CH (the independence, the Cohen). The key point: the \(\mathbf{Sh}(\mathbb{P},\neg\neg)\) the Boolean, the CH the independent — the forcing the topos.
Check¶
Explain the \(\neg\neg\) topology and the Boolean topos, and the independence of CH.
The \(\neg\neg\): the \(j=\neg\neg:\Omega\to\Omega\) the Lawvere–Tierney topology (the double-negation, the foundations). The \(\mathbf{Sh}(\mathbb{P},\neg\neg)\): the \(\neg\neg\)-sheaves the Boolean (the \(\neg\neg=\mathrm{id}\) the Boolean, the category theory). The CH: the \(\mathbb{P}\) the Cohen poset (the collapsing / the independent), the \(\mathbf{Sh}(\mathbb{P},\neg\neg)\) the internal \(\neg\) CH (the independence). The Solovay: the Boolean-valued model \(V^{\mathbb{P}}\) the \(\mathbf{Sh}(\mathbb{P},\neg\neg)\) (the Boolean-valued, the category theory). So the \(\neg\neg\) the Boolean, the CH the independent.
Explain the LEM and the intuitionistic, and the Boolean vs the Heyting.
The LEM: the \(\neg\neg=\mathrm{id}\) the Boolean (the law of excluded middle, the \(\Omega\) the Boolean algebra). The intuitionistic: the Heyting (\(\Omega\) the Heyting algebra, the \(\neg\neg\ne\mathrm{id}\), the category theory / categorical logic). The \(\mathbf{Set}\): the Boolean (the \(\neg\neg=\mathrm{id}\), the LEM). The \(\mathbf{Sh}(X)\): the Heyting (the \(\neg\neg\ne\mathrm{id}\), the intuitionistic, the foundations). The \(\mathbf{Sh}(\mathbb{P},\neg\neg)\): the Boolean (the \(\neg\neg\) the Boolean, the LEM). So the LEM the Boolean, the intuitionistic the Heyting.
Pitfalls¶
- The Boolean \(\neg\neg=\mathrm{id}\) (the LEM, the category theory) — the Boolean the LEM, the Heyting the intuitionistic.
- The Cohen forcing \(\mathbf{Sh}(\mathbb{P},\neg\neg)\) (the \(\neg\neg\) the double-negation, the Boolean) — the Cohen the poset, the \(\neg\neg\) the Boolean.
- The independence of CH (the Cohen, the Boolean topos) — the CH the independent, the Solovay the Boolean-valued.
- The two-valued (\(\mathrm{Hom}(1,\Omega)=\{\bot,\top\}\)) — the two-valued the Boolean, the \(\mathbf{Set}\) the two-valued.
Refs¶
- Cohen, "The independence of the continuum hypothesis" (PNAS 1963–1964); the forcing
- Tierney, "Sheaf theory and the continuum hypothesis" (1972); the \(\neg\neg\) / the topos
- Solovay, "A model of set-theory in which every set of reals is Lebesgue measurable" (1970); the Boolean-valued
- Mac Lane–Moerdijk, Sheaves in Geometry and Logic (1992); the forcing / the topos
Next¶
TT index · Foundations · Classifying & Geometric · Cohesive & Higher · Synthetic & Infinitesimal · Category theory / categorical logic