From 3b8788fbd782c4d292ad9b32b381246e139069f6 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 22 Aug 2024 18:52:58 -0400 Subject: [PATCH] wip: some prose on ordinal of prop --- src/Order/Ordinal/Instances/Prop.lagda.md | 106 ++++++++++++++++++++++ 1 file changed, 106 insertions(+) diff --git a/src/Order/Ordinal/Instances/Prop.lagda.md b/src/Order/Ordinal/Instances/Prop.lagda.md index d26c58ce6..2e3435093 100644 --- a/src/Order/Ordinal/Instances/Prop.lagda.md +++ b/src/Order/Ordinal/Instances/Prop.lagda.md @@ -4,10 +4,15 @@ description: | --- @@ -29,16 +38,58 @@ open Ordinal Ωₒ : Ordinal lzero lzero Ωₒ .Ob = Ω Ωₒ ._≺_ P Q = ¬ ∣ P ∣ × ∣ Q ∣ +``` + +To show that $\prec$ is well-founded, observe that if $Q \prec P$, then +$\lnot R \prec P$, as we would have both $Q$ and $\lnot Q$. This means +that we only need two layers of accessiblity to reach the end of any +chain in $\Omega$. + +```agda Ωₒ .≺-wf P = go where go : Acc (λ P Q → ¬ ∣ P ∣ × ∣ Q ∣) P go = acc λ Q (¬q , _) → acc λ R (_ , q) → absurd (¬q q) +``` + +Extensionality follows from another straighforward argument. First, observe +that if $P \preceq Q$ then $P \to Q$: by definition, $R \prec P \to R \prec Q$ +for every $R$, so we can use $\bot$ and get that $\lnot \bot \times P \to \lnot \bot \times Q$. +The rest follows by propositional extensionality! + +```agda Ωₒ .≺-ext {P} {Q} P≼Q Q≼P = Ω-ua (λ p → P≼Q ⊥Ω (id , p) .snd) (λ q → Q≼P ⊥Ω (id , q) .snd) +``` + +Finally, transitivity and thinness follow almost immediately. + +```agda Ωₒ .≺-trans (¬p , q) (¬q , r) = ¬p , r Ωₒ .≺-is-prop = hlevel 1 +``` + +## Properties of the ordinal of propositions + + +We can give a nice characterisation of the preorder associated to +$(\Omega, \prec)$: $P \preceq Q$ if and only if $P \to Q$. + +```agda +Ω≼-equiv : ∀ {P Q : Ω} → (P Ωₒ.≼ Q) ≃ (∣ P ∣ → ∣ Q ∣) +Ω≼-equiv = Iso→Equiv $ + (λ P≼Q p → P≼Q ⊥Ω (id , p) .snd) , + iso (λ f R (¬r , p) → ¬r , f p) + (λ _ → prop!) + (λ _ → prop!) +``` + +This gives us an indirect way of showing that $\bot$ is a [[bottom element]] +and $\top$ is a [[top element]], but the direct proofs are honestly easier. ```agda ⊥Ω-bot : ∀ P → ⊥Ω Ωₒ.≼ P @@ -47,3 +98,58 @@ module Ωₒ = Order.Ordinal.Reasoning Ωₒ ⊤Ω-top : ∀ P → P Ωₒ.≼ ⊤Ω ⊤Ω-top P Q (¬q , _) = ¬q , tt ``` + +More interestingly, we can simulate $2$ inside of $\Omega$ by taking +$0$ to $\bot$ and $1$ to $\top$ + +```agda +Ωₒ-sim-2ₒ : Simulation 2 Ωₒ +Ωₒ-sim-2ₒ .hom fzero = ⊥Ω +Ωₒ-sim-2ₒ .hom (fsuc fzero) = ⊤Ω +``` + +
+Proving that this is a simulation is quite dry, so we omit the +details. + +```agda +Ωₒ-sim-2ₒ .pres-≺ {fzero} {fsuc fzero} x + +However, the converse is a constructive taboo! More precisely, if $2$ +simulates $\Omega$, then the [[law of excluded middle]] holds. + +```agda +2ₒ-sim-Ωₒ→lem : Simulation Ωₒ 2 → LEM +``` + +Let $P$ be a proposition. Our simulation gives us a function $f : \Omega \to 2$, +so we can check if $f$ sends $P$ to $0$ or $1$. + +```agda +2ₒ-sim-Ωₒ→lem f P with inspect (f # P) +``` + +If $f(P) = 0$, then we can show $\lnot P$. Suppose that we had some +$p : P$, and note that $\bot \prec P$, as $P$ is inhabited. +Moreover, $f$ is strictly monotone, so $f(\bot) < f(P)$. However, +$f(P) = 0$, so $f(\bot) < 0$; a contradiction! + +```agda +... | fzero , fp=0 = + no (λ p → x≮0 (≤-trans (f .pres-≺ {⊥Ω} {P} (id , p)) (≤-refl' (ap to-nat fp=0)))) +``` + +Conversely, if $f(P) = 1$, then we can prove $P$. As $f$ is a simulation +and $f(P) \leq 1$, there must exist some $Q$ in the preimage of $0$ with +$Q \prec P$, which immediately lets us prove $P$. + +```agda +... | fsuc fzero , fp=1 = + yes (snd (f .sim-≺ {P} {0} {≤-refl' (sym (ap to-nat fp=1))})) +```