Categorical Logic, Topoi, and the Internal Language¶
Job: develop the categorical logic (first-order / internal), the topos (\(\Omega\) / Grothendieck / elementary), the geometric morphism / forcing, and the internal language / synthetic — with the \(\mathbf{Set}\) / \(\mathrm{Sh}(X)\) as the worked example.
Core¶
The categorical logic¶
| Categorical logic / first-order / internal / Curry–Howard–Lambek | Description |
|---|---|
| First-order / internal | the \(\mathcal{C}\) the first-order, the internal language |
| Curry–Howard–Lambek | the CCC the logic, the homotopy type theory |
The topos and the subobject classifier¶
| Topos / \(\Omega\) / Grothendieck / elementary | Description |
|---|---|
| Topos | \(\Omega\) the subobject classifier, finite limits, power object |
| Grothendieck / elementary | Grothendieck the sheaves, elementary the finite limits + \(\Omega\) (the topos theory) |
The geometric morphism and the forcing¶
| Geometric morphism / \(f^*\dashv f_*\) / forcing | Description |
|---|---|
| Geometric morphism | \(f^*\dashv f_*\) (the topos theory) |
| Forcing / independence | the topos the forcing, the Cohen / the independence (the topos theory) |
The internal language and the synthetic¶
| Internal language / synthetic / differential | Description |
|---|---|
| Internal language | the topos the language, the synthetic |
| Synthetic / differential | the synthetic differential geometry, the Kock (the topos theory) |
See it¶
\(\mathbf{Set}\) the topos and the sheaves \(\mathrm{Sh}(X)\) the Grothendieck topos. The \(\mathbf{Set}\): the elementary topos (\(\Omega=\{0,1\}\), the finite limits, the power object \(\mathcal{P}\)). The \(\mathrm{Sh}(X)\): the Grothendieck topos (the sheaves on \(X\), the topos theory). The geometric morphism: the \(\mathrm{Sh}(X)\to\mathbf{Set}\) (the \(f^*\dashv f_*\), the topos theory). The key point: the \(\mathbf{Set}\) the topos, the \(\mathrm{Sh}(X)\) the Grothendieck, the geometric morphism.
Check¶
Show that \(\mathbf{Set}\) is a topos, and explain the subobject classifier \(\Omega\).
The \(\mathbf{Set}\): the finite limits (the products, the equalizers), the subobject classifier \(\Omega=\{0,1\}\) (the \(\mathrm{Sub}(X)\cong\mathrm{Hom}(X,\Omega)=\mathcal{P}(X)\), the characteristic function the classifier). The power object: the \(\mathcal{P}(X)=\Omega^X\) (the power set, the topos theory). The elementary topos: the finite limits + the \(\Omega\) (the \(\mathbf{Set}\) the elementary). The Grothendieck: the \(\mathrm{Sh}(X)\) the sheaves (the topos theory). So the \(\mathbf{Set}\) the topos, the \(\Omega\) the classifier.
Explain the geometric morphism and the forcing, and the internal language.
The geometric morphism: the \(f^*\dashv f_*\) (the \(f^*\) the inverse image, the \(f_*\) the direct image, the topos theory). The forcing: the topos the forcing (the \(f^*\) the extension, the Cohen the independence, the topos theory). The internal language: the topos the language (the \(\Omega\) the truth, the \(\exists\) / \(\forall\) the adjoints, the synthetic). The synthetic differential: the Kock the infinitesimal (the \(D\) the nilpotent, the topos theory). So the geometric morphism the \(f^*\dashv f_*\), the forcing the Cohen, the internal language the synthetic.
Pitfalls¶
- The topos the \(\Omega\) (the subobject classifier, the topos theory) — the \(\Omega\) the classifier, the \(\mathrm{Sub}\cong\mathrm{Hom}(-,\Omega)\).
- The Grothendieck / elementary (the sheaves / the finite limits + \(\Omega\)) — the Grothendieck the sheaves, the elementary the \(\Omega\).
- The geometric morphism the \(f^*\dashv f_*\) (the topos theory) — the \(f^*\) the inverse, the \(f_*\) the direct.
- The internal language the synthetic (the Kock, the topos theory) — the internal the language, the synthetic the differential.
Refs¶
- Mac Lane–Moerdijk, Sheaves in Geometry and Logic (1992); the topos / the \(\Omega\)
- Johnstone, Sketches of an Elephant (2002); the topos / the geometric morphism
- Kock, Synthetic Differential Geometry (2006); the synthetic / the internal
- Lambek–Scott, Introduction to Higher Order Categorical Logic (1986); the Curry–Howard–Lambek
Next¶
CT index · Foundations · Monads & Algebras · Monoidal & Enriched · Accessible & Presentable · Topos theory · HoTT