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
  ‹E⟨n: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. ⟦E⟨0: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 ⟹ E⟨n:x⟩ m = x›
  by (simp add: shift_def)

lemma shift_gt [simp]: ‹m < n ⟹ E⟨n:x⟩ m = E m›
  by (simp add: shift_def)

lemma shift_lt [simp]: ‹n < m ⟹ E⟨n:x⟩ m = E (m-1)›
  by (simp add: shift_def)

lemma shift_commute [simp]: ‹(E⟨n:y⟩⟨0:x⟩) = (E⟨0:x⟩⟨n+1:y⟩)›
proof
  fix m
  show ‹(E⟨n:y⟩⟨0:x⟩) m = (E⟨0:x⟩⟨n+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/m⟩p ❙⟶ ⟨s/m⟩q›
| ‹⟨s/m⟩(❙∀p) = ❙∀(⟨❙↑s/m+1⟩p)›

lemma lift_lemma [simp]: ‹⦇E⟨0:x⟩, F⦈ (❙↑t) = ⦇E, F⦈ t›
  by (induct t) (auto cong: map_cong)

lemma inst_tm_semantics [simp]: ‹⦇E, F⦈ (⟪s/m⟫t) = ⦇E⟨m:⦇E, F⦈ s⟩, F⦈ t›
  by (induct t) (auto cong: map_cong)

lemma inst_fm_semantics [simp]: ‹⟦E, F, G⟧ (⟨t/m⟩p) = ⟦E⟨m:⦇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/m⟩p) = 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/0⟩p›
| MP: ‹⊢ p ❙⟶ q ⟹ ⊢ p ⟹ ⊢ q›
| GR: ‹⊢ q ❙⟶ ⟨❙⋆a/0⟩p ⟹ 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/0⟩p)› 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/0⟩p ❙⟶ q ⟹ a ∉ params {p, q} ⟹ ⊢ ❙¬ (❙∀p) ❙⟶ q›
proof -
  assume *: ‹⊢ ❙¬ ⟨❙⋆a/0⟩p ❙⟶ q› and a: ‹a ∉ params {p, q}›
  have ‹⊢ ❙¬ q ❙⟶ ❙¬ ❙¬ ⟨❙⋆a/0⟩p›
    using * Tran MP by metis
  then have ‹⊢ ❙¬ q ❙⟶ ⟨❙⋆a/0⟩p›
    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/0⟩p} ∪ S)›
  unfolding consistent_def
proof
  assume ‹∃S'. set S' ⊆ {❙¬ ⟨❙⋆a/0⟩p} ∪ S ∧ S' ⊢ ❙⊥›
  then obtain S' where ‹set S' ⊆ S› and ‹(❙¬ ⟨❙⋆a/0⟩p) # S' ⊢ ❙⊥›
    using assms inconsistent_fm unfolding consistent_def by metis
  then have ‹⊢ ❙¬ ⟨❙⋆a/0⟩p ❙⟶ 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/0⟩p} ∪ S)›
  unfolding consistent_def
proof
  assume ‹∃S'. set S' ⊆ {⟨t/0⟩p} ∪ S ∧ S' ⊢ ❙⊥›
  then obtain S' where ‹set S' ⊆ S› and ‹⟨t/0⟩p # S' ⊢ ❙⊥›
    using assms inconsistent_fm unfolding consistent_def by blast
  moreover have ‹⊢ ❙∀p ❙⟶ ⟨t/0⟩p›
    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)/0⟩p}›
| ‹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/0⟩p}› 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/0⟩p) ∈ 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/0⟩p} ∪ {❙¬ (❙∀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/0⟩p ∈ 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/0⟩p ∈ 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/0⟩p ∈ 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