# 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) 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

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

lemma deduct1: ‹A ⊢⇩∀ p ❙⟶ q ⟹ p # A ⊢⇩∀ q›

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 _ _ = {}›

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›
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

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' ⊢⇩∀ ❙⊥›
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)›
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
```