--- title: "The classical boundary" module: Base.Classical lang: en site: "Bedrock" description: "The classical boundary" stage: "Foundations" reading_order: 4 canonical: https://bedrock.institute/en/Base.Classical.html html: Base.Classical.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Base/Classical.lagda.md prerequisites: [Base.Prelude, Base.Impredicativity] routes: [common-foundations] translations: [https://bedrock.institute/zh/Base.Classical.md, https://bedrock.institute/ja/Base.Classical.md] agent_guide: https://bedrock.institute/llms.txt license: "CC-BY-NC-SA-4.0" --- ```agda {-# OPTIONS --cubical --safe --guardedness #-} module Base.Classical where ``` # The classical boundary ```agda open import Base.Prelude open import Base.Impredicativity using ( Resizing; ΩResizing; ΩResizing→Resizing ) ``` This book develops classical set theory inside constructive Cubical type theory. Keeping the ambient foundation constructive makes the boundary of classical reasoning visible: definitions and proofs that do not need excluded middle remain constructive, while a theorem that does need it receives it as an explicit parameter. If classical logic were built into the ambient theory from the outset, the statements themselves would no longer reveal that distinction. Besides marking the point at which the development becomes classical, excluded middle resolves the two smallness questions left open in the preceding chapter: - Propositional resizing: given `P : hProp ℓ₁`, can we find a proposition at a chosen level `ℓ₂` whose underlying type is equivalent to that of `P`? - Ω-resizing: can the whole type `hProp ℓ₁` be presented by a single type in `Type ℓ₂`? ## Excluded middle Excluded middle supplies a decision for every proposition. Since propositions inhabit different universes, this principle must be stated one level at a time. **Definition** (`LEM`) We write `LEM ℓ` for excluded middle at level `ℓ`, and define it as the dependent function below. For each `P : hProp ℓ`, it returns a decision `Dec ⟨ P ⟩`: `yes` carries a proof of `P`, while `no` carries a refutation. Because the function ranges over the whole proposition universe `hProp ℓ`, `LEM ℓ` inhabits `Type (ℓ-suc ℓ)`. Its level index therefore records exactly which propositions the classical assumption can decide. ```agda LEM : ∀ ℓ → Type (ℓ-suc ℓ) LEM ℓ = (P : hProp ℓ) → Dec ⟨ P ⟩ ``` **Fact** (`isPropLEM`) At every level `ℓ`, excluded middle `LEM ℓ` is itself a proposition. ```agda isPropLEM : ∀ {ℓ} → isProp (LEM ℓ) ``` **Proof** For each `P : hProp ℓ`, `isPropDec` makes `Dec ⟨ P ⟩` a proposition. The closure of propositions under dependent functions, `isPropΠ`, then proves the claim pointwise. ```agda isPropLEM {ℓ} = isPropΠ λ P → isPropDec ⟨ P ⟩isProp ``` **Lemma** (`lowerLEM`) Excluded middle at a successor level implies excluded middle at the level immediately below. Repeating the lemma descends through further successor levels. ```agda lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ ``` **Proof** Let `lem : LEM (ℓ-suc ℓ)` be given, and fix `P : hProp ℓ`. The hypothesis cannot decide `P` directly because it expects a proposition at level `ℓ-suc ℓ`. We therefore form the higher-level proposition whose underlying type is `Lift ⟨ P ⟩`; its propositionhood certificate is `isOfHLevelLift 1 ⟨ P ⟩isProp`. Applying `lem` to this pair decides the lifted copy of `P`. The two panels below show how to turn that decision into `Dec ⟨ P ⟩`. The positive branch uses `lower`; the negative branch assumes a proof of `P` and refutes its lifted image. The function `mapDec` assembles these conversions. ```agda lowerLEM {ℓ} lem P = mapDec lower (λ np p → np (lift p)) (lem (Lift ⟨ P ⟩ , isOfHLevelLift 1 ⟨ P ⟩isProp)) ```
$$\operatorname{yes}\,\hat x$$
$\operatorname{Lift}\langle P\rangle$ $\hat x$ $\operatorname{lower}$ $\langle P\rangle$ $\operatorname{lower}\,\hat x$
$$\operatorname{yes}\,(\operatorname{lower}\,\hat x)$$
$$\operatorname{no}\,\mathit{np}$$
$\operatorname{Lift}\langle P\rangle$ $\operatorname{lift}\,p$ $\operatorname{lift}$ $\langle P\rangle$ $p$
$$\mathit{np}\,(\operatorname{lift}\,p):\bot_0$$
A positive decision sends its proof downward by `lower`. A negative decision refutes a hypothetical `p : ⟨ P ⟩` by sending it upward with `lift` and applying `np`
## Ω-resizing from excluded middle Once every proposition at the source level can be decided, each can be represented by one of two Boolean labels. For arbitrary levels `ℓ₁` and `ℓ₂`, `ΩResizing ℓ₁ ℓ₂` asks for one type in `Type ℓ₂` equivalent to the entire type `hProp ℓ₁`. This chapter constructs such a classifier from excluded middle at `ℓ₁`. The general theorem `ΩResizing→Resizing` then turns this small presentation of the proposition universe into `Resizing ℓ₁ ℓ₂`: every source-level proposition receives an equivalent representative at the target level. The classifier uses the previously introduced type `Bool`, whose two constructors `true` and `false` serve as its labels. The labels are codes, not themselves propositions in `hProp ℓ₁`. Since `Bool` lies in `Type ℓ-zero`, the code type is lifted to `Lift {ℓ-zero} {ℓ₂} Bool` in the target universe `Type ℓ₂`. Its two labels will represent `⊤` and `⊥`, both available in `hProp ℓ₁` at every level. Constructing an equivalence between this target-level code type and the proposition universe will therefore give the required Ω-resizing. The construction has two stages. First we define encoding from an explicit decision `Dec ⟨ P ⟩`, then decoding, and finally the two round-trip laws. We collect these four auxiliary results in the private module `BooleanCodes`; none uses excluded middle. The public theorem then invokes excluded middle to supply a decision for every `P` and assembles the four results into the equivalence.
```agda private module BooleanCodes where ```
**Lemma** (`encodeB`) There is an encoding operation that takes a proposition `P` together with its decision and returns a code in `Lift {ℓ-zero} {ℓ₂} Bool`. ```agda encodeB : ∀ {ℓ₁ ℓ₂} (P : hProp ℓ₁) → Dec ⟨ P ⟩ → Lift {ℓ-zero} {ℓ₂} Bool ``` **Proof** Inspect the supplied decision. The `yes` branch returns `lift true`, while the `no` branch returns `lift false`. Both branches discard the particular proof or refutation and retain only which outcome holds. Because the decision is supplied explicitly, encoding uses no excluded middle. ```agda encodeB P (yes _) = lift true encodeB P (no _) = lift false ``` **Lemma** (`decodeB`) There is a decoding operation that takes a code in `Lift {ℓ-zero} {ℓ₂} Bool` and returns a proposition in `hProp ℓ₁`. ```agda decodeB : ∀ {ℓ₁ ℓ₂} → Lift {ℓ-zero} {ℓ₂} Bool → hProp ℓ₁ ``` **Proof** Inspect the supplied code. The `lift true` branch returns `⊤`, while the `lift false` branch returns `⊥`. Both branches discard the label and retain only the proposition it represents. Because the two cases are handled directly, decoding also uses no excluded middle. ```agda decodeB (lift true) = ⊤ decodeB (lift false) = ⊥ ``` **Lemma** (`secB`) For every proposition `P` and decision `d`, encoding with `encodeB` and then decoding with `decodeB` recovers `P` in `hProp`: `decodeB (encodeB P d) ≡ P`. ```agda secB : ∀ {ℓ₁ ℓ₂} (P : hProp ℓ₁) (d : Dec ⟨ P ⟩) → decodeB {ℓ₁} {ℓ₂} (encodeB {ℓ₁} {ℓ₂} P d) ≡ P ``` **Proof** Split on `d`. If `d = yes p`, encoding selects `lift true` and decoding returns `⊤`, so the goal becomes `⊤ ≡ P`. Propositional extensionality `⇔toPath` constructs this path from the map returning `p` and the map returning `tt*`. If `d = no np`, encoding selects `lift false` and decoding returns `⊥`, so the goal becomes `⊥ ≡ P`. Its two maps are the absurd function `λ ()` and the refutation `np` followed by elimination from `⊥₀`. Thus decoding after encoding recovers a proposition equal to `P` in both cases. ```agda secB {ℓ₁} {ℓ₂} P (yes p) = ⇔toPath (λ _ → p) (λ _ → tt*) secB {ℓ₁} {ℓ₂} P (no np) = ⇔toPath (λ ()) (λ p → ⊥₀-rec (np p)) ``` **Lemma** (`retrB`) For every code `b̂` and decision `d` of the proposition it decodes to, decoding with `decodeB` and then encoding with `encodeB` recovers `b̂`: `encodeB (decodeB b̂) d ≡ b̂`. ```agda retrB : ∀ {ℓ₁ ℓ₂} (b̂ : Lift {ℓ-zero} {ℓ₂} Bool) (d : Dec ⟨ decodeB {ℓ₁} {ℓ₂} b̂ ⟩) → encodeB {ℓ₁} {ℓ₂} (decodeB {ℓ₁} {ℓ₂} b̂) d ≡ b̂ ``` **Proof** Split on `b̂` and then on `d`, giving four cases. If `b̂ = lift true`, decoding returns `⊤`. A proof selects `lift true` again, so the equality is `refl`; a refutation is impossible because applying it to `tt*` produces an element of `⊥₀`. If `b̂ = lift false`, decoding returns `⊥`. A proof is impossible by the empty pattern `()`; a refutation selects `lift false` again, so the equality is `refl`. Thus encoding after decoding recovers the original code in every possible case. ```agda retrB {ℓ₁} {ℓ₂} (lift true) (yes _) = refl retrB {ℓ₁} {ℓ₂} (lift true) (no n⊤) = ⊥₀-rec (n⊤ tt*) retrB {ℓ₁} {ℓ₂} (lift false) (yes ()) retrB {ℓ₁} {ℓ₂} (lift false) (no _) = refl ```
The two round-trip laws show that encoding and decoding become mutually inverse once a decision is supplied uniformly for every proposition. The resulting classifier will therefore be a genuine type equivalence, not merely a surjective labelling of propositions by two truth values. The candidate witness is the pair `(Lift Bool , ...)`. Its first component lies in `Type ℓ₂`, and its second will be an equivalence `hProp ℓ₁ ≃ Lift Bool`. No ordering between `ℓ₁` and `ℓ₂` is required. The downward instance used later takes `ℓ₁ = ℓ-suc ℓ` and `ℓ₂ = ℓ`, but equal or higher target levels are allowed as well. Excluded middle has only one remaining role: it supplies the decisions used by the encoder uniformly; all four private results above are constructive. **Theorem** (`LEM→ΩResizing`) For arbitrary levels `ℓ₁` and `ℓ₂`, excluded middle at the source level `ℓ₁` implies Ω-resizing from `ℓ₁` to `ℓ₂`. ```agda LEM→ΩResizing : ∀ {ℓ₁ ℓ₂} → LEM ℓ₁ → ΩResizing ℓ₁ ℓ₂ ``` **Proof** Choose `Lift Bool` as the first component. For the second, use `isoToEquiv` to turn the following isomorphism into an equivalence. Its forward map sends `P` to `encodeB P (lem P)`, and its backward map is `decodeB`. The round-trip laws are `retrB` and `secB`, each instantiated with the decision supplied by `lem`. These two components form the required witness of `ΩResizing ℓ₁ ℓ₂`. ```agda LEM→ΩResizing lem = Lift Bool , isoToEquiv (iso (λ P → encodeB P (lem P)) decodeB (λ b → retrB {ℓ₁ = _} b (lem (decodeB b))) (λ P → secB {ℓ₂ = _} P (lem P))) where open BooleanCodes ``` The two round-trip laws close the two triangles in the figure below. Fix `lem : LEM ℓ₁`, abbreviate the code type `Lift {ℓ-zero} {ℓ₂} Bool` by $B$, and write $E(P) := \operatorname{encodeB}\,P\,(\operatorname{lem}\,P)$ and $D := \operatorname{decodeB}$. Each round trip returns a point connected to its starting point by the indicated path.
$B$ $E(P)$ $\operatorname{hProp}\,\ell_1$ $P$ $D(E(P))$ $E$ $D$ $\operatorname{secB}$
$\operatorname{hProp}\,\ell_1$ $D(b)$ $B$ $b$ $E(D(b))$ $D$ $E$ $\operatorname{retrB}$
Encoding and decoding are inverse up to paths. Excluded middle supplies the decisions in $E$; with explicit decisions, encoding, decoding and both round-trip laws are constructive
**Corollary** (`LEM→Resizing`) For arbitrary levels `ℓ₁` and `ℓ₂`, excluded middle at the source level `ℓ₁` implies propositional resizing from `ℓ₁` to `ℓ₂`. **Proof** Apply `LEM→ΩResizing`, then convert the resulting proposition-universe resizing with the general theorem `ΩResizing→Resizing`. ```agda LEM→Resizing : ∀ {ℓ₁ ℓ₂} → LEM ℓ₁ → Resizing ℓ₁ ℓ₂ LEM→Resizing lem = ΩResizing→Resizing (LEM→ΩResizing lem) ``` ## Recap This chapter stated excluded middle level by level as `LEM ℓ`, proved that it is itself a proposition, and used `lowerLEM` to obtain the instance immediately below a successor level. From `LEM ℓ₁`, `LEM→ΩResizing` constructs `ΩResizing ℓ₁ ℓ₂` at any target level `ℓ₂`; composing this result with `ΩResizing→Resizing` gives `Resizing ℓ₁ ℓ₂`. Thus one source-level assumption of excluded middle resolves both size questions posed at the beginning of the chapter.