[FOM] Re: Arithmetic-free theory of formal systems

[A.P. Hazen]

    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 
the theorem.)
     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 
think".)
---
Allen Hazen
Philosophy Department, University of Melbourne
Logical Antiquarian