[FOM] Re: PA with few symbols
a.hazen at philosophy.unimelb.edu.au
Mon Jul 26 05:23:46 EDT 2004
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.
(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
(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.
University of Melbourne
More information about the FOM