 This result of Gödel’s (Gödel 1933f), which marks the beginning of provability logic, makes exact the difference between the concept of “provability in a specified formal system” and that of “provability by any correct means.”