Theory MSOinHOL_experiments

theory MSOinHOL_experiments
  imports
    MSOinHOL_deep
    MSOinHOL_shallow
    MSOinHOL_shallow_minimal
begin

abbreviation "(x::V) ≡ 1"
abbreviation "(y::V) ≡ 2"
abbreviation "(z::V) ≡ 3"
abbreviation "(X::V2) ≡ 1"
abbreviation "(Y::V2) ≡ 2"

consts P :: R

subsubsection ‹Propositional tautologies, lifted to MSO in all three embeddings›

lemma "⊨⇧^d (P⇧^d(x,x) ⊃⇧^d P⇧^d(x,x))"
  unfolding DefD by simp

lemma "⊨⇧^s (P⇧^s(x,x) ⊃⇧^s P⇧^s(x,x))"
  unfolding DefS by simp

lemma "⊨⇧^m (P⇧^m(x,x) ⊃⇧^m P⇧^m(x,x))"
  unfolding DefM by simp

lemma "⊨⇧^d (¬⇧^d¬⇧^d P⇧^d(x,y)) ⊃⇧^d P⇧^d(x,y)"
  unfolding DefD by auto

lemma "⊨⇧^s (¬⇧^s¬⇧^s P⇧^s(x,y)) ⊃⇧^s P⇧^s(x,y)"
  unfolding DefS by auto

lemma "⊨⇧^m (¬⇧^m¬⇧^m P⇧^m(x,y)) ⊃⇧^m P⇧^m(x,y)"
  unfolding DefM by auto

subsubsection ‹First-order tautologies›

text ‹The individual domain is inhabited whenever some assignment exists.›

lemma "⊨⇧^d (∀⇧^dx. P⇧^d(x,x)) ⊃⇧^d (∃⇧^dx. P⇧^d(x,x))"
  unfolding DefD by auto

lemma "⊨⇧^s (∀⇧^sx. P⇧^s(x,x)) ⊃⇧^s (∃⇧^sx. P⇧^s(x,x))"
  unfolding DefS by auto

lemma "⊨⇧^m (∀⇧^mx. P⇧^m(x,x)) ⊃⇧^m (∃⇧^mx. P⇧^m(x,x))"
  unfolding DefM by auto

subsubsection ‹Membership tautology›

text ‹Every individual that is in ‹X› is in ‹X›.›

lemma "⊨⇧^d (∀⇧^dx. (X⇧^d(x) ⊃⇧^d X⇧^d(x)))"
  unfolding DefD by auto

lemma "⊨⇧^s (∀⇧^sx. (X⇧^s(x) ⊃⇧^s X⇧^s(x)))"
  unfolding DefS by auto

lemma "⊨⇧^m (∀⇧^mx. (X⇧^m(x) ⊃⇧^m X⇧^m(x)))"
  unfolding DefM by auto

subsubsection ‹Monadic comprehension›

text ‹Headline second-order validity: the set of ‹P›-self-related
  individuals exists.  Stated over the full second-order domain, where
  every monadic set is admissible.›

lemma comprehension_d:
  "⊨⇧^d' (∃⇧^d⇩₂X. ∀⇧^dx. ((X⇧^d(x)) ⟷⇧^d P⇧^d(x,x)))"
  unfolding DefD by (intro allI; simp) meson

lemma comprehension_s:
  "⊨⇧^s' (∃⇧^s⇩₂X. ∀⇧^sx. ((X⇧^s(x)) ⟷⇧^s P⇧^s(x,x)))"
  unfolding DefS by (intro allI; simp) meson

text ‹A universal monadic set exists over the full domain (the predicate
  that holds everywhere).›

lemma "⊨⇧^d' (∃⇧^d⇩₂X. ∀⇧^dx. (X⇧^d(x)))"
  unfolding DefD by (simp, rule exI[where x="λd. True"]) simp

subsubsection ‹Invalid schemata›

text ‹‹nitpick› reports finite countermodels (using the full-domain
  relation).›

text ‹Not every monadic set is inhabited: the empty set is a countermodel
  to ‹∀X. ∃x. x ∈ X›.›

lemma "⊨⇧^d' (∀⇧^d⇩₂X. ∃⇧^dx. (X⇧^d(x)))"
  unfolding DefD apply simp nitpick oops

text ‹Symmetry of ‹P› is not implied: ‹nitpick› produces a 2-element
  countermodel.›

lemma "⊨⇧^d' (∀⇧^dx. ∀⇧^dy. (P⇧^d(x,y) ⊃⇧^d P⇧^d(y,x)))"
  unfolding DefD apply simp nitpick oops

text ‹No monadic set can contain and exclude every individual at once:
  ‹∃X. ∀x. x∈X ∧ ¬x∈X› is unsatisfiable, hence invalid.›

lemma "⊨⇧^d' (∃⇧^d⇩₂X. ∀⇧^dx. ((X⇧^d(x)) ∧⇧^d ¬⇧^d(X⇧^d(x))))"
  unfolding DefD apply simp nitpick oops

end