Theory HOML

section‹Higher-Order Modal Logic in HOL (cf.~\<^cite>‹"J23"› and Fig.~1 in \<^cite>‹"C85"›).›

theory HOML imports Main
begin
nitpick_params[user_axioms,expect=genuine]

text‹Type i is associated with possible worlds and type e with entities:›
typedecl i ―‹Possible worlds›  
typedecl e ―‹Individuals›      
type_synonym σ = "i⇒bool" ―‹World-lifted propositions›
type_synonym γ = "e⇒σ" ―‹Lifted predicates›
type_synonym μ = "σ⇒σ" ―‹Unary modal connectives›
type_synonym ν = "σ⇒σ⇒σ" ―‹Binary modal connectives›

text‹Logical connectives (operating on truth-sets):›
abbreviation c1::σ ("❙⊥") where "❙⊥ ≡ λw. False"
abbreviation c2::σ ("❙⊤") where "❙⊤ ≡ λw. True"
abbreviation c3::μ ("❙¬_"[52]53) where "❙¬φ ≡ λw.¬(φ w)"
abbreviation c4::ν (infix"❙∧"50) where "φ❙∧ψ ≡ λw.(φ w)∧(ψ w)"   
abbreviation c5::ν (infix"❙∨"49) where "φ❙∨ψ ≡ λw.(φ w)∨(ψ w)"
abbreviation c6::ν (infix"❙→"48) where "φ❙→ψ ≡ λw.(φ w)⟶(ψ w)"  
abbreviation c7::ν (infix"❙↔"47) where "φ❙↔ψ ≡ λw.(φ w)⟷(ψ w)"
consts R::"i⇒i⇒bool" ("_❙r_")  ―‹Accessibility relation›
abbreviation c8::μ ("❙□_"[54]55) where "❙□φ ≡ λw.∀v.(w❙rv)⟶(φ v)"
abbreviation c9::μ ("❙◇_"[54]55) where "❙◇φ ≡ λw.∃v.(w❙rv)∧(φ v)"
abbreviation c10::"γ⇒γ" ("❙¬_"[52]53) where "❙¬Φ ≡ λx.λw.¬(Φ x w)"
abbreviation c11::"γ⇒γ" ("❙⇁_") where "❙⇁Φ ≡ λx.λw.¬(Φ x w)"
abbreviation c12::"e⇒e⇒σ" ("_❙=_") where "x❙=y ≡ λw.(x=y)"
abbreviation c13::"e⇒e⇒σ" ("_❙≠_") where "x❙≠y ≡ λw.(x≠y)"

text‹Polymorphic possibilist quantification:›
abbreviation q1::"('a⇒σ)⇒σ" ("❙∀") where "❙∀Φ ≡ λw.∀x.(Φ x w)"
abbreviation q2 (binder"❙∀"[10]11) where "❙∀x. φ(x) ≡ ❙∀φ"  
abbreviation q3::"('a⇒σ)⇒σ" ("❙∃") where "❙∃Φ ≡ λw.∃x.(Φ x w)"   
abbreviation q4 (binder"❙∃"[10]11) where "❙∃x. φ(x) ≡ ❙∃φ" 

text‹Actualist quantification for individuals/entities:›
consts existsAt::γ ("_❙@_")  
abbreviation q5::"γ⇒σ" ("❙∀⇧E") where "❙∀⇧EΦ ≡ λw.∀x.(x❙@w)⟶(Φ x w)"
abbreviation q6 (binder"❙∀⇧E"[8]9) where "❙∀⇧Ex. φ(x) ≡ ❙∀⇧Eφ"     
abbreviation q7::"γ⇒σ" ("❙∃⇧E") where "❙∃⇧EΦ ≡ λw.∃x.(x❙@w)∧(Φ x w)"
abbreviation q8 (binder"❙∃⇧E"[8]9) where "❙∃⇧Ex. φ(x) ≡ ❙∃⇧Eφ"

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

text‹Barcan and converse Barcan formula:›
lemma True nitpick[satisfy] oops  ―‹Model found by Nitpick›
lemma "⌊(❙∀⇧Ex.❙□(φ x)) ❙→ ❙□(❙∀⇧Ex.(φ x))⌋" nitpick oops ―‹Ctm›
lemma "⌊❙□(❙∀⇧Ex.(φ x)) ❙→ (❙∀⇧Ex.❙□(φ x))⌋" nitpick oops ―‹Ctm›
lemma "⌊(❙∀x.❙□(φ x)) ❙→ ❙□(❙∀x. φ x)⌋" by simp 
lemma "⌊❙□(❙∀x.(φ x)) ❙→ (❙∀x.❙□(φ x))⌋" by simp
end