## 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 ^))
``````