Theory logics_quantifiers_example

theory logics_quantifiers_example
  imports logics_quantifiers conditions_positive_infinitary
begin

subsection ‹Examples on Quantifiers›

text‹First-order quantification example.›
lemma "(∀x. A x ⟶ (∃y. B x y)) ⟷ (∀x. ∃y. A x ⟶ B x y)" by simp
lemma "(❙∀x. A x  ❙→ (❙∃y. B x y))  ❙= (❙∀x. ❙∃y. A x  ❙→  B x y)" by (simp add: impl_def mexists_def setequ_def)

text‹Propositional quantification example.›
lemma "∀A. (∃B. (A ⟷ ¬B))" by blast
lemma "(❙∀A. (❙∃B. A  ❙↔ ❙─B)) ❙= ❙⊤" unfolding mforall_def mexists_def by (smt (verit) compl_def dimpl_def setequ_def top_def)

text‹Drinker's principle.›
lemma "❙∃x. Drunk x ❙→ (❙∀y. Drunk y) ❙= ❙⊤"
  by (simp add: impl_def mexists_def mforall_def setequ_def top_def)

text‹Example in non-classical logics.›
typedecl w 
type_synonym σ = "(w σ)"

consts 𝒞::"σ ⇒ σ"
abbreviation "ℐ ≡ 𝒞⇧d"
abbreviation "CLOSURE φ ≡ ADDI φ ∧ EXPN φ ∧ NORM φ ∧ IDEM φ"
abbreviation "INTERIOR φ ≡ MULT φ ∧ CNTR φ ∧ DNRM φ ∧ IDEM φ"

definition mforallInt::"(σ ⇒ σ) ⇒ σ" (‹❙Π⇧I_›) 
  where "❙Π⇧Iφ ≡ ❙Π[fp ℐ]φ"
definition mexistsInt::"(σ ⇒ σ) ⇒ σ" (‹❙Σ⇧I_›) 
  where "❙Σ⇧Iφ ≡ ❙Σ[fp ℐ]φ"

(*To improve readability, we introduce for them standard binder notation.*)
notation mforallInt (binder ‹❙∀⇧I› [48]49) 
notation mexistsInt (binder ‹❙∃⇧I› [48]49) 

abbreviation intneg (‹❙¬⇧I_›) where "❙¬⇧IA ≡ ℐ⇧d⇧- A"
abbreviation parneg (‹❙¬⇧C_›) where "❙¬⇧CA ≡ 𝒞⇧d⇧- A"

lemma "(❙∀X. (❙∃B. (X  ❙↔ ❙─B))) ❙= ❙⊤" by (smt (verit, del_insts) compl_def dimpl_def mexists_def mforall_def setequ_def top_def)
lemma "(❙∀⇧IX. (❙∃⇧IB. (X  ❙↔ ❙¬⇧IB))) ❙= ❙⊤" nitpick oops ―‹ counterexample ›


subsection ‹Barcan formula and its converse›

text‹The converse Barcan formula follows readily from monotonicity.›
lemma CBarcan1: "MONO φ ⟹ ∀π.  φ(❙∀x. π x)  ❙≤ (❙∀x. φ(π x))" by (smt (verit, ccfv_SIG) MONO_def mforall_def subset_def)
lemma CBarcan2: "MONO φ ⟹ ∀π. (❙∃x. φ(π x)) ❙≤ φ(❙∃x. π x)" by (smt (verit) MONO_def mexists_def subset_def)

text‹However, the Barcan formula requires a stronger assumption (of an infinitary character).›
lemma Barcan1: "iMULT⇧b φ ⟹ ∀π. (❙∀x. φ(π x)) ❙≤ φ(❙∀x. π x)" unfolding iMULT_b_def by (smt (verit) infimum_def mforall_char image_def range_char1 subset_def)
lemma Barcan2: "iADDI⇧a φ ⟹ ∀π. φ(❙∃x. π x) ❙≤ (❙∃x. φ(π x))" unfolding iADDI_a_def by (smt (verit, ccfv_threshold) mexists_char image_def range_char1 subset_def supremum_def)

text‹Converse Barcan Formula and composition.›
lemma "MONO φ ⟹ ∀π.  φ(❙Π π) ❙≤ ❙Π(φ ∘ π)" by (metis MONO_iMULTa iMULT_a_def mforall_char mforall_comp mforall_const_char)
lemma "MONO φ ⟹ ∀π.  φ(❙Π[D] π) ❙≤ ❙Π[D](φ ∘ π)"  by (smt (verit) MONO_iMULTa fun_comp_def iMULT_a_def mforall_const_char mforall_const_def image_def subset_def)
lemma "CNTR φ ⟹ iMULT φ ⟹ IDEM φ ⟹  ∀π.  φ(❙Π{ψ} π) ❙≤ ❙Π{ψ}(φ ∘ π)" nitpick oops ―‹ counterexample ›

text‹Barcan Formula and composition.›
lemma "iMULT⇧b φ ⟹ ∀π. ❙Π(φ ∘ π) ❙≤ φ(❙Π π)" by (metis iMULT_b_def mforall_char mforall_comp mforall_const_char)
lemma "iMULT⇧b φ ⟹ ∀π. ❙Π[D](φ ∘ π) ❙≤ φ(❙Π[D] π)" by (smt (verit) fun_comp_def iMULT_b_def infimum_def mforall_const_char image_def subset_def)
lemma "iADDI φ ⟹ iMULT φ ⟹ ∀π. ❙Π{ψ}(φ ∘ π) ❙≤ φ(❙Π{ψ} π)" nitpick oops ―‹ counterexample ›

end