Theory Definitions_Main

section‹Main definitions of the development›

theory Definitions_Main
  imports
    Not_CH
    Absolute_Versions
begin

text‹This theory gathers the main definitions of the Forcing session.

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 in which our development is based, might jump
directly there. But in case one wants to dive deeper, the following
sections treat some basic concepts in 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]]
no_notation add (infixl ‹#+› 65)
notation add (infixl ‹+⇩ω› 65)
hide_const (open) Order.pred

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
text‹@{thm [display] lt_def}›
(*
  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 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 show 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)
*)
txt‹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,[])))" ..

txt‹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 .

txt‹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}›
txt‹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)))
*)


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

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

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

txt‹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)*)

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

txt‹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∈list(M).
      arity(φ) ≤ 2 +⇩ω length(env) ⟶
      strong_replacement(##M, λx y. M, [x, y] @ env ⊨ φ))

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

thm ZF_fin_def ZF_inf_def ZF_def ZFC_fin_def ZFC_def
text‹@{thm [display] ZF_fin_def ZF_inf_def ZF_def ZFC_fin_def
  ZFC_def}›
(*
  ZF_fin ≡ {⋅Extensionality⋅, ⋅Foundation⋅, ⋅Pairing⋅, ⋅Union Ax⋅, ⋅Infinity⋅, ⋅Powerset Ax⋅}
  ZF_inf ≡ {⋅Separation(p)⋅ . p ∈ formula} ∪ {⋅Replacement(p)⋅ . p ∈ formula}
  ZF ≡ ZF_inf ∪ ZF_fin
  ZFC_fin ≡ ZF_fin ∪ {⋅AC⋅}
  ZFC ≡ ZF_inf ∪ ZFC_fin
*)

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

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

txt‹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

txt‹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"
    "CH⇗M⇖ ≡ ℵ⇘1⇙⇗M⇖ = 2⇗↑ℵ⇘0⇙⇗M⇖,M⇖"
  unfolding cardinal_rel_def cexp_rel_def
    csucc_rel_def Card_rel_def ContHyp_rel_def .

context M_aleph
begin

txt‹As in 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 (* M_aleph *)

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

txt‹Under appropriate hypothesis (this time, from the locale \<^term>‹M_master›),
   \<^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_master.is_ContHyp_iff is_ContHyp_iff_CH[unfolded ContHyp_def]
text‹@{thm [display] M_master.is_ContHyp_iff
    is_ContHyp_iff_CH[unfolded ContHyp_def]}›
(*
  M_master(M) ⟹ is_ContHyp(M) ⟷ CH⇗M⇖
  is_ContHyp(𝒱) ⟷ ℵ⇘1⇙ = 2⇗↑ℵ⇘0⇙⇖
*)

txt‹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⋅
*)

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

end