Theory System_W

(*
   Authors: Asta Halkjær From & Jørgen Villadsen, DTU Compute
*)

chapter ‹Formalizing Wajsberg's Axioms for Propositional Logic›

theory System_W imports Main begin

text ‹All references are to Alonzo Church (1956): Introduction to Mathematical Logic›

section ‹Syntax / Axiomatics / Semantics›

datatype form = Falsity (‹⊥›) | Pro nat | Imp form form (infix ‹→› 0)

text ‹Wajsberg 1937 building on work by Frege, Tarski and Bernays [Church page 159]›

inductive Axiomatics (‹⊢›) where
  ‹⊢ q› if ‹⊢ p› and ‹⊢ (p → q)› |
  ‹⊢ (p → (q → p))› |
  ‹⊢ ((p → q) → ((q → r) → (p → r)))› |
  ‹⊢ (((p → q) → p) → p)› |
  ‹⊢ (⊥ → p)›

abbreviation Truth (‹⊤›) where ‹⊤ ≡ (⊥ → ⊥)›

theorem ‹⊢ ⊤› using Axiomatics.intros(5) .

primrec semantics (infix ‹⊨› 0) where
  ‹(I ⊨ ⊥) = False› |
  ‹(I ⊨ (Pro n)) = I n› |
  ‹(I ⊨ (p → q)) = (if I ⊨ p then I ⊨ q else True)›

theorem ‹I ⊨ p› if ‹⊢ p› using that by induct auto

definition ‹valid p ≡ ∀I. (I ⊨ p)›

theorem ‹valid p = ⊢ p› oops ― ‹Proof at end›

abbreviation (input) ‹Neg p ≡ (p → ⊥)›

lemmas MP = Axiomatics.intros(1)
lemmas Imp1 = Axiomatics.intros(2)
lemmas Tran = Axiomatics.intros(3)
lemmas Clas = Axiomatics.intros(4)
lemmas Expl = Axiomatics.intros(5)

section ‹Soundness›

theorem soundness: ‹⊢ p ⟹ I ⊨ p›
  by (induct rule: Axiomatics.induct) auto

section ‹Derived Rules›

lemma Chu1: ‹⊢ ((p → (p → q)) → (p → q))›
  by (meson Tran Clas MP)

lemma Chu2: ‹⊢ (p → ((p → q) → q))›
  by (meson Chu1 Imp1 Tran MP)

lemma Chu3: ‹⊢ ((p → (q → r)) → (q → (p → r)))›
  by (meson Chu2 Tran MP)

lemma Chu4: ‹⊢ ((q → r) → ((p → q) → (p → r)))›
  by (meson Chu3 Tran MP)

lemma Imp2: ‹⊢ ((p → (q → r)) → ((p → q) → (p → r)))›
  by (meson Chu4 Chu1 Chu3 MP)

lemma Imp3: ‹⊢ (p → p)›
  by (meson Imp1 Tran Clas MP)

lemma Neg: ‹⊢ (((p → ⊥) → ⊥) → p)›
  by (meson Chu4 Clas Expl MP)

text ‹Wajsberg 1939 building on work by Frege [Church page 163]›

inductive FW (‹⊩›) where
  ‹⊩ q› if ‹⊩ p› and ‹⊩ (p → q)› |
  ‹⊩ (p → (q → p))› |
  ‹⊩ ((p → (q → r)) → ((p → q) → (p → r)))› |
  ‹⊩ (((p → ⊥) → ⊥) → p)›

theorem Axiomatics_FW: ‹⊢ p ⟷ ⊩ p›
proof
  have *: ‹⊩ ((p → q) → ((q → r) → (p → r)))› for p q r
    by (metis FW.intros(1-3))
  then have **: ‹⊩ (((p → q) → p) → p)› for p q
    by (metis FW.intros(1-4))
  show ‹⊢ p› if ‹⊩ p›
    using that by induct (use Imp1 Imp2 Neg Axiomatics.intros in meson)+
  show ‹⊩ p› if ‹⊢ p›
    using that by induct (use * ** FW.intros in meson)+
qed

lemma Neg1: ‹⊢ (p → (Neg p → q))›
  by (meson Chu3 Chu4 Expl MP)

