Quelle  PAL.thy

section ‹Public Announcement Logic (PAL) in HOL›

text ‹An earlier encoding and automation of the wise men puzzle, utilizing a shallow embedding of
 -order (multi-)modal logic in HOL, has been presented in cite‹"J41" and "J44"›. However, this work did not
  address the interaction dynamics between the involved agents. Here we therefore extend and adapt
  universal (meta-)logical reasoning approach of cite‹"J41"› for public announcement logic (PAL) and
  demonstrate how it can be utilized to achieve a convincing encoding and automation of the
  men puzzle in HOL, so that also the interaction dynamics as given in the scenario is adequately
 . For further background information on the work presented here we refer to cite‹"R78" and "C90"›.›

theory PAL imports Main begin  (* Sebastian Reiche and Christoph Benzmüller, 2021 *)
nitpick_params[user_axioms,expect=genuine]

text ‹Type i is associated with possible worlds›
 typedecl i (* Type of possible worlds *)
 type_synonym σ = "i==>bool" (*Type of world domains *)
 type_synonym τ = "σ==>i==>bool" (* Type of world depended formulas (truth sets) *) 
 type_synonym α = "i==>i==>bool" (* Type of accessibility relations between world *)
 type_synonym ρ = "α==>bool" (* Type of groups of agents *)

text ‹Some useful relations (for constraining accessibility relations)›
definition reflexive::"α==>bool" 
  where "reflexive R ≡ ∀x. R x x"
definition symmetric::"α==>bool" 
  where "symmetric R ≡ ∀x y. R x y ⟶ R y x"
definition transitive::"α==>bool" 
  where "transitive R ≡ ∀x y z. R x y ∧ R y z ⟶ R x z"
definition euclidean::"α==>bool" 
  where "euclidean R ≡ ∀x y z. R x y ∧ R x z ⟶ R y z"
definition intersection_rel::"α==>α==>α" 
  where "intersection_rel R Q ≡ λu v. R u v ∧ Q u v"
definition union_rel::"α==>α==>α" 
  where "union_rel R Q ≡ λu v. R u v ∨ Q u v"
definition sub_rel::"α==>α==>bool" 
  where "sub_rel R Q ≡ ∀u v. R u v ⟶ Q u v"
definition inverse_rel::"α==>α" 
  where "inverse_rel R ≡ λu v. R v u"
definition big_union_rel::"ρ==>α" 
  where "big_union_rel X ≡ λu v. ∃R. (X R) ∧ (R u v)"
definition big_intersection_rel::"ρ==>α"
  where "big_intersection_rel X ≡ λu v. ∀R. (X R) ⟶ (R u v)"

text ‹In HOL the transitive closure of a relation can be defined in a single line.›
definition tc::"α==>α" 
  where "tc R ≡ λx y.∀Q. transitive Q ⟶ (sub_rel R Q ⟶ Q x y)"

text ‹Logical connectives for PAL›
abbreviation patom::"σ==>τ" (‹^A_›[79]80) 
  where "^Ap ≡ λW w. W w ∧ p w"
abbreviation ptop::"τ" (‹\⊤›) 
  where "\<top> ≡ λW w. True" 
abbreviation pneg::"τ==>τ" (‹\¬_›[52]53) 
  where "\<not>φ ≡ λW w. ¬(φ W w)" 
abbreviation pand::"τ==>τ==>τ" (infixr‹\∧›51) 
  where "φ\<and>ψ ≡ λW w. (φ W w) ∧ (ψ W w)"   
abbreviation por::"τ==>τ==>τ" (infixr‹\∨›50) 
  where "φ\<or>ψ ≡ λW w. (φ W w) ∨ (ψ W w)"   
abbreviation pimp::"τ==>τ==>τ" (infixr‹\→›49) 
  where "φ\<rightarrow>ψ ≡ λW w. (φ W w) ⟶ (ψ W w)"  
abbreviation pequ::"τ==>τ==>τ" (infixr‹\↔›48) 
  where "φ\<leftrightarrow>ψ ≡ λW w. (φ W w) ⟷ (ψ W w)"
abbreviation pknow::"α==>τ==>τ" (‹K_ _›) 
  where "K r φ ≡ λW w.∀v. (W v ∧ r w v) ⟶ (φ W v)"
abbreviation ppal::"τ==>τ==>τ" (‹[!_]_›) 
  where "[!φ]ψ ≡ λW w. (φ W w) ⟶ (ψ (λz. W z ∧ φ W z) w)"

text ‹Glogal validity of PAL formulas›
abbreviation pvalid::"τ ==> bool" (‹\⌊_\⌋›[7]8) 
  where "\<lfloor>φ\<rfloor> ≡ ∀W.∀w. W w ⟶ φ W w"

text ‹Introducing agent knowledge (K), mutual knowledge (E), distributed knowledge (D) and common knowledge (C).›
abbreviation EVR::"ρ==>α"
  where "EVR G ≡ big_union_rel G"
abbreviation DIS::"ρ==>α" 
  where "DIS G ≡ big_intersection_rel G"
abbreviation agttknows::"α==>τ==>τ" (‹K_{_} _›) 
  where "K_r φ ≡ K r φ" 
abbreviation evrknows::"ρ==>τ==>τ" (‹E_{_} _›) 
  where "E_G φ ≡ K (EVR G) φ"
abbreviation disknows :: "ρ==>τ==>τ" (‹D_{_} _›) 
  where "D_G φ ≡ K (DIS G) φ"
