-- Dummett disjunction in Martin-Lӧf Type Theory
--
-- (This file is in Martin-Lӧf Type Theory in Agda notation.)
--
-- Martín Escardó, 31 March 2016, updated 1st April 2016.
-- Last updated 6 Sep 2016 with the addition of weak Dummet disjunction.
--
-- We consider the behaviour of what we call "Dummett disjunction" in
-- intuitionistic logic in its MLTT rendering. (A motivation coming
-- from univalent type theory is discussed at the end.)

-- Curry-Howard conjunction:

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

outl : {A B : Set} → A × B → A
outl (a , b) = a

outr : {A B : Set} → A × B → B
outr (a , b) = b

-- Curry-Howard disjunction. 

data _+_ (A B : Set) : Set where
  inl : A → A + B
  inr : B → A + B

-- NB. We could instead work with HoTT disjunction of -1-types, to get
-- the same results. By the way, here "equivalent" means logically
-- equivalent (there are implications both ways).

-- Curry-Howard falsum (empty type):

data 𝟘 : Set where

efq : (P : Set) → 𝟘 → P
efq P ()

¬ : Set → Set
¬ P = P → 𝟘

-- We refer to the following as Dummett disjunction in intuitionistic
-- logic (see below for a justification):

_⊞_ : Set → Set → Set
P ⊞ Q = ((P → Q) → Q) × ((Q → P) → P)

inL : (P Q : Set) → P → P ⊞ Q
inL P Q p = (λ u → u p) , (λ _ → p)

inR : (P Q : Set) → Q → P ⊞ Q
inR P Q q = (λ _ → q) , (λ v → v q)

-- Dummett disjunction _⊞_ weakens intuitionistic disjunction _+_:

weaker-than-intuitionistic : (P Q : Set) → P + Q → P ⊞ Q
weaker-than-intuitionistic P Q (inl p) = inL P Q p
weaker-than-intuitionistic P Q (inr q) = inR P Q q

-- and strengthens classical disjunction:

stronger-than-classical : (P Q : Set) → P ⊞ Q → ¬(¬ P × ¬ Q)
stronger-than-classical P Q = more-generally 𝟘 (efq P)
  where
    more-generally : (R : Set) → (R → P) → P ⊞ Q → ((P → R) × (Q → R)) → R
    more-generally R e (_ , γ) (u , v) = u (γ (λ q → e (v q)))

-- Dummett's linearity axiom for implication,

linearity-axiom : Set → Set → Set
linearity-axiom P Q = (P → Q) + (Q → P)

-- makes Dummett disjunction logically equivalent to _+_:

equivalent-to-intuitionistic : (P Q : Set) → linearity-axiom P Q → P ⊞ Q → P + Q
equivalent-to-intuitionistic P Q (inl u) (φ , _) = inr (φ u)
equivalent-to-intuitionistic P Q (inr v) (_ , γ) = inl (γ v)

-- We may wish to reformulate the above as follows:

LA : Set₁
LA = (P Q : Set) → linearity-axiom P Q

LA-gives-agreement : LA → (P Q : Set) → P ⊞ Q → P + Q
LA-gives-agreement la P Q = equivalent-to-intuitionistic P Q (la P Q)

-- In other words, in Gӧdel-Dummett logic, disjunction is definable
-- from conjunction and implication as _⊞_ (M. Dummett, A
-- propositional calculus with denumerable matrix, Journal of Symbolic
-- Logic, Vol. 24, No. 2, pp. 97-106, 1959).

-- It is also well known, and obvious, that linearity just holds if
-- one of the propositions is decidable:

decidable : Set → Set
decidable P = P + ¬ P

dl : (P Q : Set) → decidable P → linearity-axiom P Q
dl P Q (inl p) = inr (λ _ → p)
dl P Q (inr u) = inl (λ p → efq Q (u p))

-- Hence if we assume excluded middle (all propositions are
-- decidable), Dummett disjunction agrees with (intuitionistic
-- and classical) disjunction.
--
-- More generally, without assuming excluded middle, if one of the
-- propositions is decidable, then P ⊞ Q and P + Q are equivalent:

