Theory MSOinHOL_lowenheim_skolem

theory MSOinHOL_lowenheim_skolem
  imports MSOinHOL_lowenheim_skolem_lemmas
begin

text ‹Two-sorted elementary substructure (Tarski--Vaught form).›

definition ElementarySubstructure
    ("⟨_,_,_⟩ ⊆⇩E ⟨_,_,_⟩")
  where
    "⟨I',D',E'⟩ ⊆⇩E ⟨I,D,E⟩ ≡
       D' ❙⊆ D ∧ E' ❙⊆ E
       ∧ (∀g G φ. G into E' ⟶ g into D'
            ⟶ ((⟨I,D,E⟩,g,G ⊨⇧d φ) = (⟨I',D',E'⟩,g,G ⊨⇧d φ)))"

text ‹Minimal interpretation whose range model is elementary in a larger
  model.›

locale MinS_ES = MinS +
  fixes DD :: 𝒟 and EE :: 𝒫
  assumes ES: "⟨II,Range gg, Range GG⟩ ⊆⇩E ⟨II,DD,EE⟩"
begin

lemma 𝒩_valid_ES:
  "⟨II,DD,EE⟩,gg,GG ⊨⇧d φ = ⟨II,Range gg, Range GG⟩,gg,GG ⊨⇧d φ"
  using ES ElementarySubstructure_def by (smt (verit))

end

text ‹Specialisation to the standard model
  @{text "⟨II,Univ,Univ⟩"}.›

locale MinS_ES_Univ = MinS_ES II gg GG Univ Univ for II gg GG
begin

lemma 𝒩_valid_ES_Univ:
  "⟨II,Univ,Univ⟩,gg,GG ⊨⇧d φ = ⟨II,Range gg,Range GG⟩,gg,GG ⊨⇧d φ"
  using 𝒩_valid_ES .

end

text ‹Range-relative validity: the right-hand side of
  ‹FaithfulMS_all›.›

definition RangeValid ("⊨⇧r _" 9)
  where "⊨⇧r φ ≡ ∀I g G. ⟨I, Range g, Range G⟩,g,G ⊨⇧d φ"

lemma into_Range: "f into Range f"
  by auto

text ‹Easy direction.›

lemma ValD_imp_RangeValid: "⊨⇧d φ ⟹ ⊨⇧r φ"
  unfolding RangeValid_def ValD_def using into_Range by smt

text ‹Truth preservation across a Tarski--Vaught-closed sub-pair
  @{text "(D0,E0)"}.›

lemma truth_pres:
  assumes subD: "D⇩0 ❙⊆ D" and subE: "E⇩0 ❙⊆ E"
    and TVfo:
      "⋀y ψ a b.
         a into D⇩0 ⟹ b into E⇩0 ⟹
         (∃d. D d ∧ ⟨I,D,E⟩,a[y←d],b ⊨⇧d ψ) ⟹
         (∃d. D⇩0 d ∧ ⟨I,D,E⟩,a[y←d],b ⊨⇧d ψ)"
    and TVso:
      "⋀Y ψ a b.
         a into D⇩0 ⟹ b into E⇩0 ⟹
         (∃S. E S ∧ ⟨I,D,E⟩,a,b⟨Y←S⟩ ⊨⇧d ψ) ⟹
         (∃S. E⇩0 S ∧ ⟨I,D,E⟩,a,b⟨Y←S⟩ ⊨⇧d ψ)"
    and aD: "a into D⇩0" and bE: "b into E⇩0"
  shows "(⟨I,D⇩0,E⇩0⟩,a,b ⊨⇧d ψ) = (⟨I,D,E⟩,a,b ⊨⇧d ψ)"
  using aD bE
proof (induct ψ arbitrary: a b)
  case (ExD y ψ)
  thus ?case
    using ExD.hyps[of "a[y←_]" b] TVfo[of a b y ψ] subD
    by (force simp: EnvMod_def)
next
  case (ExD2 Y ψ)
  thus ?case
    using ExD2.hyps[of a "b⟨Y←_⟩"] TVso[of a b Y ψ] subE
    by (force simp: SetMod_def)
qed simp_all

text ‹Countable seed-form Tarski--Vaught hull: extends any countable
  nonempty @{text "(D0,E0) ⊆ (D,E)"} to a countable TV-closed pair
  @{text "(N,M)"} between them.›

lemma skolem_hull:
  assumes "D⇩0 ❙⊆ D" and "E⇩0 ❙⊆ E"
    and "∃x. D⇩0 x" and "∃S. E⇩0 S"
    and "countable {d. D⇩0 d}" and "countable {d. E⇩0 d}"
  obtains N M
    where "N ❙⊆ D" and "M ❙⊆ E"
      and "D⇩0 ❙⊆ N" and "E⇩0 ❙⊆ M"
      and "countable {d. N d}" and "countable {S. M S}"
      and "⋀y ψ a b.
             a into N ⟹ b into M ⟹
             (∃d. D d ∧ ⟨I,D,E⟩,a[y←d],b ⊨⇧d ψ) ⟹
             (∃d. N d ∧ ⟨I,D,E⟩,a[y←d],b ⊨⇧d ψ)"
      and "⋀Y ψ a b.
             a into N ⟹ b into M ⟹
             (∃S. E S ∧ ⟨I,D,E⟩,a,b⟨Y←S⟩ ⊨⇧d ψ) ⟹
             (∃S. M S ∧ ⟨I,D,E⟩,a,b⟨Y←S⟩ ⊨⇧d ψ)"
proof -
  obtain g :: "ℰ" where g: "Range g = D⇩0"
    by (metis (mono_tags, lifting) Collect_inj
        assms(3,5) empty_Collect_eq full_SetCompr_eq
        range_from_nat_into)
  obtain G :: "𝒢" where G: "Range G = E⇩0"
    by (metis (mono_tags, lifting) Collect_inj
        assms(4,6) empty_Collect_eq full_SetCompr_eq
        range_from_nat_into)
  define Dh where Dh: "Dh = (λd. ∃n. fst (stage I D E g G n) d)"
  define Eh where Eh: "Eh = (λS. ∃n. snd (stage I D E g G n) S)"
  have base:
      "Range g d ⟹ fst (stage I D E g G 0) d"
      "Range G S ⟹ snd (stage I D E g G 0) S"
    for d S
    by simp_all
  have RgDh: "Range g ❙⊆ Dh"
    and RGEh: "Range G ❙⊆ Eh"
    using base unfolding Dh Eh by blast+
  have DhsubD: "Dh ❙⊆ D"
    using fst_stage_subD assms(1)
    unfolding Dh by (metis (full_types) g)
  have EhsubE: "Eh ❙⊆ E"
    using snd_stage_subE assms(2)
    unfolding Eh by (metis (mono_tags, lifting) G)
  have cDh: "countable {d. Dh d}"
    and cEh: "countable {S. Eh S}"
    unfolding Dh Eh by (rule stage_omega_countable)+
  have TVfo:
      "a into Dh ⟹ b into Eh ⟹
       (∃d. D d ∧ ⟨I,D,E⟩,a[y←d],b ⊨⇧d ψ) ⟹
       (∃d. Dh d ∧ ⟨I,D,E⟩,a[y←d],b ⊨⇧d ψ)"
    for y ψ a b
    unfolding Dh Eh by (rule stage_TV_FO)
  have TVso:
      "a into Dh ⟹ b into Eh ⟹
       (∃S. E S ∧ ⟨I,D,E⟩,a,b⟨Y←S⟩ ⊨⇧d ψ) ⟹
       (∃S. Eh S ∧ ⟨I,D,E⟩,a,b⟨Y←S⟩ ⊨⇧d ψ)"
    for Y ψ a b
    unfolding Dh Eh by (rule stage_TV_SO)
  show ?thesis
    using DhsubD EhsubE G RGEh RgDh TVfo TVso cDh cEh g that
    by force
qed

text ‹Downward L\"owenheim--Skolem: TV-closure is upgraded to genuine
  elementarity via @{text truth_pres}.›

theorem DownwardLowenheimSkolem:
  assumes "D⇩0 ❙⊆ D" and "E⇩0 ❙⊆ E"
    and "∃x. D⇩0 x" and "∃x. E⇩0 x"
    and "countable {d. D⇩0 d}" and "countable {S. E⇩0 S}"
  shows "∃N M.
           D⇩0 ❙⊆ N ∧ countable {d. N d}
           ∧ E⇩0 ❙⊆ M ∧ countable {S. M S}
           ∧ ⟨I,N,M⟩ ⊆⇩E ⟨I,D,E⟩"
proof -
  obtain N M
    where "N ❙⊆ D" "M ❙⊆ E"
      "D⇩0 ❙⊆ N" "E⇩0 ❙⊆ M"
      "countable {d. N d}" "countable {S. M S}"
      "⋀y ψ a b.
         a into N ⟹ b into M ⟹
         ∃d:D. ⟨I,D,E⟩,a[y ← d],b ⊨⇧d ψ ⟹
         ∃d:N. ⟨I,D,E⟩,a[y ← d],b ⊨⇧d ψ"
      "⋀Y ψ a b.
         a into N ⟹ b into M ⟹
         ∃S:E. ⟨I,D,E⟩,a,b⟨Y ← S⟩ ⊨⇧d ψ ⟹
         ∃S:M. ⟨I,D,E⟩,a,b⟨Y ← S⟩ ⊨⇧d ψ"
    using skolem_hull[of D⇩0 D E⇩0 E, OF assms] by blast
  hence "D⇩0 ❙⊆ N ∧ countable {d. N d}
         ∧ E⇩0 ❙⊆ M ∧ countable {S. M S}
         ∧ ⟨I,N,M⟩ ⊆⇩E ⟨I,D,E⟩"
    using ElementarySubstructure_def truth_pres
          skolem_hull[of D⇩0 D E⇩0 E, OF assms]
    by auto
  thus ?thesis by blast
qed

text ‹Strongest faithfulness: standard validity = minimal validity over
  elementary interpretations.›

theorem Deep'_to_MinS:
  "(⊨⇧d' φ) = (∀II gg GG. MinS_ES_Univ II gg GG ⟶ MinS.ValM (MinS.DpToShM II gg GG φ))"
proof
  assume "⊨⇧d' φ"
  thus "∀II gg. MinS_ES_Univ II gg ❙⊆ (λGG. MinS.ValM (MinS.DpToShM II gg GG φ))"
    using MinS.FaithfulMD MinS_ES.𝒩_valid_ES
          MinS_ES_Univ_def ValD'_def
    by blast
next
  assume A: "∀II gg GG.
               MinS_ES_Univ II gg GG
                 ⟶ MinS.ValM (MinS.DpToShM II gg GG φ)"
  show "⊨⇧d' φ"
    unfolding ValD'_def
  proof (safe)
    fix I :: ℐ and g :: ℰ and G :: 𝒢
    have "Range g ❙⊆ Univ" "Range G ❙⊆ Univ"
         "∃x. Range g x" "∃x. Range G x"
         "countable {d. MSOinHOL_preliminaries.Range g d}"
         "countable {S. MSOinHOL_preliminaries.Range G S}"
      by (auto simp add: full_SetCompr_eq)
    then obtain N M
      where 7: "Range g ❙⊆ N" "countable {d. N d}"
               "Range G ❙⊆ M" "countable {S. M S}"
        and ES: "⟨I,N,M⟩ ⊆⇩E ⟨I,Univ,Univ⟩"
      using DownwardLowenheimSkolem
              [where D⇩0="Range g" and E⇩0="Range G"
                 and D=Univ and E=Univ]
      by metis
    then obtain g' G'
      where g': "Range g' = N" and G': "Range G' = M"
        and g'G':
          "(⟨I,Range g',Range G'⟩,g',G' ⊨⇧d φ)
             = (⟨I,N,M⟩,g,G ⊨⇧d φ)"
      using reindex by (smt (verit, best) reindex_coincide)
    hence "⟨I,Range g',Range G'⟩ ⊆⇩E ⟨I,Univ,Univ⟩"
      using ES by presburger
    then interpret MinS_ES_Univ I g' G'
      by (simp add: MinS_ES.intro MinS_ES_Univ_def)
    have "MinS.ValM (MinS.DpToShM I g' G' φ)"
      using A MinS_ES_Univ_axioms by blast
    hence "⟨I,N,M⟩,g,G ⊨⇧d φ"
      using FaithfulMDlem ValM_def g' G' g'G' by blast
    thus "⟨I,Univ,Univ⟩,g,G ⊨⇧d φ"
      using ES
      unfolding ElementarySubstructure_def
      by (smt (verit, best) "7"(1,3) G' g')
  qed
qed

text ‹Faithfulness to the standard reading (companion of
  @{text Faithful_to_Henkin}).›

corollary Faithful_to_Standard:
  "(⊨⇧d' φ) = (∀II gg GG. MinS_ES_Univ II gg GG ⟶ MinS.ValM (MinS.DpToShM II gg GG φ))"
  using Deep'_to_MinS .

text ‹Earlier Range-seeded route to the general-reading converse: the
  hull packaged with its truth-preservation payoff, derived in one step
  from @{text DownwardLowenheimSkolem}.›

lemma ls_hull:
  assumes gD: "g into D" and GE: "G into E"
  obtains D⇩0 E⇩0
    where "D⇩0 ❙⊆ D" and "E⇩0 ❙⊆ E"
      and "Range g ❙⊆ D⇩0" and "Range G ❙⊆ E⇩0"
      and "countable {d. D⇩0 d}" and "countable {S. E⇩0 S}"
      and "(⟨I,D⇩0,E⇩0⟩,g,G ⊨⇧d φ) = (⟨I,D,E⟩,g,G ⊨⇧d φ)"
proof -
  have *:
      "Range g ❙⊆ D" "Range G ❙⊆ E"
      "∃x. Range g x" "∃x. Range G x"
      "countable {d. Range g d}" "countable {S. Range G S}"
    using assms by (auto simp: full_SetCompr_eq)
  obtain N M
    where N: "Range g ❙⊆ N" "countable {d. N d}"
              "Range G ❙⊆ M" "countable {S. M S}"
      and ES: "⟨I,N,M⟩ ⊆⇩E ⟨I,D,E⟩"
    using DownwardLowenheimSkolem
            [where D⇩0="Range g" and E⇩0="Range G",
             OF *(1,2,3,4,5,6), of I]
    by metis
  have sub: "N ❙⊆ D" "M ❙⊆ E"
    and ES':
      "⋀g G φ. G into M ⟹ g into N ⟹
        (⟨I,D,E⟩,g,G ⊨⇧d φ) = (⟨I,N,M⟩,g,G ⊨⇧d φ)"
    using ES unfolding ElementarySubstructure_def by auto
  have gn: "g into N" "G into M"
    using into_Range N(1,3) by (metis (mono_tags, lifting))+
  show thesis
    using that[OF sub N(1,3,2,4) ES'[OF gn(2) gn(1), symmetric]] .
qed

text ‹Range reduction: countermodels reduce to range-only
  countermodels.›

lemma Range_reduction:
  assumes "g into D" and "G into E"
  obtains g' G'
    where "(⟨I,Range g',Range G'⟩,g',G' ⊨⇧d φ)
             = (⟨I,D,E⟩,g,G ⊨⇧d φ)"
proof -
  obtain D⇩0 E⇩0
    where *:
        "Range g ❙⊆ D⇩0" "Range G ❙⊆ E⇩0"
        "countable {d. D⇩0 d}" "countable {S. E⇩0 S}"
      and eq:
        "(⟨I,D⇩0,E⇩0⟩,g,G ⊨⇧d φ) = (⟨I,D,E⟩,g,G ⊨⇧d φ)"
    using assms by (rule ls_hull)
  obtain g' G'
    where rg: "Range g' = D⇩0" and rG: "Range G' = E⇩0"
      and coin:
        "(⟨I,D⇩0,E⇩0⟩,g,G ⊨⇧d φ)
           = (⟨I,D⇩0,E⇩0⟩,g',G' ⊨⇧d φ)"
    using reindex_coincide[OF *(3,4,1,2)] by blast
  show thesis using that[of g' G'] rg rG eq coin by simp
qed

text ‹Range-relative = general (Henkin) deep validity.›

theorem RangeValid_imp_ValD: "⊨⇧r φ ⟹ ⊨⇧d φ"
  unfolding RangeValid_def ValD_def
  using Range_reduction by metis

corollary RangeValid_iff_ValD: "(⊨⇧r φ) = (⊨⇧d φ)"
  using RangeValid_imp_ValD ValD_imp_RangeValid by blast

text ‹Faithfulness to the general (Henkin) reading.  Together with
  @{text Faithful_to_Standard} it yields the two faithfulness results;
  the limitative @{text Standard_strictly_stronger} below separates them.›

corollary Faithful_to_Henkin: "(⊨⇧r φ) = (⊨⇧d φ)"
  using RangeValid_iff_ValD .

text ‹The standard reading is strictly stronger; comprehension witnesses
  the gap.›

lemma Standard_strictly_stronger:
  "(∀(φ::ℱ). (⊨⇧d φ) ⟶ (⊨⇧d' φ)) ∧ (∃(φ::ℱ). (⊨⇧d' φ) ∧ ¬ (⊨⇧d φ))"
proof
  show "∀(φ::ℱ). (⊨⇧d φ) ⟶ (⊨⇧d' φ)"
    using Val by blast
next
  let ?φ = "∃⇧d⇩2(0::V2). ∀⇧d(0::V).
              (((0::V2)⇧d((0::V)))
                 ⟷⇧d ((0::R)⇧d((0::V),(0::V))))"
  have "⊨⇧d' ?φ" by (rule comprehension_atom)
  moreover have "¬ (⊨⇧d ?φ)"
    unfolding DefD
    apply (rule notI,
           drule spec[where x="λr (a::D) b. a = b"],
           drule spec[where x="Univ::D⇒bool"],
           drule spec[where x="λS::D⇒bool. ∃d::D. ¬S d"],
           drule spec[where x="λx::V. undefined::D"],
           drule spec[where x="λX::V2. λd::D. False"])
    by (auto simp: SetMod_def EnvMod_def)
  ultimately show "∃(φ::ℱ). (⊨⇧d' φ) ∧ ¬ (⊨⇧d φ)"
    by blast
qed

end