Type Definition prop::modal::NNPos

pub type NNPos<A> = Not<Not<Pos<A>>>;

¬¬◇p.

A proposition is existential possibly true if it is not not theoretical possibly true. This is also the same as not necessary not true ¬□¬p or ∃ true { p } (using hooo::Exists).

This corresponds to possibly true in most modal logics. However, in this model, this is weaker due to use of hooo::Theory in the definition.