Mathematical Logic
Categorical Logic
A topos is a category that behaves like a 'universe of sets' but with a different logic. Different toposes support different logics: in one the axiom of choice holds, in another it does not; in one the law of excluded middle holds, in another it does not. This makes toposes a powerful tool for studying the foundations of mathematics.
- Proof assistants Coq and Lean 4: based on type theory corresponding to topos logic via the Curry-Howard-Lambek correspondence
- Synthetic differential geometry (SDG): in a suitable topos genuine infinitesimals exist and classical differential geometry is built axiomatically
- Forcing in set theory (Cohen): the proof of independence of CH uses a topos corresponding to a forcing extension of ZFC
- Programming language semantics: topos semantics is used to model parallel and non-deterministic computations
Toposes and Internal Logic
Lawvere and Tierney in 1970 defined an elementary topos as a category generalizing Set: Cartesian closed with a subobject classifier Omega. The logic inside a topos is intuitionistic: the law of excluded middle may fail. Proof assistants Lean 4 and Coq are based on types whose theoretical foundation is topos and homotopy logic.
Why is the internal logic of a topos intuitionistic rather than classical?
The logic of a topos is determined by the structure of Omega: in Set Omega = {T,F} (Boolean), logic is classical. In a presheaf topos Omega is a Heyting lattice, and the law of excluded middle is not a theorem.
Geometric Morphisms and Applications
Geometric morphisms between toposes are morphisms of theories. Each topos defines its own logic; a geometric morphism f: E -> F preserves geometric formulas (with existential quantifiers and finite conjunctions). This generalizes the model relation in logic.
Connection to type theory: via the Curry-Howard-Lambek correspondence, toposes correspond to type systems with dependent types. This is the foundation of proof assistants Coq (Calculus of Constructions) and Lean (based on CIC). Types = objects of a topos, terms = morphisms, proofs = elements of a type.
What is a classifying topos for a theory T?
Classifying topos Set[T]: for any topos E, models of theory T in E are in bijection with geometric morphisms E -> Set[T]. This unifies the semantics of theories in categorical language.
Итоги
- Topos = category with finite limits, internal homs (Cartesian closure), and subobject classifier Omega
- Omega forms a Heyting algebra: the law of excluded middle may fail, giving intuitionistic internal logic
- Internal language: judgments = morphisms in the topos, theorems = constructions (Curry-Howard-Lambek)
- Presheaf topos Set^{C^op}: object = functor C^op -> Set, Omega(c) = sieves on c (Heyting lattice)
- Geometric morphism f: E -> F - morphism between toposes preserving geometric logic
- Classifying topos Set[T]: models of T in E are in bijection with geometric morphisms E -> Set[T]