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

[Timothy Y. Chow]

On Tue, 18 May 2004, William Tait wrote:
> I THINK that the reference to Quine's Mathematical Logic (the Chapter on
> Syntax) is relevant to your question---but you must read through (or
> not) a lot of informal discussion.

I took a preliminary look at Quine's book and his "protosyntax" is indeed 
close to what I'm looking for.  So, here is the project as I currently 
envisage it.

Goal: To make more precise the argument that "skepticism about the natural 
numbers leads naturally to skepticism about syntactic rules," and see how 
valid the argument really is.  Also, to make more precise Auerbach's 
argument that the usual arithmetization of the concept of consistency is
intensionally correct.

Method: Set up a first-order language of syntax---Quine's protosyntax or
something like it---that allows syntactic concepts to be captured 
directly, or at least more directly than they are captured by the 
first-order language of arithmetic.  Compare the first-order language
of syntax with the first-order language of arithmetic (relative 
interpretability, strength of various axioms, etc.).

It has seemed to me that some people are more skeptical of natural numbers 
than of syntactic rules for the simple reason that arithmetic has gotten 
"more press"; the incompleteness of arithmetic and nonstandard models of
PA are familiar concepts that we are used to thinking about, whereas the
analogous facts about syntactic rules (e.g., the simple concept of 
"nonstandard proof" that arises when one contemplates, say, models of
PA + ~Con(PA)) are less familiar.  The hope is that by setting up two
languages side-by-side, these biases will be eliminated and we will be
able to see more objectively whether (for example) there is a sense in 
which syntactic entities really are simpler than arithmetic entities,
or whether belief in syntactic entities requires just as much platonism
as belief in arithmetic entities.

The project won't be very interesting if the only way to develop the
syntactic side of the equation is through slavish imitation of the
arithmetic side in thinly disguised form.  Ideally, we should be
driven directly by our intuitions about syntax, so that we can formulate
nontrivial conjectures and prove them.

I don't think I'm the right person to carry out such a project in detail, 
but I think it would interesting to see it done.

Tim