Theory logics_quantifiers

theory logics_quantifiers
  imports boolean_algebra_infinitary
begin

subsection ‹Quantifiers (restricted and unrestricted)›

text‹Introduce pedagogically convenient notation.›
notation HOL.All (‹Π›) notation HOL.Ex (‹Σ›)

text‹Let us recall that in HOL we have: ›
lemma "(∀x. P) = Π(λx. P)" by simp
lemma "(∃x. P) = Σ(λx. P)" by simp
lemma "Σ = (λP. ¬Π(λx. ¬P x))" by simp

text‹We can introduce their respective 'w-type-lifted variants as follows: ›
definition mforall::"('i⇒'w σ)⇒'w σ" (‹❙Π_›)
  where "❙Πφ ≡ λw. ∀X. φ X w"
definition mexists::"('i⇒'w σ)⇒'w σ" (‹❙Σ_›) 
  where "❙Σφ ≡ λw. ∃X. φ X w"

text‹To improve readability, we introduce for them standard binder notation.›
notation mforall (binder ‹❙∀› [48]49)  notation mexists (binder ‹❙∃› [48]49) 

text‹And thus we obtain the 'w-type-lifted variant of the standard (variable-binding) quantifiers.›
lemma "(❙∀X. φ) = ❙Π(λX. φ)" by (simp add: mforall_def)
lemma "(❙∃X. φ) = ❙Σ(λX. φ)" by (simp add: mexists_def)

text‹Quantifiers are dual to each other in the expected way.›
lemma "❙Πφ = ❙─(❙Σφ⇧-)" by (simp add: compl_def mexists_def mforall_def svfun_compl_def)
lemma "(❙∀X. φ X) = ❙─(❙∃X. ❙─(φ X))" by (simp add: compl_def mexists_def mforall_def)

text‹Relationship between quantifiers and the infinitary supremum and infimum operations.›
lemma mforall_char: "❙Πφ = ❙⋀⟦φ _⟧" unfolding infimum_def mforall_def range_def by metis
lemma mexists_char:  "❙Σφ = ❙⋁⟦φ _⟧" unfolding supremum_def mexists_def range_def by metis
(*Using binder notation:*)
lemma mforallb_char: "(❙∀X. φ) = ❙⋀⟦(λX. φ) _⟧" unfolding infimum_def mforall_def range_def by simp
lemma mexistsb_char: "(❙∃X. φ) = ❙⋁⟦(λX. φ) _⟧" unfolding supremum_def mexists_def range_def by simp


text‹We now consider quantification restricted over constant and varying domains.›

text‹Constant domains: first generalization of quantifiers above (e.g. free logic).›
definition mforall_const::"'i σ ⇒ ('i ⇒ 'w σ) ⇒ 'w σ" (‹❙Π[_]_›) 
  where "❙Π[D]φ ≡ λw. ∀X. (D X) ⟶ (φ X) w" 
definition mexists_const::"'i σ ⇒ ('i ⇒ 'w σ) ⇒ 'w σ" (‹❙Σ[_]_›) 
  where "❙Σ[D]φ ≡ λw. ∃X. (D X)  ∧  (φ X) w"

(*Alas! the convenient binder notation cannot be easily introduced for restricted quantifiers.*)

text‹Constant-domain quantification generalises its unrestricted counterpart.›
lemma "❙Πφ = ❙Π[❙⊤]φ" by (simp add: mforall_const_def mforall_def top_def)
lemma "❙Σφ = ❙Σ[❙⊤]φ" by (simp add: mexists_const_def mexists_def top_def)

text‹Constant-domain quantification can also be characterised using infimum and supremum.›
lemma mforall_const_char: "❙Π[D]φ = ❙⋀⟦φ D⟧" unfolding image_def infimum_def mforall_const_def by metis
lemma mexists_const_char: "❙Σ[D]φ = ❙⋁⟦φ D⟧" unfolding image_def supremum_def mexists_const_def by metis

