Theory MSOinHOL_shallow_minimal_elementary

theory MSOinHOL_shallow_minimal_elementary
  imports
    MSOinHOL_faithfulness_locale
    MSOinHOL_lowenheim_skolem
begin

text ‹Extra simp rules for @{term DpToShS} (derived quantifiers and
  connectives).›

lemma (in MinS) DpToShS_All [simp]:
  "⦇∀⇧dx. φ⦈ = (∀⇧md. ⦇[x ←⇩r d](φ)⦈)"
  unfolding DefD DefM by (simp add: ExM_def NegM_def ren_subst_def)

lemma (in MinS) DpToShS_All2 [simp]:
  "⦇∀⇧d⇩2x. φ⦈ = (∀⇧m⇩2d. ⦇[x ←⇩r⇩2 d](φ)⦈)"
  unfolding DefD DefM using MinS.FaithfulMDlem by auto

lemma (in MinS) DpToShS_Equiv [simp]:
  "⦇φ ⟷⇧d ψ⦈ = (⦇φ⦈ ⟷⇧m ⦇ψ⦈)"
  unfolding DefD DefM by (simp add: AndM_def NegM_def)

lemma (in MinS) DpToShS_Imp [simp]:
  "⦇φ ⊃⇧d ψ⦈ = (⦇φ⦈ ⊃⇧m ⦇ψ⦈)"
  unfolding DefD DefM by (simp add: AndM_def NegM_def)

text ‹Elementary constants-only presentation: @{text II}, @{text gg},
  @{text GG} chosen so that the global interpretation is a
  @{text MinS_ES_Univ} (existence via @{text Deep'_to_MinS}).›

consts II :: ℐ  gg :: ℰ  GG :: 𝒢

specification (II gg GG) ES_Univ: "MinS_ES_Univ II gg GG"
  by (meson Deep'_to_MinS RelativeTruthD.simps ValD'_def)

global_interpretation MinS_ES_Univ II gg GG
  using ES_Univ by auto

notation AtmM    ("_⇧m'(_,_')")
    and PrdM    ("_⇧m'(_')")
    and NegM    ("¬⇧m _" [58] 59)
    and AndM    (infixr "∧⇧m" 56)
    and ExM     (binder "∃⇧m" 53)
    and ExM2    (binder "∃⇧m⇩2" 53)
    and OrM     (infixr "∨⇧m" 54)
    and ImpM    (infixr "⊃⇧m" 55)
    and IffM    (infixr "⟷⇧m" 54)
    and AllM    (binder "∀⇧m" 53)
    and AllM2   (binder "∀⇧m⇩2" 53)
    and ValM    ("⊨⇧m _" 9)
    and DpToShM ("⦇_⦈")

text ‹Faithfulness under universal carriers.›

lemma FaithfulMD_ES: "(⊨⇧m ⦇φ⦈) = ⟨II,Univ,Univ⟩,gg,GG ⊨⇧d φ"
  using FaithfulMD 𝒩_valid_ES_Univ by blast

text ‹Inheritance: standard validity transfers to minimal validity.›

lemma ValidM_if_ValidD': "(⊨⇧d' φ) ⟹ (⊨⇧m ⦇φ⦈)"
  by (metis MinS_ES_Univ_axioms Deep'_to_MinS)

end