Chapter 143Core route

Categorical Logic, Hyperdoctrines, and Internal Languages

Let $X$ and $Y$ be sets and $f : X \to Y$ a function. A predicate on $Y$ is a subset $V \subseteq Y$ , and substituting $f$ into it produces the predicate $f^{- 1} (V) \subseteq X$ . Two further operations turn a predicate on $X$ back into a predicate on $Y$ : $\begin{aligned} \exists_{f} (U) & : = {y \in Y ∣ y = f (x) for some x \in U}, \\ \forall_{f} (U) & : = {y \in Y ∣ x \in U for every x with f (x) = y} . \end{aligned}$ Take $Y = N$ , $X = N \times N$ , $f (m, n) = m$ , and $U = {(m, n) ∣ m \leq n}$ . Then $\exists_{f} (U) = N$ , because every $m$ has some $n$ above it, and $\forall_{f} (U) = \emptyset$ , because no $m$ is below every $n$ . These are the sets denoted by $\exists n . m \leq n$ and $\forall n . m \leq n$ .

The three operations are not independent. For $U \subseteq X$ and $V \subseteq Y$ , $\exists_{f} (U) \subseteq V ⟺ U \subseteq f^{- 1} (V), f^{- 1} (V) \subseteq U ⟺ V \subseteq \forall_{f} (U),$ each of which is checked by expanding both sides on an element. Read the first as a rule of inference: a proof of $V$ from $\exists x . U$ is the same thing as a proof of $V$ from $U$ , in a context where $V$ does not mention $x$ . That is the elimination rule for the existential quantifier, and the side condition “ $x$ not free in $V$ ” is not a restriction imposed on the rule but the statement that $V$ is a predicate on $Y$ rather than on $X$ .

Equation 143.2 says that $\exists_{f}$ and $\forall_{f}$ are adjoint to $f^{- 1}$ in the sense of exercise 142.11: in a preorder an adjunction is exactly a pair of two-way rules. This chapter takes that observation as a definition, proves what it forces, and stops where the proofs stop.

Predicates and reindexing

Fix a set $X$ and let $P (X)$ be its powerset, preordered by inclusion and regarded as a category as in example 142.5: one arrow $U ⟶ U^{'}$ when $U \subseteq U^{'}$ , none otherwise. Meets are intersections, joins are unions, the top element is $X$ and the bottom is $\emptyset$ . One further operation is needed before any quantifier appears.

Definition 143.1 — Heyting algebra ¶

A Heyting algebra is a preorder $H$ with finite meets $⊤, \land$ and finite joins $⊥, \lor$ in the sense of example 142.5 and its dual, together with a binary operation $\Rightarrow$ satisfying, for all $a, b, c \in H$ , $a \land b \leq c ⟺ a \leq (b \Rightarrow c) .$ A homomorphism of Heyting algebras is a monotone map that preserves each of $⊤$ , $⊥$ , $\land$ , $\lor$ and $\Rightarrow$ up to the equivalence of the preorder. We write $Heyt$ for the category of Heyting algebras and homomorphisms.

Referenced from 4 locations

Equation 143.3 is the statement that $(-) \land b ⊣ (b \Rightarrow -)$ , so a Heyting algebra is a preorder that is cartesian closed in the sense of definition 142.26 and also has finite joins. Nothing else is assumed: $a \lor (a \Rightarrow ⊥) = ⊤$ is not required and generally fails.

Example 143.2 — The powerset is a Heyting algebra ¶

In $P (X)$ put $V \Rightarrow W : = {x \in X ∣ x \in V implies x \in W}$ , which is $(X ∖ V) \cup W$ . For $U \cap V \subseteq W$ and $x \in U$ : if $x \in V$ then $x \in W$ , so $x \in V \Rightarrow W$ ; conversely if $U \subseteq V \Rightarrow W$ and $x \in U \cap V$ then $x \in W$ . This algebra is Boolean, since $V \lor (V \Rightarrow ⊥) = V \cup (X ∖ V) = X$ .

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Example 143.3 — A Heyting algebra that is not Boolean ¶

Let $O (R)$ be the open subsets of the real line ordered by inclusion, with $\land$ intersection and $\lor$ union. Both are open, so these are meets and joins. Put $V \Rightarrow W : = int ((R ∖ V) \cup W)$ , the largest open set contained in the displayed union; (143.3) holds because an open $U$ is contained in that union exactly when it is contained in its interior. Take $V = R ∖ {0}$ . Then $V \Rightarrow ⊥ = int {0} = \emptyset$ , so $V \lor (V \Rightarrow ⊥) = V \neq R$ . Excluded middle therefore fails in this algebra, while every clause of definition 143.1 holds.

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proposition 143.4 — Inverse image is a homomorphism ¶

For $f : X \to Y$ the map $f^{*} : = f^{- 1} (-) : P (Y) \to P (X)$ preserves $⊤, ⊥, \land, \lor$ and $\Rightarrow$ , and ${id}_{X}^{*} = {id}_{P (X)}, (g \circ f)^{*} = f^{*} \circ g^{*} for g : Y \to Z .$

Referenced from 4 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Proposition 143.4 — Inverse image is a homomorphism

Proof. Each clause is an equality of subsets, checked on an element $x \in X$ . For the meet, $x \in f^{- 1} (V \cap W)$ iff $f (x) \in V$ and $f (x) \in W$ iff $x \in f^{- 1} (V) \cap f^{- 1} (W)$ ; joins, $⊤$ and $⊥$ are the same calculation. For implication, $\begin{aligned} x \in f^{- 1} (V \Rightarrow W) & ⟺ (f (x) \in V implies f (x) \in W) \\ ⟺ (x \in f^{*} V implies x \in f^{*} W), \end{aligned}$ which is $x \in f^{*} V \Rightarrow f^{*} W$ . For (143.4), $x \in (g \circ f)^{- 1} (W)$ iff $g (f (x)) \in W$ iff $f (x) \in g^{- 1} (W)$ iff $x \in f^{- 1} (g^{- 1} (W))$ ; and ${id}_{X}^{- 1} (V) = V$ . ◻

The second equation of (143.4) is an identity of operations, not an isomorphism. It is the same strictness that equation 142.11 demanded of type substitution, and here it holds on the nose because $f^{*}$ is defined by a formula rather than by a universal property.

Exercise 143.1 ¶

★☆☆ In any Heyting algebra put $\neg a : = (a \Rightarrow ⊥)$ . Prove $a \leq \neg \neg a$ from (143.3) alone, and exhibit an element of $O (R)$ with $\neg \neg a \neq a$ .

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Exercise 143.2 ¶

★★☆ Show that the direct image $\exists_{f}$ of (143.1) preserves $⊥$ and $\lor$ but need not preserve $\land$ : take $f : {0, 1} \to {*}$ and two disjoint singletons. Which clause of corollary 142.24 explains why $f^{*}$ preserves $\land$ while $\exists_{f}$ need not?

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Quantifiers as adjoints

Theorem 143.5 — The powerset quantifiers ¶