classical-logic-gives-agreement : (P Q : Set) → decidable P → P ⊞ Q → P + Q
classical-logic-gives-agreement P Q dp = equivalent-to-intuitionistic P Q (dl P Q dp)

-- The linearity axiom just holds, in intuitionistic logic, for all
-- propositions, if we formulate it with Dummett disjunction rather
-- than intuitionistic disjunction:

⊞-linearity : (P Q : Set) → (P → Q) ⊞ (Q → P)
⊞-linearity P Q = (λ φ q → φ (λ _ → q) q) , (λ γ p → γ (λ _ → p) p)

-- I don't know whether this has already been observed. It must have been.

-- Therefore we also get that if Dummett disjunction _⊞_ is equivalent
-- to _+_ in intuitionistic logic, then the linearity axiom must hold:

agreement-gives-LA : ((P Q : Set) → P ⊞ Q → P + Q) → LA
agreement-gives-LA f P Q = f (P → Q) (Q → P) (⊞-linearity P Q)

-- And I don't know either whether this is known. It probably is.

-- The following is adapted from
-- http://www.jstor.org/stable/20016490?seq=2#page_scan_tab_contents
-- page 154, replacing disjunction by Dummett disjunction.
--
-- Jan von Plato, Skolem's Discovery of Gödel-Dummett Logic.
-- Studia Logica: An International Journal for Symbolic Logic
-- Vol. 73, No. 1, Constructivism in Non-Classical Logics and Computer
-- Science (Feb., 2003), pp. 153-157

skolem : (A B C : Set) → (A → B ⊞ C) → (A → B) ⊞ (A → C)
skolem A B C h = (λ f a → outl(h a) (λ b → f (λ _ → b) a)) ,
                 (λ g a → outr(h a) (λ c → g (λ _ → c) a))

dummett : (A B C : Set) → (A × B → C) → (A → C) ⊞ (B → C)
dummett A B C h = (λ f b → f (λ a → h (a , b)) b) ,
                  (λ g a → g (λ b → h (a , b)) a)

-- The point is that we don't use the linearity axiom for implication
-- to prove the above, by weakening disjunction to Dummett
-- disjunction.

-- Dummett also has weak excluded middle ¬P ∨ ¬¬P in his logic. This
-- again holds in intuitionistic logic if we replace disjunction by
-- Dummett disjunction. Because the proof doesn't use efq, as noted by
-- Dummett, we have, more generally, with 𝟘 generalized to any
-- proposition Q:

⊞-wem : (P Q : Set) → (P → Q) ⊞ ((P → Q) → Q)
⊞-wem P Q = (λ f g → f g g) , (λ f p → f (λ g → g p) p)

-- What about excluded middle? Peirce's Law arises directly.

Peirce's-Law : Set → Set → Set
Peirce's-Law P Q = ((P → Q) → P) → P

PL₀ : Set₁
PL₀ = (P : Set) → Peirce's-Law P 𝟘

⊞-EM : Set₁
⊞-EM = (P : Set) → P ⊞ ¬ P

⊞-EM-gives-PL₀ : ⊞-EM → PL₀
⊞-EM-gives-PL₀ dem P = more-generally 𝟘 (dem P)
 where
  more-generally : (Q : Set) → P ⊞ (P → Q) → Peirce's-Law P Q
  more-generally Q (_ , γ)= γ

-- The converse holds, but we don't need it:

PL₀-gives-⊞-EM : PL₀ → ⊞-EM
PL₀-gives-⊞-EM pl₀ P = more-generally 𝟘 (pl₀ P)
 where
  more-generally : (Q : Set) → Peirce's-Law P Q → P ⊞ (P → Q)
  more-generally Q pl = (λ f p → f p p) , pl

PL : Set₁
PL = (P Q : Set) → Peirce's-Law P Q

PL-gives-PL₀ : PL → PL₀
PL-gives-PL₀ pl P = pl P 𝟘

PL₀-gives-PL : PL₀ → PL
PL₀-gives-PL pl₀ P Q ε = pl₀ P (λ u → ε (λ p → pl₀ Q (λ _ → efq Q (u p))))

EM : Set₁
EM = (P : Set) → P + ¬ P

PL-gives-EM : PL → EM
PL-gives-EM pl P = pl (P + ¬ P) P (λ f → inl (pl P 𝟘 (λ g → f (inr g))))

