Briefly, x is a variable, while underline{x} is a numeral — i.e., the string 1cdots1 where 1 occurs x times. I just learned that the standard notation is not underline{x} but dot{x}.
Less briefly: As I say in this comment, when I write
), what I really ought to write is
)), where
) interprets z as the Gödel number of a string of symbols and replaces every occurrence of the first free variable with the string 1+...+1, where 1 occurs x times.
Briefly, x is a variable, while underline{x} is a numeral — i.e., the string 1 cdots 1 where 1 occurs x times. I just learned that the standard notation is not underline{x} but dot{x}.
Less briefly: As I say in this comment, when I write