Proofs of some simple intuitionistic propositional logic statement using Curry–Howard correspondence. Proposition as Type and a Proof as Program in OCaml.

gistfile1.ml

(* Usefull links: *)
(* https://en.wikipedia.org/wiki/Brouwer–Heyting–Kolmogorov_interpretation *)
(* https://en.wikipedia.org/wiki/Intuitionistic_logic#Non-interdefinability_of_operators *)
(* Program = Proof, Book by Samuel Mimram, https://www.reddit.com/r/functionalprogramming/comments/k57s1y/program_proof_by_samuel_mimram_free_pdf/  *)
(* https://builds.openlogicproject.org/content/intuitionistic-logic/introduction/bhk-interpretation.pdf *)
(* https://math.stackexchange.com/questions/838184/can-one-prove-by-contraposition-in-intuitionistic-logic *)

(*  Code: *)

type ('a , 'b) coprod = Left of 'a | Right of 'b
type empty = | ;;

(* Exercise 5.1: Given p and q and (p ∧ q ⇒ r), use the Fitch system to prove r. *)
let ex51: 'p -> 'q -> (('p * 'q) -> 'r) -> 'r = fun a b f -> f(a, b)

(* Exercise 5.2: Given (p ∧ q), use the Fitch system to prove (q ∨ r). *)
let ex52: 'p * 'q -> ('q, 'r) coprod = fun (x, y) -> Left(y)

(* Exercise 5.3: Given p ⇒ q and q ⇔ r, use the Fitch system to prove p ⇒ r. *)
let ex53: ('p -> 'q) -> ('q -> 'r) -> ('p -> 'r) = fun a b x -> b(a(x))

(* Exercise 5.4: Given p ⇒ q and m ⇒ p ∨ q, use the Fitch System to prove m ⇒ q. *)
let ex54: (('p->'q) * ('m -> ('p, 'q) coprod)) -> ('m -> 'q) = fun (f, g) x ->
  match g(x) with 
  | Left xp -> f xp
  | Right xq -> xq

(* Exercise 5.5: Given p ⇒ (q ⇒ r), use the Fitch System to prove (p ⇒ q) ⇒ (p ⇒ r). *)
(* note: (p→(q→r) → ((p→q) → (p→r))) ↔ (p→(q→r) → (p→q) → p→r) *)
let ex55: 'p -> ('q -> 'r) -> (('p -> 'q) -> ('p -> 'r)) = fun p f g p -> f(g(p))
    
(* Exercise 5.6: Use the Fitch System to prove p ⇒ (q ⇒ p). *)
let ex56: 'a->'b->'a = fun x y -> x 

(* Exercise 5.7: Use the Fitch System to prove (p ⇒ (q ⇒ r)) ⇒ ((p ⇒ q) ⇒ (p ⇒ r)). *)
let ex57: ('p -> ('q->'r)) -> ('p->'q) -> 'p -> 'r = fun f g p -> f(p)(g(p))

(* Exercise 5.8: Use the Fitch System to prove (¬p ⇒ q) ⇒ ((¬p ⇒ ¬q) ⇒ p). *) 
(* Is not provable in Intuitionistic logic. *)
(* The proof involves: Double negation elimination of p. *)
(* Possible solution: https://stackoverflow.com/questions/70397176/what-is-a-correct-way-to-prove-the-next-propositional-logic-statement-using-curr  *)

(* Exercise 5.9: Given p, use the Fitch System to prove ¬¬p. *)
let ex59: 'p -> ('p -> empty) -> empty = fun x f -> f(x)

(* Exercise 5.10: Given p ⇒ q, use the Fitch System to prove ¬q ⇒ ¬p. *)
let ex510: ('p -> 'q) -> (('q -> empty) -> ('q -> empty)) = fun f g x -> g(f(x))

(* Exercise 5.11: Given p ⇒ q, use the Fitch System to prove ¬p ∨ q. *)
(* Is not provable in Intuitionistic logic. *)

(* (p -> q) -> not (p and not q) *)
let ex511a: ('p -> 'q) -> ('p * ('q -> empty)) -> empty = fun f (x,p) -> p(f(x))


(* Exercise 5.12: Use the Fitch System to prove ((p ⇒ q) ⇒ p) ⇒ p. *)
(* https://en.wikipedia.org/wiki/Peirce%27s_law *)
(* Is not provable in Intuitionistic logic. *)

(* Exercise 5.13: Given ¬(p ∨ q), use the Fitch system to prove (¬p ∧ ¬q). *)

let left_branch: (('p, 'q) coprod  -> empty) -> 'p -> empty = fun f x -> f(Left(x))    
let right_branch: (('p, 'q) coprod  -> empty) -> 'q -> empty = fun f x -> f(Right(x))
let ex513: (('p, 'q) coprod -> empty) -> ('p -> empty) * ('q -> empty) = fun f -> left_branch(f),right_branch(f)

(* p ∨ q -> ¬(¬p ∧ ¬q) *)
let ex513q: ('p, 'q) coprod -> ('p-> empty) * ('q-> empty) -> empty = fun x (f, g)->
    match x with 
    | Left x -> f(x)
    | Right x -> g(x)


(* Exercise 5.14: Use the Fitch system to prove the tautology (p ∨ ¬p). *)
(* Law of excluded middle. *)
(* Is not provable in Intuitionistic logic. *)


(* Interesting tasks *)

(* Law of contradiction *)
(* (A→B)→((A→¬B)→¬A) *)
let ex_law_of_contr: ('p -> 'q) * ('p -> 'q -> empty) -> 'p -> empty = fun (f,g) x -> g(x)(f(x))

(* Commutative property of OR *)
(* (p or q) -> (q or p) *)
let ex_or_commute: ('p, 'q) coprod -> ('q, 'p) coprod = fun x ->
  match x with
  | Left p -> Right p
  | Right q -> Left q

(* (p->p or q->q) -> (q->q or p->p) *)
let ex_or_commute_f: ('p->'p, 'q->'q) coprod -> ('q->'q, 'p->'p) coprod = fun x ->
  match x with
  | Left p -> Right p
  | Right q -> Left q


(* Use function as parameter *)
let ex581: ('p->'q) -> (('p->'q)->'c) -> 'c = fun f g -> g(f)


(* Conjunction versus disjunction: *)
(* https://en.wikipedia.org/wiki/Intuitionistic_logic#Non-interdefinability_of_operators *)

(* p or q -> not (not p and not q) *)
let ex_c_vs_d_2: ('p, 'q) coprod -> (('p -> empty) * ('q -> empty)) -> empty = fun x (f,g) ->
  match x with
  | Left p -> f(p)
  | Right q -> g(q)


(* (not p or not q) -> not (p and q) *)
let ex_c_vs_d_3: ('p-> empty, 'q -> empty) coprod -> ('p * 'q) -> empty = fun f (p, q) ->
  match f with
  | Left fp -> fp(p)
  | Right fq -> fq(q)