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