View LGTC as if it were a standard language L for first-order arithmetic. Suppose we extend it with a theory for talking about the syntax of L (this would not be a Tarskian metalanguage, since it would not include a “sufficiently developed system of mathematical logic”, but all this is just for purposes of illustration). Call the extension L+. Then L+ can be “interpreted” in L using Gödelian techniques, by which Tarski means, roughly, that one can translate L+ into L arithmetizing it in such a way that the translations of theorems of L+ will be theorems of L. Now suppose that φ(n) is the nth expression of L (and that this function is definable in L+), that d(x) is a diagonal function for expressions of L (which is definable in L+; here I have in mind one involving substitution of numerals for free variables), and let n be the numeral of n. Then for every predicate E(x) of expressions of L defined in L+ one can prove in L+ a general sentence of the form ∀n[¬E(d(φ(n)))↔ψ(n)], where ψ(n) is a formula with one free variable entirely constructed in L (through the arithmetization of the L+ predicate “¬E(d(φ(n)))”). Then one can also prove the sentence ¬E(d(φ(k)))↔ψ(k), where k is the Gödel number of ψ(n). d(φ(k)) is the sentence ψ(k), so ψ(k) is a “fixed point” of the predicate ¬E(x): it “says of itself” that it has the property expressed by ¬E(x). The sentence ¬E(d(φ(k)))↔ψ(k) is already equivalent to the sentence ¬[E(d(φ(k)))↔ψ(k)], and part (a) of Theorem I is proved.