Martin Escardo, 15th November 2023.

Lesser Limited Principle of Omniscience.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Taboos.LLPO where

open import CoNaturals.BothTypes
open import MLTT.Plus-Properties
open import MLTT.Spartan
open import MLTT.Two-Properties
open import Naturals.Parity
open import Naturals.Properties
open import Notation.CanonicalMap
open import Taboos.BasicDiscontinuity
open import Taboos.WLPO
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons

open ββ-equivalence

private
T : (β β π) β π€β Μ
T Ξ± = Ξ£ n κ β , Ξ± n οΌ β

Β¬T : (β β π) β π€β Μ
Β¬T Ξ± = (n : β) β Ξ± n οΌ β

private
instance
Canonical-Map-β-ββ' : Canonical-Map β ββ'
ΞΉ {{Canonical-Map-β-ββ'}} = β-to-ββ'

instance
canonical-map-ββ'-ββπ : Canonical-Map ββ' (β β π)
ΞΉ {{canonical-map-ββ'-ββπ}} = ββ'-to-ββπ

\end{code}

The definition of LLPO uses _β¨_ rather than _+_. We show that with
_+_, LLPO implies WLPO, but it is known that LLPO with _β¨_ doesn't
(there are counter-models).

\begin{code}

untruncated-LLPO : π€β Μ
untruncated-LLPO = (Ξ± : β β π)
β is-prop (T Ξ±)
β ((n : β) β Ξ± ( double n) οΌ β)
+ ((n : β) β Ξ± (sdouble n) οΌ β)

\end{code}

The following version is logically equivalent, which shows that
untruncated LLPO is an instance of De Morgan Law.

\begin{code}

untruncated-LLPO' : π€β Μ
untruncated-LLPO' = (Ξ² Ξ³ : β β π)
β is-prop (T Ξ²)
β is-prop (T Ξ³)
β Β¬ (T Ξ² Γ T Ξ³) β Β¬ T Ξ² + Β¬ T Ξ³

untrucated-LLPO'-gives-untruncated-LLPO : untruncated-LLPO' β untruncated-LLPO
untrucated-LLPO'-gives-untruncated-LLPO llpo' Ξ± h = III
where
Ξ² Ξ³ : β β π
Ξ² n = Ξ± ( double n)
Ξ³ n = Ξ± (sdouble n)

i : is-prop (T Ξ²)
i (n , e) (n' , e') = to-T-οΌ (double-lc (index-uniqueness Ξ± h e e'))

j : is-prop (T Ξ³)
j (n , e) (n' , e') = to-T-οΌ (sdouble-lc (index-uniqueness Ξ± h e e'))

I : Β¬ (T Ξ² Γ T Ξ³)
I ((k , e) , (k' , e')) = even-not-odd' k k' (index-uniqueness Ξ± h e e')

II : Β¬ T Ξ² + Β¬ T Ξ³
II = llpo' Ξ² Ξ³ i j I

III : ((n : β) β Ξ± (double n) οΌ β) + ((n : β) β Ξ± (sdouble n) οΌ β)
III = +functor not-T-gives-Β¬T not-T-gives-Β¬T II

untrucated-LLPO-gives-untruncated-LLPO' : untruncated-LLPO β untruncated-LLPO'
untrucated-LLPO-gives-untruncated-LLPO' llpo Ξ² Ξ³ i j Ξ½ = III
where
f : (n : β) β is-even' n + is-odd' n β π
f n (inl (k , _)) = Ξ² k
f n (inr (k , _)) = Ξ³ k

Ξ± : β β π
Ξ± n = f n (even-or-odd' n)

Ξ±-Ξ² : (n : β) β Ξ± (double n) οΌ Ξ² n
Ξ±-Ξ² n = a (even-or-odd' (double n))
where
a : (d : is-even' (double n) + is-odd' (double n)) β f (double n) d οΌ Ξ² n
a (inl (k , e)) = ap Ξ² (double-lc e)
a (inr (k , e)) = π-elim (even-not-odd' n k (e β»ΒΉ))

Ξ±-Ξ³ : (n : β) β Ξ± (sdouble n) οΌ Ξ³ n
Ξ±-Ξ³ n = a (even-or-odd' (sdouble n))
where
a : (d : is-even' (sdouble n) + is-odd' (sdouble n)) β f (sdouble n) d οΌ Ξ³ n
a (inl (k , e)) = π-elim (even-not-odd' k n e)
a (inr (k , e)) = ap Ξ³ (sdouble-lc e)

I : is-prop (T Ξ±)
I (n , e) (n' , e') = a (even-or-odd' n) (even-or-odd' n')
where
a : (d  : is-even' n  + is-odd' n )
(d' : is-even' n' + is-odd' n')
β (n , e) οΌ[ T Ξ± ] (n' , e')
a (inl (k , refl)) (inl (k' , refl)) =
to-T-οΌ (ap  double (index-uniqueness Ξ² i ((Ξ±-Ξ² k)β»ΒΉ β e) ((Ξ±-Ξ² k') β»ΒΉ β e')))
a (inl (k , refl)) (inr (k' , refl)) =
π-elim (Ξ½ ((k  , ((Ξ±-Ξ² k )β»ΒΉ β e )) , (k' , (( Ξ±-Ξ³ k')β»ΒΉ β e'))))
a (inr (k , refl)) (inl (k' , refl)) =
π-elim (Ξ½ ((k' , ((Ξ±-Ξ² k')β»ΒΉ β e')) , (k  , (( Ξ±-Ξ³ k )β»ΒΉ β e ))))
a (inr (k , refl)) (inr (k' , refl)) =
to-T-οΌ (ap sdouble (index-uniqueness Ξ³ j ((Ξ±-Ξ³ k)β»ΒΉ β e) ((Ξ±-Ξ³ k') β»ΒΉ β e')))

II : ((n : β) β Ξ± (double n) οΌ β) + ((n : β) β Ξ± (sdouble n) οΌ β)
II = llpo Ξ± I

III : Β¬ T Ξ² + Β¬ T Ξ³
III = +functor
(Ξ» (Ο : (n : β) β Ξ± ( double n) οΌ β)
β Β¬T-gives-not-T (Ξ» n β (Ξ±-Ξ² n)β»ΒΉ β Ο n))
(Ξ» (Ο : (n : β) β Ξ± (sdouble n) οΌ β)
β Β¬T-gives-not-T (Ξ» n β (Ξ±-Ξ³ n)β»ΒΉ β Ο n))
II

\end{code}

Two more equivalent formulations of LLPO.

\begin{code}

untruncated-ββ-LLPO : π€β Μ
untruncated-ββ-LLPO = (u v : ββ)
β Β¬ (is-finite u Γ is-finite v)
β (u οΌ β) + (v οΌ β)

untruncated-ββ'-LLPO : π€β Μ
untruncated-ββ'-LLPO = (u v : ββ')
β Β¬ (is-finite' u Γ is-finite' v)
β (u οΌ β') + (v οΌ β')

untruncated-LLPO'-gives-untruncated-ββ'-LLPO : funextβ
β untruncated-LLPO'
β untruncated-ββ'-LLPO
untruncated-LLPO'-gives-untruncated-ββ'-LLPO fe llpo u v ΞΌ = II I
where
I : Β¬ T (ΞΉ u) + Β¬ T (ΞΉ v)
I = llpo (ΞΉ u) (ΞΉ v) (ββ'-to-ββπ-at-most-one-β u) (ββ'-to-ββπ-at-most-one-β v) ΞΌ

II : type-of I β (u οΌ β') + (v οΌ β')
II (inl a) = inl (not-T-is-β' fe u a)
II (inr b) = inr (not-T-is-β' fe v b)

untruncated-ββ'-LLPO-gives-untruncated-LLPO' : funextβ
β untruncated-ββ'-LLPO
β untruncated-LLPO'
untruncated-ββ'-LLPO-gives-untruncated-LLPO' fe llpo Ξ± Ξ² a b ΞΌ = II I
where
I : ((Ξ± , a) οΌ β') + ((Ξ² , b) οΌ β')
I = llpo (Ξ± , a) (Ξ² , b) (Ξ» (Ο , Ξ³) β ΞΌ (Ο , Ξ³))

II : type-of I β Β¬ T Ξ± + Β¬ T Ξ²
II (inl e) = inl (Β¬T-gives-not-T (Ξ» n β ap (Ξ» - β prβ - n) e))
II (inr e) = inr (Β¬T-gives-not-T (Ξ» n β ap (Ξ» - β prβ - n) e))

untruncated-ββ-LLPO-gives-untruncated-ββ'-LLPO : funextβ
β untruncated-ββ-LLPO
β untruncated-ββ'-LLPO
untruncated-ββ-LLPO-gives-untruncated-ββ'-LLPO fe llpo u v ΞΌ = II I
where
I : (ββ'-to-ββ fe u οΌ β) + (ββ'-to-ββ fe v οΌ β)
I = llpo
(ββ'-to-ββ fe u)
(ββ'-to-ββ fe v)
(Ξ» (a , b) β ΞΌ (finite-gives-finite' fe u a ,
finite-gives-finite' fe v b))

II : type-of I β (u οΌ β') + (v οΌ β')
II (inl d) = inl (β-gives-β' fe u d)
II (inr e) = inr (β-gives-β' fe v e)

untruncated-ββ'-LLPO-gives-untruncated-ββ-LLPO : funextβ
β untruncated-ββ'-LLPO
β untruncated-ββ-LLPO
untruncated-ββ'-LLPO-gives-untruncated-ββ-LLPO fe llpo u v ΞΌ = II I
where
I : (ββ-to-ββ' fe u οΌ β') + (ββ-to-ββ' fe v οΌ β')
I = llpo
(ββ-to-ββ' fe u)
(ββ-to-ββ' fe v)
(Ξ» (a , b) β ΞΌ (finite'-gives-finite fe u a ,
finite'-gives-finite fe v b))

II : type-of I β (u οΌ β) + (v οΌ β)
II (inl d) = inl (β'-gives-β fe u d)
II (inr e) = inr (β'-gives-β fe v e)

untruncated-ββ-LLPO-gives-untruncated-LPO : funextβ
β untruncated-ββ-LLPO
β untruncated-LLPO
untruncated-ββ-LLPO-gives-untruncated-LPO fe unllpo =
untrucated-LLPO'-gives-untruncated-LLPO
(untruncated-ββ'-LLPO-gives-untruncated-LLPO' fe
(untruncated-ββ-LLPO-gives-untruncated-ββ'-LLPO fe unllpo))

untruncated-LLPO-gives-untruncated-ββ-LPO : funextβ
β untruncated-LLPO
β untruncated-ββ-LLPO
untruncated-LLPO-gives-untruncated-ββ-LPO fe ullpo =
untruncated-ββ'-LLPO-gives-untruncated-ββ-LLPO fe
(untruncated-LLPO'-gives-untruncated-ββ'-LLPO fe
(untrucated-LLPO-gives-untruncated-LLPO' ullpo))

\end{code}

The following result seems to be new (and I announced it years ago in
the constructivenews mailing list). The idea is to construct a
non-continuous function using untruncated LLPO, and then derive WLPO
from this. This proof was written here 15th November 2023, simplified
28th February 2023, for which we included the above ββ-versions of
LLPO and their equivalences.

\begin{code}

untruncated-ββ-LLPO-gives-WLPO : funextβ β untruncated-ββ-LLPO β WLPO
untruncated-ββ-LLPO-gives-WLPO fe llpo = wlpo
where
D : ββ β ββ β π€β Μ
D u v = (u οΌ β) + (v οΌ β)

Ο : (u v : ββ) β D u v β π
Ο u v (inl _) = β
Ο u v (inr _) = β

lβ : (u : ββ) β D u β
lβ u = llpo u β (Ξ» (_ , β-is-finite) β is-infinite-β β-is-finite)

lβ : (u : ββ) β D β u
lβ u = llpo β u (Ξ» (β-is-finite , _) β is-infinite-β β-is-finite)

l-β-agreement : lβ β οΌ lβ β
l-β-agreement = refl

fβ fβ : ββ β π
fβ u = Ο u β (lβ u)
fβ u = Ο β u (lβ u)

f-β-agreement : fβ β οΌ fβ β
f-β-agreement = refl

Οβ-property : (u : ββ) (d : D u β) β is-finite u β Ο u β d οΌ β
Οβ-property .β (inl refl) β-is-finite = π-elim (is-infinite-β β-is-finite)
Οβ-property u  (inr _)    _           = refl

Οβ-property : (u : ββ) (d : D β u) β is-finite u β Ο β u d οΌ β
Οβ-property u  (inl _)    _           = refl
Οβ-property .β (inr refl) β-is-finite = π-elim (is-infinite-β β-is-finite)

fβ-property : (u : ββ) β is-finite u β fβ u οΌ β
fβ-property u = Οβ-property u (lβ u)

fβ-property : (u : ββ) β is-finite u β fβ u οΌ β
fβ-property u = Οβ-property u (lβ u)

wlpoβ : fβ β οΌ β β WLPO
wlpoβ e = wlpo
where
gβ : ββ β π
gβ = complement β fβ

bβ : (n : β) β gβ (ΞΉ n) οΌ β
bβ n = ap complement (fβ-property (ΞΉ n) (β-to-ββ-is-finite n))

bβ : gβ β οΌ β
bβ = ap complement e

wlpo : WLPO
wlpo = basic-discontinuity-taboo fe gβ (bβ , bβ)

wlpoβ : fβ β οΌ β β WLPO
wlpoβ bβ = wlpo
where
bβ : (n : β) β fβ (ΞΉ n) οΌ β
bβ n = fβ-property (ΞΉ n) (β-to-ββ-is-finite n)

wlpo : WLPO
wlpo = basic-discontinuity-taboo fe fβ (bβ , bβ)

wlpo : WLPO
wlpo = Cases (π-possibilities (fβ β))
(Ξ» (a : fβ β οΌ β)
β wlpoβ a)
(Ξ» (b : fβ β οΌ β)
β Cases (π-possibilities (fβ β))
(Ξ» (c : fβ β οΌ β)
β π-elim (zero-is-not-one
(β    οΌβ¨ c β»ΒΉ β©
fβ β οΌβ¨ f-β-agreement β©
fβ β οΌβ¨ b β©
β    β)))
(Ξ» (d : fβ β οΌ β)
β wlpoβ d))

\end{code}

Added 27th Feb 2024. The converse also holds with a simpler proof, and
so there isn't any difference between WLPO and untruncated LLPO.

\begin{code}

WLPO-gives-untruncated-LLPO : WLPO-traditional β untruncated-LLPO
WLPO-gives-untruncated-LLPO wlpo Ξ± TΞ±-is-prop =
Cases (wlpo (complement β Ξ± β double))
(Ξ» (a : (n : β) β complement (Ξ± (double n)) οΌ β)
β inl (Ξ» n β complementβ (a n)))
(Ξ» (b : Β¬ ((n : β) β complement (Ξ± (double n)) οΌ β))
β inr (Ξ» n β π-equality-cases
(Ξ» (c : Ξ± (sdouble n) οΌ β)
β c)
(Ξ» (d : Ξ± (sdouble n) οΌ β)
β π-elim
(b (Ξ» m β ap
complement
(different-from-β-equal-β
(Ξ» (p : Ξ± (double m) οΌ β)
β double-is-not-sdouble
(index-uniqueness
Ξ±
TΞ±-is-prop
p
d))))))))
\end{code}

End of 27th Feb 2024 addition.

We now formulate (truncated) LLPO.

\begin{code}

module _ (pt : propositional-truncations-exist) where

open PropositionalTruncation pt

LLPO : π€β Μ
LLPO = (Ξ± : β β π)
β is-prop (Ξ£ n κ β , Ξ± n οΌ β)
β ((n : β) β Ξ± (double n) οΌ β) β¨ ((n : β) β Ξ± (sdouble n) οΌ β)

LLPO' : π€β Μ
LLPO' = (Ξ² Ξ³ : β β π)
β is-prop (T Ξ²)
β is-prop (T Ξ³)
β Β¬ (T Ξ² Γ T Ξ³) β Β¬ T Ξ² β¨ Β¬ T Ξ³

ββ-LLPO : π€β Μ
ββ-LLPO = (u v : ββ) β Β¬ (is-finite u Γ is-finite v) β (u οΌ β) β¨ (v οΌ β)

ββ-LLPO' : π€β Μ
ββ-LLPO' = (u v : ββ) β Β¬ ((u β  β) Γ (v β  β)) β (u οΌ β) β¨ (v οΌ β)

ββ'-LLPO : π€β Μ
ββ'-LLPO = (u v : ββ') β Β¬ (is-finite' u Γ is-finite' v) β (u οΌ β') β¨ (v οΌ β')

untruncated-LLPO-gives-LLPO : untruncated-LLPO β LLPO
untruncated-LLPO-gives-LLPO ullpo Ξ± i = β£ ullpo Ξ± i β£

\end{code}

TODO. Show that all these variants are equivalent.

LLPO doesn't imply WLPO (there are published refereces - find and
include them here). One example seems to Johnstone's topological
topos, but this is unpublished as far as I know.

Added 17th July 2024. There is a proof by Chris Grossack here:
https://grossack.site/2024/07/03/topological-topos-3-bonus-axioms