Modal operator ($\square$)

A modal operator forms a new formula from a formula, such as $A\mapsto \square 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.