Theory MFilter

section‹Presentation of All Variants as Studied in \<^cite>‹"C85"› \label{sec:all}›

subsection‹Preliminaries: Modal Ultrafilter (Fig.~2 in \<^cite>‹"C85"›)›

theory MFilter imports HOML
begin 
text‹Some abbreviations for auxiliary operations.›
abbreviation a::"γ⇒(γ⇒σ)⇒σ" ("_❙∈_") where "x❙∈S ≡ S x"
abbreviation b::γ ("❙∅") where "❙∅ ≡ λx. ❙⊥"  
abbreviation c::γ ("❙U") where "❙U ≡ λx. ❙⊤"
abbreviation d::"γ⇒γ⇒σ" ("_❙⊆_") where "φ❙⊆ψ ≡ ❙∀x.((φ x) ❙→ (ψ x))"
abbreviation e::"γ⇒γ⇒γ" ("_❙⊓_") where "φ❙⊓ψ ≡ λx.((φ x) ❙∧ (ψ x))"
abbreviation f::"γ⇒γ" ("¯_") where "¯ψ ≡ λx. ❙¬(ψ x)"  

text‹Definition of modal filter.›
abbreviation g::"(γ⇒σ)⇒σ" ("Filter") 
 where "Filter Φ ≡ (((❙U❙∈Φ) ❙∧ ❙¬(❙∅❙∈Φ))
         ❙∧ (❙∀φ ψ. (((φ❙∈Φ) ❙∧ (φ❙⊆ψ)) ❙→ (ψ❙∈Φ))))
         ❙∧ (❙∀φ ψ. (((φ❙∈Φ) ❙∧ (ψ❙∈Φ)) ❙→ ((φ❙⊓ψ)❙∈Φ)))"

text‹Definition of modal ultrafilter .›
abbreviation h::"(γ⇒σ)⇒σ" ("UFilter") where 
 "UFilter Φ ≡ (Filter Φ)❙∧(❙∀φ.((φ❙∈Φ) ❙∨ ((¯φ)❙∈Φ)))"

text‹Modal filter and modal ultrafilter are consistent.›
lemma "⌊❙∀Φ φ.((UFilter Φ) ❙→ ❙¬((φ❙∈Φ) ❙∧ ((¯φ)❙∈Φ)))⌋" by force
end