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❙
❚