[FOM] Re: PA with few symbols

[A.P. Hazen]

Neil Tennant  has suggested (as an answer to a question that may not 
have been the one intended) that we can get the number of symbols of 
a formalized language down to a finite stock by thinking of variables 
as complex expressions consisting of a "head" or "base" followed by a 
"distinguisher": a string of primes (or, for that matter, a string of 
digits forming a numerical subscript).

Herb Enderton has added philosophical reasons for thinking that this 
is what variables "really" are in formal systems people actually use.

Four observations:
(i) Even when the text just blandly speaks of an "infinite set" of 
variables, textbooks USE numerical subscripts.
(ii) When you are doing formal metatheory, you CAN ignore the 
internal structure of variables (by reserving some infinite set of 
numbers to be the Gödel numbers of variables), but it's about as 
easy, and probably a bit more perspicuous for the beginning student, 
to treat them as complex: Quine's treatment (using his "Protosyntax" 
to give a direct description of syntactic entities without 
Gödel-numbering) in the "Syntax" chapter of his "Mathematical Logic" 
book is-- as one would expect from him-- a model of clarity in this 
regard.
(iii) People  working on length-of-proofs theory and/or automated 
theorem proving HAVE to remember that variables are complex (and so 
don't all contribute equally to length).
(iv) If you like MULTI-SORTED systems, it's easier to think of 
variables as consisting of a base that gives the sort and a 
distinguisher that distinguishes variables of the same sort, and it's 
just as easy to think of the distinguishers as being the same for 
every sort.  If you want to go beyond simple multi-sortedness and 
think about systems that allow the definition of NEW sorts of 
variables (e.g. Hailperin's (JSL 1956,1958) "Theory of Restricted 
Quantification," or type theories with dependent types) it seems very 
hard NOT to think this way.
---

Allen Hazen
Philosophy Department
University of Melbourne