\( \DeclareMathOperator{\Hom}{Hom} \DeclareMathOperator{\uHom}{\,\underline{\!Hom\!}\,} \DeclareMathOperator{\Mor}{Mor} \DeclareMathOperator{\Map}{Map} \DeclareMathOperator{\map}{map} \DeclareMathOperator*{\colim}{colim} \DeclareMathOperator{\id}{id} \DeclareMathOperator{\Id}{Id} \DeclareMathOperator{\Ob}{Ob} \DeclareMathOperator{\comp}{comp} \DeclareMathOperator{\Fun}{Fun} \DeclareMathOperator{\true}{true} \DeclareMathOperator{\Sub}{Sub} \DeclareMathOperator{\Lan}{Lan} \DeclareMathOperator{\Ran}{Ran} \DeclareMathOperator{\PSh}{PSh} \DeclareMathOperator{\Sh}{Sh} \DeclareMathOperator{\Sp}{Sp} \DeclareMathOperator{\Glue}{Glue} \DeclareMathOperator{\Res}{Res} \DeclareMathOperator{\End}{End} \DeclareMathOperator{\oneim}{1im} \DeclareMathOperator{\twoim}{2im} \DeclareMathOperator{\charr}{char} \DeclareMathOperator{\Spec}{Spec} \newcommand{\ProFinSet}{\mathrm{ProFinSet}} \newcommand{\sSet}{\mathrm{sSet}} \newcommand{\Top}{\mathrm{Top}} \newcommand{\deltacat}{\boldsymbol{\Delta}} \newcommand{\Cat}{\mathrm{Cat}} \newcommand{\Set}{\mathrm{Set}} \newcommand{\Ring}{\mathrm{Ring}} \newcommand{\CatMon}{\mathrm{CatMon}} \newcommand{\Cof}{\mathrm{Cof}} \newcommand{\Fib}{\mathrm{Fib}} \newcommand{\Frm}{\mathrm{Frm}} \newcommand{\Loc}{\mathrm{Loc}}\)

Categorical Logic

Table of Contents

Source: https://www.math.ias.edu/~lurie/278x.html

1. Lecture 1: Overview

