Theory HOMLinHOL

section‹Mechanization of higher-order modal logic (HOML)›
subsection‹HOMLinHOL.thy (Figure 3 of \cite{J75})›
text‹Shallow embedding of higher-order modal logic (HOML) in the classical higher-order logic (HOL)
of Isabelle/HOL utilizing the logic-pluralistic LogiKEy methodology. Here logic S5 is introduced.›
theory HOMLinHOL imports Main
begin

―‹Global parameters setting for the model finder nitpick and the parser; unimport for the reader›
 nitpick_params[user_axioms,expect=genuine,show_all,format=2,max_genuine=3]
 declare[[syntax_ambiguity_warning=false]] 

―‹Type i is associated with possible worlds and type e with entities›
typedecl i ―‹Possible worlds› 
typedecl e ―‹Individuals/entities› 
type_synonym σ = "i⇒bool" ―‹World-lifted propositions›
type_synonym τ = "e⇒σ" ―‹Modal properties›

consts R::"i⇒i⇒bool" ("_❙r_") ―‹Accessibility relation between worlds›

axiomatization where
 Rrefl: "∀x. x❙rx" and 
 Rsymm: "∀x y. x❙ry ⟶ y❙rx" and 
 Rtrans: "∀x y z. x❙ry ∧ y❙rz ⟶ x❙rz" 

―‹Logical connectives (operating on truth-sets)›
abbreviation Mbot::σ ("❙⊥") where "❙⊥ ≡ λw. False"
abbreviation Mtop::σ ("❙⊤") where "❙⊤ ≡ λw. True"
abbreviation Mneg::"σ⇒σ" ("❙¬_" [52]53) where "❙¬φ ≡ λw. ¬(φ w)"
abbreviation Mand::"σ⇒σ⇒σ" (infixl "❙∧" 50) where "φ❙∧ψ ≡ λw. φ w ∧ ψ w" 
abbreviation Mor::"σ⇒σ⇒σ" (infixl "❙∨" 49) where "φ❙∨ψ ≡ λw. φ w ∨ ψ w "
abbreviation Mimp::"σ⇒σ⇒σ" (infixr "❙⊃" 48) where "φ❙⊃ψ ≡ λw. φ w ⟶ ψ w" 
abbreviation Mequiv::"σ⇒σ⇒σ" (infixl "❙↔" 47) where "φ❙↔ψ ≡ λw. φ w ⟷ ψ w"
abbreviation Mbox::"σ⇒σ" ("❙□_" [54]55) where "❙□φ ≡ λw.∀v. w ❙r v ⟶ φ v"
abbreviation Mdia::"σ⇒σ" ("❙◇_" [54]55) where "❙◇φ ≡ λw.∃v. w ❙r v ∧ φ v"
abbreviation Mprimeq::"'a⇒'a⇒σ" ("_❙=_") where "x❙=y ≡ λw. x=y"
abbreviation Mprimneg::"'a⇒'a⇒σ" ("_❙≠_") where "x❙≠y ≡ λw. x≠y"
abbreviation Mnegpred::"τ⇒τ" ("❙~_") where "❙~Φ ≡ λx.λw. ¬Φ x w"
abbreviation Mconpred::"τ⇒τ⇒τ" (infixl "❙." 50) where "Φ❙.Ψ ≡ λx.λw. Φ x w ∧ Ψ x w"
abbreviation Mexclor::"σ⇒σ⇒σ" (infixl "❙∨⇧e" 49) where "φ❙∨⇧eψ ≡ (φ ❙∨ ψ) ❙∧ ❙¬(φ ❙∧ ψ)" 

―‹Possibilist quantifiers (polymorphic)›
abbreviation Mallposs::"('a⇒σ)⇒σ" ("❙∀") where "❙∀Φ ≡ λw.∀x. Φ x w"
abbreviation Mallpossb (binder "❙∀" [8]9) where "❙∀x. φ(x) ≡ ❙∀φ" 
abbreviation Mexiposs::"('a⇒σ)⇒σ" ("❙∃") where "❙∃Φ ≡ λw.∃x. Φ x w" 
abbreviation Mexipossb (binder "❙∃" [8]9) where "❙∃x. φ(x) ≡ ❙∃φ" 

―‹Actualist quantifiers (for individuals/entities)›
consts existsAt::"e⇒σ" ("_❙@_") 
abbreviation Mallact::"(e⇒σ)⇒σ" ("❙∀⇧E") where "❙∀⇧EΦ ≡ λw.∀x. x❙@w ⟶ Φ x w"
abbreviation Mallactb (binder "❙∀⇧E" [8]9) where "❙∀⇧Ex. φ(x) ≡ ❙∀⇧Eφ" 
abbreviation Mexiact::"(e⇒σ)⇒σ" ("❙∃⇧E") where "❙∃⇧EΦ ≡ λw.∃x. x❙@w ∧ Φ x w"
abbreviation Mexiactb (binder "❙∃⇧E" [8]9) where "❙∃⇧Ex. φ(x) ≡ ❙∃⇧Eφ"

―‹Leibniz equality (polymorphic)›
abbreviation Mleibeq::"'a⇒'a⇒σ" ("_❙≡_") where "x❙≡y ≡ ❙∀P. P x ❙⊃ P y"

―‹Meta-logical predicate for global validity›
abbreviation Mvalid::"σ⇒bool" ("⌊_⌋") where "⌊ψ⌋ ≡ ∀w. ψ w"

end