  Axiom \((GL)\) captures the content of Loeb’s Theorem, an important result in the foundations of arithmetic. \(\Box A\rightarrow A\) says that \(\mathbf{PA}\) is sound for \(A\), i.e. that if \(A\) were proven, A would be true. (Such a claim might not be secure for an arbitrarily selected system \(\mathbf{S}\), since A might be provable in \(\mathbf{S}\) and false.) \((GL)\) claims that if \(\mathbf{PA}\) manages to prove the sentence that claims soundness for a given sentence \(A\), then \(A\) is already provable in \(\mathbf{PA}\). Loeb’s Theorem reports a kind of modesty on \(\mathbf{PA}\)’s part (Boolos, 1993, p. 55). \(\mathbf{PA}\) never insists (proves) that a proof of \(A\) entails \(A\)’s truth, unless it already has a proof of \(A\) to back up that claim.