 Of course, this result concerns provability relative to a system. One system can prove another system’s Gödel sentence. Kurt Gödel (1983, 271) thought that proof was not needed for knowledge that arithmetic is consistent.