# Theory Maximal_Consistent_Sets

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

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

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

lemma split_finite_sets:
assumes ‹finite A› ‹finite B›
assumes ‹A ⊆ B ∪ S›
shows ‹∃B' C. finite C ∧ (B' ∪ C = A) ∧ B' ⊆ B ∧ C ⊆ S›
using assms subset_UnE by fastforce

lemma split_list:
assumes ‹set A ⊆ set B ∪ S›
shows ‹∃B' C. set (B' @ C) = set A ∧ set B' ⊆ set B ∧ set C ⊆ S›
using assms split_finite_sets[where A=‹set A› and B=‹set B› and S=S]
by (metis List.finite_set finite_Un finite_list set_append)

lemma struct_split:
assumes ‹⋀A B. P A ⟹ set A ⊆ set B ⟹ P B› ‹P A› ‹set A ⊆ set B ∪ X›
shows ‹∃C. set C ⊆ X ∧ P (B @ C)›
proof -
obtain B' C where C: ‹set (B' @ C) = set A› ‹set B' ⊆ set B› ‹set C ⊆ X›
using assms(3) split_list by meson
then have ‹P (B @ C)›
using assms(1)[where B=‹B @ C›] assms(2) by fastforce
then show ?thesis
using C by blast
qed

context wo_rel begin

