Theory Maximal_Consistent_Sets

(*
  Title:  Maximal Consistent Sets
  Author: Asta Halkjær From

  Based on:
  - First-Order Logic (1968) by Smullyan, R.
  - Model Theory (1990) by Chang, C. C. and Keisler, H. J.
*)

chapter ‹Maximal Consistent Sets›

theory Maximal_Consistent_Sets imports "HOL-Cardinals.Cardinal_Order_Relation" begin

section ‹Utility›

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

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

lemma infinite_Diff_subset: ‹infinite (X - A) ⟹ B ⊆ A ⟹ infinite (X - B)›
  by (meson Diff_cancel Diff_eq_empty_iff Diff_mono infinite_super)

lemma finite_bound:
  fixes X :: ‹('a :: size) set›
  assumes ‹finite X› ‹X ≠ {}›
  shows ‹∃x ∈ X. ∀y ∈ X. size y ≤ size x›
  using assms by (induct X rule: finite_induct) force+

lemma infinite_UNIV_size:
  fixes f :: ‹('a :: size) ⇒ 'a›
  assumes ‹⋀x. size x < size (f x)›
  shows ‹infinite (UNIV :: 'a set)›
proof
  assume ‹finite (UNIV :: 'a set)›
  then obtain x :: 'a where ‹∀y :: 'a. size y ≤ size x›
    using finite_bound by fastforce
  moreover have ‹size x < size (f x)›
    using assms .
  ultimately show False
    using leD by blast
qed

context wo_rel begin

lemma underS_bound: ‹a ∈ underS c ⟹ b ∈ underS c ⟹ a ∈ under b ∨ b ∈ under a›
  by (meson BNF_Least_Fixpoint.underS_Field REFL Refl_under_in in_mono under_ofilter ofilter_linord)

lemma finite_underS_bound:
  assumes ‹finite X› ‹X ⊆ underS c› ‹X ≠ {}›
  shows ‹∃a ∈ X. ∀b ∈ X. b ∈ under a›
  using assms
proof (induct X rule: finite_induct)
  case (insert x F)
  then show ?case
  proof (cases ‹F = {}›)
    case True
    then show ?thesis
      using insert underS_bound by fast
  next
    case False
    then show ?thesis
      using insert underS_bound by (metis TRANS insert_absorb insert_iff insert_subset under_trans)
  qed
qed simp

lemma finite_bound_under:
  assumes ‹finite p› ‹p ⊆ (⋃a ∈ Field r. f a)›
  shows ‹∃b. p ⊆ (⋃a ∈ under b. f a)›
  using assms
proof (induct rule: finite_induct)
  case (insert x p)
  then obtain b where ‹p ⊆ (⋃a ∈ under b. f a)›
    by fast
  moreover obtain b' where ‹x ∈ f b'› ‹b' ∈ Field r›
    using insert(4) by blast
  then have ‹x ∈ (⋃a ∈ under b'. f a)›
    using REFL Refl_under_in by fast
  ultimately have ‹{x} ∪ p ⊆ (⋃a ∈ under b. f a) ∪ (⋃a ∈ under b'. f a)›
    by fast
  then show ?case
    by (metis SUP_union Un_commute insert_is_Un sup.absorb_iff2 ofilter_linord under_ofilter)
qed simp

lemma underS_trans: ‹a ∈ underS b ⟹ b ∈ underS c ⟹ a ∈ underS c›
  by (meson ANTISYM TRANS underS_underS_trans)

end

lemma card_of_infinite_smaller_Union:
  assumes ‹∀x. |f x| <o |X|› ‹infinite X›
  shows ‹|⋃x ∈ X. f x| ≤o |X|›
  using assms by (metis (full_types) Field_card_of card_of_UNION_ordLeq_infinite
      card_of_well_order_on ordLeq_iff_ordLess_or_ordIso ordLess_or_ordLeq)

lemma card_of_params_marker_lists:
  assumes ‹infinite (UNIV :: 'i set)› ‹|UNIV :: 'm set| ≤o |UNIV :: nat set|›
  shows ‹|UNIV :: ('i + 'm × nat) list set| ≤o |UNIV :: 'i set|›
proof -
  have ‹(UNIV :: 'm set) ≠ {}›
    by simp
  then have ‹|UNIV :: 'm set| *c |UNIV :: nat set| ≤o |UNIV :: nat set|›
    using assms(2) by (simp add: cinfinite_def cprod_cinfinite_bound ordLess_imp_ordLeq)
  then have ‹|UNIV :: ('m × nat) set| ≤o |UNIV :: nat set|›
    unfolding cprod_def by simp
  moreover have ‹|UNIV :: nat set| ≤o |UNIV :: 'i set|›
    using assms infinite_iff_card_of_nat by blast
  ultimately have ‹|UNIV :: ('m × nat) set| ≤o |UNIV :: 'i set|›
    using ordLeq_transitive by blast
  moreover have ‹Cinfinite |UNIV :: 'i set|›
    using assms by (simp add: cinfinite_def)
  ultimately have ‹|UNIV :: 'i set| +c |UNIV :: ('m × nat) set| =o |UNIV :: 'i set|›
    using csum_absorb1 by blast
  then have ‹|UNIV :: ('i + 'm × nat) set| =o |UNIV :: 'i set|›
    unfolding csum_def by simp
  then have ‹|UNIV :: ('i + 'm × nat) set| ≤o |UNIV :: 'i set|›
    using ordIso_iff_ordLeq by blast
  moreover have ‹infinite (UNIV :: ('i + 'm × nat) set)›
    using assms by simp
  then have ‹|UNIV :: ('i + 'm × nat) list set| =o |UNIV :: ('i + 'm × nat) set|›
    by (metis card_of_lists_infinite lists_UNIV)
  ultimately have ‹|UNIV :: ('i + 'm × nat) list set| ≤o |UNIV :: 'i set|›
    using ordIso_ordLeq_trans by blast
  then show ?thesis
    using ordLeq_transitive by blast
qed

section ‹Base Locales›

locale MCS_Base =
  fixes consistent :: ‹'a set ⇒ bool›
  assumes consistent_hereditary: ‹⋀S S'. consistent S ⟹ S' ⊆ S ⟹ consistent S'›
    and inconsistent_finite: ‹⋀S. ¬ consistent S ⟹ ∃S' ⊆ S. finite S' ∧ ¬ consistent S'›
begin

definition maximal :: ‹'a set ⇒ bool› where
  ‹maximal S ≡ ∀p. consistent ({p} ∪ S) ⟶ p ∈ S›

end

locale MCS_Witness = MCS_Base consistent
  for consistent :: ‹'a set ⇒ bool› +
  fixes witness :: ‹'a ⇒ 'a set ⇒ 'a set›
    and params :: ‹'a ⇒ 'i set›
  assumes finite_params: ‹⋀p. finite (params p)›
    and finite_witness_params: ‹⋀p S. finite (⋃q ∈ witness p S. params q)›
    and consistent_witness: ‹⋀p S. consistent ({p} ∪ S)
      ⟹ infinite (UNIV - (⋃q ∈ S. params q))
      ⟹ consistent ({p} ∪ S ∪ witness p S)›
begin

definition witnessed :: ‹'a set ⇒ bool› where
  ‹witnessed S ≡ ∀p ∈ S. ∃S'. witness p S' ⊆ S›

abbreviation MCS :: ‹'a set ⇒ bool› where
  ‹MCS S ≡ consistent S ∧ maximal S ∧ witnessed S›

end

locale MCS_No_Witness = MCS_Base consistent for consistent :: ‹'a set ⇒ bool›

sublocale MCS_No_Witness ⊆ MCS_Witness consistent ‹λ_ _. {}› ‹λ_. {}›
proof qed simp_all

section ‹Ordinal Locale›

locale MCS_Lim_Ord = MCS_Witness consistent witness params
  for consistent :: ‹'a set ⇒ bool›
    and witness :: ‹'a ⇒ 'a set ⇒ 'a set›
    and params :: ‹'a ⇒ 'i set› +
  fixes r :: ‹'a rel›
  assumes Cinfinite_r: ‹Cinfinite r›
begin

lemma WELL: ‹Well_order r›
  using Cinfinite_r by simp

lemma wo_rel_r: ‹wo_rel r›
  by (simp add: WELL wo_rel.intro)

lemma isLimOrd_r: ‹isLimOrd r›
  using Cinfinite_r card_order_infinite_isLimOrd cinfinite_def by blast

lemma nonempty_Field_r: ‹Field r ≠ {}›
  using Cinfinite_r cinfinite_def infinite_imp_nonempty by blast

subsection ‹Lindenbaum Extension›

abbreviation paramss :: ‹'a set ⇒ 'i set› where
  ‹paramss S ≡ ⋃p ∈ S. params p›

definition extendS :: ‹'a ⇒ 'a set ⇒ 'a set› where
  ‹extendS a prev ≡ if consistent ({a} ∪ prev) then {a} ∪ prev ∪ witness a prev else prev›

definition extendL :: ‹('a ⇒ 'a set) ⇒ 'a ⇒ 'a set› where
  ‹extendL rec a ≡ ⋃b ∈ underS r a. rec b›

definition extend :: ‹'a set ⇒ 'a ⇒ 'a set› where
  ‹extend S a ≡ worecZSL r S extendS extendL a›

lemma adm_woL_extendL: ‹adm_woL r extendL›
  unfolding extendL_def wo_rel.adm_woL_def[OF wo_rel_r] by blast

definition Extend :: ‹'a set ⇒ 'a set› where
  ‹Extend S ≡ ⋃a ∈ Field r. extend S a›

lemma extend_subset: ‹a ∈ Field r ⟹ S ⊆ extend S a›
proof (induct a rule: wo_rel.well_order_inductZSL[OF wo_rel_r])
  case 1
  then show ?case
    unfolding extend_def wo_rel.worecZSL_zero[OF wo_rel_r adm_woL_extendL]
    by simp
next
  case (2 i)
  moreover from this have ‹i ∈ Field r›
    by (meson FieldI1 wo_rel.succ_in wo_rel_r)
  ultimately show ?case
    unfolding extend_def extendS_def wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL 2(1)]
    by auto
next
  case (3 i)
  then show ?case
    unfolding extend_def extendL_def wo_rel.worecZSL_isLim[OF wo_rel_r adm_woL_extendL 3(1-2)]
    using wo_rel.zero_in_Field[OF wo_rel_r] wo_rel.zero_smallest[OF wo_rel_r]
    by (metis SUP_upper2 emptyE underS_I)
qed

lemma Extend_subset: ‹S ⊆ Extend S›
  unfolding Extend_def using extend_subset nonempty_Field_r by fast

lemma extend_underS: ‹b ∈ underS r a ⟹ extend S b ⊆ extend S a›
proof (induct a rule: wo_rel.well_order_inductZSL[OF wo_rel_r])
  case 1
  then show ?case
    unfolding extend_def using wo_rel.underS_zero[OF wo_rel_r] by fast
next
  case (2 i)
  moreover from this have ‹b = i ∨ b ∈ underS r i›
    by (metis wo_rel.less_succ[OF wo_rel_r] underS_E underS_I)
  ultimately show ?case
    unfolding extend_def extendS_def wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL 2(1)] by auto
next
  case (3 i)
  then show ?case
    unfolding extend_def extendL_def wo_rel.worecZSL_isLim[OF wo_rel_r adm_woL_extendL 3(1-2)]
    by blast
qed

lemma extend_under: ‹b ∈ under r a ⟹ extend S b ⊆ extend S a›
  using extend_underS wo_rel.supr_greater[OF wo_rel_r] wo_rel.supr_under[OF wo_rel_r]
  by (metis emptyE in_Above_under set_eq_subset underS_I under_empty)

subsection ‹Consistency›

lemma params_origin:
  assumes ‹x ∈ paramss (extend S a)›
  shows ‹x ∈ paramss S ∨ (∃b ∈ underS r a. x ∈ paramss ({b} ∪ witness b (extend S b)))›
  using assms
proof (induct a rule: wo_rel.well_order_inductZSL[OF wo_rel_r])
  case 1
  then show ?case
    unfolding extend_def wo_rel.worecZSL_zero[OF wo_rel_r adm_woL_extendL]
    by blast
next
  case (2 i)
  then consider (here) ‹x ∈ paramss ({i} ∪ witness i (extend S i))› | (there) ‹x ∈ paramss (extend S i)›
    using wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL 2(1)] extendS_def extend_def
    by (auto split: if_splits)
  then show ?case
  proof cases
    case here
    moreover have ‹i ∈ Field r›
      by (meson WELL 2(1) well_order_on_domain wo_rel.succ_in_diff[OF wo_rel_r])
    ultimately show ?thesis
      using 2(1) by (metis Refl_under_in wo_rel.underS_succ[OF wo_rel_r] wo_rel.REFL[OF wo_rel_r])
  next
    case there
    then show ?thesis
      using 2 by (metis in_mono underS_subset_under wo_rel.underS_succ[OF wo_rel_r])
  next
  qed
next
  case (3 i)
  then obtain j where ‹j ∈ underS r i› ‹x ∈ paramss (extend S j)›
    unfolding extend_def extendL_def wo_rel.worecZSL_isLim[OF wo_rel_r adm_woL_extendL 3(1-2)]
    by blast
  then show ?case
    using 3 wo_rel.underS_trans[OF wo_rel_r, of _ j i] by meson
qed

lemma consistent_extend:
  assumes ‹consistent S› ‹r ≤o |UNIV - paramss S|›
  shows ‹consistent (extend S a)›
  using assms(1)
proof (induct a rule: wo_rel.well_order_inductZSL[OF wo_rel_r])
  case 1
  then show ?case
    unfolding extend_def wo_rel.worecZSL_zero[OF wo_rel_r adm_woL_extendL]
    by blast
next
  case (2 i)
  then have ‹i ∈ Field r›
    by (meson WELL  well_order_on_domain wo_rel.succ_in_diff[OF wo_rel_r])
  then have *: ‹|underS r i| <o r›
    using card_of_underS by (simp add: Cinfinite_r)
  let ?paramss = ‹λk. paramss ({k} ∪ witness k (extend S k))›
  let ?X = ‹⋃k ∈ underS r i. ?paramss k›
  have ‹|?X| <o r›
  proof (cases ‹finite (underS r i)›)
    case True
    then have ‹finite ?X›
      by (simp add: finite_params finite_witness_params)
    then show ?thesis
      using Cinfinite_r assms(2) unfolding cinfinite_def by (simp add: finite_ordLess_infinite)
  next
    case False
    moreover have ‹∀k. finite (?paramss k)›
      by (simp add: finite_params finite_witness_params)
    then have ‹∀k. |?paramss k| <o |underS r i|›
      using False by simp
    ultimately have ‹|?X| ≤o |underS r i|›
      using card_of_infinite_smaller_Union by fast
    then show ?thesis
      using * ordLeq_ordLess_trans by blast
  qed
  then have ‹|?X| <o |UNIV - paramss S|›
    using assms(2) ordLess_ordLeq_trans by blast
  moreover have ‹infinite (UNIV - paramss S)›
    using assms(2) Cinfinite_r unfolding cinfinite_def by (metis Field_card_of ordLeq_finite_Field)
  ultimately have ‹|UNIV - paramss S - ?X| =o |UNIV - paramss S|›
    using card_of_Un_diff_infinite by blast
  moreover from this have ‹infinite (UNIV - paramss S - ?X)›
    using ‹infinite (UNIV - paramss S)› card_of_ordIso_finite by blast
  moreover have ‹⋀a. a ∈ paramss (extend S i) ⟹ a ∈ paramss S ∨ a ∈ ?X›
    using params_origin by simp
  then have ‹paramss (extend S i) ⊆ paramss S ∪ ?X›
    by fast
  ultimately have ‹infinite (UNIV - paramss (extend S i))›
    using infinite_Diff_subset by (metis (no_types, lifting) Set_Diff_Un)
  with 2 show ?case
    unfolding extend_def extendS_def wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL 2(1)]
    using consistent_witness by simp
  next
  case (3 i)
  show ?case
  proof (rule ccontr)
    assume ‹¬ consistent (extend S i)›
    then obtain S' where S': ‹finite S'› ‹S' ⊆ (⋃a ∈ underS r i. extend S a)› ‹¬ consistent S'›
      unfolding extend_def extendL_def wo_rel.worecZSL_isLim[OF wo_rel_r adm_woL_extendL 3(1-2)]
      using inconsistent_finite by auto
    then obtain as where as: ‹S' ⊆ (⋃a ∈ as. extend S a)› ‹as ⊆ underS r i› ‹finite as›
      by (metis finite_subset_Union finite_subset_image)
    moreover have ‹as ≠ {}›
      using S'(3) assms calculation(1) consistent_hereditary by auto
    ultimately obtain j where ‹∀a ∈ as. a ∈ under r j› ‹j ∈ underS r i›
      using wo_rel.finite_underS_bound wo_rel_r as by (meson subset_iff)
    then have ‹∀a ∈ as. extend S a ⊆ extend S j›
      using extend_under by fast
    then have ‹S' ⊆ extend S j›
      using S' as(1) by blast
    then show False
      using 3(3-) ‹¬ consistent S'› consistent_hereditary ‹j ∈ underS r i›
      by (meson BNF_Least_Fixpoint.underS_Field)
  qed
qed

lemma consistent_Extend:
  assumes ‹consistent S› ‹r ≤o |UNIV - paramss S|›
  shows ‹consistent (Extend S)›
  unfolding Extend_def
proof (rule ccontr)
  assume ‹¬ consistent (⋃a ∈ Field r. extend S a)›
  then obtain S' where ‹finite S'› ‹S' ⊆ (⋃a ∈ Field r. extend S a)› ‹¬ consistent S'›
    using inconsistent_finite by metis
  then obtain b where ‹S' ⊆ (⋃a ∈ under r b. extend S a)› ‹b ∈ Field r›
    using wo_rel.finite_bound_under[OF wo_rel_r] assms consistent_hereditary
    by (metis Sup_empty emptyE image_empty subsetI under_empty)
  then have ‹S' ⊆ extend S b›
    using extend_under by fast
  moreover have ‹consistent (extend S b)›
    using assms consistent_extend ‹b ∈ Field r› by blast
  ultimately show False
    using ‹¬ consistent S'› consistent_hereditary by blast
qed

lemma Extend_bound: ‹a ∈ Field r ⟹ extend S a ⊆ Extend S›
  unfolding Extend_def by blast

subsection ‹Maximality›

definition maximal' :: ‹'a set ⇒ bool› where
  ‹maximal' S ≡ ∀p ∈ Field r. consistent ({p} ∪ S) ⟶ p ∈ S›

lemma maximal'_Extend: ‹maximal' (Extend S)›
  unfolding maximal'_def
proof safe
  fix p
  assume *: ‹p ∈ Field r› ‹consistent ({p} ∪ Extend S)›
  then have ‹{p} ∪ extend S p ⊆ {p} ∪ Extend S›
    unfolding Extend_def by blast
  then have **: ‹consistent ({p} ∪ extend S p)›
    using * consistent_hereditary by blast
  moreover have succ: ‹aboveS r p ≠ {}›
    using * isLimOrd_r wo_rel.isLimOrd_aboveS[OF wo_rel_r] by blast
  then have ‹succ r p ∈ Field r›
    using wo_rel.succ_in_Field[OF wo_rel_r] by blast
  moreover have ‹p ∈ extend S (succ r p)›
    using ** unfolding extend_def extendS_def wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL succ]
    by simp
  ultimately show ‹p ∈ Extend S›
    using Extend_bound by fast
qed

subsection ‹Witnessing›

definition witnessed' :: ‹'a set ⇒ bool› where
  ‹witnessed' S ≡ ∀p ∈ Field r. p ∈ S ⟶ (∃S'. witness p S' ⊆ S)›

lemma witnessed'_Extend:
  assumes ‹consistent (Extend S)›
  shows ‹witnessed' (Extend S)›
  unfolding witnessed'_def
proof safe
  fix p
  assume *: ‹p ∈ Field r› ‹p ∈ Extend S›
  then have ‹extend S p ⊆ Extend S›
    unfolding Extend_def by blast
  then have ‹consistent ({p} ∪ extend S p)›
    using assms(1) * consistent_hereditary by auto
  moreover have succ: ‹aboveS r p ≠ {}›
    using * isLimOrd_r wo_rel.isLimOrd_aboveS wo_rel_r by fast
  then have ‹succ r p ∈ Field r›
    using wo_rel_r by (simp add: wo_rel.succ_in_Field)
  ultimately have ‹extend S (succ r p) = {p} ∪ extend S p ∪ witness p (extend S p)›
    unfolding extend_def extendS_def wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL succ]
    by simp
  moreover have ‹extend S (succ r p) ⊆ Extend S›
    unfolding Extend_def using ‹succ r p ∈ Field r› by blast
  ultimately show ‹∃a. witness p a ⊆ Extend S›
    by fast
qed

end

section ‹Locales for Universe Well-Order›

locale MCS_Witness_UNIV = MCS_Witness consistent witness params
  for consistent :: ‹'a set ⇒ bool›
    and witness :: ‹'a ⇒ 'a set ⇒ 'a set›
    and params :: ‹'a ⇒ 'i set› +
  assumes infinite_UNIV: ‹infinite (UNIV :: 'a set)›

sublocale MCS_Witness_UNIV ⊆ MCS_Lim_Ord consistent witness params ‹|UNIV|›
proof
  show ‹Cinfinite |UNIV :: 'a set|›
    unfolding cinfinite_def using infinite_UNIV by simp
qed

context MCS_Witness_UNIV begin

lemma maximal_maximal': ‹maximal S ⟷ maximal' S›
  unfolding maximal_def maximal'_def by simp

lemma maximal_Extend: ‹maximal (Extend S)›
  using maximal'_Extend maximal_maximal' by fast

lemma witnessed_witnessed': ‹witnessed S ⟷ witnessed' S›
  unfolding witnessed_def witnessed'_def by auto

lemma witnessed_Extend:
  assumes ‹consistent (Extend S)›
  shows ‹witnessed (Extend S)›
  using assms witnessed'_Extend witnessed_witnessed' by blast

theorem MCS_Extend:
  assumes ‹consistent S› ‹|UNIV :: 'a set| ≤o |UNIV - paramss S|›
  shows ‹MCS (Extend S)›
  using assms consistent_Extend maximal_Extend witnessed_Extend by blast

end

locale MCS_No_Witness_UNIV = MCS_No_Witness consistent
  for consistent :: ‹'a set ⇒ bool› +
  assumes infinite_UNIV' [simp]: ‹infinite (UNIV :: 'a set)›

sublocale MCS_No_Witness_UNIV ⊆ MCS_Witness_UNIV consistent ‹λ_ _. {}› ‹λ_. {}›
proof qed simp

context MCS_No_Witness_UNIV
begin

theorem MCS_Extend':
  assumes ‹consistent S›
  shows ‹MCS (Extend S)›
  unfolding witnessed_def using assms consistent_Extend maximal_Extend
  by (metis Diff_empty UN_constant card_of_UNIV empty_subsetI)

end

section ‹Truth Lemma›

locale Truth_Base =
  fixes semics :: ‹'model ⇒ ('model ⇒ 'fm ⇒ bool) ⇒ 'fm ⇒ bool› (‹(_ ⟦_⟧ _)› [55, 0, 55] 55)
    and semantics :: ‹'model ⇒ 'fm ⇒ bool› (infix ‹⊨› 50)
    and ℳ :: ‹'a set ⇒ 'model set›
    and ℛ :: ‹'a set ⇒ 'model ⇒ 'fm ⇒ bool›
  assumes semics_semantics: ‹M ⊨ p ⟷ M ⟦(⊨)⟧ p›
begin

abbreviation saturated :: ‹'a set ⇒ bool› where
  ‹saturated S ≡ ∀p. ∀M ∈ ℳ(S). M ⟦ℛ(S)⟧ p ⟷ ℛ(S) M p›

end

locale Truth_Witness = Truth_Base semics semantics ℳ ℛ + MCS_Witness consistent witness params
  for semics :: ‹'model ⇒ ('model ⇒ 'fm ⇒ bool) ⇒ 'fm ⇒ bool› (‹(_ ⟦_⟧ _)› [55, 0, 55] 55)
    and semantics :: ‹'model ⇒ 'fm ⇒ bool› (infix ‹⊨› 50)
    and ℳ :: ‹'a set ⇒ 'model set›
    and ℛ :: ‹'a set ⇒ 'model ⇒ 'fm ⇒ bool›
    and consistent :: ‹'a set ⇒ bool›
    and witness :: ‹'a ⇒ 'a set ⇒ 'a set›
    and params :: ‹'a ⇒ 'i set› +
  assumes saturated_semantics: ‹⋀S M p. saturated S ⟹ M ∈ ℳ(S) ⟹ M ⊨ p ⟷ ℛ(S) M p›
    and MCS_saturated: ‹⋀S. MCS S ⟹ saturated S›
begin

theorem truth_lemma:
  assumes ‹MCS S› ‹M ∈ ℳ(S)›
  shows ‹M ⊨ p ⟷ ℛ(S) M p›
  using saturated_semantics MCS_saturated assms by blast

end

locale Truth_No_Witness = Truth_Witness semics semantics ℳ ℛ consistent  ‹λ_ _. {}› ‹λ_. {}›
  for semics :: ‹'model ⇒ ('model ⇒ 'fm ⇒ bool) ⇒ 'fm ⇒ bool›
    and semantics :: ‹'model ⇒ 'fm ⇒ bool›
    and ℳ :: ‹'a set ⇒ 'model set›
    and ℛ :: ‹'a set ⇒ 'model ⇒ 'fm ⇒ bool›
    and consistent :: ‹'a set ⇒ bool›

end