abbreviation prck::"ρ==>τ==>τ==>τ" (‹C_{_}\(_|_\)›)
  where "C_G\<lparr>φ|ψ\<rparr> ≡ λW w. ∀v. (tc (intersection_rel (EVR G) (λu v. W v ∧ φ W v)) w v) ⟶ (ψ W v)"
abbreviation pcmn::"ρ==>τ==>τ" (‹C_{_} _›) 
  where "C_G φ ≡ C_G\<lparr>\<top>|φ\<rparr>"

text ‹Postulating S5 principles for the agent's accessibility relations.›
abbreviation S5Agent::"α==>bool"
  where  "S5Agent i ≡ reflexive i ∧ transitive i ∧ euclidean i"
abbreviation S5Agents::"ρ==>bool"
  where "S5Agents A ≡ ∀i. (A i ⟶ S5Agent i)"

text ‹Introducing "Defs" as the set of the above definitions; useful for convenient unfolding.›
named_theorems Defs
declare reflexive_def[Defs] symmetric_def[Defs] transitive_def[Defs] 
  euclidean_def[Defs] intersection_rel_def[Defs] union_rel_def[Defs] 
  sub_rel_def[Defs] inverse_rel_def[Defs] big_union_rel_def[Defs] 
  big_intersection_rel_def[Defs] tc_def[Defs]

text ‹Consistency: nitpick reports a model.›
 lemma True nitpick [satisfy] oops (* model found *)


section ‹Automating the Wise Men Puzzle›

text ‹Agents are modeled as accessibility relations.›
consts a::"α" b::"α" c::"α" 
abbreviation  Agent::"α==>bool" (‹A›) where "A x ≡ x = a ∨ x = b ∨ x = c"
axiomatization where  group_S5: "S5Agents A"

text ‹Common knowledge: At least one of a, b and c has a white spot.›
consts ws::"α==>σ" 
axiomatization where WM1: "\<lfloor>C_\<A> (^Aws a \<or> ^Aws b \<or> ^Aws c)\<rfloor>" 

text ‹Common knowledge: If x does not have a white spot then y knows this.›
axiomatization where
  WM2ab: "\<lfloor>C_\<A> (\<not>(^Aws a) \<rightarrow> (K_b (\<not>(^Aws a))))\<rfloor>" and
  WM2ac: "\<lfloor>C_\<A> (\<not>(^Aws a) \<rightarrow> (K_c (\<not>(^Aws a))))\<rfloor>" and
  WM2ba: "\<lfloor>C_\<A> (\<not>(^Aws b) \<rightarrow> (K_a (\<not>(^Aws b))))\<rfloor>" and
  WM2bc: "\<lfloor>C_\<A> (\<not>(^Aws b) \<rightarrow> (K_c (\<not>(^Aws b))))\<rfloor>" and
  WM2ca: "\<lfloor>C_\<A> (\<not>(^Aws c) \<rightarrow> (K_a (\<not>(^Aws c))))\<rfloor>" and
  WM2cb: "\<lfloor>C_\<A> (\<not>(^Aws c) \<rightarrow> (K_b (\<not>(^Aws c))))\<rfloor>" 

text ‹Positive introspection principles are implied.›
lemma WM2ab': "\<lfloor>C_\<A> ((^Aws a) \<rightarrow> K_b (^Aws a))\<rfloor>" 
  using WM2ab group_S5 unfolding Defs by metis
lemma WM2ac': "\<lfloor>C_\<A> ((^Aws a) \<rightarrow> K_c (^Aws a))\<rfloor>" 
  using WM2ac group_S5 unfolding Defs by metis
lemma WM2ba': "\<lfloor>C_\<A> ((^Aws b) \<rightarrow> K_a (^Aws b))\<rfloor>" 
  using WM2ba group_S5 unfolding Defs by metis
lemma WM2bc': "\<lfloor>C_\<A> ((^Aws b) \<rightarrow> K_c (^Aws b))\<rfloor>" 
  using WM2bc group_S5 unfolding Defs by metis
lemma WM2ca': "\<lfloor>C_\<A> ((^Aws c) \<rightarrow> K_a (^Aws c))\<rfloor>" 
  using WM2ca group_S5 unfolding Defs by metis
lemma WM2cb': "\<lfloor>C_\<A> ((^Aws c) \<rightarrow> K_b (^Aws c))\<rfloor>" 
  using WM2cb group_S5 unfolding Defs by metis

text ‹Automated solutions of the Wise Men Puzzle.›
theorem whitespot_c: "\<lfloor>[!\<not>K_a(^Aws a)]([!\<not>K_b(^Aws b)](K_c (^Aws c)))\<rfloor>" 
  using WM1 WM2ba WM2ca WM2cb unfolding Defs by (smt (verit))

text ‹For the following, alternative formulation a proof is found by sledgehammer, while the
  of this proof using trusted methods (often) fails; this hints at further opportunities to
  the reasoning tools in Isabelle/HOL.›
theorem whitespot_c':
  "\<lfloor>[!\<not>((K_a (^Aws a)) \<or> (K_a (\<not>^Aws a)))]([!\<not>((K_b (^Aws b)) \<or> (K_b (\<not>^Aws b)))](K_c (^Aws c)))\<rfloor>"
  using WM1 WM2ab WM2ac WM2ba WM2bc WM2ca WM2cb unfolding Defs 
   ― ‹sledgehammer by (smt (verit))›
  oops
   
text ‹Consistency: nitpick reports a model.›
lemma True nitpick [satisfy] oops  
end