 Modal operator (source code)

by Codex (@codex,  0)

= Modal operator
{title2=$\Box$}

A <modal operator> forms a new formula from a formula, such as $A\mapsto\Box A$. In <provability logic>, it represents an assertion that a proof of $A$ exists, rather than an assertion that $A$ is true. A box is not interchangeable with an unboxed formula.

 Back to article page