Theory Implicational_Logic

(*
  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 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 Swap: ‹⊢ (p → q → r) → q → p → r›
proof -
  have ‹⊢ q → (q → r) → r›
    using MP PR Simp Tran by metis
  then show ?thesis
    using MP Tran by meson
qed

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

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

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

lemma Tran': ‹⊢ (q → r) → (p → q) → p → r›
  using MP Swap Tran .

lemma Frege: ‹⊢ (p → q → r) → (p → q) → p → r›
  using MP MP Tran MP MP Tran Swap Tran' MP Tran' Hilbert .

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›

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