Module prop::modal

Modal Logic

This modal logic builds upon the hooo module using Exponential Propositions (HOOO EP).

The Modal Logic variant derived is S5 or stronger for decidable propositions. For more information about variants of Modal Logic, see wikipedia article.

It is currently known that HOOO EP implies S5, but it is unknown whether S5 implies HOOO EP.

Functions

• b
  a => □◇a.
• eq_nec_pos_strong_pos
  □◇a == strong_pos(a).
• eq_nnpos_nnecn
  ¬¬◇a == ¬□¬a.
• five
  ◇a => □◇a.
• four
  □a => □□a.
• k
  □(a => b) => (□a => □b).
• lob_triv
  □(□p => p).
• n
  (|- a) => (|- □a).
• nec_consistency
  □¬□⊥.
• nec_not_godel
  □¬(¬□⊥ => ¬□¬□⊥).
• nec_not_lob
  □¬(□(□⊥ => ⊥) => □⊥).
• nec_pos_to_strong_pos
  □◇a => strong_pos(a).
• nec_to_nposn
  □a => ¬◇¬a.
• nec_to_pos
  □a => ◇a.
• nnecn_to_nnpos
  ¬□¬a => ¬¬◇a.
• nnecn_to_pos
  ¬□¬a => ◇a.
• nnpos_to_nnecn
  ¬¬◇a => ¬□¬a.
• npara_to_pos
  ¬(false^a) => ◇a.
• npos_to_para
  ¬◇a => false^a.
• npos_to_posn
  ¬◇a => ◇¬a.
• nposn_to_nec
  ¬◇¬a => □a.
• para_godel
  ⊥^(¬□⊥ => ¬□¬□⊥).
• para_lob
  ⊥^(□(□⊥ => ⊥) => □⊥).
• para_para_to_pos
  false^(false^a) => ◇a.
• para_to_npos
  false^a => ¬◇a.
• pos_to_nnecn
  ◇a => ¬□¬a.
• pos_to_npara
  ◇a => ¬(false^a).
• pos_to_para_para
  ◇a => false^(false^a).
• posn_to_npos
  ◇¬a => ¬◇a.
• strong_pos_to_nec_pos
  strong_pos(a) => □◇a.
• t
  □a => a.
• to_nnpos
  a => ¬¬◇a.

Type Definitions

• NNPos
  ¬¬◇p.
• Nec
  □p := p^true.
• Pos
  ◇p := p^true ⋁ theory(p).
• StrongPos
  strong_pos(a) := p^true ⋁ false^(p^true ⋁ false^p).