lemma Neg2: ‹⊢ (Neg (p → q) → p)›
  by (metis Neg1 Tran MP Neg)

lemma Neg3: ‹⊢ (Neg (p → q) → Neg q)›
  by (metis Imp1 Tran MP)

primrec imply :: ‹form list ⇒ form ⇒ form› where
  ‹imply [] q = q›
| ‹imply (p # ps) q = (p → imply ps q)›

lemma imply_head: ‹⊢ (imply (p # ps) p)›
  by (induct ps) (simp add: Imp3, metis Imp1 Imp2 MP imply.simps(2))

lemma imply_Cons: ‹⊢ (imply ps q) ⟹ ⊢ (imply (p # ps) q)›
  by (metis Imp1 MP imply.simps(2))

lemma imply_mem: ‹p ∈ set ps ⟹ ⊢ (imply ps p)›
  using imply_head imply_Cons by (induct ps) auto

lemma imply_MP: ‹⊢ (imply ps p → (imply ps (p → q) → imply ps q))›
proof (induct ps)
  case Nil
  then show ?case
    by (metis Imp1 Imp2 MP imply.simps(1))
next
  case (Cons r ps)
  then show ?case
  proof -
    have ‹⊢ ((r → imply ps p) → (r → (imply ps (p → q) → imply ps q)))›
      by (meson Cons.hyps Imp1 Imp2 MP)
    then have ‹⊢ ((r → imply ps p) → ((r → imply ps (p → q)) → (r → imply ps q)))›
      by (meson Imp2 Tran MP)
    then show ?thesis
      by simp
  qed
qed

lemma imply_mp': ‹⊢ (imply ps p) ⟹ ⊢ (imply ps (p → q)) ⟹ ⊢ (imply ps q)›
  using imply_MP by (meson MP)

lemma add_imply: ‹⊢ q ⟹ ⊢ (imply ps q)›
  using imply_Cons by (induct ps) simp_all

lemma imply_append: ‹imply (ps @ qs) r = imply ps (imply qs r)›
  by (induct ps) simp_all

lemma imply_swap: ‹⊢ (imply (ps @ qs) r) ⟹ ⊢ (imply (qs @ ps) r)›
proof (induct qs arbitrary: ps)
  case (Cons q qs)
  then show ?case
    by (metis imply_Cons imply_head imply_mp' imply.simps(2) imply_append)
qed simp

lemma deduct: ‹⊢ (imply (p # ps) q) ⟷ ⊢ (imply ps (p → q))›
  using imply_swap by (metis imply.simps(1-2) imply_append)

theorem imply_weaken: ‹⊢ (imply ps q) ⟹ set ps ⊆ set ps' ⟹ ⊢ (imply ps' q)›
proof (induct ps arbitrary: q)
  case (Cons p ps)
  note ‹⊢ (imply (p # ps) q)›
  then have ‹⊢ (imply ps (p → q))›
    using deduct by blast
  then have ‹⊢ (imply ps' (p → q))›
    using Cons by simp
  then show ?case
    using Cons(3) by (meson imply_mem imply_mp' list.set_intros(1) subset_code(1))
qed (simp add: add_imply)

lemma cut: ‹⊢ (imply ps p) ⟹ ⊢ (imply (p # ps) q) ⟹ ⊢ (imply ps q)›
  using deduct imply_mp' by blast

lemma imply4: ‹⊢ (imply (p # q # ps) r) ⟹ ⊢ (imply (q # p # ps) r)›
  by (metis Imp1 Imp2 MP imply.simps(2))

lemma cut': ‹⊢ (imply (p # ps) r) ⟹ ⊢ (imply (q # ps) p) ⟹ ⊢ (imply (q # ps) r)›
  using imply_Cons cut imply4 by blast

lemma imply_lift: ‹⊢ (p → q) ⟹ ⊢ (imply ps p → imply ps q)›
proof (induct ps)
  case (Cons r ps)
  then show ?case
    by (metis MP Chu4 imply.simps(2))
qed simp

lemma Neg': ‹⊢ (imply ps (Neg (Neg p)) → imply ps p)›
  using Neg imply_lift by simp

lemma Boole: ‹⊢ (imply ((Neg p) # ps) ⊥) ⟹ ⊢ (imply ps p)›
  using deduct MP Neg' by blast

lemma imply_front: ‹⊢ (imply S p) ⟹ set S - {q} ⊆ set S' ⟹ ⊢ (imply (q # S') p)›
  by (metis Diff_single_insert imply_weaken list.set(2))

section ‹Consistent›

definition consistent :: ‹form set ⇒ bool› where
  ‹consistent S ≡ ∄S'. set S' ⊆ S ∧ ⊢ (imply S' ⊥)›

lemma UN_finite_bound:
  assumes ‹finite A› ‹A ⊆ (⋃n. f n)›
  shows ‹∃m :: nat. A ⊆ (⋃n ≤ m. f n)›
  using assms
proof (induct rule: finite_induct)
  case (insert x A)
  then obtain m where ‹A ⊆ (⋃n ≤ m. f n)›
    by fast
  then have ‹A ⊆ (⋃n ≤ (m + k). f n)› for k
    by fastforce
  moreover obtain m' where ‹x ∈ f m'›
    using insert(4) by blast
  ultimately have ‹{x} ∪ A ⊆ (⋃n ≤ m + m'. f n)›
    by auto
  then show ?case
    by blast
qed simp

section ‹Extension›

primrec extend :: ‹form set ⇒ (nat ⇒ form) ⇒ nat ⇒ form set› where
  ‹extend S f 0 = S›
| ‹extend S f (Suc n) =
    (if consistent ({f n} ∪ extend S f n)
     then {f n} ∪ extend S f n
     else extend S f n)›

definition Extend :: ‹form set ⇒ (nat ⇒ form) ⇒ form set› where
  ‹Extend S f ≡ ⋃n. extend S f n›

lemma Extend_subset: ‹S ⊆ Extend S f›
  unfolding Extend_def by (metis Union_upper extend.simps(1) range_eqI)

lemma extend_chain: ‹extend S f n ⊆ extend S f (Suc n)›
  by auto

lemma extend_bound: ‹(⋃n ≤ m. extend S f n) = extend S f m›
  by (induct m) (simp_all add: atMost_Suc)

lemma consistent_extend: ‹consistent S ⟹ consistent (extend S f n)›
  by (induct n) simp_all

lemma consistent_Extend:
  assumes ‹consistent S›
  shows ‹consistent (Extend S f)›
  unfolding Extend_def
proof (rule ccontr)
  assume ‹¬ consistent (⋃n. extend S f n)›
  then obtain S' where ‹⊢ (imply S' ⊥)› ‹set S' ⊆ (⋃n. extend S f n)›
    unfolding consistent_def by blast
  then obtain m where ‹set S' ⊆ (⋃n ≤ m. extend S f n)›
    using UN_finite_bound by (metis List.finite_set)
  then have ‹set S' ⊆ extend S f m›
    using extend_bound by blast
  moreover have ‹consistent (extend S f m)›
    using assms consistent_extend by blast
  ultimately show False
    unfolding consistent_def using ‹⊢ (imply S' ⊥)› by blast
qed

section ‹Maximal›

definition maximal :: ‹form set ⇒ bool› where
  ‹maximal S ≡ ∀p. p ∉ S ⟶ ¬ consistent ({p} ∪ S)›

lemma maximal_Extend:
  assumes ‹surj f›
  shows ‹maximal (Extend S f)›
proof (rule ccontr)
  assume ‹¬ maximal (Extend S f)›
  then obtain p where ‹p ∉ Extend S f› ‹consistent ({p} ∪ Extend S f)›
    unfolding maximal_def using assms consistent_Extend by blast
  obtain n where n: ‹f n = p›
    using ‹surj f› unfolding surj_def by metis
  then have ‹p ∉ extend S f (Suc n)›
    using ‹p ∉ Extend S f› unfolding Extend_def by blast
  then have ‹¬ consistent ({p} ∪ extend S f n)›
    using n by fastforce
  moreover have ‹p ∉ extend S f n›
    using ‹p ∉ extend S f (Suc n)› extend_chain by blast
  then have ‹{p} ∪ extend S f n ⊆ {p} ∪ Extend S f›
    unfolding Extend_def by blast
  ultimately have ‹¬ consistent ({p} ∪ Extend S f)›
    unfolding consistent_def by fastforce
  then show False
    using ‹consistent ({p} ∪ Extend S f)› by blast
qed

section ‹Hintikka›

definition hintikka :: ‹form set ⇒ bool› where
  ‹hintikka H ≡
    ⊥ ∉ H ∧
    (∀n. Pro n ∈ H ⟶ (Neg (Pro n)) ∉ H) ∧
    (∀p q. (p → q) ∈ H ⟶ (Neg p) ∈ H ∨ q ∈ H) ∧
    (∀p q. (Neg (p → q)) ∈ H ⟶ p ∈ H ∧ (Neg q) ∈ H)›

abbreviation (input) ‹model H n ≡ Pro n ∈ H›

lemma hintikka_model: ‹hintikka H ⟹
                        (p ∈ H ⟶ (model H ⊨ p)) ∧ ((Neg p) ∈ H ⟶ ¬ (model H ⊨ p))›
  by (induct p) (simp; unfold hintikka_def, blast)+

lemma inconsistent_head:
  assumes ‹maximal S› ‹consistent S› ‹p ∉ S›
  shows ‹∃S'. ⊢ (imply (p # S') ⊥) ∧ set S' ⊆ S›
proof -
  obtain S' where S': ‹⊢ (imply S' ⊥)› ‹set S' ⊆ {p} ∪ S› ‹p ∈ set S'›
    using assms unfolding maximal_def consistent_def by fast
  then obtain S'' where S'': ‹⊢ (imply (p # S'') ⊥)› ‹set S'' = set S' - {p}›
    by (metis imply_front set_removeAll subset_refl)
  then show ?thesis
    using S'(2) by fast
qed

lemma hintikka_Extend:
  assumes ‹maximal S› ‹consistent S›
  shows ‹hintikka S›
  unfolding hintikka_def
proof safe
  assume ‹⊥ ∈ S›
  then show False
    using assms(2) imply_head unfolding consistent_def
    by (metis all_not_in_conv empty_set insert_subset list.simps(15) subsetI)
next
  fix n
  assume ‹Pro n ∈ S› ‹(Neg (Pro n)) ∈ S›
  moreover have ‹⊢ (imply [Pro n, Neg (Pro n)] ⊥)›
    by (simp add: Neg1)
  ultimately show False
    using assms(2) unfolding consistent_def
    by (metis bot.extremum empty_set insert_subset list.set(2))
next
  fix p q
  assume *: ‹(p → q) ∈ S› ‹q ∉ S›
  then obtain Sq' where Sq': ‹⊢ (imply (q # Sq') ⊥)› ‹set Sq' ⊆ S›
    using assms inconsistent_head by blast

  show ‹(Neg p) ∈ S›
  proof (rule ccontr)
    assume ‹(Neg p) ∉ S›
    then obtain Sp' where Sp': ‹⊢ (imply ((Neg p) # Sp') ⊥)› ‹set Sp' ⊆ S›
      using assms inconsistent_head by blast

    obtain S' where S': ‹set S' = set Sp' ∪ set Sq'›
      by (meson set_append)
    then have ‹⊢ (imply ((Neg p) # S') ⊥)› ‹⊢ (imply (q # S') ⊥)›
    proof -
      have ‹set Sp' ⊆ set S'›
        using S' by blast
      then show ‹⊢ (imply ((Neg p) # S') ⊥)›
        by (metis Sp'(1) deduct imply_weaken)
      have ‹set Sq' ⊆ set S'›
        using S' by blast
      then show ‹⊢ (imply (q # S') ⊥)›
        by (metis Sq'(1) deduct imply_weaken)
    qed
    then have ‹⊢ (imply ((p → q) # S') ⊥)›
      using Boole imply_Cons imply_head imply_mp' cut' by metis
    moreover have ‹set ((p → q) # S') ⊆ S›
      using *(1) S' Sp'(2) Sq'(2) by auto
    ultimately show False
      using assms unfolding consistent_def by blast
  qed
next
  fix p q
  assume *: ‹(Neg (p → q)) ∈ S›
  show ‹p ∈ S›
  proof (rule ccontr)
    assume ‹p ∉ S›
    then obtain S' where S': ‹⊢ (imply (p # S') ⊥)› ‹set S' ⊆ S›
      using assms inconsistent_head by blast
    moreover have ‹⊢ (imply ((Neg (p → q)) # S') p)›
      using add_imply Neg2 deduct by blast
    ultimately have ‹⊢ (imply ((Neg (p → q)) # S') ⊥)›
      using cut' by blast
    moreover have ‹set ((Neg (p → q)) # S') ⊆ S›
      using *(1) S'(2) by fastforce
    ultimately show False
      using assms unfolding consistent_def by blast
  qed
next
  fix p q
  assume *: ‹(Neg (p → q)) ∈ S›
  show ‹(Neg q) ∈ S›
  proof (rule ccontr)
    assume ‹(Neg q) ∉ S›
    then obtain S' where S': ‹⊢ (imply ((Neg q) # S') ⊥)› ‹set S' ⊆ S›
      using assms inconsistent_head by blast
    moreover have ‹⊢ (imply ((Neg (p → q)) # S') (Neg q))›
      using add_imply Neg3 deduct by blast
    ultimately have ‹⊢ (imply ((Neg (p → q)) # S') ⊥)›
      using cut' by blast
    moreover have ‹set ((Neg (p → q)) # S') ⊆ S›
      using *(1) S'(2) by fastforce
    ultimately show False
      using assms unfolding consistent_def by blast
  qed
qed

section ‹Countable Formulas›

primrec diag :: ‹nat ⇒ (nat × nat)› where
  ‹diag 0 = (0, 0)›
| ‹diag (Suc n) =
     (let (x, y) = diag n
      in case y of
          0 ⇒ (0, Suc x)
        | Suc y ⇒ (Suc x, y))›

theorem diag_le1: ‹fst (diag (Suc n)) < Suc n›
  by (induct n) (simp_all add: Let_def split_def split: nat.split)

theorem diag_le2: ‹snd (diag (Suc (Suc n))) < Suc (Suc n)›
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n')
  then show ?case
  proof (induct n')
    case 0
    then show ?case by simp
  next
    case (Suc _)
    then show ?case
      using diag_le1 by (simp add: Let_def split_def split: nat.split)
  qed
qed

theorem diag_le3: ‹fst (diag n) = Suc x ⟹ snd (diag n) < n›
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n')
  then show ?case
  proof (induct n')
    case 0
    then show ?case by simp
  next
    case (Suc n'')
    then show ?case using diag_le2 by simp
  qed
qed

theorem diag_le4: ‹fst (diag n) = Suc x ⟹ x < n›
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n')
  then have ‹fst (diag (Suc n')) < Suc n'›
    using diag_le1 by blast
  then show ?case using Suc by simp
qed

function undiag :: ‹nat × nat ⇒ nat› where
  ‹undiag (0, 0) = 0›
| ‹undiag (0, Suc y) = Suc (undiag (y, 0))›
| ‹undiag (Suc x, y) = Suc (undiag (x, Suc y))›
  by pat_completeness auto
termination
  by (relation ‹measure (λ(x, y). ((x + y) * (x + y + 1)) div 2 + x)›) auto

theorem diag_undiag [simp]: ‹diag (undiag (x, y)) = (x, y)›
  by (induct rule: undiag.induct) simp_all

datatype btree = Leaf nat | Branch btree btree

function diag_btree :: ‹nat ⇒ btree› where
  ‹diag_btree n = (case fst (diag n) of
       0 ⇒ Leaf (snd (diag n))
     | Suc x ⇒ Branch (diag_btree x) (diag_btree (snd (diag n))))›
  by auto
termination
  by (relation ‹measure id›) (auto intro: diag_le3 diag_le4)

primrec undiag_btree :: ‹btree ⇒ nat› where
  ‹undiag_btree (Leaf n) = undiag (0, n)›
| ‹undiag_btree (Branch t1 t2) = undiag (Suc (undiag_btree t1), undiag_btree t2)›

theorem diag_undiag_btree [simp]: ‹diag_btree (undiag_btree t) = t›
  by (induct t) simp_all

declare diag_btree.simps [simp del] undiag_btree.simps [simp del]

fun form_of_btree :: ‹btree ⇒ form› where
  ‹form_of_btree (Leaf 0) = Falsity›
| ‹form_of_btree (Branch (Leaf 0) (Leaf n)) = Pro n›
| ‹form_of_btree (Branch (Leaf (Suc 0)) (Branch t1 t2)) =
     Imp (form_of_btree t1) (form_of_btree t2)›
| ‹form_of_btree (Leaf (Suc _)) = undefined›
| ‹form_of_btree (Branch (Leaf 0) (Branch _ _)) = undefined›
| ‹form_of_btree (Branch (Leaf (Suc 0)) (Leaf _)) = undefined›
| ‹form_of_btree (Branch (Leaf (Suc (Suc _))) _) = undefined›
| ‹form_of_btree (Branch (Branch _ _) _) = undefined›

primrec btree_of_form :: ‹form ⇒ btree› where
  ‹btree_of_form Falsity = Leaf 0›
| ‹btree_of_form (Pro n) = Branch (Leaf 0) (Leaf n)›
| ‹btree_of_form (Imp p q) = Branch (Leaf (Suc 0))
     (Branch (btree_of_form p) (btree_of_form q))›

definition diag_form :: ‹nat ⇒ form› where
  ‹diag_form n = form_of_btree (diag_btree n)›

definition undiag_form :: ‹form ⇒ nat› where
  ‹undiag_form p = undiag_btree (btree_of_form p)›

theorem diag_undiag_form [simp]: ‹diag_form (undiag_form p) = p›
  unfolding diag_form_def undiag_form_def by (induct p) simp_all

abbreviation ‹from_nat ≡ diag_form›
abbreviation ‹to_nat ≡ undiag_form›

lemma surj_from_nat: ‹surj from_nat›
  by (metis diag_undiag_form surj_def)

section ‹Completeness›

lemma imply_completeness:
  assumes valid: ‹∀I. list_all (λq. (I ⊨ q)) ps ⟶ (I ⊨ p)›
  shows ‹⊢ (imply ps p)›
proof (rule ccontr)
  assume ‹¬ ⊢ (imply ps p)›
  then have *: ‹¬ ⊢ (imply ((Neg p) # ps) ⊥)›
    using Boole by blast

  let ?S = ‹set ((Neg p) # ps)›
  let ?H = ‹Extend ?S from_nat›

  have ‹consistent ?S›
    unfolding consistent_def using * imply_weaken by blast
  then have ‹consistent ?H› ‹maximal ?H›
    using consistent_Extend maximal_Extend surj_from_nat by blast+
  then have ‹hintikka ?H›
    using hintikka_Extend by blast

  have ‹model ?H ⊨ p› if ‹p ∈ ?S› for p
    using that Extend_subset hintikka_model ‹hintikka ?H› by blast
  then have ‹model ?H ⊨ (Neg p)› ‹list_all (λp. (model ?H ⊨ p)) ps›
    unfolding list_all_def by fastforce+
  then have ‹model ?H ⊨ p›
    using valid by blast
  then show False
    using ‹model ?H ⊨ (Neg p)› by simp
qed

theorem completeness: ‹∀I. (I ⊨ p) ⟹ ⊢ p›
  using imply_completeness[where ps=‹[]›] by simp

section ‹Main Result›

theorem main: ‹valid p = ⊢ p›
proof
  assume ‹valid p›
  with completeness show ‹⊢ p›
    unfolding valid_def .
next
  assume ‹⊢ p›
  with soundness show ‹valid p›
    unfolding valid_def by (intro allI)
qed

section ‹Using Shortest Axiom for Implicational Logic - Łukasiewicz 1936/1937›

text ‹Łukasiewicz 1948 building on work by Wajsberg, Tarski and Bernays [Church page 159]›

inductive WL (‹⪢›) where
  ‹⪢ q› if ‹⪢ p› and ‹⪢ (p → q)› |
  ‹⪢ (((p → q) → r) → ((r → p) → (s → p)))› |
  ‹⪢ (⊥ → p)›

abbreviation (input) C :: ‹form ⇒ form ⇒ form› (‹C _ _› [0, 0] 1) where ‹(C p q) ≡ (p → q)›

lemma l1: ‹⪢ (C C C p q r C C r p C s p)›
  using WL.intros(2) .

lemma l2: ‹⪢ (C C C C r p C s p C p q C r C p q)›
  using l1 by (meson WL.intros(1))

lemma l3: ‹⪢ (C C C r C p q C C r p C s p C t C C r p C s p)›
  using l1 l2 by (meson WL.intros(1))

lemma l4: ‹⪢ (C C C p q p C s p)›
  using l3 l1 by (meson WL.intros(1))

lemma l5: ‹⪢ (C C C s p C p q C r C p q)›
  using l1 l4 by (meson WL.intros(1))

lemma l6: ‹⪢ (C C C r C p q C s p C t C s p)›
  using l1 l5 by (meson WL.intros(1))

lemma l7: ‹⪢ (C C C t C s p C r C p q C u C r C p q)›
  using l1 l6 by (meson WL.intros(1))

lemma l8: ‹⪢ (C C C s q p C q p)›
  using l7 l1 by (meson WL.intros(1))

lemma l9: ‹⪢ (C r C C r p C s p)›
  using l8 l1 by (meson WL.intros(1))

lemma l10: ‹⪢ (C C C C C r q p C s p r C t r)›
  using l1 l9 by (meson WL.intros(1))

lemma l11: ‹⪢ (C C C t r C C C r q p C s p C u C C C r q p C s p)›
  using l1 l10 by (meson WL.intros(1))

lemma l12: ‹⪢ (C C C u C C C r q p C s p C t r C v C t r)›
  using l1 l11 by (meson WL.intros(1))

lemma l13: ‹⪢ (C C C v C t r C u C C C r q p C s p C w C u C C C r q p C s p)›
  using l1 l12 by (meson WL.intros(1))

lemma l14: ‹⪢ (C C C t r C s p C C C r q p C s p)›
  using l13 l1 by (meson WL.intros(1))

lemma l15: ‹⪢ (C C C r q C s p C C r p C s p)›
  using l14 l1 by (meson WL.intros(1))

lemma l16: ‹⪢ (C C r C s p C C C r q p C s p)›
  using l15 l9 by (meson WL.intros(1))

lemma l17: ‹⪢ (C C C C C p q r t C s p C C r p C s p)›
  using l16 l1 by (meson WL.intros(1))

lemma l18: ‹⪢ (C C C C r p C s p C C C p q r t C u C C C p q r t)›
  using l1 l17 by (meson WL.intros(1))

lemma l19: ‹⪢ (C C C C s p q C r p C C C p q r C s p)›
  using l18 by (meson WL.intros(1))

lemma l20: ‹⪢ (C C C C r p p C s p C C C p q r C s p)›
  using l14 l19 by (meson WL.intros(1))

lemma l21: ‹⪢ (C C C C p r q q C C q r C p r)›
  using l20 l15 by (meson WL.intros(1))

lemma l22: ‹⪢ (C p p)›
  using l5 l4 by (meson WL.intros(1))

lemma l23: ‹⪢ (C C C p q r C C r p p)›
  using l20 l22 by (meson WL.intros(1))

lemma l24: ‹⪢ (C r C C r p p)›
  using l8 l23 by (meson WL.intros(1))

lemma l25: ‹⪢ (C C p q C C C p r q q)›
  using l15 l24 by (meson WL.intros(1))

lemma l26: ‹⪢ (C C C C p q C C q r C p r C C C p r q q C C C p r q q)›
  using l25 by (meson WL.intros(1))

lemma l27: ‹⪢ (C p C q p)›
  using l8 by (meson WL.intros(1))

lemma l28: ‹⪢ (C C C p q p p)›
  using l25 l22 by (meson WL.intros(1))

lemma l29: ‹⪢ (C C p q C C q r C p r)›
  using l21 l26 by (meson WL.intros(1))

theorem equivalence: ‹⪢ p ⟷ ⊢ p›
proof
  have *: ‹⊢ (((p → q) → r) → ((r → p) → (s → p)))› for p q r s
    using completeness by simp
  show ‹⊢ p› if ‹⪢ p›
    using that by induct (auto simp: * intro: Axiomatics.intros)
  show ‹⪢ p› if ‹⊢ p›
    using that by induct (auto simp: l27 l28 l29 intro: WL.intros)
qed

end