A question about intuitionistic logic

[Andrej Bauer]

We work in intuitionistic logic, and let H be the complete Heyting
altebra of truth values.

Given a truth value r, define the "continuation monad"

cont_r : H → H
cont_r(p) := ((p ⇒ r) ⇒ r)

What, if anything, can be said about those r for which it is valid that

∀ p ∈ H . cont_r(cont_r(p) ⇒ p)

or spelled out:

∀ p ∈ H . ((((p ⇒ r) ⇒ r) ⇒ p) ⇒ r) ⇒ r ?

If r is True or False then it holds. But is that all?

By an observation of Todd Wilson from a while ago (on the categories
list), the condition is equivalent to:

∀ p, q ∈ H . (p ⇒ cont_r(q)) ⇒ cont_r (p ⇒ q)

And the reverse implication always holds.

With kind regards,

Andrej

[Andrew Polonsky]

Dear Andrej,

The following should answer your question.

PROPOSITION. Let r ∈ H. TFAE:
- ∀ p ∈ H . cont_r(cont_r(p) ⇒ p).
- r is ¬¬-closed.

NOTATION. Given p ∈ H, put
p^rr := (p->r)->r,
Cr(p) := (p^rr ->p)^rr.

Notice that your condition is ∀ p ∈ H. Cr(p).

The proof is in three steps.

LEMMA 1. p ≤ q => Cr(p) ≤ Cr(q).

LEMMA 2. ∀ p ∈ H. Cr(p) <=> Cr(⊥).

LEMMA 3. Cr(⊥) <=> (¬¬r -> r).

The proofs are given in the attached Agda file.

Cheers,
Andrew

> --
> You received this message because you are subscribed to the Google Groups "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.