Modal formula
= Modal formula
A <modal formula> is built from <propositional variables> and logical constants using Boolean connectives and <modal operators>, such as the box operator. In <provability logic>, arithmetic realization replaces propositional letters by arithmetic sentences and interprets a box as the corresponding arithmetic provability assertion. Modal validity, theoremhood and truth under a particular arithmetic realization are distinct notions.