-- The converse of course holds, but again we don't need it:

EM-gives-PL : EM → PL
EM-gives-PL em P Q ε = f (em P)
  where
    f : P + ¬ P → P
    f (inl p) = p
    f (inr u) = efq P (u (ε (λ p → efq Q (u p))))

-- Hence although weak excluded middle formulated with Dummett
-- disjunction just holds, we have that excluded middle formulated
-- with Dummett or Curry-Howard disjunction are logically equivalent:

⊞-EM-gives-EM : ⊞-EM → EM
⊞-EM-gives-EM dem = PL-gives-EM (PL₀-gives-PL (⊞-EM-gives-PL₀ dem))

-- Also, the above shows that Peirce's Law is equivalent to 
-- (P Q : Set) → P ⊞ (P → Q).


{-

I hadn't looked at Gӧdel-Dummett logic before.

I came across this as follows.

In univalent foundations, the -1-truncation of a type X can be defined as

   ∥ X ∥ = (P : U) → is--1-type P → (X → P) → P.

A -1-type (or a subsingleton) is a type whose elements are all equal
in the sense of the identity type.

(If X lives in a universe U then ∥ X ∥ lives in the next universe.)

Then disjunction, of -1-types, is defined by

   P ∨ Q = ∥ P + Q ∥.

One can consider a variation of the definition of -1-truncation that
preserves the universe level, by working with a family of -1-types
P : I → U with I:U:

  J X = (i : I) → (X → P i) → P i.

(Cf. Aczel, "The Russell–Prawitz modality", Mathematical Structures in
Computer Science archive Volume 11 Issue 4, August 2001 Pages 541-554.)

Now, Dummett disjunction arises as

  P ⊞ Q = J(P + Q)

for the choice of I as the two-point type (the booleans) with one
point mapped to P and the other to Q.

I wondered what we got in this case, and the answer was Dummett
disjunction. But notice that you won't find "Dummett disjunction" in
the literature. What Dummett proved was that in his (intermediate)
logic, disjunction P‌‌∨Q agrees with ((P → Q) → Q) ∧ ((Q → P) → P), and
hence is definable from implication and conjunction.

Here, instead, we have considered the behaviour of what we call
Dummett disjunction in intuitionistic logic.

-}

-- Added 6 Sep 2016. Weak Dummet disjunction.
--
-- We can decompose P ⊞ Q as (P ⊕ Q) × (Q ⊕ P) in the obvious way.

-- Weak Dummet disjunction:

_⊕_ : Set → Set → Set
P ⊕ Q = (P → Q) → Q

⊕-inL : (P Q : Set) → P → P ⊕ Q
⊕-inL P Q p = λ u → u p

⊕-inR : (P Q : Set) → Q → P ⊕ Q
⊕-inR P Q q = λ _ → q

⊕-weaker-than-intuitionistic : (P Q : Set) → P + Q → P ⊕ Q
⊕-weaker-than-intuitionistic P Q (inl p) = ⊕-inL P Q p
⊕-weaker-than-intuitionistic P Q (inr q) = ⊕-inR P Q q

⊕-stronger-than-classical : (P Q : Set) → P ⊕ Q → ¬(¬ P × ¬ Q)
⊕-stronger-than-classical P Q = more-generally 𝟘 (efq Q)
  where
    more-generally : (R : Set) → (R → Q) → P ⊕ Q → ((P → R) × (Q → R)) → R
    more-generally R e γ (u , v) = v (γ (λ p → e (u p)))

-- Right excluded middle just holds for this notion of disjunction:

⊕-em-right : (P : Set) → P ⊕ ¬ P
⊕-em-right P = λ u p → u p p

-- But the lack of commutativity shows here: left ⊕-excluded middle is
-- equivalent to excluded middle.

-- Notice that this doesn't use efq:

⊕-EM-left-gives-EM : ((P : Set) → ¬ P ⊕ P) → EM
⊕-EM-left-gives-EM e P = e (P + ¬ P) (λ φ → inr (λ p → φ (inl p)))

-- Notice also that ¬ P ⊕ P is (¬ P → P) → P, which is a particular
-- case of Peirce's Law with an empty type.

