namespace http://cds.omdoc.org/examples❚

theory TopologicalArgumentationTheory : http://cds.omdoc.org/urtheories?LF =
  include ?PL❙
  
  K : prop ⟶ prop❙
  B : prop ⟶ prop❙
  box: prop  ⟶ prop ❘ # □ 1❙

  world : type❙
  
  argument: type❙
  attacks : argument ⟶ argument ⟶ type ❘# 1 ← 2❙
  
  in : world ⟶ argument ⟶ type ❘# 1 ‍∈ 2❙
  holds : world ⟶ prop ⟶ type ❘ # 1 ⊧ 2❙
  Fix : argument ⟶ type❙
  
  holds_conj : {w,F,G} w ⊧ F ⟶ w ⊧ G ⟶ w ⊧ F ∧ G❙
  holds_disj1 : {w,F,G} w ⊧ F ⟶ w ⊧ F ∨ G❙
  holds_disj2 : {w,F,G} w ⊧ G ⟶ w ⊧ F ∨ G❙
  
  holds_K : {w,F} ({v} v ⊧ F) ⟶ w ⊧ K F❙
  holds_box : {w,F,T} w ‍∈ T ⟶ ({v} v ‍∈ T ⟶ v ⊧ F) ⟶ w ⊧ □ F❙
  holds_B : {w,F,T} w ‍∈ T ⟶ Fix T ⟶ ({v} v ‍∈ T ⟶ v ⊧ F) ⟶ w ⊧ B F❙
❚