lemma underS_bound: ‹a ∈ underS n ⟹ b ∈ underS n ⟹ 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 n› ‹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 ⊆ (⋃n ∈ Field r. f n)›
shows ‹∃m. p ⊆ (⋃n ∈ under m. f n)›
using assms
proof (induct rule: finite_induct)
case (insert x p)
then obtain m where ‹p ⊆ (⋃n ∈ under m. f n)›
by fast
moreover obtain m' where ‹x ∈ f m'› ‹m' ∈ Field r›
using insert(4) by blast
then have ‹x ∈ (⋃n ∈ under m'. f n)›
using REFL Refl_under_in by fast
ultimately have ‹{x} ∪ p ⊆ (⋃n ∈ under m. f n) ∪ (⋃n ∈ under m'. f n)›
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 Locale›

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

section ‹Ordinal Locale›

locale MCS_Lim_Ord = MCS_Base +
fixes r :: ‹'a rel›
assumes WELL: ‹Well_order r›
and Cinfinite_r: ‹Cinfinite r›
fixes params :: ‹'a ⇒ 'i set›
and witness :: ‹'a ⇒ 'a set ⇒ 'a 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 (witness p S ∪ {p} ∪ S)›
begin

lemma wo_rel_r: ‹wo_rel r›

lemma isLimOrd_r: ‹isLimOrd r›
using Cinfinite_r card_order_infinite_isLimOrd cinfinite_def 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 n prev ≡ if consistent ({n} ∪ prev) then witness n prev ∪ {n} ∪ prev else prev›

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

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

unfolding extendL_def wo_rel.adm_woL_def[OF wo_rel_r] by blast

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

lemma extend_subset: ‹n ∈ Field r ⟹ S ⊆ extend S n›
proof (induct n rule: wo_rel.well_order_inductZSL[OF wo_rel_r])
case 1
then show ?case
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': ‹Field r ≠ {} ⟹ S ⊆ Extend S›
unfolding Extend_def using extend_subset by fast

lemma extend_underS: ‹m ∈ underS r n ⟹ extend S m ⊆ extend S n›
proof (induct n 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 ‹m = i ∨ m ∈ 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: ‹m ∈ under r n ⟹ extend S m ⊆ extend S n›
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_Field under_empty)

subsection ‹Consistency›

lemma params_origin:
assumes ‹a ∈ paramss (extend S n)›
shows ‹a ∈ paramss S ∨ (∃m ∈ underS r n. a ∈ paramss (witness m (extend S m) ∪ {m}))›
using assms
proof (induct n rule: wo_rel.well_order_inductZSL[OF wo_rel_r])
case 1
then show ?case
by blast
next
case (2 i)
then consider (here) ‹a ∈ paramss (witness i (extend S i) ∪ {i})› | (there) ‹a ∈ paramss (extend S i)›
using wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL 2(1)] extendS_def extend_def
by (metis (no_types, lifting) UN_Un UnE)
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› ‹a ∈ 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 n)›
using assms(1)
proof (induct n rule: wo_rel.well_order_inductZSL[OF wo_rel_r])
case 1
then show ?case
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 (witness k (extend S k) ∪ {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›
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)›
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 auto
next
case (3 i)
show ?case
proof (rule ccontr)
assume ‹¬ consistent (extend S i)›
then obtain S' where S': ‹finite S'› ‹S' ⊆ (⋃n ∈ underS r i. extend S n)› ‹¬ 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 ns where ns: ‹S' ⊆ (⋃n ∈ ns. extend S n)› ‹ns ⊆ underS r i› ‹finite ns›
by (metis finite_subset_Union finite_subset_image)
moreover have ‹ns ≠ {}›
using S'(3) assms calculation(1) consistent_hereditary by auto
ultimately obtain j where ‹∀n ∈ ns. n ∈ under r j› ‹j ∈ underS r i›
using wo_rel.finite_underS_bound wo_rel_r ns by (meson subset_iff)
then have ‹∀n ∈ ns. extend S n ⊆ extend S j›
using extend_under by fast
then have ‹S' ⊆ extend S j›
using S' ns(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 (⋃n ∈ Field r. extend S n)›
then obtain S' where ‹finite S'› ‹S' ⊆ (⋃n ∈ Field r. extend S n)› ‹¬ consistent S'›
using inconsistent_finite by metis
then obtain m where ‹S' ⊆ (⋃n ∈ under r m. extend S n)› ‹m ∈ 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 m›
using extend_under by fast
moreover have ‹consistent (extend S m)›
using assms consistent_extend ‹m ∈ Field r› by blast
ultimately show False
using ‹¬ consistent S'› consistent_hereditary by blast
qed

lemma Extend_bound: ‹n ∈ Field r ⟹ extend S n ⊆ 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 ‹Saturation›

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

lemma saturated'_Extend:
assumes ‹consistent (Extend S)›
shows ‹saturated' (Extend S)›
unfolding saturated'_def
proof safe
fix p
assume *: ‹p ∈ Extend S› ‹p ∈ Field r›
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) = witness p (extend S p) ∪ {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 ‹Locale with Saturation›

locale MCS_Saturation = MCS_Base +
assumes infinite_UNIV: ‹infinite (UNIV :: 'a set)›
fixes params :: ‹'a ⇒ 'i set›
and witness :: ‹'a ⇒ 'a set ⇒ 'a set›
assumes ‹⋀p. finite (params p)›
and ‹⋀p S. finite (⋃q ∈ witness p S. params q)›
and ‹⋀p S. consistent ({p} ∪ S) ⟹ infinite (UNIV - (⋃q ∈ S. params q))
⟹ consistent (witness p S ∪ {p} ∪ S)›

sublocale MCS_Saturation ⊆ MCS_Lim_Ord _ ‹|UNIV|›
proof
show ‹Well_order |UNIV|›
by simp
next
show ‹Cinfinite |UNIV :: 'a set|›
unfolding cinfinite_def using infinite_UNIV by simp
next
fix p
show ‹finite (params p)›
by (metis MCS_Saturation_axioms MCS_Saturation_axioms_def MCS_Saturation_def)
next
fix p S
show ‹finite (⋃q ∈ witness p S. params q)›
by (metis MCS_Saturation_axioms MCS_Saturation_axioms_def MCS_Saturation_def)
next
fix p S
show ‹consistent ({p} ∪ S) ⟹
infinite (UNIV - (⋃q ∈ S. params q)) ⟹
consistent (witness p S ∪ {p} ∪ S)›
by (metis MCS_Saturation_axioms MCS_Saturation_axioms_def MCS_Saturation_def)
qed

context MCS_Saturation begin

theorem Extend_subset: ‹S ⊆ Extend S›

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

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

lemma saturated_saturated': ‹saturated S ⟷ saturated' S›
unfolding saturated_def saturated'_def by simp

lemma saturated_Extend:
assumes ‹consistent (Extend S)›
shows ‹saturated (Extend S)›
using assms saturated'_Extend saturated_saturated' by blast

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

end

section ‹Locale without Saturation›

locale MCS_No_Saturation = MCS_Base +
assumes ‹infinite (UNIV :: 'a set)›

sublocale MCS_No_Saturation ⊆ MCS_Saturation consistent ‹λ_. {} :: 'a set› ‹λ_ _. {}›
proof
show ‹infinite (UNIV :: 'a set)›
using MCS_No_Saturation_axioms MCS_No_Saturation_axioms_def MCS_No_Saturation_def by blast
next
show ‹finite {}› ..
next
show ‹finite (⋃_∈{}. {})›
by fast
next
fix p S
show ‹consistent ({p} ∪ S) ⟹ consistent ({} ∪ {p} ∪ S)›
by simp
qed

context MCS_No_Saturation begin

lemma always_saturated [simp]: ‹saturated H›
unfolding saturated_def by simp

theorem MCS_Extend':
assumes ‹consistent S›
shows ‹consistent (Extend S)› ‹maximal (Extend S)›
using assms consistent_Extend maximal_Extend by simp_all

end

section ‹Truth Lemma›

locale Truth_Base =
fixes semics :: ‹'model ⇒ ('model ⇒ 'fm ⇒ bool) ⇒ 'fm ⇒ bool›
and semantics :: ‹'model ⇒ 'fm ⇒ bool›
and models_from :: ‹'a set ⇒ 'model set›
and rel :: ‹'a set ⇒ 'model ⇒ 'fm ⇒ bool›
assumes semics_semantics: ‹semantics M p ⟷ semics M semantics p›
and Hintikka_model: ‹⋀H M p. ∀M ∈ models_from H. ∀p. semics M (rel H) p ⟷ rel H M p ⟹
M ∈ models_from H ⟹ semantics M p ⟷ rel H M p›

locale Truth_Saturation = MCS_Saturation + Truth_Base +
assumes MCS_Hintikka: ‹⋀H. consistent H ⟹ maximal H ⟹ saturated H ⟹
∀M ∈ models_from H. ∀p. semics M (rel H) p ⟷ rel H M p›
begin

theorem truth_lemma_saturation:
assumes ‹consistent H› ‹maximal H› ‹saturated H› ‹M ∈ models_from H›
shows ‹semantics M p ⟷ rel H M p›
using Hintikka_model MCS_Hintikka assms .

end

locale Truth_No_Saturation = MCS_No_Saturation + Truth_Base +
assumes MCS_Hintikka: ‹⋀H. consistent H ⟹ maximal H ⟹
∀M ∈ models_from H. ∀p. semics M (rel H) p ⟷ rel H M p›
begin

theorem truth_lemma_no_saturation:
assumes ‹consistent H› ‹maximal H› ‹M ∈ models_from H›
shows ‹semantics M p ⟷ rel H M p›
using Hintikka_model MCS_Hintikka assms .

end

end
```