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.