What is a correct way to prove the next propositional logic statement using Curry–Howard correspondence?

Question

I am studying Curry–Howard correspondence.

Given propositional logic statement: (¬p -> q) -> ((¬p -> ¬q) -> p).

I need to define a type (as proposition) and a function (as a proof) in OCaml.

I came up with the next code and stuck:

type empty = | ;; 
let ex58: (('p->empty) -> 'q) -> (('p->empty) -> ('q->empty)) -> 'p = fun f g -> g(f)

Error:

This expression has type ('p -> empty) -> 'q but an expression was expected of type 'p -> empty.

Answer 1

When working on this exercise, it will probably easier to start with introducing a type constructor for not:

type empty = |
type 'a not = 'a -> empty

then use an explicit universal quantification to rewrite the exercise:

let proof_by_contradiction: type p q. (p not -> q) -> (p not -> q not) -> p =
   ...

which should improve slightly error messages

Error: This expression has type p not -> q but an expression was expected of type p not = p -> empty

Before diving into this exercise, it might be useful to try your hand at

let proof_by_negation:  type p q. (p -> q) -> (p -> q not) -> p not =
  ...

first.

Answer 2

I'm pretty sure that it's not constructively provable.

First, note that

¬¬p -> (¬p -> a)

holds for completely arbitrary p and a (from ¬¬p and ¬p you first obtain proof of falsehood, then by ex falso quodlibet you obtain any a).

In particular, for any q,

    ¬¬p -> ((¬p -> q) /\ (¬p -> ¬q))             // ("lemma")

holds (apply previous statement to a = q and a = ¬q).

Now, if your original statement ((¬p -> q) /\ (¬p -> ¬q)) -> p were true, then you could precompose ¬¬p -> ((¬p -> q) /\ (¬p -> ¬q)), hence obtaining ¬¬p -> p. But this is double negation elimination, which is known to not be provable constructively.

Here is the full construction in Scala 3 (somewhat close-ish-ly related to OCaml; The subset of the language used here should be easily translatable to OCaml):

type ¬[A] = A => Nothing                               // negation
type /\[A, B] = (A, B)                                 // conjunction / product
type Claim[P, Q] = (¬[P] => Q) => (¬[P] => ¬[Q]) => P  // your claim
type DoubleNegationElimination[P] = ¬[¬[P]] => P

/** Ex falso quodlibet. */
def efq[X]: Nothing => X = f => f

/** Lemma, as explained above. */
def lemma[P, Q](a: ¬[¬[P]]): (¬[P] => Q) /\ (¬[P] => ¬[Q]) =
  val left: ¬[P] => Q = notP => efq(a(notP))
  val right: ¬[P] => ¬[Q] = notP => efq(a(notP))
  (left, right)

/** This shows that if you could prove your claim for any `P`, `Q`,
  * then you would also be able to prove double negation elimination
  * for `P`.
  */
def claimImpliesDoubleNegationElimination[P, Q](
  c: Claim[P, Q]
): DoubleNegationElimination[P] =
  notNotP => {
    val (left, right) = lemma[P, Q](notNotP)
    c(left)(right)
  }

/** This is an (incomplete, because impossible) proof of the double
  * negation elimination for any `P`. It is incomplete, because it
  * relies on the validity of your original claim.
  */
def doubleNegationElimination[P]: DoubleNegationElimination[P] =
  claimImpliesDoubleNegationElimination(claim[P, Unit])

/** There cannot be a constructive proof of this, because otherwise
  * we would obtain a constructive proof of `doubleNegationElimination`.
  */
def claim[P, Q]: Claim[P, Q] = ???