[FOM] Re: PA with few symbols

[Vladimir Sazonov]

Timothy Y. Chow wrote:

 > 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.


It depends on concrete formulations and our fantasy. It seems Bill 
Taylor had in mind something that would avoid such kind of
counterarguments:

 > Perhaps in the case of PA the effect of an unlimited number of
 > quantifiers can be cunningly handled
 > by using only a small number of them and
 > "coding up" the rest in much the same way that all PR functions
 > can be coded up using just + and * .

The following comments on using variables are of a general character.

In the line of last postings from Ali Enayat and Randall Holmes,
we can always work in an algebraic (or category theory) manner
without variables at all. Another related example is the combinatory
algebra (no variables) which has the same expressive power as lambda
calculus (based on the play with variables). On the other hand, the
pathos of category theory of working with functions having no
arguments (variables) does not seem to me very exciting (although
in many situations this may be quite useful, interesting and even nice).
Also note that functors still have arguments (variables for objects
and arrows). And we know that, for example, category of cartesian
closed categories is in fact, equivalent to the category of
(intuitionistic(*)) equational typed lambda theories (with variables).
(Analogously - for toposes.) From my point of view, this fact makes
the concept of ccc more intuitively understandable (probably, except
the intuitionistic flavour giving the full generality of ccc) for
the majority of mathematicians -- non-categorists.

Properly speaking, I would say that there should be some good
balance between these two trends.

Another example from database theory is relational algebra vs.
relational calculus (essentially the language of first order
logic with variables). The algebra may be better from the point
of view of (efficient) implementation. However, a human writing
a formal query to DB (or any computer program) would rather prefer
to use (free and quantified) variables like in the query language
SQL.


Footnote (*)
In intuitionistic (typed) lambda theory, given forall xy s(x,y)=t(x,y),
we can infer forall xyz s(x,y)=t(x,y), with z "fictitious", but not
vice versa as in the classical case. A model for such a lambda theory
should be either a ccc, or a Kripke style model with "growing"
universes for each type. Some types, say, for z above, may be even
empty (either currently or permanently, that is, in the current Kripke
world or in all worlds). In this case we really cannot omit fictitious
variable z.


Vladimir Sazonov