14.2 First Incompleteness
14.2 First Incompleteness Theorem The goal is to construct a sentence that talks about its own provability. This requires combining arithmetization with a method for controlled self-reference. Representing Provability From the previous section, we have an arithmetic relation: $$ \mathrm{Proof}(x,y) $$ which means “$x$ codes a valid proof of the formula with code $y$”. Using this, define the provability predicate: $$ \mathrm{Prov}(y) ;\equiv; \exists x, \mathrm{Proof}(x,y) $$ So: $$ \mathrm{Prov}(\ulcorner...