nnProver

Formula

neg ea false or equivalently neg (ea a and aa neg a): No set of neighbourhoods contains the empty set.
aa a -> ea a: The sets of neighbourhoods are non-empty.
neg (aa a and aa neg a): Every set of neighbourhoods contains a non-empty neighbourhood. (Implies aa a -> ea a.)

Examples

Syntax
phi ::= a,b,c,... | false | true | neg phi | phi and phi | phi or phi | phi -> phi | ea phi | aa phi

Common axioms and interesting examples
 Monotonicity for ea: ea (a and b) -> ea a and ea b Necessitation for ea: ea true Aggregation for ea: ea a and ea b -> ea (a and b) Interaction between the operators: aa (a -> b) and ea a -> ea b Axiom D for ea: neg (ea a and ea neg a) Axiom D for ea and aa: neg (ea a and aa neg a) Axiom T for ea: ea a -> a Large model: ea (ea c and d -> aa a or ea b or f) and ea(ea m -> k or ea l or ea n) and aa( ea x and aa y -> ea( ea z and ea w)) -> aa (g or aa h) or ea ea ea ea i or ea(aa o -> ea p)
K
?(5, p + q) , ?(4, r + t), !(1, p ^ * t ^)
?(1, q)  && ?(1, p)  && !(1, p ^ * q ^)
?(1, p * q ^) && ?(1, p ^) && !(1, q)

K + 4
?(1, p), !(1, !(1, p ^))
?(3, p + q), !(2, !(1, p ^ ))
?(5, p) , ?(4, q), !(2, !(1, p ^ * q ^))
?(3, p ^) , !(2, !(1, p))

K + D
?(1,p) , ?(1, p ^)
?(2,?(1, p)) , ?(2, !(1, p ^))
?(1, ?(1, p)) && ?(1, ?(1, p ^))

K + T
?(1,p), p ^

K + D + 4
?(2, p) && ?(2, ?(1, p ^))
?(3, ?(2, p)) && ?(2, ?(1, p ^))