Theory Implicational_Logic_Appendix

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

section ‹Formalization of Łukasiewicz's Axiom System from 1924 for Classical Propositional Logic›

subsection ‹Syntax, Semantics and Axiom System›

theory Implicational_Logic_Appendix imports Main begin

datatype form =
  Pro nat (‹⋅›) |
  Neg form (‹∼›) |
  Imp form form (infixr ‹→› 55)

primrec semantics (infix ‹⊨› 50) where
  ‹I ⊨ ⋅ n = I n› |
  ‹I ⊨ ∼ p = (¬ I ⊨ p)› |
  ‹I ⊨ p → q = (I ⊨ p ⟶ I ⊨ q)›

inductive Ax (‹⊢ _› 50) where
  01: ‹⊢ (p → q) → (q → r) → p → r› |
  02: ‹⊢ (∼ p → p) → p› |
  03: ‹⊢ p → ∼ p → q› |
  MP: ‹⊢ p → q ⟹ ⊢ p ⟹ ⊢ q›

subsection ‹Soundness and Derived Formulas›

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

lemma 04: ‹⊢ (((q → r) → p → r) → s) → (p → q) → s›
  using MP 01 01 .

lemma 05: ‹⊢ (p → q → r) → (s → q) → p → s → r›
  using MP 04 04 .

lemma 06: ‹⊢ (p → q) → ((p → r) → s) → (q → r) → s›
  using MP 04 01 .

lemma 07: ‹⊢ (t → (p → r) → s) → (p → q) → t → (q → r) → s›
  using MP 05 06 .

lemma 09: ‹⊢ ((∼ p → q) → r) → p → r›
  using MP 01 03 .

lemma 10: ‹⊢ p → ((∼ p → p) → p) → (q → p) → p›
  using MP 09 06 .

lemma 11: ‹⊢ (q → (∼ p → p) → p) → (∼ p → p) → p›
  using MP MP 10 02 02 .

lemma 12: ‹⊢ t → (∼ p → p) → p›
  using MP 09 11 .

lemma 13: ‹⊢ (∼ p → q) → t → (q → p) → p›
  using MP 07 12 .

lemma 14: ‹⊢ ((t → (q → p) → p) → r) → (∼ p → q) → r›
  using MP 01 13 .

lemma 15: ‹⊢ (∼ p → q) → (q → p) → p›
  using MP 14 02 .

lemma 16: ‹⊢ p → p›
  using MP 09 02 .

lemma 17: ‹⊢ p → (q → p) → p›
  using MP 09 15 .

lemma 18: ‹⊢ q → p → q›
  using MP MP 05 17 03 .

lemma 19: ‹⊢ ((p → q) → r) → q → r›
  using MP 01 18 .

lemma 20: ‹⊢ p → (p → q) → q›
  using MP 19 15 .

lemma 21: ‹⊢ (p → q → r) → q → p → r›
  using MP 05 20 .

lemma 22: ‹⊢ (q → r) → (p → q) → p → r›
  using MP 21 01 .

lemma 23: ‹⊢ ((q → p → r) → s) → (p → q → r) → s›
  using MP 01 21 .

lemma 24: ‹⊢ ((p → q) → p) → p›
  using MP MP 23 15 03 .

lemma 25: ‹⊢ ((p → r) → s) → (p → q) → (q → r) → s›
  using MP 21 06 .

lemma 26: ‹⊢ ((p → q) → r) → (r → p) → p›
  using MP 25 24 .

lemma 28: ‹⊢ (((r → p) → p) → s) → ((p → q) → r) → s›
  using MP 01 26 .

lemma 29: ‹⊢ ((p → q) → r) → (p → r) → r›
  using MP 28 26 .

lemma 31: ‹⊢ (p → s) → ((p → q) → r) → (s → r) → r›
  using MP 07 29 .

lemma 32: ‹⊢ ((p → q) → r) → (p → s) → (s → r) → r›
  using MP 21 31 .

lemma 33: ‹⊢ (p → s) → (s → q → p → r) → q → p → r›
  using MP 32 18 .

lemma 34: ‹⊢ (s → q → p → r) → (p → s) → q → p → r›
  using MP 21 33 .

