Martín Escardó, 31 March 2016, updated 1st April 2016.

Dummett disjunction in Martin-Lӧf Type Theory.

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 in Agda notation. (A
motivation coming from univalent type theory is also discussed.)

\begin{code}

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

module Various.DummettDisjunction where

open import MLTT.Spartan

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

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

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

\end{code}

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

\begin{code}

weaker-than-intuitionistic : (P Q : Type) → 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

\end{code}

and strengthens classical disjunction:

\begin{code}

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

\end{code}

Dummett's linearity axiom for implication,

\begin{code}

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

\end{code}

makes Dummett disjunction logically equivalent to _+_:

\begin{code}

equivalent-to-intuitionistic : (P Q : Type) → 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)

\end{code}

We may wish to reformulate the above as follows:

\begin{code}

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

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

\end{code}

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:

\begin{code}

dl : (P Q : Type) → is-decidable P → linearity-axiom P Q
dl P Q (inl p) = inr (λ _ → p)
dl P Q (inr u) = inl (λ p → 𝟘-elim (u p))

\end{code}

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:

\begin{code}

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

\end{code}

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

\begin{code}

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

\end{code}

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:

\begin{code}

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

\end{code}

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

\begin{code}

skolem : (A B C : Type) → (A → B ⊞ C) → (A → B) ⊞ (A → C)
skolem A B C h = (λ f a → pr₁ (h a) (λ b → f (λ _ → b) a)) ,
                 (λ g a → pr₂ (h a) (λ c → g (λ _ → c) a))

dummett : (A B C : Type) → (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)

\end{code}

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:

\begin{code}

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

⊞-wem : (P Q : Type) → ¬ P ⊞ ¬¬ P
⊞-wem P Q = ⊞-wem' P 𝟘

\end{code}

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

\begin{code}

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

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

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

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

\end{code}

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

\begin{code}

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

PL : Type₁
PL = (P Q : Type) → 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 (λ _ → 𝟘-elim (u p))))

Curry-Howard-EM : Type₁
Curry-Howard-EM = (P : Type) → P + ¬ P

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

\end{code}

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

\begin{code}

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

\end{code}

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:

\begin{code}

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

\end{code}

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

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

I came across this as follows.

In univalent foundations, the propositional of a type X can be defined as

   ∥ X ∥ = (P : 𝓤) → is-prop P → (X → P) → P.

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

(If X lives in a universe 𝓤 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 propositional
truncation that preserves the universe level, by working with a family
of propositions P : I → U with I : 𝓤:

  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 get 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:

\begin{code}

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

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

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

⊕-weaker-than-intuitionistic : (P Q : Type) → 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 : Type) → P ⊕ Q → ¬ (¬ P × ¬ Q)
⊕-stronger-than-classical P Q = more-generally 𝟘 𝟘-elim
  where
    more-generally : (R : Type) → (R → Q) → P ⊕ Q → ((P → R) × (Q → R)) → R
    more-generally R e γ (u , v) = v (γ (λ p → e (u p)))

\end{code}

Right excluded middle just holds for this notion of disjunction:

\begin{code}

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

\end{code}

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

Notice that this doesn't use 𝟘-elim:

\begin{code}

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

\end{code}

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

\begin{code}

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

\end{code}

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

\begin{code}

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

\end{code}

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

\begin{code}

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

Curry-Howard-EM-gives-agreement : Curry-Howard-EM → (P Q : Type) → P ⊕ Q → P + Q
Curry-Howard-EM-gives-agreement em P Q = more-generally P Q (em P)
 where
  more-generally : (P Q : Type) → is-decidable P → P ⊕ Q → P + Q
  more-generally P Q (inl p) φ = inl p
  more-generally P Q (inr u) φ = inr (φ (λ p → 𝟘-elim (u p)))

\end{code}

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

\begin{code}

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

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

\end{code}

We also have, of course:

\begin{code}

equivalent-to-classical : Curry-Howard-EM → (P Q : Type) → ¬ (¬ P × ¬ Q) → P ⊕ Q
equivalent-to-classical em P Q = more-generally P Q (em P) (em Q)
 where
  more-generally : (P Q : Type) → is-decidable P → is-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 = 𝟘-elim (v ((λ p → q (w p)) , q))

\end{code}

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

\begin{code}

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

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

\end{code}

Added April 2016:

We can apply the same idea to the existential quantifier.

Given a family of propositions P : X → Type, 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:

\begin{code}

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

\end{code}

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:

\begin{code}

D-stronger-than-classical : {X : Type} (P : X → Type) → ¬¬ X → D P → ¬ (∀ x → ¬ P x)
D-stronger-than-classical P ne d u = ne (λ i → u i (d i (λ x p → 𝟘-elim (u x p))))

\end{code}

More slowly:

\begin{code}
 where
  a : ∀ i x → P x → P i
  a i x p = 𝟘-elim (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 : Type} (P : X → Type) → D (λ i → D (λ x → P i → P x))
D-lin P i _ _ f = f i (λ p → p)

\end{code}