text‹Constant-domain quantifiers also  allow us to nicely characterize the interaction between
 function composition and (restricted) quantification:›
lemma mforall_comp: "❙Π(φ∘ψ) = ❙Π[⟦ψ _⟧] φ" unfolding fun_comp_def mforall_const_def mforall_def range_def by metis
lemma mexists_comp: "❙Σ(φ∘ψ) = ❙Σ[⟦ψ _⟧] φ" unfolding fun_comp_def mexists_const_def mexists_def range_def by metis


text‹Varying domains: we can also restrict quantifiers by taking a 'functional domain' as additional parameter.
The latter is a set-valued mapping each element 'i to a set of points (e.g. where it 'exists').›
definition mforall_var::"('i ⇒ 'w σ) ⇒ ('i ⇒ 'w σ) ⇒ 'w σ" (‹❙Π{_}_›) 
  where "❙Π{ψ}φ ≡ λw. ∀X. (ψ X) w ⟶ (φ X) w" 
definition mexists_var::"('i ⇒ 'w σ) ⇒ ('i ⇒ 'w σ) ⇒ 'w σ" (‹❙Σ{_}_›) 
  where "❙Σ{ψ}φ ≡ λw. ∃X. (ψ X) w  ∧  (φ X) w"

text‹Varying-domain quantification generalizes its constant-domain counterpart.›
lemma "❙Π[D]φ = ❙Π{D↿}φ" by (simp add: mforall_const_def mforall_var_def)
lemma "❙Σ[D]φ = ❙Σ{D↿}φ" by (simp add: mexists_const_def mexists_var_def)

text‹Restricted quantifiers are dual to each other in the expected way.›
lemma "❙Π[D]φ = ❙─(❙Σ[D]φ⇧-)" by (metis iDM_b im_prop2 mexists_const_char mforall_const_char setequ_ext)
lemma "❙Π{ψ}φ = ❙─(❙Σ{ψ}φ⇧-)" by (simp add: compl_def mexists_var_def mforall_var_def svfun_compl_def)

text‹We can use 2nd-order connectives on set-valued functions to encode restricted quantifiers as unrestricted.›
lemma "❙Π{ψ}φ = ❙Π(ψ ❙→⇧: φ)" by (simp add: impl_def mforall_def mforall_var_def svfun_impl_def)
lemma "❙Σ{ψ}φ = ❙Σ(ψ ❙∧⇧: φ)" by (simp add: meet_def mexists_def mexists_var_def svfun_meet_def)

text‹Observe that using these operators has the advantage of allowing for binder notation.›
lemma "❙Π{ψ}φ = (❙∀X. (ψ ❙→⇧: φ) X)" by (simp add: impl_def mforall_def mforall_var_def svfun_impl_def)
lemma "❙Σ{ψ}φ = (❙∃X. (ψ ❙∧⇧: φ) X)" by (simp add: meet_def mexists_def mexists_var_def svfun_meet_def)

text‹To sumarize: different sorts of restricted quantification can be emulated 
  by employing 2nd-order operations to adequately relativize predicates.›
lemma "❙Π[D]φ = (❙∀X. (D↿ ❙→⇧: φ) X)" by (simp add: impl_def mforall_const_def mforall_def svfun_impl_def)
lemma "❙Π{❙⊤⇧:}φ = (❙∀X. (❙⊤⇧: ❙→⇧: φ) X)" by (simp add: impl_def mforall_def mforall_var_def svfun_impl_def)
lemma "❙Πφ = ❙Π{❙⊤⇧:}φ" by (simp add: mforall_def mforall_var_def svfun_top_def top_def)
lemma "(❙∀X. φ X) = ❙Π{❙⊤⇧:}φ" by (simp add: mforall_def mforall_var_def svfun_top_def top_def)

named_theorems quant (*to group together definitions related to quantification*)
declare mforall_def[quant] mexists_def[quant]
        mforall_const_def[quant] mexists_const_def[quant]
        mforall_var_def[quant] mexists_var_def[quant]

end