lemma 35: ‹⊢ (p → q → r) → (p → q) → p → r›
  using MP 34 22 .

lemma 36: ‹⊢ ∼ p → p → q›
  using MP 21 03 .

lemmas
  Tran = 01 and
  Clavius = 02 and
  Expl = 03 and
  Frege' = 05 and
  Clavius' = 15 and
  Id = 16 and
  Simp = 18 and
  Swap = 21 and
  Tran' = 22 and
  Peirce = 24 and
  Frege = 35 and
  Expl' = 36

lemma Neg1: ‹⊢ (q → s) → (∼ q → s) → s›
  using MP Clavius' Expl' Frege' Swap by meson

lemma Neg2: ‹⊢ ((q → s) → s) → ∼ q → s›
  using MP Tran MP Swap Expl .

lemma Imp1: ‹⊢ (q → s) → ((q → r) → s) → s›
  using MP Peirce Tran Tran' by meson

lemma Imp2: ‹⊢ ((r → s) → s) → ((q → r) → s) → s›
  using MP Tran MP Tran Simp .

lemma Imp3: ‹⊢ ((q → s) → s) → (r → s) → (q → r) → s›
  using MP Swap Tran by meson

subsection ‹Completeness and Main Theorem›

primrec pros where
  ‹pros (⋅ n) = [n]› |
  ‹pros (∼ p) = pros p› |
  ‹pros (p → q) = remdups (pros p @ pros q)›

lemma distinct_pros: ‹distinct (pros p)›
  by (induct p) simp_all

primrec imply (infixr ‹↝› 56) where
  ‹[] ↝ q = q› |
  ‹p # ps ↝ q = p → ps ↝ q›

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

abbreviation Ax_assms (infix ‹⊢› 50) where ‹ps ⊢ q ≡ ⊢ ps ↝ q›

lemma imply_Cons: ‹ps ⊢ q ⟹ p # ps ⊢ q›
proof -
  assume ‹ps ⊢ q›
  with MP Simp have ‹⊢ p → ps ↝ q› .
  then show ?thesis
    by simp
qed

lemma imply_head: ‹p # ps ⊢ p›
  by (induct ps) (use MP Frege Simp imply.simps in metis)+

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

lemma imply_MP: ‹⊢ ps ↝ (p → q) → ps ↝ p → ps ↝ q›
proof (induct ps)
  case (Cons r ps)
  then have ‹⊢ (r → ps ↝ (p → q)) → (r → ps ↝ p) → r → ps ↝ q›
    using MP Frege Simp by meson
  then show ?case
    by simp
qed (auto intro: Id)

lemma MP': ‹ps ⊢ p → q ⟹ ps ⊢ p ⟹ ps ⊢ q›
  using MP imply_MP by metis

