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

[Vladimir Sazonov]

Timothy Y. Chow wrote:

whether (for example) there is a sense in
> which syntactic entities really are simpler than arithmetic entities,

In my previous posting to which you have replied
"I find that I disagree with you much less than I originally thought"
I already suggested *in which informal sense* syntactic entities *may
be considered* as really simpler. It looks that you did not notice that.
May be it is because you want to compare PA with a formal metatheory?
Please see below a corresponding version of my views.


> 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.

It is interesting what do you mean by not slavish imitation.
I am really unsure what do you really want. Do you assume that
in this non-slavish imitation the following should hold?

1. there is no longest formula and, moreover,
2. if A and B are formulas then A & B and A V B, etc. are formulas
(the analogue of arithmetical addition);
3. substitution of a term into a formula (A[t/x]) is always
possible, giving a finite formula
(the analogue of arithmetical multiplication);
4. quantification over formulas and other syntactical entities
is always allowed, as well as the ordinary first order logic reasoning;
5. structural induction over any assertion (of any logical complexity)
F(A) on formulas A or F(D) on derivations D is allowed.

Then you will evidently get something equivalent to PA.

On the other hand, taking into account that real formulas and
derivations considered in mathematics are of feasible length,
may be we could consider as "not slavish imitation" a theory
of feasible numbers or, better, of binary strings of a feasible
length as an approach to metamathematics. This will be really
different from metamathematics formalized/encoded via PA or even
Bounded Arithmetic. By this approach syntactical entities are
really simpler - shorter than natural numbers of PA, even shorter
than 2^1000 in unary notation. Things become more problematic
(although probably have some solution) if you want, besides the
syntax in this way, also a model theory. Note, that the theory of
feasible numbers itself (as I presented it very briefly in a
previous posting) has no model in the framework of ZFC. A really
new approach is necessary.

However, I should note that for the theory of feasible numbers
of binary strings (unlike PA) the above consideration does not
give a simpler syntax. This theory, as any mathematical theory,
is abstract, although devoted to describe the idea of feasible
(concrete) objects. Then we should consider syntactical objects
of this theory in an informal, naive way to avoid the vicious
circle, as I discussed in my recent posting.

As I see in FOM, there is another approach consistent in a
sense with the ideas of feasibility suggested by Andrew Boucher
(FOM, 17/05/04). Allen Hazen (FOM, 18/05/04) mentions earlier
works by Quine and (Nelson) Goodman, and Ermanno Bencivenga which,
as I understand, also avoid the existential assumptions (even
concerning the result of successor operation or something like
that?).

What do you really want?

Vladimir