Theory FOL_Axiomatic

(*
  File:      FOL_Axiomatic.thy
  Author:    Asta Halkjær From

  This work is a formalization of the soundness and completeness of an axiomatic system
  for first-order logic. The proof system is based on System Q1 by Smullyan
  and the completeness proof follows his textbook "First-Order Logic" (Springer-Verlag 1968).
  The completeness proof is in the Henkin style where a consistent set
  is extended to a maximal consistent set using Lindenbaum's construction
  and Henkin witnesses are added during the construction to ensure saturation as well.
  The resulting set is a Hintikka set which, by the model existence theorem, is satisfiable
  in the Herbrand universe.
*)

theory FOL_Axiomatic imports "HOL-Library.Countable" begin

section Syntax

datatype (params_tm: 'f) tm
  = Var nat (#)
  | Fun 'f 'f tm list ()

abbreviation Const () where a  a []

datatype (params_fm: 'f, 'p) fm
  = Falsity ()
  | Pre 'p 'f tm list ()
  | Imp ('f, 'p) fm ('f, 'p) fm (infixr  55)
  | Uni ('f, 'p) fm ()

abbreviation Neg (¬ _ [70] 70) where ¬ p  p  

term (  ''P'' [''f'' [#0]])

section Semantics

definition shift (__:_) where
  En:x m  if m < n then E m else if m = n then x else E (m-1)

primrec semantics_tm (_, _) where
  E, F (#n) = E n
| E, F (f ts) = F f (map E, F ts)

primrec semantics_fm (_, _, _) where
  _, _, _  = False
| E, F, G (P ts) = G P (map E, F ts)
| E, F, G (p  q) = (E, F, G p  E, F, G q)
| E, F, G (p) = (x. E0:x, F, G p)

proposition E, F, G ((P [# 0])  P [a])
  by (simp add: shift_def)

section Operations

subsection Shift

context fixes n m :: nat begin

lemma shift_eq [simp]: n = m  En:x m = x
  by (simp add: shift_def)

lemma shift_gt [simp]: m < n  En:x m = E m
  by (simp add: shift_def)

lemma shift_lt [simp]: n < m  En:x m = E (m-1)
  by (simp add: shift_def)

lemma shift_commute [simp]: (En:y0:x) = (E0:xn+1:y)
proof
  fix m
  show (En:y0:x) m = (E0:xn+1:y) m
    unfolding shift_def by (cases m) simp_all
qed

end

subsection Parameters

abbreviation params S  p  S. params_fm p

lemma upd_params_tm [simp]: f  params_tm t  E, F(f := x) t = E, F t
  by (induct t) (auto cong: map_cong)

lemma upd_params_fm [simp]: f  params_fm p  E, F(f := x), G p = E, F, G p
  by (induct p arbitrary: E) (auto cong: map_cong)

lemma finite_params_tm [simp]: finite (params_tm t)
  by (induct t) simp_all

lemma finite_params_fm [simp]: finite (params_fm p)
  by (induct p) simp_all

subsection Instantiation

primrec lift_tm () where
  (#n) = #(n+1)
| (f ts) = f (map  ts)

primrec inst_tm (_'/_) where
  s/m(#n) = (if n < m then #n else if n = m then s else #(n-1))
| s/m(f ts) = f (map s/m ts)

primrec inst_fm (_'/_) where
  _/_ = 
| s/m(P ts) = P (map s/m ts)
| s/m(p  q) = s/mp  s/mq
| s/m(p) = (s/m+1p)

lemma lift_lemma [simp]: E0:x, F (t) = E, F t
  by (induct t) (auto cong: map_cong)

lemma inst_tm_semantics [simp]: E, F (s/mt) = Em:E, F s, F t
  by (induct t) (auto cong: map_cong)

lemma inst_fm_semantics [simp]: E, F, G (t/mp) = Em:E, F t, F, G p
  by (induct p arbitrary: E m t) (auto cong: map_cong)

subsection Size

text The built-in size› is not invariant under substitution.

primrec size_fm where
  size_fm  = 1
| size_fm (_ _) = 1
| size_fm (p  q) = 1 + size_fm p + size_fm q
| size_fm (p) = 1 + size_fm p

lemma size_inst_fm [simp]: size_fm (t/mp) = size_fm p
  by (induct p arbitrary: m t) simp_all

section Propositional Semantics

primrec boolean where
  boolean _ _  = False
| boolean G _ (P ts) = G P ts
| boolean G A (p  q) = (boolean G A p  boolean G A q)
| boolean _ A (p) = A (p)

abbreviation tautology p  G A. boolean G A p

proposition tautology ((P [#0])  (P [#0]))
  by simp

lemma boolean_semantics: boolean (λa. G a  map E, F) E, F, G = E, F, G
proof
  fix p
  show boolean (λa. G a  map E, F) E, F, G p = E, F, G p
    by (induct p) simp_all
qed

lemma tautology[simp]: tautology p  E, F, G p
  using boolean_semantics by metis

proposition p. (E F G. E, F, G p)  ¬ tautology p
  by (metis boolean.simps(4) fm.simps(36) semantics_fm.simps(1,3,4))

section Calculus

text Adapted from System Q1 by Smullyan in First-Order Logic (1968).

inductive Axiomatic ( _ [50] 50) where
  TA: tautology p   p
| IA:  p  t/0p
| MP:  p  q   p   q
| GR:  q  a/0p  a  params {p, q}   q  p

text We simulate assumptions on the lhs of ⊢› with a chain of implications on the rhs.

primrec imply (infixr  56) where
  ([]  q) = q
| (p # ps  q) = (p  ps  q)

abbreviation Axiomatic_assms (_  _ [50, 50] 50) where
  ps  q   ps  q

section Soundness

theorem soundness:  p  E, F, G p
proof (induct p arbitrary: F rule: Axiomatic.induct)
  case (GR q a p)
  moreover from this have E, F(a := x), G (q  a/0p) for x
    by blast
  ultimately show ?case
    by fastforce
qed auto

corollary ¬ ( )
  using soundness by fastforce

section Derived Rules

lemma Imp1:  q  p  q
  and Imp2:  (p  q  r)  (p  q)  p  r
  and Neg:  ¬ ¬ p  p
  by (auto intro: TA)

text The tautology axiom TA is not used directly beyond this point.

lemma Tran':  (q  r)  (p  q)  p  r
  by (meson Imp1 Imp2 MP)

lemma Swap:  (p  q  r)  q  p  r
  by (meson Imp1 Imp2 Tran' MP)

lemma Tran:  (p  q)  (q  r)  p  r
  by (meson Swap Tran' MP)

text Note that contraposition in the other direction is an instance of the lemma Tran.

lemma contraposition:  (¬ q  ¬ p)  p  q
  by (meson Neg Swap Tran MP)

lemma GR':  ¬ a/0p  q  a  params {p, q}   ¬ (p)  q
proof -
  assume *:  ¬ a/0p  q and a: a  params {p, q}
  have  ¬ q  ¬ ¬ a/0p
    using * Tran MP by metis
  then have  ¬ q  a/0p
    using Neg Tran MP by metis
  then have  ¬ q  p
    using a by (auto intro: GR)
  then have  ¬ (p)  ¬ ¬ q
    using Tran MP by metis
  then show ?thesis
    using Neg Tran MP by metis
qed

lemma imply_ImpE:  ps  p  ps  (p  q)  ps  q
proof (induct ps)
  case Nil
  then show ?case
    by (metis Imp1 Swap MP imply.simps(1))
next
  case (Cons r ps)
  have  (r  ps  p)  r  ps  (p  q)  ps  q
    by (meson Cons.hyps Imp1 Imp2 MP)
  then have  (r  ps  p)  (r  ps  (p  q))  r  ps  q
    by (meson Imp1 Imp2 MP)
  then show ?case
    by simp
qed

lemma MP': ps  p  q  ps  p  ps  q
  using imply_ImpE MP by metis

lemma imply_Cons [intro]: ps  q  p # ps  q
  by (auto intro: MP Imp1)

lemma imply_head [intro]: p # ps  p
  by (induct ps) (metis Imp1 Imp2 MP imply.simps, metis Imp1 Imp2 MP imply.simps(2))

lemma add_imply [simp]:  q  ps  q
  using imply_head by (metis MP imply.simps(2))

lemma imply_mem [simp]: p  set ps  ps  p
  using imply_head imply_Cons by (induct ps) fastforce+

lemma deduct1: ps  p  q  p # ps  q
  by (meson MP' imply_Cons imply_head)

lemma imply_append [iff]: (ps @ qs  r) = (ps  qs  r)
  by (induct ps) simp_all

lemma imply_swap_append: ps @ qs  r  qs @ ps  r
proof (induct qs arbitrary: ps)
  case Cons
  then show ?case
    by (metis deduct1 imply.simps(2) imply_append)
qed simp

lemma deduct2: p # ps  q  ps  p  q
  by (metis imply.simps imply_append imply_swap_append)

lemmas deduct [iff] = deduct1 deduct2

lemma cut: p # ps  r  q # ps  p  q # ps  r
  by (meson MP' deduct(2) imply_Cons)

lemma Boole: (¬ p) # ps    ps  p
  by (meson MP' Neg add_imply deduct(2))

lemma imply_weaken: ps  q  set ps  set ps'  ps'  q
  by (induct ps arbitrary: q) (simp, metis MP' deduct(2) imply_mem insert_subset list.simps(15))

section Consistent

definition consistent S  S'. set S'  S  S'  

lemma UN_finite_bound:
  assumes finite A and 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

lemma split_list:
  assumes x  set A
  shows set (x # removeAll x A) = set A  x  set (removeAll x A)
  using assms by auto

lemma imply_params_fm: params_fm (ps  q) = params_fm q  (p  set ps. params_fm p)
  by (induct ps) auto

lemma inconsistent_fm:
  assumes consistent S and ¬ consistent ({p}  S)
  obtains S' where set S'  S and p # S'  
proof -
  obtain S' where S': set S'  {p}  S p  set S' S'  
    using assms unfolding consistent_def by blast
  then obtain S'' where S'': set (p # S'') = set S' p  set S''
    using split_list by metis
  then have p # S''  
    using S'   imply_weaken by blast
  then show ?thesis
    using that S'' S'(1) Diff_insert_absorb Diff_subset_conv list.simps(15) by metis
qed

lemma consistent_add_witness:
  assumes consistent S and ¬ (p)  S and a  params S
  shows consistent ({¬ a/0p}  S)
  unfolding consistent_def
proof
  assume S'. set S'  {¬ a/0p}  S  S'  
  then obtain S' where set S'  S and (¬ a/0p) # S'  
    using assms inconsistent_fm unfolding consistent_def by metis
  then have  ¬ a/0p  S'  
    by simp
  moreover have a  params_fm p
    using assms(2-3) by auto
  moreover have p  set S'. a  params_fm p
    using set S'  S assms(3) by auto
  then have a  params_fm (S'  )
    by (simp add: imply_params_fm)
  ultimately have  ¬ (p)  S'  
    using GR' by fast
  then have ¬ (p) # S'  
    by simp
  moreover have set ((¬ (p)) # S')  S
    using set S'  S assms(2) by simp
  ultimately show False
    using assms(1) unfolding consistent_def by blast
qed

lemma consistent_add_instance:
  assumes consistent S and p  S
  shows consistent ({t/0p}  S)
  unfolding consistent_def
proof
  assume S'. set S'  {t/0p}  S  S'  
  then obtain S' where set S'  S and t/0p # S'  
    using assms inconsistent_fm unfolding consistent_def by blast
  moreover have  p  t/0p
    using IA by blast
  ultimately have p # S'  
    by (meson add_imply cut deduct(1))
  moreover have set ((p) # S')  S
    using set S'  S assms(2) by simp
  ultimately show False
    using assms(1) unfolding consistent_def by blast
qed

section Extension

fun witness where
  witness used (¬ (p)) = {¬ (SOME a. a  used)/0p}
| witness _ _ = {}

primrec extend where
  extend S f 0 = S
| extend S f (Suc n) =
   (let Sn = extend S f n in
     if consistent ({f n}  Sn)
     then witness (params ({f n}  Sn)) (f n)  {f n}  Sn
     else Sn)

definition Extend S f  n. extend S f n

lemma extend_subset: S  extend S f n
  by (induct n) (fastforce simp: Let_def)+

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

lemma extend_bound: (n  m. extend S f n) = extend S f m
  by (induct m) (simp_all add: atMost_Suc Let_def)

lemma finite_params_witness [simp]: finite (params (witness used p))
  by (induct used p rule: witness.induct) simp_all

lemma finite_params_extend [simp]: finite (params (extend S f n) - params S)
  by (induct n) (simp_all add: Let_def Un_Diff)

lemma Set_Diff_Un: X - (Y  Z) = X - Y - Z
  by blast

lemma infinite_params_extend:
  assumes infinite (UNIV - params S)
  shows infinite (UNIV - params (extend S f n))
proof -
  have finite (params (extend S f n) - params S)
    by simp
  then obtain extra where finite extra params (extend S f n) = extra  params S
    using extend_subset by fast
  then have ?thesis = infinite (UNIV - (extra  params S))
    by simp
  also have  = infinite (UNIV - extra - params S)
    by (simp add: Set_Diff_Un)
  also have  = infinite (UNIV - params S)
    using finite extra by (metis Set_Diff_Un Un_commute finite_Diff2)
  finally show ?thesis
    using assms ..
qed

lemma consistent_witness:
  assumes consistent S and p  S and params S  used
    and infinite (UNIV - used)
  shows consistent (witness used p  S)
  using assms
proof (induct used p rule: witness.induct)
  case (1 used p)
  moreover have a. a  used
    using 1(4) by (meson Diff_iff finite_params_fm finite_subset subset_iff)
  ultimately obtain a where a: witness used (¬ (p)) = {¬ a/0p} and a  used
    by (metis someI_ex witness.simps(1))
  then have a  params S
    using 1(3) by fast
  then show ?case
    using 1(1-2) a(1) consistent_add_witness by metis
qed (auto simp: assms)

lemma consistent_extend:
  assumes consistent S and infinite (UNIV - params S)
  shows consistent (extend S f n)
proof (induct n)
  case (Suc n)
  have infinite (UNIV - params (extend S f n))
    using assms(2) infinite_params_extend by fast
  with finite_params_fm have infinite (UNIV - (params_fm (f n)  params (extend S f n)))
    by (metis Set_Diff_Un Un_commute finite_Diff2)
  with Suc consistent_witness[where S={f n}  extend S f n] show ?case
    by (simp add: Let_def)
qed (use assms(1) in simp)

lemma consistent_Extend:
  assumes consistent S and infinite (UNIV - params S)
  shows consistent (Extend S f)
  unfolding consistent_def
proof
  assume S'. set S'  Extend S f  S'  
  then obtain S' where S'   and set S'  Extend S f
    unfolding consistent_def by blast
  then obtain m where set S'  (n  m. extend S f n)
    unfolding Extend_def using UN_finite_bound by (metis 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 S'   by blast
qed

section Maximal

definition maximal S  p. p  S  ¬ consistent ({p}  S)

lemma maximal_exactly_one:
  assumes consistent S and maximal S
  shows p  S  (¬ p)  S
proof
  assume p  S
  show (¬ p)  S
  proof
    assume (¬ p)  S
    then have set [p, ¬ p]  S
      using p  S by simp
    moreover have [p, ¬ p]  
      by blast
    ultimately show False
      using consistent S unfolding consistent_def by blast
  qed
next
  assume (¬ p)  S
  then have ¬ consistent ({¬ p}  S)
    using maximal S unfolding maximal_def by blast
  then obtain S' where set S'  S (¬ p) # S'  
    using consistent S inconsistent_fm by blast
  then have S'  p
    using Boole by blast
  have consistent ({p}  S)
    unfolding consistent_def
  proof
    assume S'. set S'  {p}  S  S'  
    then obtain S'' where set S''  S and p # S''  
      using assms inconsistent_fm unfolding consistent_def by blast
    then have S' @ S''  
      using S'  p by (metis MP' add_imply imply.simps(2) imply_append)
    moreover have set (S' @ S'')  S
      using set S'  S set S''  S by simp
    ultimately show False
      using consistent S unfolding consistent_def by blast
  qed
  then show p  S
    using maximal S unfolding maximal_def by blast
qed

lemma maximal_Extend:
  assumes surj f
  shows maximal (Extend S f)
  unfolding maximal_def
proof safe
  fix p
  assume p  Extend S f and consistent ({p}  Extend S f)
  obtain k where k: f k = p
    using surj f unfolding surj_def by metis
  then have p  extend S f (Suc k)
    using p  Extend S f unfolding Extend_def by blast
  then have ¬ consistent ({p}  extend S f k)
    using k by (auto simp: Let_def)
  moreover have {p}  extend S f k  {p}  Extend S f
    unfolding Extend_def by blast
  ultimately have ¬ consistent ({p}  Extend S f)
    unfolding consistent_def by auto
  then show False
    using consistent ({p}  Extend S f) by blast
qed

section Saturation

definition saturated S  p. ¬ (p)  S  (a. (¬ a/0p)  S)

lemma saturated_Extend:
  assumes consistent (Extend S f) and surj f
  shows saturated (Extend S f)
  unfolding saturated_def
proof safe
  fix p
  assume *: ¬ (p)  Extend S f
  obtain k where k: f k = ¬ (p)
    using surj f unfolding surj_def by metis
  have extend S f k  Extend S f
    unfolding Extend_def by auto
  then have consistent ({¬ (p)}  extend S f k)
    using assms(1) * unfolding consistent_def by blast
  then have a. extend S f (Suc k) = {¬ a/0p}  {¬ (p)}  extend S f k
    using k by (auto simp: Let_def)
  moreover have extend S f (Suc k)  Extend S f
    unfolding Extend_def by blast
  ultimately show a. ¬  a/0p  Extend S f
    by blast
qed

section Hintikka

locale Hintikka =
  fixes H :: ('f, 'p) fm set
  assumes
    FlsH:   H and
    ImpH: (p  q)  H  (p  H  q  H) and
    UniH: (p  H)  (t. t/0p  H)

subsection Model Existence

abbreviation hmodel (_) where H  #, , λP ts. P ts  H

lemma semantics_tm_id [simp]: #,  t = t
  by (induct t) (auto cong: map_cong)

lemma semantics_tm_id_map [simp]: map #,  ts = ts
  by (auto cong: map_cong)

theorem Hintikka_model:
  assumes Hintikka H
  shows p  H  H p
proof (induct p rule: wf_induct[where r=measure size_fm])
  case 1
  then show ?case ..
next
  case (2 x)
  then show ?case
    using assms unfolding Hintikka_def by (cases x) auto
qed

subsection Maximal Consistent Sets are Hintikka Sets

lemma deriv_iff_MCS:
  assumes consistent S and maximal S
  shows (ps. set ps  S  ps  p)  p  S
proof
  from assms maximal_exactly_one[OF assms(1)] show ps. set ps  S  ps  p  p  S
    unfolding consistent_def using MP add_imply deduct1 imply.simps(1) imply_ImpE
    by (metis insert_absorb insert_mono list.simps(15))
next
  show p  S  ps. set ps  S  ps  p
    using imply_head by (metis empty_subsetI insert_absorb insert_mono list.set(1) list.simps(15))
qed

lemma Hintikka_Extend:
  assumes consistent H and maximal H and saturated H
  shows Hintikka H
proof
  show   H
    using assms deriv_iff_MCS unfolding consistent_def by fast
next
  fix p q
  show (p  q)  H  (p  H  q  H)
    using deriv_iff_MCS[OF assms(1-2)] maximal_exactly_one[OF assms(1-2)]
    by (metis Imp1 contraposition add_imply deduct1 insert_subset list.simps(15))
next
  fix p
  show (p  H)  (t. t/0p  H)
    using assms consistent_add_instance maximal_exactly_one
    unfolding maximal_def saturated_def by metis
qed

section Countable Formulas

instance tm :: (countable) countable
  by countable_datatype

instance fm :: (countable, countable) countable
  by countable_datatype

section Completeness

lemma infinite_Diff_fin_Un: infinite (X - Y)  finite Z  infinite (X - (Z  Y))
  by (simp add: Set_Diff_Un Un_commute)

theorem strong_completeness:
  fixes p :: ('f :: countable, 'p :: countable) fm
  assumes (E :: _  'f tm) F G. (q  X. E, F, G q)  E, F, G p
    and infinite (UNIV - params X)
  shows ps. set ps  X  ps  p
proof (rule ccontr)
  assume ps. set ps  X  ps  p
  then have *: ps. set ps  X  ((¬ p) # ps  )
    using Boole by blast

  let ?S = {¬ p}  X
  let ?H = Extend ?S from_nat

  from inconsistent_fm have consistent ?S
    unfolding consistent_def using * imply_Cons by metis
  moreover have infinite (UNIV - params ?S)
    using assms(2) finite_params_fm by (simp add: infinite_Diff_fin_Un)
  ultimately have consistent ?H and maximal ?H
    using consistent_Extend maximal_Extend surj_from_nat by blast+
  moreover from this have saturated ?H
    using saturated_Extend by fastforce
  ultimately have Hintikka ?H
    using assms(2) Hintikka_Extend by blast

  have ?H p if p  ?S for p
    using that Extend_subset Hintikka_model Hintikka ?H by blast
  then have ?H (¬ p) and q  X. ?H q
    by blast+
  moreover from this have ?H p
    using assms(1) by blast
  ultimately show False
    by simp
qed

theorem completeness:
  fixes p :: (nat, nat) fm
  assumes (E :: nat  nat tm) F G. E, F, G p
  shows  p
  using assms strong_completeness[where X={}] by auto

section Main Result

abbreviation valid :: (nat, nat) fm  bool where
  valid p  (E :: nat  nat tm) F G. E, F, G p

theorem main: valid p  ( p)
  using completeness soundness by blast

end