= Solution
The <Gödel-Löb logic> $\mathrm{GL}$ uses propositional variables, $\bot$, implication, and a unary <modal operator> $\Box$. Other Boolean connectives are abbreviations; for example $\neg A$ means $A\to\bot$ and $\top$ means $\bot\to\bot$.
Its axioms are all classical propositional tautologies and the two schemes
$$
\boxed{\begin{aligned}
\mathrm K:&\quad\Box(A\to B)\to(\Box A\to\Box B),\\
\mathrm L:&\quad\Box(\Box A\to A)\to\Box A.
\end{aligned}}
$$
Its rules are the <modus ponens rule> and the <necessitation rule>, $\mathrm{GL}\vdash A\Rightarrow\mathrm{GL}\vdash\Box A$. Uniform <propositional substitution> is allowed, or equivalently built into the axiom schemes. <necessitation rule> applies to theorems; a temporary assumption cannot simply be boxed. In <provability logic>, $\Box A$ is read as the formal assertion that $A$ is provable.
Back to article page