EM-gives-⊕-EM-left : EM → (P : Set) → ¬ P ⊕ P
EM-gives-⊕-EM-left em P = more-generally P (em P)
 where
  more-generally : (P : Set) → decidable P → ¬ P ⊕ P
  more-generally P (inl p) = λ φ → p
  more-generally P (inr u) = λ φ → φ u

-- Notice, however, that we do have weak excluded middle for our
-- asymetric notion of disjunction, on both sides, but we already know
-- the right case:

⊕-wem-left : (P : Set) → ¬(¬ P) ⊕ ¬ P
⊕-wem-left P = λ φ p → φ (λ u → u p) p

-- Curry-Howard disjunction agrees with weak Dummet disjunction iff
-- excluded middle holds:

agreement-gives-EM : ((P Q : Set) → P ⊕ Q → P + Q) → EM
agreement-gives-EM f P = f P (¬ P) (⊕-em-right P)

EM-gives-agreement : EM → (P Q : Set) → P ⊕ Q → P + Q
EM-gives-agreement em P Q = more-generally P Q (em P)
 where
  more-generally : (P Q : Set) → decidable P → P ⊕ Q → P + Q
  more-generally P Q (inl p) φ = inl p
  more-generally P Q (inr u) φ = inr (φ (λ p → efq Q (u p)))

-- Interestingly, also the commutativity of ⊕ is equivalent to excluded middle:

⊕-commutative : Set₁
⊕-commutative = (P Q : Set) → P ⊕ Q → Q ⊕ P

⊕-commutative-gives-EM : ⊕-commutative → EM
⊕-commutative-gives-EM c P = c (P + ¬ P) (¬ P) (λ φ p → φ (inl {P} {¬ P} p) p) (inr {P} {¬ P})

-- We also have, of course:

equivalent-to-classical : EM → (P Q : Set) → ¬(¬ P × ¬ Q) → P ⊕ Q
equivalent-to-classical em P Q = more-generally P Q (em P) (em Q)
 where
  more-generally : (P Q : Set) → decidable P → decidable Q → ¬(¬ P × ¬ Q) → P ⊕ Q
  more-generally P Q (inl p) e v w = w p
  more-generally P Q (inr p) (inl q) v w = q
  more-generally P Q (inr p) (inr q) v w = efq Q (v ((λ p → q (w p)) , q))

-- The Skolem and Dummet properties also hold for our weakened notion
-- of Dummet disjunction:

⊕-skolem : (A B C : Set) → (A → B ⊕ C) → (A → B) ⊕ (A → C)
⊕-skolem A B C h = λ φ a → h a (λ b → φ (λ _ → b) a)

⊕-dummett : (A B C : Set) → (A × B → C) → (A → C) ⊕ (B → C)
⊕-dummett A B C h = λ φ b → φ (λ a → h (a , b)) b

{-

Added April 2016:

We can apply the same idea to the existential quantifier.

Given a family of propositions P : X → Set, we consider

   (i : X) → ((Σ(x:X).P x) → P i) → P i

which is equivalent to

   (i : X) → ((x : X) → P x → P i) → P i

-}

-- A Dummet existential quantifier:

D : {X : Set} (P : X → Set) → Set
D P = ∀ i → (∀ x → P x → P i) → P i

-- If X is empty then D P holds, but ¬(∀ x → ¬(P x)) fails 
-- because ∀ x → ¬(P x) holds vacuously.  However D strengthens the
-- classical existential quantifier for X non-empty:

D-stronger-than-classical : {X : Set} (P : X → Set) → ¬(¬ X) → D P → ¬(∀ x → ¬(P x))
D-stronger-than-classical P ne d u = ne (λ i → u i (d i (λ x p → efq (P i) (u x p))))
 where
  -- More slowly:
  a : ∀ i x → P x → P i
  a i x p = efq (P i) (u x p)
  b : ∀ i → P i
  b i = d i (a i)
  c : ∀ i → 𝟘
  c i = u i (b i)
  g : 𝟘
  g = ne c

D-lin : {X : Set} (P : X → Set) → D \i → D \x → P i → P x
D-lin P i _ _ f = f i (λ p → p)