[FOM] PA with few symbols

[Randall Holmes]

No more than three variables are needed for any first-order theory, as
long as an ordered pair is provided -- and there is a definable
ordered pair in PA.  Now it might be that more variables would be
wanted in the course of the derivation of the fact that the definable
ordered pair is an ordered pair -- but certainly not more than
finitely many.

This falls out of Tarski and Givant's reduction of first-order logic
(for theories all of whose models are infinite) to relation algebra
plus existence of (the projection relations of) an ordered pair, which
has the effect of showing that three variables are sufficient.

I wouldn't actually want to work with three variables, though...

Reference:  A formalization of set theory without variables, Alfred Tarski and
Steven Givant, AMS Colloquium Publications vol. 41.  Section 7.6 (along
with the results of sections 3.7-9) contains the proof that Peano arithemetic
can be expressed in a theory using only three variables.  However, one
needs to follow the argument of the whole book to see that it all works.

--Randall Holmes