Theory Definitions_Main

section‹Main definitions of the development\label{sec:main-definitions}›

theory Definitions_Main
  imports
    Absolute_Versions
begin

text‹This theory gathers the main definitions of the
\<^session>‹Transitive_Models› session and the present one.

It might be considered as the bare minimum reading requisite to
trust that our development indeed formalizes the theory of
forcing. This should be mathematically clear since this is the
only known method for obtaining proper extensions of ctms while
preserving the ordinals.

The main theorem of this session and all of its relevant definitions
appear in Section~\ref{sec:def-main-forcing}. The reader trusting
all the libraries on which our development is based, might jump
directly to Section~\ref{sec:relative-arith}, which treats relative
cardinal arithmetic as implemented in
\<^session>‹Transitive_Models›. But in case one wants to dive deeper, the
following sections treat some basic concepts of the ZF logic
(Section~\ref{sec:def-main-ZF}) and in the
ZF-Constructible library (Section~\ref{sec:def-main-relative})
on which our definitions are built.
›

declare [[show_question_marks=false]]

subsection‹ZF\label{sec:def-main-ZF}›

text‹For the basic logic ZF we restrict ourselves to just a few
concepts.›

thm bij_def[unfolded inj_def surj_def]
text‹@{thm [display] bij_def[unfolded inj_def surj_def]}›
(*
bij(A, B) ≡
  {f ∈ A → B . ∀w∈A. ∀x∈A. f ` w = f ` x ⟶ w = x} ∩
  {f ∈ A → B . ∀y∈B. ∃x∈A. f ` x = y}
*)

thm eqpoll_def
text‹@{thm [display] eqpoll_def}›
(*
  A ≈ B ≡ ∃f. f ∈ bij(A, B)
*)

thm Transset_def
text‹@{thm [display] Transset_def}›
(*
  Transset(i) ≡ ∀x∈i. x ⊆ i
*)

thm Ord_def
text‹@{thm [display] Ord_def}›
(*
  Ord(i) ≡ Transset(i) ∧ (∀x∈i. Transset(x))
*)

thm lt_def le_iff
text‹@{thm [display] lt_def le_iff}›
(*
  i < j ≡ i ∈ j ∧ Ord(j)
  i ≤ j ⟷ i < j ∨ i = j ∧ Ord(j)
*)

text‹With the concepts of empty set and successor in place,›
lemma empty_def': "∀x. x ∉ 0" by simp
lemma succ_def': "succ(i) = i ∪ {i}" by blast

text‹we can define the set of natural numbers \<^term>‹ω›. In the
sources, it is  defined as a fixpoint, but here we just write
its characterization as the first limit ordinal.›
thm Limit_nat[unfolded Limit_def] nat_le_Limit[unfolded Limit_def]
text‹@{thm [display] Limit_nat[unfolded Limit_def]
 nat_le_Limit[unfolded Limit_def]}›
(*
  Ord(ω) ∧ 0 < ω ∧ (∀y. y < ω ⟶ succ(y) < ω)
  Ord(i) ∧ 0 < i ∧ (∀y. y < i ⟶ succ(y) < i) ⟹ ω ≤ i
*)

text‹Then, addition and predecessor on \<^term>‹ω› are inductively
characterized as follows:›
thm add_0_right add_succ_right pred_0 pred_succ_eq
text‹@{thm [display] add_succ_right add_0_right pred_0 pred_succ_eq}›
(*
  m ∈ ω ⟹ m +⇩ω 0 = m
  m +⇩ω succ(n) = succ(m +⇩ω n)

  pred(0) = 0
  pred(succ(y)) = y
*)

text‹Lists on a set \<^term>‹A› can be characterized by being
recursively generated from the empty list \<^term>‹[]› and the
operation \<^term>‹Cons› that adds a new element to the left end;
the induction theorem for them shows that the characterization is
“complete”.›

thm Nil Cons list.induct
text‹@{thm [display] Nil Cons list.induct }›
(*
  [] ∈ list(A)
  a ∈ A ⟹ l ∈ list(A) ⟹ Cons(a, l) ∈ list(A)
  x ∈ list(A) ⟹
  P([]) ⟹ (⋀a l. a ∈ A ⟹ l ∈ list(A) ⟹ P(l) ⟹ P(Cons(a, l))) ⟹ P(x)
*)

text‹Length, concatenation, and \<^term>‹n›th element of lists are
recursively characterized as follows.›
thm length.simps app.simps nth_0 nth_Cons
text‹@{thm [display] length.simps app.simps nth_0 nth_Cons}›
(*
  length([]) = 0
  length(Cons(a, l)) = succ(length(l))

  [] @ ys = ys
  Cons(a, l) @ ys = Cons(a, l @ ys)

  nth(0, Cons(a, l)) = a
  n ∈ ω ⟹ nth(succ(n), Cons(a, l)) = nth(n, l)
*)
text‹We have the usual Haskell-like notation for iterated applications
of \<^term>‹Cons›:›
lemma Cons_app: "[a,b,c] = Cons(a,Cons(b,Cons(c,[])))" ..

text‹Relative quantifiers restrict the range of the bound variable to a
class \<^term>‹M› of type \<^typ>‹i⇒o›; that is, a truth-valued function with
set arguments.›
lemma "∀x[M]. P(x) ≡ ∀x. M(x) ⟶ P(x)"
      "∃x[M]. P(x) ≡ ∃x. M(x) ∧ P(x)"
  unfolding rall_def rex_def .

text‹Finally, a set can be viewed (“cast”) as a class using the
following function of type \<^typ>‹i⇒(i⇒o)›.›
thm setclass_iff
text‹@{thm [display] setclass_iff}›
(*
  (##A)(x) ⟷ x ∈ A
*)

subsection‹Relative concepts\label{sec:def-main-relative}›
text‹A list of relative concepts (mostly from the ZF-Constructible
    library) follows next.›

thm big_union_def
text‹@{thm [display] big_union_def}›
(*
  big_union(M, A, z) ≡ ∀x[M]. x ∈ z ⟷ (∃y[M]. y ∈ A ∧ x ∈ y)
*)

thm upair_def
text‹@{thm [display] upair_def}›
(*
  upair(M, a, b, z) ≡ a ∈ z ∧ b ∈ z ∧ (∀x[M]. x ∈ z ⟶ x = a ∨ x = b)
*)

thm pair_def
text‹@{thm [display] pair_def}›
(*
  pair(M, a, b, z) ≡ ∃x[M]. upair(M, a, a, x) ∧
                        (∃y[M]. upair(M, a, b, y) ∧ upair(M, x, y, z))
*)

thm successor_def[unfolded is_cons_def union_def]
text‹@{thm [display] successor_def[unfolded is_cons_def union_def]}›
(*
  successor(M, a, z) ≡ ∃x[M]. upair(M, a, a, x) ∧ (∀xa[M]. xa ∈ z ⟷ xa ∈ x ∨ xa ∈ a)
*)

thm empty_def
text‹@{thm [display] empty_def}›
(*
  empty(M, z) ≡ ∀x[M]. x ∉ z
*)

thm transitive_set_def[unfolded subset_def]
text‹@{thm [display] transitive_set_def[unfolded subset_def]}›
(*
  transitive_set(M, a) ≡ ∀x[M]. x ∈ a ⟶ (∀xa[M]. xa ∈ x ⟶ xa ∈ a)
*)


thm ordinal_def
text‹@{thm [display] ordinal_def}›
(*
  ordinal(M, a) ≡ transitive_set(M, a) ∧ (∀x[M]. x ∈ a ⟶
                                              transitive_set(M, x))
*)

thm image_def
text‹@{thm [display] image_def}›
(*
  image(M, r, A, z) ≡ ∀y[M]. y ∈ z ⟷
                (∃w[M]. w ∈ r ∧ (∃x[M]. x ∈ A ∧ pair(M, x, y, w)))
*)

thm fun_apply_def
text‹@{thm [display] fun_apply_def}›
(*
  fun_apply(M, f, x, y) ≡ ∃xs[M]. ∃fxs[M]. upair(M, x, x, xs) ∧
                       image(M, f, xs, fxs) ∧ big_union(M, fxs, y)
*)

thm is_function_def
text‹@{thm [display] is_function_def}›
(*
  is_function(M, r) ≡ ∀x[M]. ∀y[M]. ∀y'[M]. ∀p[M]. ∀p'[M].
       pair(M, x, y, p) ⟶ pair(M, x, y', p') ⟶ p ∈ r ⟶ p' ∈ r ⟶ y = y'
*)

thm is_relation_def
text‹@{thm [display] is_relation_def}›
(*
  is_relation(M, r) ≡ ∀z[M]. z ∈ r ⟶ (∃x[M]. ∃y[M]. pair(M, x, y, z))
*)

thm is_domain_def
text‹@{thm [display] is_domain_def}›
(*
  is_domain(M, r, z) ≡ ∀x[M]. x ∈ z ⟷
                        (∃w[M]. w ∈ r ∧ (∃y[M]. pair(M, x, y, w)))
*)

thm typed_function_def
text‹@{thm [display] typed_function_def}›
(*
  typed_function(M, A, B, r) ≡ is_function(M, r) ∧ is_relation(M, r) ∧
                                is_domain(M, r, A) ∧
            (∀u[M]. u ∈ r ⟶ (∀x[M]. ∀y[M]. pair(M, x, y, u) ⟶ y ∈ B))
*)

thm is_function_space_def[unfolded is_funspace_def]
  function_space_rel_def surjection_def
text‹@{thm [display] is_function_space_def[unfolded is_funspace_def]
  function_space_rel_def surjection_def}›
(*
  is_function_space(M, A, B, fs) ≡
  M(fs) ∧ (∀f[M]. f ∈ fs ⟷ typed_function(M, A, B, f))

  A →⇗M⇖ B ≡ THE d. is_function_space(M, A, B, d)

  surjection(M, A, B, f) ≡
  typed_function(M, A, B, f) ∧
  (∀y[M]. y ∈ B ⟶ (∃x[M]. x ∈ A ∧ is_apply(M, f, x, y)))
*)


text‹Relative version of the $\ZFC$ axioms›
thm extensionality_def
text‹@{thm [display] extensionality_def}›
(*
  extensionality(M) ≡ ∀x[M]. ∀y[M]. (∀z[M]. z ∈ x ⟷ z ∈ y) ⟶ x = y
*)

thm foundation_ax_def
text‹@{thm [display] foundation_ax_def}›
(*
  foundation_ax(M) ≡ ∀x[M]. (∃y[M]. y ∈ x) ⟶ (∃y[M]. y ∈ x ∧ ¬ (∃z[M]. z ∈ x ∧ z ∈ y))
*)

thm upair_ax_def
text‹@{thm [display] upair_ax_def}›
(*
  upair_ax(M) ≡ ∀x[M]. ∀y[M]. ∃z[M]. upair(M, x, y, z)
*)

thm Union_ax_def
text‹@{thm [display] Union_ax_def}›
(*
  Union_ax(M) ≡ ∀x[M]. ∃z[M]. ∀xa[M]. xa ∈ z ⟷ (∃y[M]. y ∈ x ∧ xa ∈ y)
*)

thm power_ax_def[unfolded powerset_def subset_def]
text‹@{thm [display] power_ax_def[unfolded powerset_def subset_def]}›
(*
  power_ax(M) ≡ ∀x[M]. ∃z[M]. ∀xa[M]. xa ∈ z ⟷ (∀xb[M]. xb ∈ xa ⟶ xb ∈ x)
*)

thm infinity_ax_def
text‹@{thm [display] infinity_ax_def}›
(*
  infinity_ax(M) ≡ ∃I[M]. (∃z[M]. empty(M, z) ∧ z ∈ I) ∧ (∀y[M]. y ∈ I ⟶
                        (∃sy[M]. successor(M, y, sy) ∧ sy ∈ I))
*)

thm choice_ax_def
text‹@{thm [display] choice_ax_def}›
(*
  choice_ax(M) ≡ ∀x[M]. ∃a[M]. ∃f[M]. ordinal(M, a) ∧ surjection(M, a, x, f)
*)

thm separation_def
text‹@{thm [display] separation_def}›
(*
  separation(M, P) ≡ ∀z[M]. ∃y[M]. ∀x[M]. x ∈ y ⟷ x ∈ z ∧ P(x)
*)

thm univalent_def
text‹@{thm [display] univalent_def}›
(*
  univalent(M, A, P) ≡ ∀x[M]. x ∈ A ⟶
                          (∀y[M]. ∀z[M]. P(x, y) ∧ P(x, z) ⟶ y = z)
*)

thm strong_replacement_def
text‹@{thm [display] strong_replacement_def}›
(*
  strong_replacement(M, P) ≡ ∀A[M]. univalent(M, A, P) ⟶
       (∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ A ∧ P(x, b)))
*)

text‹Internalized formulas›

text‹“Codes” for formulas (as sets) are constructed from natural
numbers using \<^term>‹Member›, \<^term>‹Equal›, \<^term>‹Nand›,
and \<^term>‹Forall›.›

thm Member Equal Nand Forall formula.induct
text‹@{thm [display] Member Equal Nand Forall formula.induct}›
(*
  x ∈ ω ⟹ y ∈ ω ⟹ ⋅x ∈ y⋅ ∈ formula
  x ∈ ω ⟹ y ∈ ω ⟹ ⋅x = y⋅ ∈ formula
  p ∈ formula ⟹ q ∈ formula ⟹ ⋅¬(p ∧ q)⋅ ∈ formula
  p ∈ formula ⟹ (∀p) ∈ formula

  x ∈ formula ⟹
  (⋀x y. x ∈ ω ⟹ y ∈ ω ⟹ P(⋅x ∈ y⋅)) ⟹
  (⋀x y. x ∈ ω ⟹ y ∈ ω ⟹ P(⋅x = y⋅)) ⟹
  (⋀p q. p ∈ formula ⟹ P(p) ⟹ q ∈ formula ⟹ P(q) ⟹ P(⋅¬(p ∧ q)⋅)) ⟹
  (⋀p. p ∈ formula ⟹ P(p) ⟹ P((∀p))) ⟹ P(x)
*)

text‹Definitions for the other connectives and the internal existential
quantifier are also provided. For instance, negation:›
thm Neg_def
text‹@{thm [display] Neg_def}›
(*
  ⋅¬p⋅ ≡ ⋅¬(p ∧ p)⋅
*)

thm arity.simps
text‹@{thm [display] arity.simps}›
(*
  arity(⋅x ∈ y⋅) = succ(x) ∪ succ(y)
  arity(⋅x = y⋅) = succ(x) ∪ succ(y)
  arity(⋅¬(p ∧ q)⋅) = arity(p) ∪ arity(q)
  arity((∀p)) = pred(arity(p))
*)

text‹We have the satisfaction relation between $\in$-models and
    first order formulas (given a “environment” list representing
    the assignment of free variables),›
thm mem_iff_sats equal_iff_sats sats_Nand_iff sats_Forall_iff
text‹@{thm [display] mem_iff_sats equal_iff_sats sats_Nand_iff sats_Forall_iff}›
(*
  nth(i, env) = x ⟹ nth(j, env) = y ⟹ env ∈ list(A) ⟹ x ∈ y ⟷ A, env ⊨ ⋅i ∈ j⋅
  nth(i, env) = x ⟹ nth(j, env) = y ⟹ env ∈ list(A) ⟹ x = y ⟷ A, env ⊨ ⋅i = j⋅
  env ∈ list(A) ⟹ (A, env ⊨ ⋅¬(p ∧ q)⋅) ⟷ ¬ ((A, env ⊨ p) ∧ (A, env ⊨ q))
  env ∈ list(A) ⟹ (A, env ⊨ (⋅∀p⋅)) ⟷ (∀x∈A. A, Cons(x, env) ⊨ p)*)

text‹as well as the satisfaction of an arbitrary set of sentences.›
thm satT_def
text‹@{thm [display] satT_def}›
(*
  A ⊨ Φ  ≡  ∀φ∈Φ. A, [] ⊨ φ
*)

text‹The internalized (viz. as elements of the set \<^term>‹formula›)
    version of the axioms follow next.›

thm ZF_union_iff_sats ZF_power_iff_sats ZF_pairing_iff_sats
  ZF_foundation_iff_sats ZF_extensionality_iff_sats
  ZF_infinity_iff_sats sats_ZF_separation_fm_iff
  sats_ZF_replacement_fm_iff ZF_choice_iff_sats
text‹@{thm [display] ZF_union_iff_sats ZF_power_iff_sats
  ZF_pairing_iff_sats
  ZF_foundation_iff_sats ZF_extensionality_iff_sats
  ZF_infinity_iff_sats sats_ZF_separation_fm_iff
  sats_ZF_replacement_fm_iff ZF_choice_iff_sats}›
(*
  Union_ax(##A) ⟷ A, [] ⊨ ⋅Union Ax⋅
  power_ax(##A) ⟷ A, [] ⊨ ⋅Powerset Ax⋅
  upair_ax(##A) ⟷ A, [] ⊨ ⋅Pairing⋅
  foundation_ax(##A) ⟷ A, [] ⊨ ⋅Foundation⋅
  extensionality(##A) ⟷ A, [] ⊨ ⋅Extensionality⋅
  infinity_ax(##A) ⟷ A, [] ⊨ ⋅Infinity⋅

  φ ∈ formula ⟹
  (M, [] ⊨ ⋅Separation(φ)⋅) ⟷
  (∀env∈list(M).
      arity(φ) ≤ 1 +⇩ω length(env) ⟶ separation(##M, λx. M, [x] @ env ⊨ φ))

  φ ∈ formula ⟹
  (M, [] ⊨ ⋅Replacement(φ)⋅) ⟷ (∀env. replacement_assm(M, env, φ))

  choice_ax(##A) ⟷ A, [] ⊨ ⋅AC⋅
*)

text‹Above, we use the following:›

thm replacement_assm_def
text‹@{thm [display] replacement_assm_def}›
(*
replacement_assm(M, env, φ) ≡
φ ∈ formula ⟶
env ∈ list(M) ⟶
arity(φ) ≤ 2 +⇩ω length(env) ⟶
strong_replacement(##M, λx y. M, [x, y] @ env ⊨ φ
*)

text‹Finally, the axiom sets are defined as follows.›

thm ZF_fin_def ZF_schemes_def Zermelo_fms_def ZC_def ZF_def ZFC_def
text‹@{thm [display] ZF_fin_def ZF_schemes_def Zermelo_fms_def ZC_def ZF_def
  ZFC_def}›
(*
  ZF_fin ≡ {⋅Extensionality⋅, ⋅Foundation⋅, ⋅Pairing⋅, ⋅Union Ax⋅, ⋅Infinity⋅, ⋅Powerset Ax⋅}
  ZF_schemes ≡ {⋅Separation(p)⋅ . p ∈ formula} ∪ {⋅Replacement(p)⋅ . p ∈ formula}
  ⋅Z⋅ ≡ ZF_fin ∪ {⋅Separation(p)⋅ . p ∈ formula}
  ZC ≡ ⋅Z⋅ ∪ {⋅AC⋅}
  ZF ≡ ZF_schemes ∪ ZF_fin
  ZFC ≡ ZF ∪ {⋅AC⋅}
*)

subsection‹Relativization of infinitary arithmetic\label{sec:relative-arith}›

text‹In order to state the defining property of the relative
    equipotence relation, we work under the assumptions of the
    locale \<^term>‹M_cardinals›. They comprise a finite set
    of instances of Separation and Replacement to prove
    closure properties of the transitive class \<^term>‹M›.›

lemma (in M_cardinals) eqpoll_def':
  assumes "M(A)" "M(B)" shows "A ≈⇗M⇖ B ⟷ (∃f[M]. f ∈ bij(A,B))"
  using assms unfolding eqpoll_rel_def by auto

text‹Below, $\mu$ denotes the minimum operator on the ordinals.›
lemma cardinalities_defs:
  fixes M::"i⇒o"
  shows
    "|A|⇗M⇖ ≡ μ i. M(i) ∧ i ≈⇗M⇖ A"
    "Card⇗M⇖(α) ≡ α = |α|⇗M⇖"
    "κ⇗↑ν,M⇖ ≡ |ν →⇗M⇖ κ|⇗M⇖"
    "(κ⇧+)⇗M⇖ ≡ μ x. M(x) ∧ Card⇗M⇖(x) ∧ κ < x"
  unfolding cardinal_rel_def cexp_rel_def
    csucc_rel_def Card_rel_def .

context M_aleph
begin

text‹Analogous to the previous Lemma @{thm [source] eqpoll_def'}, we are now under
    the assumptions of the locale \<^term>‹M_aleph›. The axiom instances
    included are sufficient to state and prove the defining
    properties of the relativized \<^term>‹Aleph› function
    (in particular, the required ability to perform transfinite recursions).›

thm Aleph_rel_zero Aleph_rel_succ Aleph_rel_limit
text‹@{thm [display] Aleph_rel_zero Aleph_rel_succ Aleph_rel_limit}›
(*
  ℵ⇘0⇙⇗M⇖ = ω
  Ord(α) ⟹ M(α) ⟹ ℵ⇘succ(α)⇙⇗M⇖ = (ℵ⇘α⇙⇗M⇖⇧+)⇗M⇖
  Limit(α) ⟹ M(α) ⟹ ℵ⇘α⇙⇗M⇖ = (⋃j∈α. ℵ⇘j⇙⇗M⇖)
*)

end ― ‹\<^locale>‹M_aleph››

lemma ContHyp_rel_def':
  fixes N::"i⇒o"
  shows
    "CH⇗N⇖ ≡ ℵ⇘1⇙⇗N⇖ = 2⇗↑ℵ⇘0⇙⇗N⇖,N⇖"
  unfolding ContHyp_rel_def .

text‹Under appropriate hypotheses (this time, from the locale \<^term>‹M_ZF_library›),
   \<^term>‹CH⇗M⇖› is equivalent to its fully relational version \<^term>‹is_ContHyp›.
    As a sanity check, we see that if the transitive class is indeed \<^term>‹𝒱›,
    we recover the original $\CH$.›

thm M_ZF_library.is_ContHyp_iff is_ContHyp_iff_CH[unfolded ContHyp_def]
text‹@{thm [display] M_ZF_library.is_ContHyp_iff
    is_ContHyp_iff_CH[unfolded ContHyp_def]}›
(*
  M_ZF_library(M) ⟹ is_ContHyp(M) ⟷ CH⇗M⇖
  is_ContHyp(𝒱) ⟷ ℵ⇘1⇙ = 2⇗↑ℵ⇘0⇙⇖
*)

text‹In turn, the fully relational version evaluated on a nonempty
    transitive \<^term>‹A› is equivalent to the satisfaction of the
    first-order formula \<^term>‹⋅CH⋅›.›
thm is_ContHyp_iff_sats
text‹@{thm [display] is_ContHyp_iff_sats}›
(*
  env ∈ list(A) ⟹ 0 ∈ A ⟹ is_ContHyp(##A) ⟷ A, env ⊨ ⋅CH⋅
*)


subsection‹Forcing \label{sec:def-main-forcing}›

text‹Our first milestone was to obtain a proper extension using forcing.
Its original proof didn't required the previous developments involving
the relativization of material on cardinal arithmetic. Now it is
derived from a stronger result, namely @{thm [source] extensions_of_ctms}
below.›

thm extensions_of_ctms_ZF
text‹@{thm [display] extensions_of_ctms_ZF}›
(*
  M ≈ ω ⟹
  Transset(M) ⟹
  M ⊨ ZF ⟹
  ∃N. M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ N ⊨ ZF ∧ M ≠ N ∧
    (∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N) ∧ ((M, [] ⊨ ⋅AC⋅) ⟶ N ⊨ ZFC)
*)

text‹We can finally state our main results, namely, the existence of models
for $\ZFC + \CH$ and $\ZFC + \neg\CH$ under the assumption of a ctm of $\ZFC$.›

thm ctm_ZFC_imp_ctm_not_CH
text‹@{thm [display] ctm_ZFC_imp_ctm_not_CH}›
(*
  M ≈ ω ⟹
  Transset(M) ⟹
  M ⊨ ZFC ⟹
  ∃N. M ⊆ N ∧
    N ≈ ω ∧ Transset(N) ∧ N ⊨ ZFC ∪ {⋅¬⋅CH⋅⋅} ∧
    (∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N)
*)

thm ctm_ZFC_imp_ctm_CH
text‹@{thm [display] ctm_ZFC_imp_ctm_CH}›
(*
  M ≈ ω ⟹
  Transset(M) ⟹
  M ⊨ ZFC ⟹
  ∃N. M ⊆ N ∧
      N ≈ ω ∧
      Transset(N) ∧ N ⊨ ZFC ∪ {⋅CH⋅} ∧ (∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N)
*)

text‹These results can be strengthened by enumerating six finite sets of
replacement instances which are sufficient to develop forcing and for
the construction of the aforementioned models: \<^term>‹instances1_fms›
through \<^term>‹instances3_fms›, \<^term>‹instances_ground_fms›, and
\<^term>‹instances_ground_notCH_fms›,
which are then collected into the $31$-element set \<^term>‹overhead_notCH›.
For example, we have:›

thm instances1_fms_def
text‹@{thm [display] instances1_fms_def}›
(*
instances1_fms ≡
{ eclose_closed_fm, eclose_abs_fm,
  wfrec_rank_fm, transrec_VFrom_fm }
*)

thm overhead_def overhead_notCH_def
text‹@{thm [display] overhead_def overhead_notCH_def overhead_CH_def}›
(*
  overhead ≡ instances1_fms ∪ instances_ground_fms

  overhead_notCH ≡ overhead ∪
    instances2_fms ∪ instances3_fms ∪ instances_ground_notCH_fms
*)

text‹One further instance is needed to force $\CH$, with a total count
of $32$ instances:›
thm overhead_CH_def
text‹@{thm [display] overhead_CH_def}›
(*
  overhead_CH ≡ overhead_notCH ∪ {dc_abs_fm}
*)

thm extensions_of_ctms
text‹@{thm [display] extensions_of_ctms}›
(*
M ≈ ω ⟹
Transset(M) ⟹
M ⊨ ⋅Z⋅ ∪ {⋅Replacement(p)⋅ . p ∈ overhead} ⟹
Φ ⊆ formula ⟹
M ⊨ {⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ} ⟹
∃N. M ⊆ N ∧
    N ≈ ω ∧
    Transset(N) ∧
    M ≠ N ∧
    (∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N) ∧
    ((M, [] ⊨ ⋅AC⋅) ⟶ N, [] ⊨ ⋅AC⋅) ∧ N ⊨ ⋅Z⋅ ∪ {⋅Replacement(φ)⋅ . φ ∈ Φ}
*)

thm ctm_of_not_CH
text‹@{thm [display] ctm_of_not_CH}›
(*
M ≈ ω ⟹
Transset(M) ⟹
M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH} ⟹
Φ ⊆ formula ⟹
M ⊨ {⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ} ⟹
∃N. M ⊆ N ∧
    N ≈ ω ∧
    Transset(N) ∧
    N ⊨ ZC ∪ {⋅¬⋅CH⋅⋅} ∪ {⋅Replacement(φ)⋅ . φ ∈ Φ} ∧
    (∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N)
*)

thm ctm_of_CH
text‹@{thm [display] ctm_of_CH}›
(*
M ≈ ω ⟹
Transset(M) ⟹
M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_CH} ⟹
Φ ⊆ formula ⟹
M ⊨ {⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ} ⟹
∃N. M ⊆ N ∧
    N ≈ ω ∧
    Transset(N) ∧
    N ⊨ ZC ∪ {⋅CH⋅} ∪ {⋅Replacement(φ)⋅ . φ ∈ Φ} ∧
    (∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N)
*)

text‹In the above three statements, the function \<^term>‹ground_repl_fm›
takes an element \<^term>‹φ› of \<^term>‹formula› and returns the
replacement instance in the ground model that produces the
\<^term>‹φ›-replacement instance in the generic extension. The next
result is stated in the context \<^locale>‹G_generic1›, which assumes
the existence of a generic filter.›

context G_generic1
begin

thm sats_ground_repl_fm_imp_sats_ZF_replacement_fm
text‹@{thm [display] sats_ground_repl_fm_imp_sats_ZF_replacement_fm}›
(*
  φ ∈ formula ⟹
  M, [] ⊨ ⋅Replacement(ground_repl_fm(φ))⋅ ⟹ M[G], [] ⊨ ⋅Replacement(φ)⋅
*)

end ― ‹\<^locale>‹G_generic1››

end