 Gödel’s translation associates with every formula F(x) of the language of Peano arithmetic a formula F′(x) = ∃y∀zA(y, z, x) of the language of the theory T, where A is quantifier free and the (boldface) bound variables are finite sequences of variables thought to range over functionals of a finite type determined by the type of the variable. Intuitively, y is a concrete analogue of the abstract notion of a construction constituting the meaning of F.