 The notion \(\GL \vdash A\) denotes provability of a modal formula \(A\) in propositional provability logic. It is not difficult to see that the modal axiom \(\Box A \rightarrow \Box\Box A\) (known as Axiom 4 of modal logic) is indeed provable in GL. To prove this, one uses the substitution \(A \wedge \Box A\) for \(A\) in the axiom (GL). Then, seeing that the antecedent of the resulting implication follows from \(\Box A\), one applies the Distribution Axiom and the Generalization Rule as well as some propositional logic. Unless explicitly stated otherwise, in the sequel “provability logic” stands for the system GL of propositional provability logic.