[FOM] Re: Arithmetic-free theory of formal systems
a.hazen at philosophy.unimelb.edu.au
Tue May 18 05:12:31 EDT 2004
Several people had already replied to Timothy Chow's enquiry (is
there a formal treatment that talks about symbols, etc, directly,
without going through arithmeticization). One of them had mentioned
my favorite, Quine's system of "protosyntax," (=first-order syntax
language) presented in the final chapter of his "Mathematical Logic."
Quine's chapter is very nice, presenting a version of the first
incompleteness theorem that is eawsy to follow: no switching back and
forth between languages involved, since the system whose
incompleteness is proved is "ABOUT" itself. (Quine proves that the
set of truths in the system is not merely not r.e., but --
essentially -- that it is not even arithmètic. I'm not sure, but
this may have been the first publication of this strengthening of
From the point of view of someone with real sceptical doubts
about the existence an ininite series of numbers, however....
Quine's theore and arithmetic are interpretable in each other.
(Gödel showed that you could interpret essentially what Quine later
took as his protosyntax in arithmetic. Quine, in "Concatenation as a
basis for arithmetic" -- JSL 1946; repr. in Quine's "Selected Logic
Papers" -- showed the converse. Corcoran, Frank & Maloney, "String
Theory," JSL 1975, showed that second-order arithmetic and a
second-order version of Quine's system are "theoretically
synonymous": except for the interpretation, the same theory.) So
anyone wit doubts about numbers ought to have similar ...reservations
... about syntax.
Two things come to mind as possibly relevant, though neither goes very far.
--Ermanno Bencivenga, in the 1976 (I think) volume of the "Journal
of Philosophical Logic," studied a formalization of arithmetic within
"free logic" (so not making the assumption that addition,
multiplication, or even successor, are everywhere defined). If one
were to construct a theory of symbols and formulas that didn't
assume at the outset the existence of formulas of arbitrary length,
the concatenation function would be treated similarly.
--Quine and (Nelson) Goodman, "Steps toward a constructive
nominalism," JSL 1947, explored the first steps of a theory of
formulas, etc, that avoids the existential assumption mentioned.
They didn't get very far, but I think some of the definitions they
give ***may*** repay re-examination: they might be usable in theories
of "feasible" mathematics. (But that's not even a conjecture: just a
suspicion of "maybe there's more in this old paper than most people
Philosophy Department, University of Melbourne
More information about the FOM