lemma imply_swap_append: ‹ps @ qs ⊢ r ⟹ qs @ ps ⊢ r›
  by (induct qs arbitrary: ps) (simp, metis MP' imply_append imply_Cons imply_head imply.simps(2))

lemma imply_deduct: ‹p # ps ⊢ q ⟹ ps ⊢ p → q›
  using imply_append imply_swap_append imply.simps by metis

lemma add_imply [simp]: ‹⊢ p ⟹ ps ⊢ p›
proof -
  note MP
  moreover have ‹⊢ p → ps ↝ p›
    using imply_head by simp
  moreover assume ‹⊢ p›
  ultimately show ?thesis .
qed

lemma imply_weaken: ‹ps ⊢ p ⟹ set ps ⊆ set ps' ⟹ ps' ⊢ p›
  by (induct ps arbitrary: p) (simp, metis MP' imply_deduct imply_mem insert_subset list.set(2))

abbreviation ‹lift t s p ≡ if t then (p → s) → s else p → s›

abbreviation ‹lifts I s ≡ map (λn. lift (I n) s (⋅ n))›

lemma lifts_weaken: ‹lifts I s l ⊢ p ⟹ set l ⊆ set l' ⟹ lifts I s l' ⊢ p›
  using imply_weaken by (metis (no_types, lifting) image_mono set_map)

lemma lifts_pros_lift: ‹lifts I s (pros p) ⊢ lift (I ⊨ p) s p›
proof (induct p)
  case (Neg q)
  consider ‹¬ I ⊨ q› | ‹I ⊨ q›
    by blast
  then show ?case
  proof cases
    case 1
    then have ‹lifts I s (pros (∼ q)) ⊢ q → s›
      using Neg by simp
    then have ‹lifts I s (pros (∼ q)) ⊢ (∼ q → s) → s›
      using MP' Neg1 add_imply by blast
    with 1 show ?thesis
      by simp
  next
    case 2
    then have ‹lifts I s (pros (∼ q)) ⊢ (q → s) → s›
      using Neg by simp
    then have ‹lifts I s (pros (∼ q)) ⊢ ∼ q → s›
      using MP' Neg2 add_imply by blast
    with 2 show ?thesis
      by simp
  qed
next
  case (Imp q r)
  consider ‹¬ I ⊨ q› | ‹I ⊨ r› | ‹I ⊨ q› ‹¬ I ⊨ r›
    by blast
  then show ?case
  proof cases
    case 1
    then have ‹lifts I s (pros (q → r)) ⊢ q → s›
      using Imp(1) lifts_weaken[where l' = ‹pros (q → r)›] by simp
    then have ‹lifts I s (pros (q → r)) ⊢ ((q → r) → s) → s›
      using Imp1 MP' add_imply by blast
    with 1 show ?thesis
      by simp
  next
    case 2
    then have ‹lifts I s (pros (q → r)) ⊢ (r → s) → s›
      using Imp(2) lifts_weaken[where l' = ‹pros (q → r)›] by simp
    then have ‹lifts I s (pros (q → r)) ⊢ ((q → r) → s) → s›
      using Imp2 MP' add_imply by blast
    with 2 show ?thesis
      by simp
  next
    case 3
    then have ‹lifts I s (pros (q → r)) ⊢ (q → s) → s› ‹lifts I s (pros (q → r)) ⊢ r → s›
      using Imp lifts_weaken[where l' = ‹pros (q → r)›] by simp_all
    then have ‹lifts I s (pros (q → r)) ⊢ (q → r) → s›
      using Imp3 MP' add_imply by blast
    with 3 show ?thesis
      by simp
  qed
qed (auto intro: Id)

lemma lifts_pros: ‹I ⊨ p ⟹ lifts I p (pros p) ⊢ p›
proof -
  assume ‹I ⊨ p›
  then have ‹lifts I p (pros p) ⊢ (p → p) → p›
    using lifts_pros_lift[of I p p] by simp
  then show ?thesis
    using Id MP' add_imply by blast
qed

theorem completeness: ‹∀I. I ⊨ p ⟹ ⊢ p›
proof -
  let ?A = ‹λl I. lifts I p l ⊢ p›
  let ?B = ‹λl. ∀I. ?A l I ∧ distinct l›
  assume ‹∀I. I ⊨ p›
  moreover have ‹?B l ⟹ (⋀n l. ?B (n # l) ⟹ ?B l) ⟹ ?B []› for l
    by (induct l) blast+
  moreover have ‹?B (n # l) ⟹ ?B l› for n l
  proof -
    assume *: ‹?B (n # l)›
    show ‹?B l›
    proof
      fix I
      from * have ‹?A (n # l) (I(n := True))› ‹?A (n # l) (I(n := False))›
        by blast+
      moreover from * have ‹∀m ∈ set l. ∀t. (I(n := t)) m = I m›
        by simp
      ultimately have ‹((⋅ n → p) → p) # lifts I p l ⊢ p› ‹(⋅ n → p) # lifts I p l ⊢ p›
        by (simp_all cong: map_cong)
      then have ‹?A l I›
        using MP' imply_deduct by blast
      moreover from * have ‹distinct (n # l)›
        by blast
      ultimately show ‹?A l I ∧ distinct l›
        by simp
    qed
  qed
  ultimately have ‹?B []›
    using lifts_pros distinct_pros by blast
  then show ?thesis
    by simp
qed

theorem main: ‹(⊢ p) = (∀I. I ⊨ p)›
  using soundness completeness by blast

subsection ‹Reference›

text ‹Numbered lemmas are from Jan Łukasiewicz: Elements of Mathematical Logic (English Tr. 1963)›

end