Theory Implicational_Logic_New

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

section ‹Formalization of the Bernays-Tarski Axiom System for Classical Implicational Logic›

(* Uncomment for Full Classical Propositional Logic *)

subsection ‹Syntax, Semantics and Axiom System›

theory Implicational_Logic_New imports Main begin

datatype form =
  (*Falsity (‹⊥›) |*)
  Pro nat (‹⋅›) |
  Imp form form (infixr ‹→› 55)

primrec semantics (infix ‹⊨› 50) where
  (*‹I ⊨ ⊥ = False› |*)
  ‹I ⊨ ⋅ n = I n› |
  ‹I ⊨ p → q = (I ⊨ p ⟶ I ⊨ q)›

inductive Ax (‹⊢ _› 50) where
  (*Expl: ‹⊢ ⊥ → p› |*)
  Simp: ‹⊢ p → q → p› |
  Tran: ‹⊢ (p → q) → (q → r) → p → r› |
  MP: ‹⊢ p → q ⟹ ⊢ p ⟹ ⊢ q› |
  PR: ‹⊢ (p → q) → p ⟹ ⊢ p›

subsection ‹Soundness and Derived Formulas›

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

lemma Peirce: ‹⊢ ((p → q) → p) → p›
  using PR MP MP MP Tran Tran MP Tran PR MP MP MP Tran Tran PR MP Tran MP Tran MP Simp Simp MP Tran
    MP MP Tran Tran PR MP Tran MP Tran MP Simp Simp MP Tran MP Tran Simp .

lemma Frege: ‹⊢ (p → q → r) → (p → q) → p → r›
  using MP MP Tran MP MP Tran MP MP Tran Tran MP Tran PR MP MP MP Tran Tran PR MP Tran MP Tran MP
    Simp Simp MP Tran MP MP Tran Tran PR MP Tran MP Tran MP Simp Simp MP MP MP Tran Tran MP Tran PR
    MP MP MP Tran Tran PR MP Tran MP Tran MP Simp Simp MP Tran MP MP Tran Tran PR MP Tran MP Tran MP
    Simp Simp Tran MP MP MP MP Tran Tran MP Tran PR MP MP MP Tran Tran PR MP Tran MP Tran MP Simp
    Simp MP Tran MP MP Tran Tran PR MP Tran MP Tran MP Simp Simp Tran MP MP Tran Tran Peirce .

lemma Id: ‹⊢ p → p›
  using MP MP Frege Simp Simp .

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

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 MP MP Tran Tran MP Tran PR MP MP MP Tran Tran PR MP Tran MP Tran MP Simp Simp MP Tran MP
    MP Tran Tran PR MP Tran MP Tran MP Simp Simp MP MP Tran MP MP MP Tran Tran MP Tran PR MP MP MP
    Tran Tran PR MP Tran MP Tran MP Simp Simp MP Tran MP MP Tran Tran PR MP Tran MP Tran MP Simp
    Simp Tran Tran .

subsection ‹Completeness and Main Theorem›

fun pros where
  ‹pros (p → q) = remdups (pros p @ pros q)› |
  ‹pros p = (case p of (⋅ n) ⇒ [n] | _ ⇒ [])›

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 (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 Ax.intros)

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 ‹Wikipedia 🌐‹https://en.wikipedia.org/wiki/Implicational_propositional_calculus› July 2022›

end