[FOM] Re: PA with few symbols

[Timothy Y. Chow]

Neil Tennant <neilt at mercutio.cohums.ohio-state.edu> wrote:
>Instead of taking as lexical primitives infinite many distinct variables,
>simply *generate* infinitely many variables from two symbols.

I think Bill Taylor was asking a different question, namely whether it's
possible to formulate a recursive set of axioms (in the first-order
language of arithmetic) that is logically equivalent to PA but that uses
only a finite number of variables.

The answer is surely no, and probably follows from the fact that the 
arithmetical hierarchy is proper, but I don't see an immediate proof.

Tim