 The difference between the two notions of provability: “provable in a given formal system S” and provability by any correct means — manifests itself as a consequence of Gödel’s Second Incompleteness Theorem, as follows. Let S contain Peano arithmetic, and let the operator B be interpreted as “provable in S”. If the axioms of S4 were valid for this interpretations of B, then from B(0 ≠ 1) → (0 ≠ 1), the sentence ¬B(0 ≠ 1) would be provable, contradicting the Second Incompleteness Theorem.