Let $f : X \to Y$ . With $\exists_{f}$ and $\forall_{f}$ as in (143.1) and $f^{*} = f^{- 1} (-)$ , $\exists_{f} ⊣ f^{*} ⊣ \forall_{f}$ as functors between the preorders $P (X)$ and $P (Y)$ .

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Theorem 143.5 — The powerset quantifiers

Proof. All three maps are monotone: if $U \subseteq U^{'}$ then every witness for $\exists_{f} (U)$ is one for $\exists_{f} (U^{'})$ , every $y$ all of whose preimages lie in $U$ has them all in $U^{'}$ , and inverse images preserve inclusion. By exercise 142.11 an adjunction between preorders is exactly the displayed two-way rule, so it suffices to prove (143.2).

First rule. Suppose $\exists_{f} (U) \subseteq V$ and let $x \in U$ . Then $f (x) \in \exists_{f} (U)$ by taking $x$ itself as the witness, so $f (x) \in V$ , that is, $x \in f^{- 1} (V)$ . Conversely suppose $U \subseteq f^{- 1} (V)$ and let $y \in \exists_{f} (U)$ , say $y = f (x)$ with $x \in U$ . Then $x \in f^{- 1} (V)$ , so $y = f (x) \in V$ .

Second rule. Suppose $f^{- 1} (V) \subseteq U$ and let $y \in V$ . For every $x$ with $f (x) = y$ we have $x \in f^{- 1} (V)$ , hence $x \in U$ ; so $y \in \forall_{f} (U)$ . Conversely suppose $V \subseteq \forall_{f} (U)$ and let $x \in f^{- 1} (V)$ . Then $f (x) \in V \subseteq \forall_{f} (U)$ , and $x$ is a preimage of $f (x)$ , so $x \in U$ . ◻

Specialize to the projection that discards one variable. Let $Γ$ and $A$ be sets and $p : Γ \times A \to Γ$ the first projection. Then $p^{*} (V) = V \times A$ adds a dummy variable, and $\begin{aligned} \exists_{p} (U) & = {g ∣ (g, a) \in U for some a \in A}, \\ \forall_{p} (U) & = {g ∣ (g, a) \in U for all a \in A}, \end{aligned}$ so the two-way rules read $\frac{\exists a . U \leq V}{U \leq p^{*} V}, \frac{p^{*} V \leq U}{V \leq \forall a . U},$ each read in both directions. The premise “ $a$ does not occur free in $V$ ” of the usual $\exists$ -elimination and $\forall$ -introduction rules is carried entirely by the requirement that $V$ be an element of $P (Γ)$ .

Proposition 143.6 — Weakening is a right adjoint, hence preserves meets ¶

In any preorder-valued situation with $\exists_{f} ⊣ f^{*}$ , the map $f^{*}$ preserves all meets that exist. In particular $f^{*} (⊤) = ⊤$ and $f^{*} (V \land W) = f^{*} V \land f^{*} W$ .

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Proposition 143.6 — Weakening is a right adjoint, hence preserves meets

Proof. Theorem 142.23 applied to the adjunction $\exists_{f} ⊣ f^{*}$ : a right adjoint preserves limits, and in a preorder the limits are exactly the meets. Corollary 142.24 names the two instances used. ◻

Lawvere records this consequence in the paper that introduced the notion: “the existence of existential quantification implies that substitution commutes with conjunction; usually substitution does not commute with implication” (Adjointness in Foundations, physical page 12). The powerset is one of the cases where substitution does commute with implication, by proposition 143.4; exercise 143.4 gives a hyperdoctrine where it does not.

Hyperdoctrines

The powerset construction used three facts about $Set$ : it has finite products, so contexts can be formed; each $P (X)$ is a Heyting algebra; and reindexing has both adjoints. One further condition is needed, and it is the condition that makes substitution commute with quantification.

Definition 143.7 — Beck–Chevalley condition ¶

Let $C$ be a category with finite products and $P : C^{op} \to Heyt$ a functor such that each $P (f)$ , written $f^{*}$ , has adjoints $\exists_{f} ⊣ f^{*} ⊣ \forall_{f}$ . The Beck–Chevalley condition requires that for every pullback square Mathematical diagram Diagram in $C$ and every $φ \in P (B)$ , $h^{*} (\exists_{f} φ) = \exists_{g} (k^{*} φ), h^{*} (\forall_{f} φ) = \forall_{g} (k^{*} φ) .$

Referenced from 3 locations

Definition 143.8 — Hyperdoctrine ¶

A hyperdoctrine is a pair $(C, P)$ where $C$ is a category with finite products and $P : C^{op} \to Heyt$ is a functor such that for every arrow $f$ of $C$ the homomorphism $f^{*}$ has a left adjoint $\exists_{f}$ and a right adjoint $\forall_{f}$ , and the Beck–Chevalley condition (143.6) holds for every pullback square that exists in $C$ .

Referenced from 11 locations

The base is required to have finite products only. That is enough for the condition to be usable, because the squares the interpretation actually needs are always pullbacks.

Lemma 143.9 — Substitution squares are pullbacks ¶

Let $C$ have finite products, let $σ : Δ ⟶ Γ$ , and let $A$ be an object. Write $p : Γ \times A ⟶ Γ$ and $q : Δ \times A ⟶ Δ$ for the first projections and $σ \times {id}_{A} : = ⟨ σ \circ q, {pr}_{2} ⟩$ . Then Mathematical diagram Diagram is a pullback square.

Referenced from 5 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Lemma 143.9 — Substitution squares are pullbacks

Proof. It commutes: $p \circ ⟨ σ \circ q, {pr}_{2} ⟩ = σ \circ q$ by (142.2). Let $u : X ⟶ Δ$ and $v : X ⟶ Γ \times A$ satisfy $σ \circ u = p \circ v$ , and put $m : = ⟨ u, {pr}_{2} \circ v ⟩ : X ⟶ Δ \times A$ . Then $q \circ m = u$ , and $\begin{aligned} (σ \times {id}_{A}) \circ m & \overset{l e m m a 142.2 (2)}{=} ⟨ σ \circ q \circ m, {pr}_{2} \circ m ⟩ \\ \overset{(142.2)}{=} ⟨ σ \circ u, {pr}_{2} \circ v ⟩ \\ \overset{h y p .}{=} ⟨ p \circ v, {pr}_{2} \circ v ⟩ \overset{l e m m a 142.2}{=} v . \end{aligned}$ If $m^{'}$ also satisfies the two equations then $q \circ m^{'} = u$ and ${pr}_{2} \circ m^{'} = {pr}_{2} \circ (σ \times {id}_{A}) \circ m^{'} = {pr}_{2} \circ v$ , so $m^{'} = ⟨ q \circ m^{'}, {pr}_{2} \circ m^{'} ⟩ = m$ by lemma 142.2(1). ◻

This is the posetal formulation, following Awodey, Introduction to Categorical Logic, Definition 3.4.1 (physical page 176 of the course draft). Lawvere’s original definition, Adjointness in Foundations, physical pages 11–12, is more general in two respects recorded here and not used later: his base $T$ is required to be cartesian closed, and his $P (X)$ is a cartesian closed category of attributes whose arrows are deductions, so that two proofs of the same entailment may differ. Definition 143.8 is the special case in which each $P (X)$ is a preorder, that is, in which entailment is proof-irrelevant, and in which the base is only required to have finite limits. No theorem below is transferred from the proof-relevant setting.

Example 143.10 — The powerset hyperdoctrine ¶

$C = Set$ , which has finite products by example 142.4 and in fact all finite limits by proposition 142.9, and $P (X) = P (X)$ with $f^{*} = f^{- 1} (-)$ . Proposition 143.4 makes $P$ a functor into $Heyt$ and theorem 143.5 supplies the adjoints; Beck–Chevalley is theorem 143.11 below.

Referenced from 4 locations

Theorem 143.11 — Beck–Chevalley in the powerset ¶

The powerset hyperdoctrine satisfies (143.6).

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Theorem 143.11 — Beck–Chevalley in the powerset

Proof. By proposition 142.9 the pullback square may be taken to be $D = {(c, b) \in C \times B ∣ h (c) = f (b)}, g (c, b) = c, k (c, b) = b,$ since any other pullback of the same pair differs from this one by a unique isomorphism commuting with $g$ and $k$ , and both sides of (143.6) are transported along that isomorphism. Let $φ \subseteq B$ and $c \in C$ .

Existential clause. $\begin{aligned} c \in h^{*} (\exists_{f} φ) & ⟺ h (c) \in \exists_{f} φ & definition of h^{*} \\ ⟺ h (c) = f (b) for some b \in φ & definition of \exists_{f} \\ ⟺ (c, b) \in D for some b \in φ & definition of D \\ ⟺ c = g (d) for some d \in k^{*} φ & definitions of g, k \\ ⟺ c \in \exists_{g} (k^{*} φ) & definition of \exists_{g} . \end{aligned}$ The middle step is where the square being a pullback is used: an element of $D$ over $c$ is exactly a $b$ with $h (c) = f (b)$ , so the two existential statements have the same witnesses.

Universal clause. $c \in h^{*} (\forall_{f} φ)$ says that every $b$ with $f (b) = h (c)$ lies in $φ$ , and $c \in \forall_{g} (k^{*} φ)$ says that every $d \in D$ with $g (d) = c$ lies in $k^{*} φ$ . The elements $d$ with $g (d) = c$ are the pairs $(c, b)$ with $f (b) = h (c)$ , and $(c, b) \in k^{*} φ$ means $b \in φ$ ; so the two statements quantify over the same $b$ and assert the same thing. ◻

Example 143.12 — Beck–Chevalley fails for a commuting square that is not a pullback ¶

Let $A = {0, 1}$ , $B = {b}$ , $C = {c}$ , $D = \emptyset$ , with $f (b) = 0$ , $h (c) = 0$ , and $g, k$ the empty maps. The square commutes, since both composites have empty domain. Take $φ = {b}$ . Then $\exists_{f} φ = {0}$ and $h^{*} (\exists_{f} φ) = {c}$ , whereas $k^{*} φ = \emptyset$ and $\exists_{g} (\emptyset) = \emptyset$ . So (143.6) fails. The square is not a pullback: the pullback of $f$ along $h$ is ${(c, b)}$ , a one-element set, not $\emptyset$ . The condition is therefore a condition on pullback squares and not on commuting squares.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proposition 143.13 — Frobenius ¶

In the powerset hyperdoctrine, for $f : X \to Y$ , $U \subseteq X$ and $V \subseteq Y$ , $\exists_{f} (U \land f^{*} V) = \exists_{f} (U) \land V .$

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Proposition 143.13 — Frobenius

Proof. Let $y \in Y$ . Membership in the left-hand side says: there is $x$ with $f (x) = y$ , $x \in U$ and $f (x) \in V$ . Membership in the right-hand side says: there is $x$ with $f (x) = y$ and $x \in U$ , and moreover $y \in V$ . Since $f (x) = y$ , the two conditions $f (x) \in V$ and $y \in V$ are the same statement, and it does not depend on $x$ ; so it may be moved outside the existential quantifier in either direction. ◻

Equation 143.7 is what allows an existential hypothesis to be eliminated in the presence of other hypotheses. Without it, the rule (143.5) discharges $\exists a . U$ only when the ambient context of assumptions is empty.

Exercise 143.3 ¶

★★☆ Derive the usual sequent form of $\exists$ -elimination, $\frac{Θ \land U \leq p^{*} V}{Θ \land \exists_{p} U \leq V} (Θ, V \in P (Γ), U \in P (Γ \times A)),$ from (143.5) together with (143.7), and identify the step at which Frobenius is used.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Exercise 143.4 ¶

★★★ Let $C = Set$ and let $P (X)$ be the Heyting algebra of $O (R)$ -valued predicates, that is, functions $X \to O (R)$ ordered pointwise, with the operations of example 143.3 computed pointwise and $f^{*} (ψ) = ψ \circ f$ . Verify that $(C, P)$ is a hyperdoctrine with $\exists_{f} (φ) (y) = ⋃_{f (x) = y} φ (x)$ and $\forall_{f} (φ) (y) = int ⋂_{f (x) = y} φ (x)$ . Then decide whether $f^{*}$ preserves $\Rightarrow$ , and give the smallest example that settles it.

Referenced from 5 locations

Exercise 143.5 ¶

★★☆ Specialize (143.6) to the pullback square formed by a map $σ : Δ \to Γ$ and the projection $p : Γ \times A \to Γ$ , and read the resulting equation as the syntactic law $(\exists a . φ) [σ] = \exists a . (φ [σ \times {id}_{A}])$ . Which arrow of the square is $σ \times {id}_{A}$ ?

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Equality and comprehension

Equality is not a primitive of definition 143.8. It is constructed from one adjoint at one arrow, the diagonal.

Definition 143.14 — Equality predicate ¶

Let $(C, P)$ be a hyperdoctrine and $A$ an object of $C$ . Let $δ_{A} : = ⟨ {id}_{A}, {id}_{A} ⟩ : A ⟶ A \times A$ be the diagonal. Put ${Eq}_{A} : = \exists_{δ_{A}} (⊤) \in P (A \times A) .$

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Theorem 143.15 — Lawvere's law ¶

For every $ρ \in P (A \times A)$ , ${Eq}_{A} \leq ρ in P (A \times A) ⟺ ⊤ \leq δ_{A}^{*} ρ in P (A) .$ Consequently ${Eq}_{A}$ is reflexive, in the sense $⊤ \leq δ_{A}^{*} {Eq}_{A}$ , and it is the least reflexive element of $P (A \times A)$ .

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Theorem 143.15 — Lawvere's law

Proof. Equation 143.8 is the adjunction $\exists_{δ_{A}} ⊣ δ_{A}^{*}$ read as a two-way rule (exercise 142.11), instantiated at $⊤ \in P (A)$ and $ρ \in P (A \times A)$ . Reflexivity is the instance $ρ : = {Eq}_{A}$ of the direction from left to right, applied to ${Eq}_{A} \leq {Eq}_{A}$ . If $ρ$ is any reflexive element, the direction from right to left gives ${Eq}_{A} \leq ρ$ . ◻

Writing $ρ$ with its two variables displayed, $δ_{A}^{*} ρ$ is $ρ (x, x)$ , so (143.8) is the two-way rule $\frac{x : A ∣ ⊤ ⊢ ρ (x, x)}{x : A, y : A ∣ {Eq}_{A} (x, y) ⊢ ρ (x, y)}$ read in both directions: ${Eq}_{A}$ is the least reflexive relation. The upward direction is the introduction rule for equality and the downward direction is substitution of equals, so the elimination rule is not an extra assumption.

Example 143.16 — Equality in the powerset ¶

For a set $A$ , $δ_{A} (a) = (a, a)$ and $⊤ = A$ , so ${Eq}_{A} = \exists_{δ_{A}} (A) = {(a, a) ∣ a \in A}$ , the diagonal subset. Reflexivity says $A \subseteq δ_{A}^{- 1} ({Eq}_{A})$ , which holds because $(a, a) \in {Eq}_{A}$ ; and any $ρ$ containing every $(a, a)$ contains the diagonal.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

A predicate carves out a subobject only if the base category has the objects to carve with. That is an extra requirement.

Definition 143.17 — Comprehension ¶

A hyperdoctrine $(C, P)$ has comprehension if for every object $Γ$ and every $φ \in P (Γ)$ there are an object ${Γ ∣ φ}$ and an arrow $i_{φ} : {Γ ∣ φ} ⟶ Γ$ such that $⊤ \leq i_{φ}^{*} φ$ , and such that every $f : Δ ⟶ Γ$ with $⊤ \leq f^{*} φ$ factors as $f = i_{φ} \circ \bar{f}$ for exactly one $\bar{f}$ .

Referenced from 4 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proposition 143.18 — The powerset hyperdoctrine has comprehension ¶

Take ${Γ ∣ φ} : = φ$ as a set and $i_{φ}$ the inclusion. Then definition 143.17 holds, and $i_{φ}$ is a monomorphism.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Proposition 143.18 — The powerset hyperdoctrine has comprehension

Proof. $i_{φ}^{- 1} (φ) = φ$ , which is the top element of $P (φ)$ , so the first condition holds. Let $f : Δ \to Γ$ satisfy $Δ \subseteq f^{- 1} (φ)$ , that is, $f (d) \in φ$ for every $d$ . Then $\bar{f} (d) : = f (d)$ is a function $Δ \to φ$ with $i_{φ} \circ \bar{f} = f$ , and it is the only one, since $i_{φ}$ is injective. Injectivity also gives the monomorphism claim by proposition 141.29. ◻

Example 143.19 — Comprehension is a genuine extra condition ¶

Let $T$ be the empty theory over one sort $S$ with no function symbols and one unary relation symbol $R$ , and let $(C_{T}, P_{T})$ be its syntactic hyperdoctrine (theorem 143.28). An arrow $Δ ⟶ (x : S)$ of $C_{T}$ is a term of sort $S$ in context $Δ$ , hence a variable of $Δ$ . Suppose ${(x : S) ∣ R (x)}$ existed with structure map $i_{R}$ . Taking $f : = i_{R}$ itself in the factorization clause is not needed; it is enough that the first clause gives $⊤ \leq i_{R}^{*} R (x)$ , that is, a variable $z$ of the context ${(x : S) ∣ R (x)}$ with $⊤ ⊢ R (z)$ derivable in $T$ . No such sequent is derivable in the empty theory: the interpretation of example 143.10 that sends $S$ to a two-element set and $R$ to a proper nonempty subset satisfies every axiom of $T$ and refutes $⊤ ⊢ R (z)$ , so by theorem 143.24 the sequent has no derivation. Hence $(C_{T}, P_{T})$ has no comprehension.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

The calculus and its interpretation

Definition 143.20 — Signature, terms, formulas, sequents ¶

A first-order signature $Σ$ consists of a set of sorts; a set of function symbols, each with an arity $(S_{1}, \dots, S_{n}) \to S$ of sorts; and a set of relation symbols, each with an arity $(S_{1}, \dots, S_{n})$ . A context $Γ = x_{1} : S_{1}, \dots, x_{n} : S_{n}$ declares distinct variables. Terms and formulas in context are generated by $\begin{aligned} \frac{(x : S) \in Γ}{Γ ⊢ x : S} \frac{Γ ⊢ t_{i} : S_{i} (1 \leq i \leq n)}{Γ ⊢ f (t_{1}, \dots, t_{n}) : S} (f : (S_{1}, \dots, S_{n}) \to S), \\ φ ::= ⊤ ∣ ⊥ ∣ R (t_{1}, \dots, t_{n}) ∣ t =_{S} t^{'} ∣ φ \land φ \\ ∣ φ \lor φ ∣ φ \Rightarrow φ ∣ \exists x : S . φ ∣ \forall x : S . φ, \end{aligned}$ where every $t_{i}$ is a term of the declared sort and the two quantifiers bind $x$ in a context extended by $x : S$ . A sequent $Γ ∣ φ ⊢ ψ$ has $φ, ψ$ formulas in context $Γ$ . A theory is a set of sequents, its axioms.

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

The rules are those of intuitionistic first-order logic in sequent form, with one formula on the left.

Definition 143.21 — Derivable sequents ¶

The derivable sequents of a theory $T$ are generated by the axioms of $T$ together with $\begin{array}{lll} I d \frac{}{Γ ∣ φ ⊢ φ} & C u t \frac{Γ ∣ φ ⊢ χ Γ ∣ χ ⊢ ψ}{Γ ∣ φ ⊢ ψ} & S u b s t \frac{Γ ∣ φ ⊢ ψ}{Δ ∣ φ [σ] ⊢ ψ [σ]} \end{array}$ for every $σ : Δ \to Γ$ , a list of terms of $Δ$ of the sorts of $Γ$ ; the lattice rules $\begin{array}{lll} \frac{}{Γ ∣ φ ⊢ ⊤} & \frac{}{Γ ∣ ⊥ ⊢ φ} & \frac{Γ ∣ φ ⊢ ψ_{1} Γ ∣ φ ⊢ ψ_{2}}{Γ ∣ φ ⊢ ψ_{1} \land ψ_{2}} \\ \frac{}{Γ ∣ ψ_{1} \land ψ_{2} ⊢ ψ_{i}} & \frac{}{Γ ∣ ψ_{i} ⊢ ψ_{1} \lor ψ_{2}} & \frac{Γ ∣ ψ_{1} ⊢ χ Γ ∣ ψ_{2} ⊢ χ}{Γ ∣ ψ_{1} \lor ψ_{2} ⊢ χ} \end{array}$ the two-way implication rule $\frac{Γ ∣ φ \land ψ ⊢ χ}{Γ ∣ φ ⊢ ψ \Rightarrow χ} (both directions),$ the two-way quantifier rules, for $φ \in$ formulas over $Γ, x : S$ and $ψ$ over $Γ$ , $\frac{Γ, x : S ∣ φ ⊢ ψ}{Γ ∣ \exists x : S . φ ⊢ ψ} \frac{Γ, x : S ∣ ψ ⊢ φ}{Γ ∣ ψ ⊢ \forall x : S . φ} (both directions),$ where $ψ$ on the upper line abbreviates its weakening to $Γ, x : S$ ; the Frobenius rule $\frac{Γ ∣ θ \land \exists x : S . φ ⊢ χ}{Γ ∣ \exists x : S . (θ \land φ) ⊢ χ} (both directions);$ and the equality rules, for $ρ$ a formula over $Γ, x : S, y : S$ , $\frac{Γ, x : S ∣ ⊤ ⊢ ρ [x / y]}{Γ, x : S, y : S ∣ x =_{S} y ⊢ ρ} (both directions) .$

Referenced from 7 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

The two-way rules are the two-way rules of (143.2), (143.3) and (143.8), transcribed. This is the exact respect in which the calculus is designed for the semantics: each connective is presented by the adjunction that will interpret it, so the soundness proof has one case per adjunction rather than one case per introduction and elimination rule.

Definition 143.22 — Interpretation ¶

Let $(C, P)$ be a hyperdoctrine. A structure $M$ for $Σ$ assigns an object $[[S]]$ to each sort, an arrow $[[f]] : [[S_{1}]] \times \dots \times [[S_{n}]] ⟶ [[S]]$ to each function symbol, and an element $[[R]] \in P ([[S_{1}]] \times \dots \times [[S_{n}]])$ to each relation symbol. Put $[[Γ]] : = [[S_{1}]] \times \dots \times [[S_{n}]]$ for $Γ = x_{1} : S_{1}, \dots, x_{n} : S_{n}$ . Terms are interpreted as arrows by $[[Γ ⊢ x_{i} : S_{i}]] : = {pr}_{i}, [[Γ ⊢ f (t_{1}, \dots, t_{n}) : S]] : = [[f]] \circ ⟨ [[t_{1}]], \dots, [[t_{n}]] ⟩,$ and formulas as elements of $P ([[Γ]])$ by $\begin{aligned} [[R (t_{1}, \dots, t_{n})]] & : = ⟨ [[t_{1}]], \dots, [[t_{n}]] ⟩^{*} [[R]], & [[t =_{S} t^{'}]] & : = ⟨ [[t]], [[t^{'}]] ⟩^{*} {Eq}_{[[S]]}, \\ [[φ \land ψ]] & : = [[φ]] \land [[ψ]], & [[φ \Rightarrow ψ]] & : = [[φ]] \Rightarrow [[ψ]], \end{aligned}$ with $⊤, ⊥, \lor$ interpreted by the corresponding operations of $P ([[Γ]])$ , and $[[\exists x : S . φ]] : = \exists_{p} [[φ]], [[\forall x : S . φ]] : = \forall_{p} [[φ]],$ where $p : [[Γ]] \times [[S]] ⟶ [[Γ]]$ is the first projection and $[[φ]] \in P ([[Γ]] \times [[S]])$ is the interpretation of $φ$ in the context $Γ, x : S$ . A sequent $Γ ∣ φ ⊢ ψ$ is valid in $M$ when $[[φ]] \leq [[ψ]]$ in $P ([[Γ]])$ .

Referenced from 6 locations

The soundness proof needs one lemma, and that lemma is where Beck–Chevalley is used.

Lemma 143.23 — Substitution ¶

Let $σ : Δ \to Γ$ be a list of terms and write $[[σ]] : = ⟨ [[σ_{1}]], \dots, [[σ_{n}]] ⟩ : [[Δ]] ⟶ [[Γ]]$ . Then for every term $Γ ⊢ t : S$ and every formula $φ$ over $Γ$ , $[[t [σ]]] = [[t]] \circ [[σ]], [[φ [σ]]] = [[σ {]]}^{*} [[φ]] .$

Referenced from 5 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Lemma 143.23 — Substitution

Proof. Terms. Induct on $t$ . For $t = x_{i}$ , $t [σ] = σ_{i}$ and $[[x_{i}]] \circ [[σ]] = {pr}_{i} \circ [[σ]] = [[σ_{i}]]$ by (142.2). For $t = f (t_{1}, \dots, t_{k})$ , $[[f (\vec{t}) [σ]]] \overset{d e f .}{=} [[f]] \circ ⟨ [[t_{1} [σ]]], \dots ⟩ \overset{I H}{=} [[f]] \circ ⟨ [[t_{1}]] \circ [[σ]], \dots ⟩ \overset{l e m m a 142.2 (2)}{=} [[f (\vec{t})]] \circ [[σ]] .$

Formulas. Induct on $φ$ .

Atomic. For $R (\vec{t})$ , the term clause and lemma 142.2(2) give $⟨ [[t_{i} [σ]]] ⟩ = ⟨ [[t_{i}]] ⟩ \circ [[σ]]$ , and $P$ is a functor, so $(⟨ [[t_{i}]] ⟩ \circ [[σ]])^{*} = [[σ {]]}^{*} \circ ⟨ [[t_{i}]] ⟩^{*}$ by (143.4). The equality formula is the same calculation with ${Eq}_{[[S]]}$ in place of $[[R]]$ .

Propositional. $[[σ {]]}^{*}$ is a Heyting homomorphism by definition 143.8, so it commutes with $⊤, ⊥, \land, \lor, \Rightarrow$ ; combine with the induction hypotheses.

Quantifier. Let $φ$ be a formula over $Γ, x : S$ , and let $p : [[Γ]] \times [[S]] ⟶ [[Γ]]$ and $q : [[Δ]] \times [[S]] ⟶ [[Δ]]$ be the first projections. The substitution $σ$ extends to $σ^{+} : = (σ, x)$ on the extended contexts, and $[[σ^{+}]] = [[σ]] \times {id}_{[[S]]}$ . The square Mathematical diagram Diagram is a pullback by lemma 143.9. Hence Beck–Chevalley (143.6) applies: $\begin{aligned} [[(\exists x : S . φ) [σ]]] & \overset{d e f .}{=} \exists_{q} [[φ [σ^{+}]]] \overset{I H}{=} \exists_{q} ([[σ^{+} {]]}^{*} [[φ]]) \\ \overset{(143.6)}{=} [[σ {]]}^{*} (\exists_{p} [[φ]]) \overset{d e f .}{=} [[σ {]]}^{*} [[\exists x : S . φ]], \end{aligned}$ and the universal clause of (143.6) gives the same for $\forall$ . ◻

Theorem 143.24 — Soundness ¶

Let $M$ be a structure in a hyperdoctrine $(C, P)$ in which every axiom of $T$ is valid. Then every sequent derivable in $T$ is valid in $M$ .

Referenced from 8 locations

Proof of Theorem 143.24 — Soundness

Proof. Induct on the derivation. Axioms are valid by hypothesis.

Id and Cut. Reflexivity and transitivity of $\leq$ in $P ([[Γ]])$ .

Subst. By the induction hypothesis $[[φ]] \leq [[ψ]]$ in $P ([[Γ]])$ . Applying the monotone map $[[σ {]]}^{*}$ gives $[[σ {]]}^{*} [[φ]] \leq [[σ {]]}^{*} [[ψ]]$ , which by lemma 143.23 is $[[φ [σ]]] \leq [[ψ [σ]]]$ .

Lattice rules. Each is a clause of the universal property of the meet or join in $P ([[Γ]])$ ; for instance the rule with two premises concluding $φ ⊢ ψ_{1} \land ψ_{2}$ is the existence half of definition 142.1 in the preorder $P ([[Γ]])$ .

Implication. The two-way rule is (143.3) at $[[φ]], [[ψ]], [[χ]]$ .

Quantifiers. The two-way rule for $\exists$ is the adjunction $\exists_{p} ⊣ p^{*}$ evaluated at $[[φ]]$ and $[[ψ]]$ , once it is checked that the weakening of $ψ$ to $Γ, x : S$ is interpreted as $p^{*} [[ψ]]$ ; that check is lemma 143.23 for the substitution that forgets $x$ . The rule for $\forall$ is the adjunction $p^{*} ⊣ \forall_{p}$ .

Frobenius. By proposition 143.13 in the powerset case, and in general by the hypothesis that the hyperdoctrine satisfies (143.7); proposition 143.25 shows that Beck–Chevalley together with the adjunctions already forces it when $C$ has finite products, so no further assumption is needed.

Equality. Write $δ$ for the arrow ${id}_{[[Γ]]} \times δ_{[[S]]}$ , the diagonal of $[[S]]$ taken in the context $Γ$ . By lemma 143.23, $[[ρ [x / y]]]$ is $δ^{*} [[ρ]]$ , and the two-way rule is then theorem 143.15 at $[[ρ]]$ . ◻

Proposition 143.25 — Frobenius from Beck–Chevalley ¶

Let $(C, P)$ be a hyperdoctrine and $p : Γ \times A ⟶ Γ$ a product projection. Then for $θ \in P (Γ)$ and $φ \in P (Γ \times A)$ , $\exists_{p} (p^{*} θ \land φ) = θ \land \exists_{p} φ$ .

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Proposition 143.25 — Frobenius from Beck–Chevalley

Proof. From left to right. Both $p^{*} θ \land φ \leq φ$ and $p^{*} θ \land φ \leq p^{*} θ$ hold. Applying the monotone $\exists_{p}$ to the first gives $\exists_{p} (p^{*} θ \land φ) \leq \exists_{p} φ$ . For the second, the adjunction $\exists_{p} ⊣ p^{*}$ turns $p^{*} θ \land φ \leq p^{*} θ$ into $\exists_{p} (p^{*} θ \land φ) \leq θ$ . The two together give the inequality into the meet.

From right to left. By (143.3) it suffices to show $\exists_{p} φ \leq (θ \Rightarrow \exists_{p} (p^{*} θ \land φ))$ , and by $\exists_{p} ⊣ p^{*}$ this is equivalent to $φ \leq p^{*} (θ \Rightarrow \exists_{p} (p^{*} θ \land φ)) .$ Now $p^{*}$ preserves $\Rightarrow$ , being a Heyting homomorphism, so the right-hand side is $p^{*} θ \Rightarrow p^{*} \exists_{p} (p^{*} θ \land φ)$ , and by (143.3) again the displayed inequality is equivalent to $φ \land p^{*} θ \leq p^{*} \exists_{p} (p^{*} θ \land φ),$ which is the unit of the adjunction $\exists_{p} ⊣ p^{*}$ at the element $p^{*} θ \land φ$ . ◻

Remark 143.26 — What is not proved here ¶

Theorem 143.24 is one direction. No completeness theorem is asserted in this chapter, for either the powerset hyperdoctrine or the class of all hyperdoctrines. A completeness statement requires a fixed calculus, a fixed class of models, and a theorem signature naming which sequents are recovered; the syntactic construction of section 143.6 produces a hyperdoctrine but is not by itself such a theorem, because the canonical structure in it validates exactly the derivable sequents by construction, which is a restatement rather than a completeness proof for an independently given class.

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

The syntactic hyperdoctrine and the internal language

Every theory produces a hyperdoctrine, and every hyperdoctrine produces a theory. Both constructions are performed here; neither is claimed to invert the other.

The first construction needs one fact about the equality rule of definition 143.21, and that fact is what makes substitution well defined on provable-equality classes of terms.

Lemma 143.27 — Equality is a congruence ¶

In every theory $T$ the following are derivable, for $Γ, x : S, y : S$ a context, $t$ a term with a distinguished variable of sort $S$ , and $φ$ a formula with a distinguished variable of sort $S$ :

$Γ, x : S ∣ ⊤ ⊢ x =_{S} x$ ;
$Γ, x : S, y : S ∣ x =_{S} y ⊢ y =_{S} x$ ;
$Γ, x : S, y : S ∣ x =_{S} y ⊢ t [x] = t [y]$ ;
$Γ, x : S, y : S ∣ x =_{S} y ⊢ φ [x] \Rightarrow φ [y]$ .

Referenced from 7 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Lemma 143.27 — Equality is a congruence

Proof. Each clause instantiates the two-way equality rule at a chosen $ρ$ .

(1) Take $ρ : = (x =_{S} y)$ . The lower line is $x =_{S} y ⊢ x =_{S} y$ , an instance of Id, so the upward direction gives the upper line $⊤ ⊢ ρ [x / y]$ , which is $⊤ ⊢ x =_{S} x$ .

(2) Take $ρ : = (y =_{S} x)$ . Then $ρ [x / y]$ is $x =_{S} x$ , derivable by (1), so the downward direction gives $x =_{S} y ⊢ y =_{S} x$ .

(3) Take $ρ : = (t [x] = t [y])$ . Then $ρ [x / y]$ is $t [x] = t [x]$ , which is derived from (1) by Subst along the substitution sending the distinguished variable to $t [x]$ . The downward direction gives the claim.

(4) Take $ρ : = (φ [x] \Rightarrow φ [y])$ . Then $ρ [x / y]$ is $φ [x] \Rightarrow φ [x]$ , and $⊤ ⊢ φ [x] \Rightarrow φ [x]$ follows from $⊤ \land φ [x] ⊢ φ [x]$ by the two-way implication rule. The downward direction gives the claim. ◻

Theorem 143.28 — The syntactic hyperdoctrine ¶

Let $T$ be a theory over $Σ$ . Define

$C_{T}$ : objects are the contexts over $Σ$ ; an arrow $Δ ⟶ Γ$ is a list $σ = (t_{1}, \dots, t_{n})$ of terms of $Δ$ with $t_{i}$ of the sort of the $i$ -th declaration of $Γ$ , taken modulo the equivalence identifying $σ$ and $σ^{'}$ when $Δ ∣ ⊤ ⊢ t_{i} = t_{i}^{'}$ is derivable for each $i$ ; composition is substitution and the identity is the variable list;
$P_{T} (Γ)$ : the formulas over $Γ$ , preordered by $φ \leq ψ$ when $Γ ∣ φ ⊢ ψ$ is derivable, and $σ^{*} φ : = φ [σ]$ .

Then $(C_{T}, P_{T})$ is a hyperdoctrine.

Referenced from 4 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Theorem 143.28 — The syntactic hyperdoctrine

Proof. $C_{T}$ is a category with finite products. Composition is well defined on equivalence classes: if $t_{i} = t_{i}^{'}$ is derivable over $Δ$ and $u_{j} = u_{j}^{'}$ over $Ξ$ , then $t_{i} [\vec{u}] = t_{i}^{'} [{\vec{u}}^{'}]$ is derivable by lemma 143.27(3) applied once for each variable, together with Subst and transitivity. The category laws are those of proposition 141.7, which hold already for representatives. The empty context is terminal and concatenation is a product, by the proof of proposition 142.7, which used only entrywise composition.

$P_{T} (Γ)$ is a Heyting algebra. The lattice rules of definition 143.21 are exactly the universal properties of $⊤, ⊥, \land, \lor$ in the preorder, and the two-way implication rule is (143.3).

$σ^{*}$ is a homomorphism and $P_{T}$ is a functor. Substitution commutes with every propositional connective by the definition of substitution on formulas, so $σ^{*}$ preserves each operation on the nose; it is monotone by Subst. Functoriality $(σ \circ τ)^{*} = τ^{*} \circ σ^{*}$ is the syntactic law $φ [σ] [τ] = φ [σ \circ τ]$ , and ${id}_{}^{*} = {id}_{}$ is $φ [\vec{x}] = φ$ .

Adjoints along a projection. For $p : Γ \times (x : S) ⟶ Γ$ the two-way quantifier rules of definition 143.21 state precisely $\exists x : S . (-) ⊣ p^{*} ⊣ \forall x : S . (-)$ .

Adjoints along an arbitrary arrow. Let $σ = (t_{1}, \dots, t_{n}) : Δ ⟶ Γ$ with $Δ = y_{1} : R_{1}, \dots, y_{m} : R_{m}$ and $Γ = x_{1} : S_{1}, \dots, x_{n} : S_{n}$ . Write $E_{σ} : = ⋀_{i = 1}^{n} (x_{i} =_{S_{i}} t_{i})$ , a formula over the concatenated context $Γ Δ$ , and for $φ$ over $Δ$ put $\begin{aligned} \exists_{σ} φ & : = \exists y_{1} : R_{1} \dots \exists y_{m} : R_{m} . (E_{σ} \land φ), \\ \forall_{σ} φ & : = \forall y_{1} : R_{1} \dots \forall y_{m} : R_{m} . (E_{σ} \Rightarrow φ), \end{aligned}$ both formulas over $Γ$ . We verify the two adjunctions.

Existential. Suppose $Γ ∣ \exists_{σ} φ ⊢ ψ$ . Applying the iterated $\exists$ -rule upward gives $Γ Δ ∣ E_{σ} \land φ ⊢ ψ$ . Substitute $σ$ for the variables of $Γ$ by Subst; this replaces each $x_{i}$ by $t_{i}$ , turning $E_{σ}$ into $\underset{i}{⋀} (t_{i} = t_{i})$ , which is derivable from $⊤$ by lemma 143.27(1). Hence $Δ ∣ φ ⊢ ψ [σ]$ , which is $φ \leq σ^{*} ψ$ .

Conversely suppose $Δ ∣ φ ⊢ ψ [σ]$ . Weakening to $Γ Δ$ and using lemma 143.27(4) once for each $i$ , the hypothesis $E_{σ}$ rewrites $ψ [σ]$ into $ψ$ : $Γ Δ ∣ E_{σ} \land φ ⊢ E_{σ} \land ψ [σ] ⊢ ψ .$ The iterated $\exists$ -rule downward gives $Γ ∣ \exists_{σ} φ ⊢ ψ$ .

Universal. Suppose $Γ ∣ σ^{*} ψ ⊢ φ$ read in $Δ$ , that is, $Δ ∣ ψ [σ] ⊢ φ$ . Weaken to $Γ Δ$ and use lemma 143.27(4) in the other direction: $E_{σ} \land ψ ⊢ ψ [σ] ⊢ φ$ , so $Γ Δ ∣ ψ ⊢ E_{σ} \Rightarrow φ$ by the implication rule. The iterated $\forall$ -rule gives $Γ ∣ ψ ⊢ \forall_{σ} φ$ . Conversely, from $Γ ∣ ψ ⊢ \forall_{σ} φ$ the $\forall$ -rule gives $Γ Δ ∣ ψ ⊢ E_{σ} \Rightarrow φ$ ; substituting $σ$ for the variables of $Γ$ makes $E_{σ}$ derivable from $⊤$ as above, so $Δ ∣ ψ [σ] ⊢ φ$ .

Beck–Chevalley. By lemma 143.9 the squares to be checked are formed by a substitution $σ : Δ ⟶ Γ$ and a projection, and there the condition reads $(\exists x : S . φ) [σ] = \exists x : S . (φ [σ^{+}]),$ where $σ^{+}$ extends $σ$ by $x \mapsto x$ and the bound variable is chosen outside the variables of $Δ$ and the terms of $σ$ . That is the definition of substitution into a quantified formula, so both sides are the same formula and in particular provably equivalent. The universal clause is identical. For a pullback square that is not of this form, the condition follows by factoring the substitution through the product projections, using the strict functoriality just proved. ◻

Definition 143.29 — Internal language ¶

Let $(C, P)$ be a hyperdoctrine. Its internal language is the signature $Σ_{C, P}$ whose sorts are the objects of $C$ , whose function symbols $\underset{―}{g} : (A_{1}, \dots, A_{n}) \to B$ are the arrows $g : A_{1} \times \dots \times A_{n} ⟶ B$ of $C$ , and whose relation symbols $\underset{―}{φ} : (A_{1}, \dots, A_{n})$ are the elements $φ \in P (A_{1} \times \dots \times A_{n})$ . Its internal theory $T_{C, P}$ has as axioms every sequent $Γ ∣ α ⊢ β$ that is valid in the canonical structure $M_{C, P}$ , which interprets each sort, function symbol and relation symbol by the object, arrow and predicate it names.

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Theorem 143.30 — The canonical structure computes names ¶

In the canonical structure of definition 143.29:

$[[Γ ⊢ \underset{―}{g} (x_{1}, \dots, x_{n}) : B]] = g$ for the context $Γ = x_{1} : A_{1}, \dots, x_{n} : A_{n}$ ;
$[[\underset{―}{φ} (x_{1}, \dots, x_{n})]] = φ$ ;
a sequent is derivable in $T_{C, P}$ only if it is valid in $M_{C, P}$ .

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Proof of Theorem 143.30 — The canonical structure computes names

Proof. (1) By lemma 142.2(1) the pairing of all the projections is the identity, $⟨ {pr}_{1}, \dots, {pr}_{n} ⟩ = {id}_{A_{1} \times \dots \times A_{n}},$ so definition 143.22 gives $[[\underset{―}{g} (\vec{x})]] = [[\underset{―}{g}]] \circ ⟨ {pr}_{1}, \dots, {pr}_{n} ⟩ = g \circ {id}_{} = g .$

(2) The same calculation: $[[\underset{―}{φ} (\vec{x})]] = ⟨ {pr}_{1}, \dots, {pr}_{n} ⟩^{*} φ = {id}_{}^{*} φ = φ$ by (143.4).

(3) Every axiom of $T_{C, P}$ is valid in $M_{C, P}$ by construction, so theorem 143.24 applies. ◻

The converse of theorem 143.30(3) is immediate here, since the axioms were taken to be all valid sequents; that is why it is not a completeness theorem. The mathematical content of the two constructions is that they translate between the two vocabularies without loss on atoms (clauses (1) and (2)) and preserve derivability in one direction (clause (3)). A theorem relating a syntactically presented theory to the class of all its hyperdoctrine models requires a separately frozen statement and is not proved here (remark 143.26).

Example 143.31 — Reading a hyperdoctrine as a logic ¶

Take the powerset hyperdoctrine. Its internal language has one sort for each set, one function symbol for each function, and one relation symbol for each subset of a finite product. The canonical structure interprets them back as themselves, and a sequent $x : A ∣ \underset{―}{U} (x) ⊢ \underset{―}{V} (x)$ is valid exactly when $U \subseteq V$ . A derivation of that sequent from the propositional and quantifier rules is therefore a proof of an inclusion of subsets, written without mentioning elements.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Exercise 143.6 ¶

★☆☆ Check directly that the empty context is terminal in $C_{T}$ and that the concatenation of two contexts satisfies definition 142.1, naming the rule of definition 143.21 used for the uniqueness clause.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Exercise 143.7 ¶

★★☆ For $σ : Δ ⟶ Γ$ in a hyperdoctrine define the graph of $σ$ as $\exists_{⟨ {id}_{Δ}, σ ⟩} (⊤) \in P (Δ \times Γ)$ . Compute it in the powerset hyperdoctrine, and prove that in $C_{T}$ it is provably equivalent to $E_{σ}$ from the proof of theorem 143.28.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Exercise 143.8 ¶

★☆☆ Derive transitivity, $Γ, x, y, z ∣ x = y \land y = z ⊢ x = z$ , from lemma 143.27 by choosing an appropriate $ρ$ . One line.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Suggested first pass.

Begin with exercise 143.9 and exercise 143.10, then complete exercise 143.13.

Exercise 143.9 ¶

★★☆ Write out the omitted lattice cases of theorem 143.24 in full: the two projection rules for $\land$ , the two injection rules for $\lor$ , and the case rule for $\lor$ . For each, name the clause of the universal property in the preorder $P ([[Γ]])$ that it instantiates.

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Exercise 143.10 ¶

★★☆ Let $C = Set$ and let $f : X \to Y$ be surjective. Show that $\exists_{f} \circ f^{*} = {id}_{}$ on $P (Y)$ and that $f^{*}$ is injective. Then exhibit a non-surjective $f$ for which $\exists_{f} \circ f^{*} \neq {id}_{}$ , and locate the failing inclusion.

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Exercise 143.11 ¶

★★☆ The powerset hyperdoctrine has Boolean fibers (example 143.2). Show that adding the sequent $Γ ∣ ⊤ ⊢ φ \lor (φ \Rightarrow ⊥)$ for all $Γ, φ$ to definition 143.21 remains sound for it, and that the resulting calculus is not sound for the hyperdoctrine of exercise 143.4. Give the refuting instance.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Exercise 143.12 ¶

★★★ Suppose $(C, P)$ has comprehension (definition 143.17). Prove that the assignment $φ \mapsto {Γ ∣ φ}$ extends to a functor $P (Γ) \to C / Γ$ right adjoint to the functor sending $f : Δ ⟶ Γ$ to $\exists_{f} (⊤)$ . Check both triangle identities of (142.6) in the powerset hyperdoctrine.

Referenced from 2 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Exercise 143.13 ¶

★★★ Practical project.hyperdoctrine-sequent-checker Implement a checker for validity of first-order sequents in a finite powerset hyperdoctrine. The input is: a finite list of sorts, each with a finite carrier given as a list of elements; a finite list of function symbols, each with an explicit table; a finite list of relation symbols, each with an explicit list of satisfying tuples; and a sequent $Γ ∣ φ ⊢ ψ$ of definition 143.20. The program computes $[[φ]]$ and $[[ψ]]$ as subsets of the finite set $[[Γ]]$ , by the clauses of definition 143.22, and reports whether $[[φ]] \subseteq [[ψ]]$ .

Invariant. Every intermediate value is a subset of the product carrier of the context in which its formula lives; the program checks the arity and sort of each subterm before evaluating, and rejects an ill-sorted input rather than producing a subset of the wrong set.

Concrete result. For a valid sequent the program prints valid; for an invalid one it prints invalid together with one element of $[[φ]] ∖ [[ψ]]$ , displayed as a tuple of carrier elements, which is a counterexample to the sequent.

Acceptance test. Use one sort $S$ with carrier ${0, 1, 2}$ , one binary relation symbol $R$ interpreted as ${(m, n) ∣ m \leq n}$ , and check the following four inputs. The sequent $x : S ∣ ⊤ ⊢ \exists y : S . R (x, y)$ must print valid; the sequent $x : S ∣ ⊤ ⊢ \forall y : S . R (x, y)$ must print invalid with counterexample $x = 1$ or $x = 2$ ; the Frobenius equation (143.7) must be confirmed in both directions on $θ : = R (x, x)$ and $φ : = R (x, y)$ ; and the Beck–Chevalley equation (143.6) must be confirmed for the square of lemma 143.9 with $σ$ the constant map at $0$ . A run reporting the second sequent valid has interpreted $\forall_{p}$ as a union rather than the intersection required by (143.1).

Referenced from 3 locations

Categorical Logic, Hyperdoctrines, and Internal Languages

Sources. Hyperdoctrines and the reading of quantifiers as adjoints to substitution are due to F. W. Lawvere, Adjointness in Foundations, Dialectica 23 (1969), 281–296, reprinted in Reprints in Theory and Applications of Categories 16 (2006); the four data of a hyperdoctrine and the powerset and higher-order-theory examples are on physical pages 11–13 of that reprint, and the observation that the existence of $\exists$ forces substitution to commute with conjunction is on page 12. The equality predicate as $\exists_{δ} (⊤)$ and comprehension as an adjoint are developed in Lawvere’s companion paper Equality in hyperdoctrines and comprehension schema as an adjoint functor, Proceedings of Symposia in Pure Mathematics 17 (1970), 1–14. The posetal definition used here, together with the syntactic, powerset and subobject examples, is Awodey, Introduction to Categorical Logic, Definition 3.4.1 and the surrounding section (course draft of 15 September 2024, physical pages 176–178) [Awo24]; the systematic fibrational treatment, including the proof-relevant version of definition 143.8, is Jacobs [Jac99], and a book-length bridge from typed calculi to these models is Asperti and Longo [AL91]. The realizability quotients that turn a hyperdoctrine into a category of extensional objects are the subject of chapter 144, whose construction and invariant differ from the ones proved here.