Martin Escardo 2011.


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

module Omniscience where

open import SetsAndFunctions
open import CurryHoward
open import Equality
open import Two

omniscient : Set  Prp
omniscient X = ∀(p : X  )  ( \(x : X)  p x  )  (∀(x : X)  p x  )

open import Naturals

LPO : Prp
LPO = omniscient 


Notice that LPO is Bishop's limited principle of
omniscience, which is a taboo, in Aczel's terminology. The
negation of LPO is false, but LPO is not provable, and hence
LPO is independent. In classical mathematics it is
uncomfortable to have independent propositions, but of
course unavoidable. Independence occurs often in
constructive mathematics, particular in classically
compatible constructive mathematics, like Bishop's
methamatics and Martin-Löf type theory (in its various
flavours); even the principle of excluded middle is
independent: it cannot be proved, but its negation is false.

We'll see that the infinite set ℕ∞ defined in the module
ConvergentSequence is omniscient.

If a set X is omniscient and a set Y has is has decidable
equality, then the function space (X → Y) has decidable
equality, if we assume extensionality. In our topological
correspondence, decidable equality is called discreteness.
More generally we have:


open import DiscreteAndSeparated
open import DecidableAndDetachable

apart-or-equal : {X : Set}  {Y : X  Set} 

   omniscient X  (∀(x : X)  discrete(Y x))
     ∀(f g : (x : X)  Y x)  f  g  f  g

apart-or-equal {X} {Y} φ d f g = lemma₂ lemma₁
  open import Extensionality

  claim :  x  f x  g x    f x  g x
  claim x = ∨-commutative(d x (f x) (g x))

  lemma₀ :  \p   x  (p x    f x  g x)  (p x    f x  g x)
  lemma₀ = indicator claim

  p : X  
  p = ∃-witness lemma₀

  lemma₁ : ( \x  p x  )  (∀(x : X)  p x  )
  lemma₁ = φ p

  lemma₂ : ( \x  p x  )  (∀(x : X)  p x  )  f  g    f  g
  lemma₂(in₀(x , r)) = in₀(∃-intro x(∧-elim₀(∃-elim lemma₀ x) r))
  lemma₂(in₁ h) =
   in₁(funext((λ x  ∧-elim₁(∃-elim lemma₀ x) (h x))))

omniscient-discrete-discrete : {X : Set}  {Y : X  Set} 

   omniscient X  (∀(x : X)  discrete(Y x))  discrete((x : X)  Y x)

omniscient-discrete-discrete {X} {Y} φ d f g = h(apart-or-equal φ d f g)
  h : f  g  f  g  f  g  f  g
  h(in₀ a) = in₁(apart-is-different a)
  h(in₁ r) = in₀ r

omniscient-discrete-discrete' : {X Y : Set}  omniscient X  discrete Y  discrete(X  Y)
omniscient-discrete-discrete' {X} {Y} φ d =
  omniscient-discrete-discrete {X}  x  Y} φ  x  d)