Theory Example_First_Order_Logic

(*
  Title:  Example Completeness Proof for a Natural Deduction Calculus for First-Order Logic
  Author: Asta Halkjær From
*)

chapter ‹Example: First-Order Logic›

theory Example_First_Order_Logic imports Derivations 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
  = Fls (‹❙⊥›)
  | 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 ❙⟶ ❙⊥›

section ‹Semantics›

type_synonym ('a, 'f, 'p) model = ‹(nat ⇒ 'a) × ('f ⇒ 'a list ⇒ 'a) × ('p ⇒ 'a list ⇒ bool)›

fun semantics_tm :: ‹(nat ⇒ 'a) × ('f ⇒ 'a list ⇒ 'a) ⇒ 'f tm ⇒ 'a› (‹⦇_⦈›) where
  ‹⦇(E, _)⦈ (❙#n) = E n›
| ‹⦇(E, F)⦈ (❙†f ts) = F f (map ⦇(E, F)⦈ ts)›

primrec add_env :: ‹'a ⇒ (nat ⇒ 'a) ⇒ nat ⇒ 'a› (infix ‹⨟› 0) where
  ‹(t ⨟ s) 0 = t›
| ‹(t ⨟ s) (Suc n) = s n›

fun semantics_fm :: ‹('a, 'f, 'p) model ⇒ ('f, 'p) fm ⇒ bool› (‹⟦_⟧›) 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. ⟦(x ⨟ E, F, G)⟧ p)›

section ‹Operations›

primrec lift_tm :: ‹'f tm ⇒ 'f tm› where
  ‹lift_tm (❙#n) = ❙#(n+1)›
| ‹lift_tm (❙†f ts) = ❙†f (map lift_tm ts)›

primrec sub_tm :: ‹(nat ⇒ 'f tm) ⇒ 'f tm ⇒ 'f tm› where
  ‹sub_tm s (❙#n) = s n›
| ‹sub_tm s (❙†f ts) = ❙†f (map (sub_tm s) ts)›

primrec sub_fm :: ‹(nat ⇒ 'f tm) ⇒ ('f, 'p) fm ⇒ ('f, 'p) fm› where
  ‹sub_fm _ ❙⊥ = ❙⊥›
| ‹sub_fm s (❙‡P ts) = ❙‡P (map (sub_tm s) ts)›
| ‹sub_fm s (p ❙⟶ q) = sub_fm s p ❙⟶ sub_fm s q›
| ‹sub_fm s (❙∀p) = ❙∀(sub_fm (❙#0 ⨟ λn. lift_tm (s n)) p)›

abbreviation inst_single :: ‹'f tm ⇒ ('f, 'p) fm ⇒ ('f, 'p) fm› (‹⟨_⟩›) where
  ‹⟨t⟩ ≡ sub_fm (t ⨟ ❙#)›

abbreviation ‹params' S ≡ ⋃p ∈ S. params_fm p›

abbreviation ‹params l ≡ params' (set l)›

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

lemma env [simp]: ‹P ((x ⨟ E) n) = (P x ⨟ λn. P (E n)) n›
  by (induct n) simp_all

lemma lift_lemma: ‹⦇(x ⨟ E, F)⦈ (lift_tm t) = ⦇(E, F)⦈ t›
  by (induct t) (auto cong: map_cong)

lemma sub_tm_semantics: ‹⦇(E, F)⦈ (sub_tm s t) = ⦇(λn. ⦇(E, F)⦈ (s n), F)⦈ t›
  by (induct t) (auto cong: map_cong)

lemma sub_fm_semantics [simp]: ‹⟦(E, F, G)⟧ (sub_fm s p) = ⟦(λn. ⦇(E, F)⦈ (s n), F, G)⟧ p›
  by (induct p arbitrary: E s) (auto cong: map_cong simp: sub_tm_semantics lift_lemma)

lemma sub_tm_Var: ‹sub_tm ❙# t = t›
  by (induct t) (auto cong: map_cong)

lemma reduce_Var [simp]: ‹(❙# 0 ⨟ λn. ❙# (Suc n)) = ❙#›
proof (rule ext)
  fix n
  show ‹(❙# 0 ⨟ λn. ❙# (Suc n)) n = ❙#n›
    by (induct n) simp_all
qed

lemma sub_fm_Var [simp]:
  fixes p :: ‹('f, 'p) fm›
  shows ‹sub_fm ❙# p = p›
proof (induct p)
  case (Pre P ts)
  then show ?case
    by (auto cong: map_cong simp: sub_tm_Var)
qed simp_all

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)

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

primrec size_fm :: ‹('f, 'p) fm ⇒ nat› 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_sub_fm [simp]: ‹size_fm (sub_fm s p) = size_fm p›
  by (induct p arbitrary: s) simp_all

section ‹Calculus›

inductive Calculus :: ‹('f, 'p) fm list ⇒ ('f, 'p) fm ⇒ bool› (‹_ ⊢⇩∀ _› [50, 50] 50) where
  Assm [intro]: ‹p ∈ set A ⟹ A ⊢⇩∀ p›
| FlsE [elim]: ‹A ⊢⇩∀ ❙⊥ ⟹ A ⊢⇩∀ p›
| ImpI [intro]: ‹p # A ⊢⇩∀ q ⟹ A ⊢⇩∀ p ❙⟶ q›
| ImpE [elim]: ‹A ⊢⇩∀ p ❙⟶ q ⟹ A ⊢⇩∀ p ⟹ A ⊢⇩∀ q›
| UniI [intro]: ‹A ⊢⇩∀ ⟨❙⋆a⟩p ⟹ a ∉ params (p # A) ⟹ A ⊢⇩∀ ❙∀p›
| UniE [elim]: ‹A ⊢⇩∀ ❙∀p ⟹ A ⊢⇩∀ ⟨t⟩p›
| Clas: ‹(p ❙⟶ q) # A ⊢⇩∀ p ⟹ A ⊢⇩∀ p›
| Weak: ‹A ⊢⇩∀ p ⟹ q # A ⊢⇩∀ p›

section ‹Soundness›

theorem soundness: ‹A ⊢⇩∀ p ⟹ list_all ⟦(E, F, G)⟧ A ⟹ ⟦(E, F, G)⟧ p›
proof (induct p arbitrary: F rule: Calculus.induct)
  case (UniI A a p)
  moreover have ‹list_all ⟦(E, F(a := x), G)⟧ A› for x
    using UniI(3-4) by (simp add: list.pred_mono_strong)
  then have ‹⟦(E, F(a := x), G)⟧ (⟨❙⋆a⟩p)› for x
    using UniI by blast
  ultimately show ?case
    by fastforce
qed (auto simp: list_all_iff)

corollary soundness': ‹[] ⊢⇩∀ p ⟹ ⟦M⟧ p›
  using soundness by (cases M) fastforce

corollary ‹¬ ([] ⊢⇩∀ ❙⊥)›
  using soundness' by fastforce

section ‹Admissible Rules›

lemma Assm_head: ‹p # A ⊢⇩∀ p›
  by auto

lemma deduct1: ‹A ⊢⇩∀ p ❙⟶ q ⟹ p # A ⊢⇩∀ q›
  by (meson ImpE Weak Assm_head)

lemma Boole: ‹(❙¬ p) # A ⊢⇩∀ ❙⊥ ⟹ A ⊢⇩∀ p›
  using Clas FlsE by blast

lemma Weak': ‹A ⊢⇩∀ p ⟹ B @ A ⊢⇩∀ p›
  by (induct B) (simp, metis Weak append_Cons)

lemma Weaken: ‹A ⊢⇩∀ p ⟹ set A ⊆ set B ⟹ B ⊢⇩∀ p›
proof (induct A arbitrary: p)
  case Nil
  then show ?case
    using Weak' by fastforce
next
  case (Cons q A)
  then show ?case
    by (metis Assm ImpE ImpI list.set_intros(1-2) subset_code(1))
qed

interpretation Derivations Calculus
proof
  fix A B and p :: ‹('f, 'p) fm›
  assume ‹A ⊢⇩∀ p› ‹set A ⊆ set B›
  then show ‹B ⊢⇩∀ p›
    using Weaken by blast
qed

section ‹Maximal Consistent Sets›

definition consistent :: ‹('f, 'p) fm set ⇒ bool› where
  ‹consistent S ≡ ∄S'. set S' ⊆ S ∧ S' ⊢⇩∀ ❙⊥›

fun witness :: ‹('f, 'p) fm ⇒ ('f, 'p) fm set ⇒ ('f, 'p) fm set› where
  ‹witness (❙¬ (❙∀p)) S = {❙¬ ⟨❙⋆(SOME a. a ∉ params' ({p} ∪ S))⟩p}›
| ‹witness _ _ = {}›

lemma consistent_add_instance:
  assumes ‹consistent S› ‹❙∀p ∈ S›
  shows ‹consistent ({⟨t⟩p} ∪ S)›
  unfolding consistent_def
proof
  assume ‹∃S'. set S' ⊆ {⟨t⟩p} ∪ S ∧ S' ⊢⇩∀ ❙⊥›
  then obtain S' where ‹set S' ⊆ S› ‹⟨t⟩p # S' ⊢⇩∀ ❙⊥›
    using assms derive_split1 by metis
  then have ‹❙∀p # S' ⊢⇩∀ ❙¬ ⟨t⟩p›
    using Weak by blast
  moreover have ‹❙∀p # S' ⊢⇩∀ ⟨t⟩p›
    using Assm_head by fast
  ultimately have ‹❙∀p # S' ⊢⇩∀ ❙⊥›
    by fast
  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_witness:
  assumes ‹consistent S› ‹❙¬ (❙∀p) ∈ S› ‹a ∉ params' S›
  shows ‹consistent ({❙¬ ⟨❙⋆a⟩p} ∪ S)›
  unfolding consistent_def
proof
  assume ‹∃S'. set S' ⊆ {❙¬ ⟨❙⋆a⟩p} ∪ S ∧ S' ⊢⇩∀ ❙⊥›
  then obtain S' where ‹set S' ⊆ S› ‹(❙¬ ⟨❙⋆a⟩p) # S' ⊢⇩∀ ❙⊥›
    using assms derive_split1 by metis
  then have ‹S' ⊢⇩∀ ⟨❙⋆a⟩p›
    using Boole by blast
  moreover have ‹a ∉ params_fm p› ‹∀p ∈ set S'. a ∉ params_fm p›
    using ‹set S' ⊆ S› assms(2-3) by auto
  then have ‹a ∉ params' ({p} ∪ set S')›
    using calculation by fast
  ultimately have ‹S' ⊢⇩∀ ❙∀p›
    by fastforce
  then have ‹❙¬ (❙∀p) # S' ⊢⇩∀ ❙⊥›
    using Weak Assm_head by fast
  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_witness':
  assumes ‹consistent ({p} ∪ S)› ‹infinite (UNIV - params' S)›
  shows ‹consistent (witness p S ∪ {p} ∪ S)›
  using assms
proof (induct p S rule: witness.induct)
  case (1 p S)
  have ‹infinite (UNIV - params' ({p} ∪ S))›
    using 1(2) finite_params_fm by (simp add: infinite_Diff_fin_Un)
  then have ‹∃a. a ∉ params' ({p} ∪ S)›
    by (simp add: not_finite_existsD set_diff_eq)
  then have ‹(SOME a. a ∉ params' ({p} ∪ S)) ∉ params' ({p} ∪ S)›
    by (rule someI_ex)
  then obtain a where a: ‹witness (❙¬ (❙∀p)) S = {❙¬ ⟨❙⋆a⟩p}› ‹a ∉ params' ({❙¬❙∀p} ∪ S)›
    by simp
  then show ?case
    using 1(1-2) a(1) consistent_add_witness[where S=‹{❙¬❙∀p} ∪ S›] by fastforce
qed (auto simp: assms)

interpretation MCS_Saturation consistent params_fm witness
proof
  fix S S' :: ‹('f, 'p) fm set›
  assume ‹consistent S› ‹S' ⊆ S›
  then show ‹consistent S'›
    unfolding consistent_def by fast
next
  fix S :: ‹('f, 'p) fm set›
  assume ‹¬ consistent S›
  then show ‹∃S'⊆S. finite S' ∧ ¬ consistent S'›
    unfolding consistent_def by blast
next
  fix p :: ‹('f, 'p) fm›
  show ‹finite (params_fm p)›
    by simp
next
  fix p and S :: ‹('f, 'p) fm set›
  show ‹finite (params' (witness p S))›
    by (induct p S rule: witness.induct) simp_all
next
  fix p and S :: ‹('f, 'p) fm set›
  assume ‹consistent ({p} ∪ S)› ‹infinite (UNIV - params' S)›
  then show ‹consistent (witness p S ∪ {p} ∪ S)›
    using consistent_witness' by fast
next
  show ‹infinite (UNIV :: ('f, 'p) fm set)›
    using infinite_UNIV_size[of ‹λp. p ❙⟶ p›] by simp
qed

interpretation Derivations_MCS_Cut Calculus consistent ‹❙⊥›
proof
  fix S :: ‹('f, 'p) fm set›
  show ‹consistent S = (∄S'. set S' ⊆ S ∧ S' ⊢⇩∀ ❙⊥)›
    unfolding consistent_def ..
next
  fix A and p :: ‹('f, 'p) fm›
  assume ‹p ∈ set A›
  then show ‹A ⊢⇩∀ p›
    by blast
next
  fix A B and p q :: ‹('f, 'p) fm›
  assume ‹A ⊢⇩∀ p› ‹p # B ⊢⇩∀ q›
  then show ‹A @ B ⊢⇩∀ q›
    using Weaken ImpI ImpE by (metis Un_upper2 inf_sup_ord(3) set_append)
qed

section ‹Truth Lemma›

abbreviation hmodel :: ‹('f, 'p) fm set ⇒ ('f tm, 'f, 'p) model› where
  ‹hmodel H ≡ (❙#, ❙†, λP ts. ❙‡P ts ∈ H)›

fun semics ::
  ‹('a, 'f, 'p) model ⇒ (('a, 'f, 'p) model ⇒ ('f, 'p) fm ⇒ bool) ⇒ ('f, 'p) fm ⇒ bool› where
  ‹semics _ _ ❙⊥ ⟷ False›
| ‹semics (E, F, G) _ (❙‡P ts) ⟷ G P (map ⦇(E, F)⦈ ts)›
| ‹semics (E, F, G) rel (p ❙⟶ q) ⟷ rel (E, F, G) p ⟶ rel (E, F, G) q›
| ‹semics (E, F, G) rel (❙∀p) ⟷ (∀x. rel (x ⨟ E, F, G) p)›

fun rel :: ‹('f, 'p) fm set ⇒ ('f tm, 'f, 'p) model ⇒ ('f, 'p) fm ⇒ bool› where
  ‹rel H (E, _, _) p = (sub_fm E p ∈ H)›

theorem Hintikka_model':
  assumes ‹⋀p. semics (hmodel H) (rel H) p ⟷ p ∈ H›
  shows ‹p ∈ H ⟷ ⟦hmodel 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[of x] by (cases x) simp_all
qed

lemma Hintikka_Extend:
  assumes ‹consistent H› ‹maximal H› ‹saturated H›
  shows ‹semics (hmodel H) (rel H) p ⟷ p ∈ H›
proof (cases p)
  case Fls
  have ‹❙⊥ ∉ H›
    using assms MCS_derive unfolding consistent_def by blast
  then show ?thesis
    using Fls by simp
next
  case (Imp p q)
  have ‹p # A ⊢⇩∀ ❙⊥ ⟹ A ⊢⇩∀ p ❙⟶ q› ‹A ⊢⇩∀ q ⟹ A ⊢⇩∀ p ❙⟶ q› for A
    by (auto simp: Weak)
  moreover have ‹A ⊢⇩∀ p ❙⟶ q ⟹ p # A ⊢⇩∀ q› for A
    using deduct1 .
  ultimately have ‹(p ∈ H ⟶ q ∈ H) ⟷ p ❙⟶ q ∈ H›
    using assms(1-2) MCS_derive MCS_derive_fls by (metis insert_subset list.simps(15))
  then show ?thesis
    using Imp by simp
next
  case (Uni p)
  have ‹(∀x. ⟨x⟩p ∈ H) ⟷ (❙∀p ∈ H)›
  proof
    assume ‹∀x. ⟨x⟩p ∈ H›
    show ‹❙∀p ∈ H›
    proof (rule ccontr)
      assume ‹❙∀p ∉ H›
      then have ‹consistent ({❙¬ ❙∀p} ∪ H)›
        using Boole assms(1-2) MCS_derive derive_split1 by (metis consistent_derive_fls)
      then have ‹❙¬ ❙∀p ∈ H›
        using assms(2) unfolding maximal_def by blast
      then obtain a where ‹❙¬ ⟨❙⋆a⟩p ∈ H›
        using assms(3) unfolding saturated_def by fastforce
      moreover have ‹⟨❙⋆a⟩p ∈ H›
        using ‹∀x. ⟨x⟩p ∈ H› by blast
      ultimately show False
        using assms(1-2) MCS_derive by (metis consistent_def deduct1 insert_subset list.simps(15))
    qed
  next
    assume ‹❙∀p ∈ H›
    then show ‹∀x. ⟨x⟩p ∈ H›
      using assms(1-2) consistent_add_instance maximal_def by blast
  qed
  then show ?thesis
    using Uni by simp
qed simp

interpretation Truth_Saturation
  consistent params_fm witness semics semantics_fm ‹λH. {hmodel H}› rel
proof unfold_locales
  fix p and M :: ‹('a tm, 'f, 'p) model›
  show ‹⟦M⟧ p ⟷ semics M semantics_fm p›
    by (cases M, induct p) auto
next
  fix p and H :: ‹('f, 'p) fm set› and M :: ‹('f tm, 'f, 'p) model›
  assume ‹∀M ∈ {hmodel H}. ∀p. semics M (rel H) p ⟷ rel H M p› ‹M ∈ {hmodel H}›
  then show ‹⟦M⟧ p ⟷ rel H M p›
    using Hintikka_model' by auto
next
  fix H :: ‹('f, 'p) fm set›
  assume ‹consistent H› ‹maximal H› ‹saturated H›
  then show ‹∀M ∈ {hmodel H}. ∀p. semics M (rel H) p ⟷ rel H M p›
    using Hintikka_Extend by auto
qed

section ‹Cardinalities›

datatype marker = VarM | FunM | TmM | FlsM | PreM | ImpM | UniM

type_synonym ('f, 'p) enc = ‹('f + 'p) + marker × nat›

abbreviation ‹FUNS f ≡ Inl (Inl f)›
abbreviation ‹PRES p ≡ Inl (Inr p)›

abbreviation ‹VAR n ≡ Inr (VarM, n)›
abbreviation ‹FUN n ≡ Inr (FunM, n)›
abbreviation ‹TM n ≡ Inr (TmM, n)›

abbreviation ‹PRE n ≡ Inr (PreM, n)›
abbreviation ‹FLS ≡ Inr (FlsM, 0)›
abbreviation ‹IMP n ≡ Inr (FlsM, n)›
abbreviation ‹UNI ≡ Inr (UniM, 0)›

primrec
  encode_tm :: ‹'f tm ⇒ ('f, 'p) enc list› and
  encode_tms :: ‹'f tm list ⇒ ('f, 'p) enc list› where
  ‹encode_tm (❙#n) = [VAR n]›
| ‹encode_tm (❙†f ts) = FUN (length ts) # FUNS f # encode_tms ts›
| ‹encode_tms [] = []›
| ‹encode_tms (t # ts) = TM (length (encode_tm t)) # encode_tm t @ encode_tms ts›

lemma encode_tm_ne [simp]: ‹encode_tm t ≠ []›
  by (induct t) auto

lemma inj_encode_tm':
  ‹(encode_tm t :: ('f, 'p) enc list) = encode_tm s ⟹ t = s›
  ‹(encode_tms ts :: ('f, 'p) enc list) = encode_tms ss ⟹ ts = ss›
proof (induct t and ts arbitrary: s and ss rule: encode_tm.induct encode_tms.induct)
  case (Var n)
  then show ?case
    by (cases s) auto
next
  case (Fun f fts)
  then show ?case
    by (cases s) auto
next
  case Nil_tm
  then show ?case
    by (cases ss) auto
next
  case (Cons_tm t ts)
  then show ?case
    by (cases ss) auto
qed

lemma inj_encode_tm: ‹inj encode_tm›
  unfolding inj_def using inj_encode_tm' by blast

primrec encode_fm :: ‹('f, 'p) fm ⇒ ('f, 'p) enc list› where
  ‹encode_fm ❙⊥ = [FLS]›
| ‹encode_fm (❙‡P ts) = PRE (length ts) # PRES P # encode_tms ts›
| ‹encode_fm (p ❙⟶ q) = IMP (length (encode_fm p)) # encode_fm p @ encode_fm q›
| ‹encode_fm (❙∀p) = UNI # encode_fm p›

lemma encode_fm_ne [simp]: ‹encode_fm p ≠ []›
  by (induct p) auto

lemma inj_encode_fm': ‹encode_fm p = encode_fm q ⟹ p = q›
proof (induct p arbitrary: q)
  case Fls
  then show ?case
    by (cases q) auto
next
  case (Pre P ts)
  then show ?case
    by (cases q) (auto simp: inj_encode_tm')
next
  case (Imp p1 p2)
  then show ?case
    by (cases q) auto
next
  case (Uni p)
  then show ?case
    by (cases q) auto
qed

lemma inj_encode_fm: ‹inj encode_fm›
  unfolding inj_def using inj_encode_fm' by blast

lemma finite_marker: ‹finite (UNIV :: marker set)›
proof -
  have ‹p ∈ {VarM, FunM, TmM, FlsM, PreM, ImpM, UniM}› for p
    by (cases p) auto
  then show ?thesis
    by (meson ex_new_if_finite finite.emptyI finite_insert)
qed

lemma card_of_fm:
  assumes ‹infinite (UNIV :: 'f set)›
  shows ‹|UNIV :: ('f, 'p) fm set| ≤o |UNIV :: 'f set| +c |UNIV :: 'p set|›
proof -
  have ‹|UNIV :: marker set| ≤o |UNIV :: nat set|›
    using finite_marker by (simp add: ordLess_imp_ordLeq)
  moreover have ‹infinite (UNIV :: ('f + 'p) set)›
    using assms by simp
  ultimately have ‹|UNIV :: ('f, 'p) enc list set| ≤o |UNIV :: ('f + 'p) set|›
    using card_of_params_marker_lists by blast
  moreover have ‹|UNIV :: ('f, 'p) fm set| ≤o |UNIV :: ('f, 'p) enc list set|›
    using card_of_ordLeq inj_encode_fm by blast
  ultimately have ‹|UNIV :: ('f, 'p) fm set| ≤o |UNIV :: ('f + 'p) set|›
    using ordLeq_transitive by blast
  then show ?thesis
    unfolding csum_def by simp
qed

section ‹Completeness›

theorem strong_completeness:
  assumes ‹∀M :: ('f tm, 'f, 'p) model. (∀q ∈ X. ⟦M⟧ q) ⟶ ⟦M⟧ p›
    ‹infinite (UNIV :: 'f set)›
    ‹|UNIV :: 'f set| +c |UNIV :: 'p set| ≤o |UNIV - params' X|›
  shows ‹∃A. set A ⊆ X ∧ A ⊢⇩∀ p›
proof (rule ccontr)
  assume ‹∄A. set A ⊆ X ∧ A ⊢⇩∀ p›
  then have *: ‹∄A. set A ⊆ X ∧ ❙¬ p # A ⊢⇩∀ ❙⊥›
    using Boole by blast

  let ?S = ‹{❙¬ p} ∪ X›
  let ?H = ‹Extend ?S›

  have ‹consistent ?S›
    using * by (meson consistent_def derive_split1)
  moreover have ‹infinite (UNIV - params' X)›
    using assms(2-3)
    by (metis Cinfinite_csum Cnotzero_UNIV Field_card_of cinfinite_def cinfinite_mono)
  then have ‹|UNIV :: 'f set| +c |UNIV :: 'p set| ≤o |UNIV - params' X - params_fm (❙¬ p)|›
    using assms(3) finite_params_fm card_of_infinite_diff_finite
    by (metis ordIso_iff_ordLeq ordLeq_transitive)
  then have ‹|UNIV :: 'f set| +c |UNIV :: 'p set| ≤o |UNIV - (params' X ∪ params_fm (❙¬ p))|›
    by (metis Set_Diff_Un)
  then have ‹|UNIV :: 'f set| +c |UNIV :: 'p set| ≤o |UNIV - params' ?S|›
    by (metis UN_insert insert_is_Un sup_commute)
  then have ‹|UNIV :: ('f, 'p) fm set| ≤o |UNIV - params' ?S|›
    using assms card_of_fm ordLeq_transitive by blast
  ultimately have ‹consistent ?H› ‹maximal ?H› ‹saturated ?H›
    using MCS_Extend by fast+
  then have ‹p ∈ ?H ⟷ ⟦hmodel ?H⟧ p› for p
    using truth_lemma_saturation by fastforce
  then have ‹p ∈ ?S ⟶ ⟦hmodel ?H⟧ p› for p
    using Extend_subset by blast
  then have ‹⟦hmodel ?H⟧ (❙¬ p)› ‹∀q ∈ X. ⟦hmodel ?H⟧ q›
    by blast+
  moreover from this have ‹⟦hmodel ?H⟧ p›
    using assms(1) by blast
  ultimately show False
    by simp
qed

abbreviation valid :: ‹('f, 'p) fm ⇒ bool› where
  ‹valid p ≡ ∀M :: ('f tm, _, _) model. ⟦M⟧ p›

theorem completeness:
  fixes p :: ‹('f, 'p) fm›
  assumes ‹valid p› ‹infinite (UNIV :: 'f set)› ‹|UNIV :: 'p set| ≤o |UNIV :: 'f set|›
  shows ‹[] ⊢⇩∀ p›
proof -
  have ‹|UNIV :: 'f set| +c |UNIV :: 'p set| ≤o |UNIV :: 'f set|›
    using assms(2-3) by (simp add: cinfinite_def csum_absorb1 ordIso_imp_ordLeq)
  then show ?thesis
    using assms strong_completeness[where X=‹{}›] infinite_UNIV_listI by auto
qed

corollary completeness':
  fixes p :: ‹('f, 'f) fm›
  assumes ‹valid p› ‹infinite (UNIV :: 'f set)›
  shows ‹[] ⊢⇩∀ p›
  using assms completeness[of p] by simp

theorem main:
  fixes p :: ‹('f, 'p) fm›
  assumes ‹infinite (UNIV :: 'f set)› ‹|UNIV :: 'p set| ≤o |UNIV :: 'f set|›
  shows ‹valid p ⟷ [] ⊢⇩∀ p›
  using assms completeness soundness' by blast

corollary main':
  fixes p :: ‹('f, 'f) fm›
  assumes ‹infinite (UNIV :: 'f set)›
  shows ‹valid p ⟷ [] ⊢⇩∀ p›
  using assms completeness' soundness' by blast

end