Module prop::ava_modal

Avatar Modal Logic

This avatar modal logic builds upon the hooo module using Exponential Propositions.

What makes Avatar Modal Logic different from normal Modal Logic, is that there is a difference between “safe” and “unsafe” proofs:

• false^(false^p) => ◇p is safe (classical in normal Modal Logic)
• ◇p => false^(false^p) is unsafe (constructive in normal Modal Logic)

The idea is to reverse decidability, but this reversed decidability should not be mixed with the normal distinction between classical and constructive proofs. Instead, one uses safe vs unsafe proofs.

1-Avatar and Unsafe code

Without distinction of safe vs unsafe, the usual semantics of “necessary” and “possibly” is collapsed, where is it possible to prove ¬◇p == ◇¬p and ¬□p == □¬p.

According Avatar Semantics, this is not a problem, because one can reconstruct hypercube topologies in Avatar Graphs from the smallest Möbius topologies possible, by identifying the diagonals using highest N-avatars. This is done by introducing a 1-avatar that covers products in Avatar Algebra.

This 1-avatar is a new-type Pos (possibly) that protects the content from being readable. The content is accessed under special circumstances where integration of information is checked by a higher N-avatar. This means, safe invariants using unsafe code.

By constructing the semantics of “necessary” and “possibly” on top of this 1-avatar, one can still prove theorems using HOOO Exponential Propositions safely.

Safe proofs are preferrable, but one can use unsafe code in edge cases by being careful.

Structs

• Pos
  ◇a.

Functions

• eq_nnec_posn
  ¬□a == ◇¬a.
• eq_nnecn_pos
  ¬□¬a <=> ◇a.
• eq_nposn_nec
  ¬◇¬a <=> □a.
• eq_posn_nnec
  ¬◇a == □¬a.
• nec_to_tauto
  □a => a^true.
• nnpara_para_to_nnpos
  ¬¬◇a => ¬¬(false^(false^a)).
• nnpos_to_nnpara_para^⚠
  ¬¬◇a => ¬¬(false^(false^a)).
• not_not_to_pos
  ¬¬a => ◇a.
• npos_to_para
  ¬◇a => false^a.
• para_to_npos^⚠
  false^a => ¬◇a.
• pos_not
  ¬◇a => false^(¬(false^a)).
• pos_to_not_not^⚠
  ◇a => ¬¬a.
• pos_to_para_para^⚠
  ◇a => false^(false^a).
• tauto_to_nec^⚠
  a^true => □a.
• to_pos_tauto_eq
  (false^(false^a) => ◇a)^true) => (false^(false^a) == ◇a)^true).

Type Definitions

• Nec
  □a.