To see how substitution works, consider the formula (∃x)(x = sy). (It reads, “There exists some variable x that is the successor of y,” or, in short, “y has a successor.”) Like all formulas, it has a Gödel number—some large integer we’ll just call m.
Now let’s introduce m into the formula in place of the symbol y. This forms a new formula, (∃x)(x = sm), meaning, “m has a successor.” What shall we call this formula’s Gödel number? There are three pieces of information to convey: We started with the formula that has Gödel number m. In it, we substituted m for the symbol y. And according to the mapping scheme introduced earlier, the symbol y has the Gödel number 17. So let’s designate the new formula’s Gödel number sub(m, m,