\(T \) theory. \( \tilde{M} \) picked subset for each model \( M \) of \( T \) st

  1. for \( f: M \rightarrow M' \) elementary embedding, \( \tilde{M} = f^{-1}( \tilde{M}) \).
  2. for models \( \{M_j\}_{j \in J} \), ultrafilter \( \mathcal{U} \) on J, \( M := (\prod_{j \in J} M_j)/ \mathcal{U} \) : \((a_j)_{j \in J} \in \tilde{M} \) iff \(a_j \in \tilde{M_j}\) for almost all \(j \in J\).

Then: ex formula \( \varphi \), \( \tilde{M} = \varphi(M) \) for every model \(M \).

This is a natural companion to Gödel’s Completeness Theorem: it describes the conditions under which there exists a formula with a certain semantic interpretation. The Completeness Theorem ensures that this formula is unique up to provable equivalence. They work to together into the direction of recovering the syntax of a theory from its semantics.

\(T \) theory. \( \operatorname{Mod}(T)\) category of models of \(T \) (morphisms are elementary embeddings). Then:

  1. \(T\) can be recovered up to equivalence from the structure of \( \operatorname{Mod}(T)\) as a category with ultraproducts.
  2. Can I reformulate this ❓
  3. More precisely: have canonical equivalence \( \operatorname{Syn}(T) \simeq \operatorname{UFun}( \operatorname{Mod}(T),\Set)\)

\(T \) := theory of abelian groups. Then \( \operatorname{Mod}(T)\) only contains elementary embeddings, ie not all group homomorphisms. But there is a “nonclassical” theory \(T'\) st \( \operatorname{Mod}(T')\) is the category of abelian groups. Therefore we want to study this “nonclassical” logic, the logic of pretopoi. What is \(T'\) ❓

2. Lecture 2:

\(T\) first-order theory. The weak syntactic category \( \operatorname{Syn}_0(T)\) of \(T\) consists of

  1. objects: \([ \varphi(x)]\) for every formula \( \varphi\).
  2. morphisms: \(f: [ \varphi(x)] \rightarrow [ \psi(y)]\) is a collection of definable maps \((f_M: M[ \varphi] \rightarrow M[ \psi])_{M \text{ model of } T}\).
  3. composition: in every model.
  4. identity: in every model the identity.

Alternatively we could define the morphisms to be equivalence classes of formulas that define the same graph. \(M \) model of \(T \). \( \operatorname{Syn}_0(T) \rightarrow \Set\), \([ \varphi] \mapsto M[ \varphi]\) is a functor.

\(T \) first-order theory. \(M\), \(N\) models of \(T \). TFAE:

  1. elementary embedding \(f_0: M \rightarrow N\).
  2. natural transformation \(f: M[-] \rightarrow N[-]\).

We can identify a model \(M\) of \(T\) and functor its functor \(M[-]: \operatorname{Syn}_0(T) \rightarrow \Set\). The functor \(M[-]\) is “unbiased”, ie it doesn’t consider one underlying set on which we interpret the language, but all sets that can be constructed form the model.

Idea: \(f_0\) restricts to morphisms between the def sets. \(f\) gives \(f_{x=x}\).

It is enough to check \(M \models \varphi(x) \Rightarrow N \models \varphi(f(x))\) to verify that \(f\) is an elementary embedding. For the other direction, use the negation of \( \varphi\)!

A typed language \( \mathcal{L}\) consists of data:

  1. a set of types \( \mathfrak{T}\).
  2. a set of predicate symbols \(\{P_i\}\).
  3. for predicate symbol \(P_i\), the arity is a finite sequence \((t_1, \dots, t_n)\) of types.

Each variable is assigned a type st each type has infinitely many variables. A (typed) formula is just a normal formula with three caveats:

  1. add a new formula \(\bot\) for “false”.
  2. \(x = y\) only if \(x\),\(y\) have the same type.
  3. \(P_i(x_1, \dots, x_n)\) only if \(x_j\) has type \(t_j\) where \((t_1, \dots, t_n)\) is the arity of \(P_i\).

This is a proper generalization if there are infinitely many types. Why ❓

Propositional logic is the typed first-order logic with zero types. Let \(T\) be a propositional theory. Then: \( \operatorname{Syn}_0(T)\) is equivalent to the partially ordered set of equivalence classes of sentences. This is a Boolean algebra via:

  1. order: \( \varphi \le \psi\) iff \( \varphi \Rightarrow \psi\)
  2. join: \( \varphi \lor \psi\)
  3. complement: \( \neg \varphi\)

3. Lecture 3: The Structure of \( \operatorname{Syn}_0(T)\)

\(T\) typed first-order theory. Then:

  1. \( \operatorname{Syn}_0(T)\) has finite limits.
  2. For \(M\) model of \(T\), \(M[-]\) preserves finite limits..

Idea: Pullback + finial object. Pullback is \( \exists z: \theta(x,z) \land \theta'(y,z)\) where \( \theta\), \( \theta'\) are the morphisms (think of sets). Final object is \( \forall x: x = x\) (gets interpreted in \(M^0 = \{pt\}\)).

\(T\) typed first-order theory. \(f: X \rightarrow Y\) in \( \operatorname{Syn}_0(T)\). TFAE:

  1. \(f\) is an isom.
  2. For \(M\) model of \(T\), \(f_M\) is an isom.

\(T\) typed first-order theory. \(f: X \rightarrow Y\) in \( \operatorname{Syn}_0(T)\). TFAE:

  1. \(f\) is a mono.
  2. For \(M\) model of \(T\), \(f_M\) is a mono.

\(T\) typed first-order theory. \( \varphi(x)\), \( \psi(x)\) formulas with the same free variables.

  1. If \(T \models \forall x: \varphi(x) \Rightarrow \psi(x)\), then for every model \(M\) of \(T\), we identify \(M[ \varphi]\) with a subset of \(M[ \psi]\).
  2. This identification determines a mono \([ \varphi] \rightarrow [ \psi]\) in \( \operatorname{Syn}_0(T)\).
  3. A mono is called special iff it arises from the above construction.

Idea: A mono is special iff it comes from inclusions.

\(T\) typed first-order theory. \(f: X \rightarrow Y\) in \( \operatorname{Syn}_0(T)\). Then:

  1. Ex factorization \( X \xrightarrow{g} Y \xrightarrow{h} Z\) of \(f\) st:
    • \(g\) is an effective epi.
    • \(h\) is a special mono.
  2. Can pick factorization st:
    • For \(M\) model of \(T\), \(M[-]\) preserves the factorization.
    • Ie \(g_M\) is surjective, \(h_M\) is an inclusion.

Idea: \(Y := \exists x: \theta(x,y)\), where \( \theta\) defines \(f\) (image).

\( \mathcal{C}\) category with fiber products. \(g: X \rightarrow Y\) in \( \mathcal{C}\).

  1. \(X \times_Y X\) is the fiber product of \(X\) with itself over \(Y\) via \(g\).
  2. \( \pi, \pi': X \times_Y X \rightarrow X\) the two projections.
  3. \(g\) is an effective epimorphisms iff \(g\) is the coequalizer of \( \pi\), \( \pi'\). Ie for \(T \in \mathcal{C}\), \( \operatorname{Hom}_{ \mathcal{C}}(Y,T) \simeq \{ f \in \operatorname{Hom}_{ \mathcal{C}}(X,T) \mid f \circ \pi = f \circ \pi' \}\) (UP of coeq).

Every effective epi is an epi.

  1. In \( \Set \): eff epi iff it’s an epi iff it’s surjective.
  2. In \( \Ring \): eff epi iff surjective. But there are non-surjective epis.

\( \mathcal{C}\) category with fiber products. \(f: X \rightarrow Y\) in \( \mathcal{C}\). Then: \(X \rightarrow Y \rightarrow Z\) factorization of \(f\) with \(h\) mono, \(g\) eff epi, then this factorization is unique up to unique isom.

Idea: Use UP of eff epi and compute it by using mono.

\(T\) typed first-order theory. \(f: X \rightarrow Y\) mono in \( \operatorname{Syn}_0(T)\). Then:

  1. Ex isom \( \phi: X \rightarrow X'\), special mono \(g: X' \rightarrow Y\), \(f = g \circ \phi\).
Proof.

\( \mathcal{C}\) category. \(X\) object.

  1. \( \operatorname{Sub}(X)\) is the set of equivalence classes of subobjects of \(X\).
  2. \(A \subset B\) in \( \operatorname{Sub}(X)\) :iff there exists a triangle from \(A\) to \(B\) over \(X\).

\(T\) typed first-order theory. \(X = [ \varphi(x)]\) object in \( \operatorname{Syn}_0(T)\). Then:

  1. For \(A \in \operatorname{Sub}(X)\), ex \( \psi(x)\) formula, \(T \models \forall x: \psi(x) \Rightarrow \varphi(x)\) and \(A = [ \psi(x)]\) with the special mono to \(X\).
  2. For \( A = [\psi_1(x)], B = [\psi_2(x)] \in \operatorname{Sub}(X)\), \(A \subset B\) iff \(T \models \forall x: \psi_1(x) \Rightarrow \psi_2(x)\).
  3. For \( A = [\psi_1(x)], B = [\psi_2(x)] \in \operatorname{Sub}(X)\), \(A = B\) iff \(T \models \forall x: \psi_1(x) \Leftrightarrow \psi_2(x)\).

\(T\) typed first-order theory. \(X \in \operatorname{Syn}_0(T)\). Then:

  1. The partially ordered set \( \operatorname{Sub}(X)\) is a Boolean algebra.
  2. \(M[-]: \operatorname{Sub}(X) \rightarrow M[X]\) is a homo of Boolean algebras, where \(M[X]\) is the lattice of all subsets.

\(T\) typed first-order theory. \(F: \operatorname{Syn}_0(T) \rightarrow \Set\) functor. TFAE:

  1. Ex \(M\) model of \(T\), \(F \cong M[-]\)
  2. \(F\) satisfies:
    1. \(F\) preserves finite limits.
    2. \(F\) sends eff epis to surjections.
    3. For \(X \in \operatorname{Syn}_0(T)\), the map \( \operatorname{Sub}(X) \rightarrow \operatorname{Sub}(F(X))\) is a homo of upper semilattices, ie it preserves least upper bounds of finite subsets.
  3. We can replace 3. by: \( \operatorname{Sub}(X) \rightarrow \operatorname{Sub}(FX)\) is a Boolean algebra homo.

In words: \(F\) has to respect finite limits (pullbacks and terminal object), eff epis and least upper bounds of finitely many subobjects.

Proof.

4. Lecture 4: Coherent Categories

\(T\) typed first-order theory. \(f: X \rightarrow Y\) in \( \operatorname{Syn}_0(T)\). TFAE:

  1. \(f\) is eff epi.
  2. For \(M\) model of \(T\), \(f_M\) is surjective.
Proof.

\( \mathcal{C}\) category.

  1. \( \mathcal{C}\) is coherent iff
    1. \( \mathcal{C}\) has finite limits.
    2. For \(f: X \rightarrow Z\), ex factorization \(X \xrightarrow{g} Y \xrightarrow{h} Z\) of \(f\), \(g\) is eff epi and \(h\) is mono.
    3. For \(X \in \mathcal{C}\), \( \operatorname{Sub}(X)\) is an upper semilattice, ie it has a least element and two subobjects \(A, B \subset X\) habe a least upper bound \(A \lor B\).
    4. The collection of eff epis is stable under pullbacks.
    5. For \(f: X \rightarrow Y\), the map \(f^{-1}: \operatorname{Sub}(Y) \rightarrow \operatorname{Sub}(X)\) is a homo of upper semilattices.

Author: Frederik Gebert

Created: 2025-02-10 Mon 21:45