 There is a question of philosophical importance that should be mentioned here: As it stands, Gödel’s second incompleteness theorem only establishes the unprovability of one sentence, \(\Cons(F)\). But does this sentence really express that \(F\) is consistent? (Compare this with the remark above that \(G_F\) does not, strictly speaking, express its own unprovability.) Furthermore, might there not be other sentences which are provable and also express the consistency of \(F\)?