13 Sep
2023
13 Sep
'23
10:34 p.m.
Godel’s first theorem claims there are statements in every formal system that are neither provable nor unprovable. Boolos made a short proof, but it hinges in agreeing on a different expression of the theorem: “There is no algorithm whose output contains all true sentences of arithmetic and no false ones." I think I’d be willing to accept that those two expressions are sufficiently comparable challenges for now.