These theories are typically developed within the domain of arithmetic, which means that in order to talk about sentences, we need to choose a way to encode sentences as numbers. This is now standard practice in computer science (where everything is encoded as binary numbers), but Gödel introduced the idea in this context, so we call the practice Gödel encoding. The current essay uses regular quotes to represent this, for familiarity. Hence, ‘‘s" here represents the Gödel code for sentence s.
Though slightly weaker systems that prove their own consistency exist: self-verifying theories. These might still have a lot of the theorems that we know and love.
Footnotes 3 and 4 do not refer to anything in the text.
Footnotes 3 and 4 do not refer to anything in the text.