Theory MSOinHOL_comprehension

theory MSOinHOL_comprehension
  imports MSOinHOL_deep_subst_lemma
begin

text ‹Monadic comprehension as a derived schema: under the full
  second-order domain (@{text "ValD'"}, ‹E = Univ›) comprehension holds
  for every ‹φ› with ‹X› not free; the witness is the set defined by
  ‹φ›.›

theorem comprehension_schema:
  assumes "X not_free2_in φ"
  shows "⊨⇧^d' (∃⇧^d⇩₂X. ∀⇧^dx. ((X⇧^d(x)) ⟷⇧^d φ))"
  unfolding ValD'_def
proof (intro allI)
  fix I g G
  let ?S = "λd. ⟨I,Univ,Univ⟩,g[x←d],G ⊨⇧^d φ"
  have "⟨I,Univ,Univ⟩,g,G⟨X←?S⟩ ⊨⇧^d (∀⇧^dx. ((X⇧^d(x)) ⟷⇧^d φ))"
    using assms by (simp add: DefD N12)
  thus "⟨I,Univ,Univ⟩,g,G ⊨⇧^d (∃⇧^d⇩₂X. ∀⇧^dx. ((X⇧^d(x)) ⟷⇧^d φ))"
    by auto
qed

text ‹Headline instance (cf. ‹comprehension_d›): the set of
  ‹r›-self-related individuals exists.›

corollary comprehension_atom:
  "⊨⇧^d' (∃⇧^d⇩₂X. ∀⇧^dx. ((X⇧^d(x)) ⟷⇧^d (r⇧^d(x,x))))"
  by (rule comprehension_schema) simp

text ‹Standard vs.\ weak (Henkin): ‹comprehension_schema› needs
  ‹E = Univ› and fails for general @{text "ValD"}---the
  standard-vs-Henkin gap behind the Loewenheim--Skolem problem, treated
  in the next section (\emph{Downward Löwenheim--Skolem}).›

end