Theory FOL_Axiomatic_Variant

(*
  File:      FOL_Axiomatic_Variant.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.

  This variant uses free variables as Henkin witnesses. This gives completeness for syntax
  with only finitely many available constants.
*)

theory FOL_Axiomatic_Variant imports "HOL-Library.Countable" begin

section ‹Syntax›

datatype 'f tm
  = Var nat (‹❙#›)
  | Fun 'f ‹'f tm list› (‹❙†›)

datatype ('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 :: ‹(nat ⇒ 'a) ⇒ nat ⇒ 'a ⇒ nat ⇒ 'a›
  (‹_⟨_:_⟩› [90, 0, 0] 91) 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›

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

subsection ‹Variables›

primrec vars_tm where
  ‹vars_tm (❙#n) = [n]›
| ‹vars_tm (❙†_ ts) = concat (map vars_tm ts)›

primrec vars_fm where
  ‹vars_fm ❙⊥ = []›
| ‹vars_fm (❙‡_ ts) = concat (map vars_tm ts)›
| ‹vars_fm (p ❙⟶ q) = vars_fm p @ vars_fm q›
| ‹vars_fm (❙∀p) = vars_fm p›

abbreviation ‹vars S ≡ ⋃p ∈ S. set (vars_fm p)›

primrec max_list :: ‹nat list ⇒ nat› where
  ‹max_list [] = 0›
| ‹max_list (x # xs) = max x (max_list xs)›

lemma max_list_append: ‹max_list (xs @ ys) = max (max_list xs) (max_list ys)›
  by (induct xs) auto

lemma upd_vars_tm [simp]: ‹n ∉ set (vars_tm t) ⟹ ⦇E(n := x), F⦈ t = ⦇E, F⦈ t›
  by (induct t) (auto cong: map_cong)

lemma shift_upd_commute: ‹m ≤ n ⟹ (E(n := x)⟨m:y⟩) = ((E⟨m:y⟩)(n + 1 := x))›
  unfolding shift_def by fastforce

lemma max_list_concat: ‹xs ∈ set xss ⟹ max_list xs ≤ max_list (concat xss)›
  by (induct xss) (auto simp: max_list_append)

lemma max_list_in: ‹max_list xs < n ⟹ n ∉ set xs›
  by (induct xs) auto

lemma upd_vars_fm [simp]: ‹max_list (vars_fm p) < n ⟹ ⟦E(n := x), F, G⟧ p = ⟦E, F, G⟧ p›
proof (induct p arbitrary: E n)
  case (Pre P ts)
  moreover have ‹max_list (concat (map vars_tm ts)) < n›
    using Pre.prems max_list_concat by simp
  then have ‹n ∉ set (concat (map vars_tm ts))›
    using max_list_in by blast
  then have ‹∀t ∈ set ts. n ∉ set (vars_tm t)›
    by simp
  ultimately show ?case
    using upd_vars_tm by (metis list.map_cong semantics_fm.simps(2))
next
  case (Uni p)
  have ‹?case = ((∀y. ⟦E(n := x)⟨0:y⟩, F, G⟧ p) = (∀y. ⟦E⟨0:y⟩, F, G⟧ p))›
    by (simp add: fun_upd_def)
  also have ‹… = ((∀y. ⟦(E⟨0:y⟩)(n + 1 := x), F, G⟧ p) = (∀y. ⟦E⟨0:y⟩, F, G⟧ p))›
    by (simp add: shift_upd_commute)
  finally show ?case
    using Uni by fastforce
qed (auto simp: max_list_append cong: map_cong)

abbreviation ‹max_var p ≡ max_list (vars_fm p)›

subsection ‹Instantiation›

primrec lift_tm (‹❙↑›) where
  ‹❙↑(❙#n) = ❙#(n+1)›
| ‹❙↑(❙†f ts) = ❙†f (map ❙↑ ts)›

primrec inst_tm (‹_'⟪_'/_'⟫› [90, 0, 0] 91) where
  ‹(❙#n)⟪s/m⟫ = (if n < m then ❙#n else if n = m then s else ❙#(n-1))›
| ‹(❙†f ts)⟪s/m⟫ = ❙†f (map (λt. t⟪s/m⟫) ts)›

primrec inst_fm (‹_'⟨_'/_'⟩› [90, 0, 0] 91) where
  ‹❙⊥⟨_/_⟩ = ❙⊥›
| ‹(❙‡P ts)⟨s/m⟩ = ❙‡P (map (λt. t⟪s/m⟫) ts)›
| ‹(p ❙⟶ q)⟨s/m⟩ = (p⟨s/m⟩ ❙⟶ q⟨s/m⟩)›
| ‹(❙∀p)⟨s/m⟩ = ❙∀(p⟨❙↑s/m+1⟩)›

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⦈ (t⟪s/m⟫) = ⦇E⟨m:⦇E, F⦈ s⟩, F⦈ t›
  by (induct t) (auto cong: map_cong)

lemma inst_fm_semantics [simp]: ‹⟦E, F, G⟧ (p⟨t/m⟩) = ⟦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 (p⟨t/m⟩) = size_fm p›
  by (induct p arbitrary: m t) auto

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: ‹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 ❙⟶ p⟨t/0⟩›
| MP: ‹⊢ p ❙⟶ q ⟹ ⊢ p ⟹ ⊢ q›
| GR: ‹⊢ q ❙⟶ p⟨❙#n/0⟩ ⟹ max_var p < n ⟹ max_var q < n ⟹ ⊢ q ❙⟶ ❙∀p›

lemmas
  TA[simp]
  MP[trans, dest]
  GR[intro]

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: E F rule: Axiomatic.induct)
  case (GR q p n)
  then have ‹⟦E(n := x), F, G⟧ (q ❙⟶ p⟨❙#n/0⟩)› for x
    by blast
  then have ‹⟦E(n := x), F, G⟧ q ⟶ ⟦E(n := x), F, G⟧ (p⟨❙#n/0⟩)› for x
    by simp
  then have ‹⟦E, F, G⟧ q ⟶ ⟦E(n := x), F, G⟧ (p⟨❙#n/0⟩)› for x
    using GR.hyps(3-4) by simp
  then have ‹⟦E, F, G⟧ q ⟶ (∀x. ⟦E(n := x), F, G⟧ (p⟨❙#n/0⟩))›
    by blast
  then have ‹⟦E, F, G⟧ q ⟶ (∀x. ⟦E(n := x)⟨0:x⟩, F, G⟧ p)›
    by simp
  then have ‹⟦E, F, G⟧ q ⟶ (∀x. ⟦(E⟨0:x⟩)(n + 1 := x), F, G⟧ p)›
    using shift_upd_commute by (metis zero_le)
  moreover have ‹max_list (vars_fm p) < n›
    using GR.hyps(3) by (simp add: max_list_append)
  ultimately have ‹⟦E, F, G⟧ q ⟶ (∀x. ⟦E⟨0:x⟩, F, G⟧ p)›
    using upd_vars_fm by simp
  then show ?case
    by simp
qed (auto simp: tautology)

corollary ‹¬ (⊢ ❙⊥)›
  using soundness by fastforce

section ‹Derived Rules›

lemma AS: ‹⊢ (p ❙⟶ q ❙⟶ r) ❙⟶ (p ❙⟶ q) ❙⟶ p ❙⟶ r›
  by auto

lemma AK: ‹⊢ q ❙⟶ p ❙⟶ q›
  by auto

lemma Neg: ‹⊢ ❙¬ ❙¬ p ❙⟶ p›
  by auto

lemma contraposition:
  ‹⊢ (p ❙⟶ q) ❙⟶ ❙¬ q ❙⟶ ❙¬ p›
  ‹⊢ (❙¬ q ❙⟶ ❙¬ p) ❙⟶ p ❙⟶ q›
  by (auto intro: TA)

lemma GR': ‹⊢ ❙¬ p⟨❙#n/0⟩ ❙⟶ q ⟹ max_var p < n ⟹ max_var q < n ⟹ ⊢ ❙¬ ❙∀p ❙⟶ q›
proof -
  assume *: ‹⊢ ❙¬ p⟨❙#n/0⟩ ❙⟶ q› and n: ‹max_var p < n› ‹max_var q < n›
  have ‹⊢ ❙¬ q ❙⟶ ❙¬ ❙¬ p⟨❙#n/0⟩›
    using * contraposition(1) by fast
  then have ‹⊢ ❙¬ q ❙⟶ p⟨❙#n/0⟩›
    by (meson AK AS MP Neg)
  then have ‹⊢ ❙¬ q ❙⟶ ❙∀p›
    using n by auto
  then have ‹⊢ ❙¬ ❙∀p ❙⟶ ❙¬ ❙¬ q›
    using contraposition(1) by fast
  then show ?thesis
    by (meson AK AS MP Neg)
qed

lemma Imp3: ‹⊢ (p ❙⟶ q ❙⟶ r) ❙⟶ ((s ❙⟶ p) ❙⟶ (s ❙⟶ q) ❙⟶ s ❙⟶ r)›
  by auto

lemma imply_ImpE: ‹⊢ ps ❙↝ p ❙⟶ ps ❙↝ (p ❙⟶ q) ❙⟶ ps ❙↝ q›
  by (induct ps) (auto intro: Imp3 MP)

lemma MP' [trans, dest]: ‹ps ⊢ p ❙⟶ q ⟹ ps ⊢ p ⟹ ps ⊢ q›
  using imply_ImpE by fast

lemma imply_Cons [intro]: ‹ps ⊢ q ⟹ p # ps ⊢ q›
  by (auto intro: MP AK)

lemma imply_head [intro]: ‹p # ps ⊢ p›
proof (induct ps)
  case (Cons q ps)
  then show ?case
    by (metis AK MP' imply.simps(1-2))
qed auto

lemma imply_lift_Imp [simp]:
  assumes ‹⊢ p ❙⟶ q›
  shows ‹⊢ p ❙⟶ ps ❙↝ q›
  using assms MP MP' imply_head by (metis imply.simps(2))

lemma add_imply [simp]: ‹⊢ q ⟹ ps ⊢ q›
  using MP imply_head by (auto simp del: TA)

lemma imply_mem [simp]: ‹p ∈ set ps ⟹ ps ⊢ p›
proof (induct ps)
  case (Cons q ps)
  then show ?case
    by (metis imply_Cons imply_head set_ConsD)
qed simp

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 q qs)
  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(1-2) imply_append imply_swap_append)

lemmas deduct [iff] = deduct1 deduct2

lemma cut [trans, dest]: ‹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›
proof (induct ps arbitrary: q)
  case (Cons p ps)
  then show ?case
    by (metis MP' deduct(2) imply_mem insert_subset list.simps(15))
qed simp

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_vars_fm: ‹vars_fm (ps ❙↝ q) = concat (map vars_fm ps) @ vars_fm q›
  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)
    by (metis Diff_insert_absorb Diff_subset_conv list.simps(15))
qed

definition max_set :: ‹nat set ⇒ nat› where
  ‹max_set X ≡ if X = {} then 0 else Max X›

lemma max_list_in_Cons: ‹xs ≠ [] ⟹ max_list xs ∈ set xs›
proof (induct xs)
  case Nil
  then show ?case
    by simp
next
  case (Cons x xs)
  then show ?case
    by (metis linorder_not_less list.set_intros(1-2) max.absorb2 max.absorb3
        max_list.simps(1-2) max_nat.right_neutral)
qed

lemma max_list_max: ‹∀x ∈ set xs. x ≤ max_list xs›
  by (induct xs) auto

lemma max_list_in_set: ‹finite S ⟹ set xs ⊆ S ⟹ max_list xs ≤ max_set S›
  unfolding max_set_def using max_list_in_Cons
  by (metis (mono_tags, lifting) Max_ge bot.extremum_uniqueI bot_nat_0.extremum max_list.simps(1)
      set_empty subsetD)

lemma consistent_add_witness:
  assumes ‹consistent S› and ‹(❙¬ ❙∀p) ∈ S›
    and ‹finite (vars S)› and ‹max_set (vars S) < n›
  shows ‹consistent ({❙¬ p⟨❙#n/0⟩} ∪ S)›
  unfolding consistent_def
proof
  assume ‹∃S'. set S' ⊆ {❙¬ p⟨❙#n/0⟩} ∪ S ∧ S' ⊢ ❙⊥›
  then obtain S' where ‹set S' ⊆ S› and ‹(❙¬ p⟨❙#n/0⟩) # S' ⊢ ❙⊥›
    using assms inconsistent_fm unfolding consistent_def by metis
  then have ‹⊢ ❙¬ p⟨❙#n/0⟩ ❙⟶ S' ❙↝ ❙⊥›
    by simp
  moreover have ‹max_list (vars_fm p) < n›
    using assms(2-4) max_list_in_set by fastforce
  moreover have ‹∀p ∈ set S'. max_list (vars_fm p) < n›
    using ‹set S' ⊆ S› assms(3-4) max_list_in_set
    by (meson Union_upper image_eqI order_le_less_trans subsetD)
  then have ‹max_list (concat (map vars_fm S')) < n›
    using assms(4) by (induct S') (auto simp: max_list_append)
  then have ‹max_list (vars_fm (S' ❙↝ ❙⊥)) < n›
    unfolding imply_vars_fm max_list_append by simp
  ultimately have ‹⊢ ❙¬ ❙∀p ❙⟶ S' ❙↝ ❙⊥›
    using GR' unfolding max_list_append by auto
  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 ({p⟨t/0⟩} ∪ S)›
  unfolding consistent_def
proof
  assume ‹∃S'. set S' ⊆ {p⟨t/0⟩} ∪ S ∧ S' ⊢ ❙⊥›
  then obtain S' where ‹set S' ⊆ S› and ‹p⟨t/0⟩ # S' ⊢ ❙⊥›
    using assms inconsistent_fm unfolding consistent_def by blast
  moreover have ‹⊢ ❙∀p ❙⟶ p⟨t/0⟩›
    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) = {❙¬ p⟨❙#(SOME n. max_set used < n)/0⟩}›
| ‹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 (vars ({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›
  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_vars_witness [simp]: ‹finite (vars (witness used p))›
  by (induct used p rule: witness.induct) simp_all

lemma finite_vars_extend [simp]: ‹finite (vars S) ⟹ finite (vars (extend S f n))›
  by (induct n) (simp_all add: Let_def)

lemma max_list_mono: ‹set xs ⊆ set ys ⟹ max_list xs ≤ max_list ys›
  using max_list_max max_list_in_Cons
  by (metis less_nat_zero_code linorder_not_le max_list.simps(1) subset_code(1))

lemma consistent_witness:
  fixes p :: ‹('f, 'p) fm›
  assumes ‹consistent S› and ‹p ∈ S› and ‹vars S ⊆ used› and ‹finite used›
  shows ‹consistent (witness used p ∪ S)›
  using assms
proof (induct used p rule: witness.induct)
  case (1 used p)
  moreover have ‹∃n. max_set used < n›
    by blast
  ultimately obtain n where n: ‹witness used (❙¬ ❙∀p) = {❙¬ p⟨❙#n/0⟩}› and ‹max_set used < n›
    by (metis someI_ex witness.simps(1))
  then have ‹max_set (vars S) < n›
    using 1(3-4) max_list_mono order_le_less_trans
    by (metis (no_types, lifting) Max.subset_imp bot.extremum_uniqueI less_nat_zero_code linorder_neqE_nat max_set_def)
  moreover have ‹finite (vars S)›
    using 1(3-4) infinite_super by blast
  ultimately show ?case
    using 1 n(1) consistent_add_witness by metis
qed (auto simp: assms)

lemma consistent_extend:
  fixes f :: ‹nat ⇒ ('f, 'p) fm›
  assumes ‹consistent S› ‹finite (vars S)›
  shows ‹consistent (extend S f n)›
  using assms
proof (induct n)
  case (Suc n)
  then show ?case
    using consistent_witness[where S=‹{f n} ∪ _›] by (auto simp: Let_def)
qed simp

lemma consistent_Extend:
  fixes f :: ‹nat ⇒ ('f, 'p) fm›
  assumes ‹consistent S› ‹finite (vars 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 List.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)›
proof (rule ccontr)
  assume ‹¬ maximal (Extend S f)›
  then obtain p where
    ‹p ∉ Extend S f› and ‹consistent ({p} ∪ Extend S f)›
    unfolding maximal_def using assms consistent_Extend by blast
  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 ⟶ (∃n. (❙¬ p⟨❙#n/0⟩) ∈ S)›

lemma saturated_Extend:
  assumes ‹consistent (Extend S f)› and ‹surj f›
  shows ‹saturated (Extend S f)›
proof (rule ccontr)
  assume ‹¬ saturated (Extend S f)›
  then obtain p where p: ‹(❙¬ ❙∀p) ∈ Extend S f› ‹∄n. (❙¬ p⟨❙#n/0⟩) ∈ Extend S f›
    unfolding saturated_def by blast
  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) p(1) unfolding consistent_def by blast
  then have ‹∃n. extend S f (Suc k) = {❙¬ p⟨❙#n/0⟩} ∪ {❙¬ ❙∀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 False
    using p(2) by auto
qed

section ‹Hintikka›

locale Hintikka =
  fixes H :: ‹('f, 'p) fm set›
  assumes
    NoFalsity: ‹❙⊥ ∉ H› and
    ImpP: ‹(p ❙⟶ q) ∈ H ⟹ p ∉ H ∨ q ∈ H› and
    ImpN: ‹(p ❙⟶ q) ∉ H ⟹ p ∈ H ∧ q ∉ H› and
    UniP: ‹❙∀p ∈ H ⟹ ∀t. p⟨t/0⟩ ∈ H› and
    UniN: ‹❙∀p ∉ H ⟹ ∃n. p⟨❙#n/0⟩ ∉ H›

subsection ‹Model Existence›

abbreviation hmodel (‹⟦_⟧›) where ‹⟦H⟧ ≡ ⟦❙#, ❙†, λP ts. Pre 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)
  show ‹x ∈ H ⟷ ⟦H⟧ x›
  proof (cases x; safe)
    case Falsity
    assume ‹❙⊥ ∈ H›
    then have False
      using assms Hintikka.NoFalsity by fast
    then show ‹⟦H⟧ ❙⊥› ..
  next
    case Falsity
    assume ‹⟦H⟧ ❙⊥›
    then have False
      by simp
    then show ‹❙⊥ ∈ H› ..
  next
    case (Pre P ts)
    assume ‹❙‡P ts ∈ H›
    then show ‹⟦H⟧ (❙‡P ts)›
      by simp
  next
    case (Pre P ts)
    assume ‹⟦H⟧ (❙‡P ts)›
    then show ‹❙‡P ts ∈ H›
      by simp
  next
    case (Imp p q)
    assume ‹(p ❙⟶ q) ∈ H›
    then have ‹p ∉ H ∨ q ∈ H›
      using assms Hintikka.ImpP by blast
    then have ‹¬ ⟦H⟧ p ∨ ⟦H⟧ q›
      using 2 Imp by simp
    then show ‹⟦H⟧ (p ❙⟶ q)›
      by simp
  next
    case (Imp p q)
    assume ‹⟦H⟧ (p ❙⟶ q)›
    then have ‹¬ ⟦H⟧ p ∨ ⟦H⟧ q›
      by simp
    then have ‹p ∉ H ∨ q ∈ H›
      using 2 Imp by simp
    then show ‹(p ❙⟶ q) ∈ H›
      using assms Hintikka.ImpN by blast
  next
    case (Uni p)
    assume ‹❙∀p ∈ H›
    then have ‹∀t. p⟨t/0⟩ ∈ H›
      using assms Hintikka.UniP by metis
    then have ‹∀t. ⟦H⟧ (p⟨t/0⟩)›
      using 2 Uni by simp
    then show ‹⟦H⟧ (❙∀p)›
      by simp
  next
    case (Uni p)
    assume ‹⟦H⟧ (❙∀p)›
    then have ‹∀t. ⟦H⟧ (p⟨t/0⟩)›
      by simp
    then have ‹∀t. p⟨t/0⟩ ∈ H›
      using 2 Uni by simp
    then show ‹❙∀p ∈ H›
      using assms Hintikka.UniN by blast
  qed
qed

subsection ‹Maximal Consistent Sets are Hintikka Sets›

lemma inconsistent_head:
  assumes ‹consistent S› and ‹maximal S› and ‹p ∉ S›
  obtains S' where ‹set S' ⊆ S› and ‹p # S' ⊢ ❙⊥›
  using assms inconsistent_fm unfolding consistent_def maximal_def by metis

lemma inconsistent_parts [simp]:
  assumes ‹ps ⊢ ❙⊥› and ‹set ps ⊆ S›
  shows ‹¬ consistent S›
  using assms unfolding consistent_def by blast

lemma Hintikka_Extend:
  fixes H :: ‹('f, 'p) fm set›
  assumes ‹consistent H› and ‹maximal H› and ‹saturated H›
  shows ‹Hintikka H›
proof
  show ‹❙⊥ ∉ H›
  proof
    assume ‹❙⊥ ∈ H›
    moreover have ‹[❙⊥] ⊢ ❙⊥›
      by blast
    ultimately have ‹¬ consistent H›
      using inconsistent_parts[where ps=‹[❙⊥]›] by simp
    then show False
      using ‹consistent H› ..
  qed
next
  fix p q
  assume *: ‹(p ❙⟶ q) ∈ H›
  show ‹p ∉ H ∨ q ∈ H›
  proof safe
    assume ‹q ∉ H›
    then obtain Hq' where Hq': ‹q # Hq' ⊢ ❙⊥› ‹set Hq' ⊆ H›
      using assms inconsistent_head by metis

    assume ‹p ∈ H›
    then have ‹(❙¬ p) ∉ H›
      using assms maximal_exactly_one by blast
    then obtain Hp' where Hp': ‹(❙¬ p) # Hp' ⊢ ❙⊥› ‹set Hp' ⊆ H›
      using assms inconsistent_head by metis

    let ?H' = ‹Hp' @ Hq'›
    have H': ‹set ?H' = set Hp' ∪ set Hq'›
      by simp
    then have ‹set Hp' ⊆ set ?H'› and ‹set Hq' ⊆ set ?H'›
      by blast+
    then have ‹(❙¬ p) # ?H' ⊢ ❙⊥› and ‹q # ?H' ⊢ ❙⊥›
      using Hp'(1) Hq'(1) deduct imply_weaken by metis+
    then have ‹(p ❙⟶ q) # ?H' ⊢ ❙⊥›
      using Boole imply_Cons imply_head MP' cut by metis
    moreover have ‹set ((p ❙⟶ q) # ?H') ⊆ H›
      using ‹q ∉ H› *(1) H' Hp'(2) Hq'(2) by auto
    ultimately show False
      using assms unfolding consistent_def by blast
  qed
next
  fix p q
  assume *: ‹(p ❙⟶ q) ∉ H›
  show ‹p ∈ H ∧ q ∉ H›
  proof (safe, rule ccontr)
    assume ‹p ∉ H›
    then obtain H' where S': ‹p # H' ⊢ ❙⊥› ‹set H' ⊆ H›
      using assms inconsistent_head by metis
    moreover have ‹(❙¬ (p ❙⟶ q)) # H' ⊢ p›
      by auto
    ultimately have ‹(❙¬ (p ❙⟶ q)) # H' ⊢ ❙⊥›
      by blast
    moreover have ‹set ((❙¬ (p ❙⟶ q)) # H') ⊆ H›
      using *(1) S'(2) assms maximal_exactly_one by auto
    ultimately show False
      using assms unfolding consistent_def by blast
  next
    assume ‹q ∈ H›
    then have ‹(❙¬ q) ∉ H›
      using assms maximal_exactly_one by blast
    then obtain H' where H': ‹(❙¬ q) # H' ⊢ ❙⊥› ‹set H' ⊆ H›
      using assms inconsistent_head by metis
    moreover have ‹(❙¬ (p ❙⟶ q)) # H' ⊢ ❙¬ q›
      by auto
    ultimately have ‹(❙¬ (p ❙⟶ q)) # H' ⊢ ❙⊥›
      by blast
    moreover have ‹set ((❙¬ (p ❙⟶ q)) # H') ⊆ H›
      using *(1) H'(2) assms maximal_exactly_one by auto
    ultimately show False
      using assms unfolding consistent_def by blast
  qed
next
  fix p
  assume ‹❙∀p ∈ H›
  then show ‹∀t. p⟨t/0⟩ ∈ H›
    using assms consistent_add_instance unfolding maximal_def by blast
next
  fix p
  assume ‹❙∀p ∉ H›
  then show ‹∃n. p⟨❙#n/0⟩ ∉ H›
    using assms maximal_exactly_one unfolding saturated_def by fast
qed

section ‹Countable Formulas›

instance tm :: (countable) countable
  by countable_datatype

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

section ‹Completeness›

theorem strong_completeness:
  fixes p :: ‹('f :: countable, 'p :: countable) fm›
  assumes ‹∀(E :: _ ⇒ 'f tm) F G. Ball X ⟦E, F, G⟧ ⟶ ⟦E, F, G⟧ p›
    and ‹finite (vars 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›

  have ‹consistent ?S›
    using * by (metis consistent_def imply_Cons inconsistent_fm)
  moreover have ‹finite (vars ?S)›
    using assms by simp
  ultimately have ‹consistent ?H› and ‹maximal ?H›
    using assms 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 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 fastforce+
  moreover from this have ‹⟦?H⟧ p›
    using assms(1) by blast
  ultimately show False
    by simp
qed

theorem completeness:
  fixes p :: ‹('f :: countable, 'p :: countable) fm›
  assumes ‹∀(E :: _ ⇒ 'f tm) F G. ⟦E, F, G⟧ p›
  shows ‹⊢ p›
  using assms strong_completeness[where X=‹{}›] by simp

corollary
  fixes p :: ‹(unit, unit) fm›
  assumes ‹∀(E :: nat ⇒ unit tm) F G. ⟦E, F, G⟧ p›
  shows ‹⊢ p›
  using completeness assms .

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