[FOM] Concerning definition of formulas

[Wayne Aitken]

I would like to echo and elaborate on some of the earlier contributions to
this thread.

(1) No formal system can provide a foundations for mathematics by itself.
Why? Because there are several concepts needed even to set up a formal
language. One needs the concept of symbol, the concept of a finite string
of symbol, and some basic logic. Essentially one need much or all of the
metalogic of Hilbert's program. A key component of this is the notion of
finite length string. So some form of the concept of "finitely many" is a
precondition for understanding formal systems.

(2) Note: as others have pointed out, one might also want to consider
finite trees built out of symbols. One then uses a metalanguage rich
enough handle finite trees.

(3) Any concept that is used in the metalogic could be put into a
foundational formal system together with axioms or rules reflecting
informal usage. Of course this is not circularity, it is just
formalization. (We typically go further and add other axioms to our
foundational formal system reflecting concepts needed in mathematics but
not in the (initial) metamathematics. For example, axioms concerning the
existence of an infinite set.)

(4) So a notion of finiteness could have been formally introduced in our
formal mathematical logic together with rules on its usage. The rules for
its usage, or the rules for any logical primitive,  could legitimately
make use of the notion of finiteness present in the metalogic.

(5) This is not done in practice because finiteness can be defined in set
theory.

(6) Also, first order mathematical logic without a formalized notion of
finiteness has several very nice theorems that are useful in model theory.

(7) Once one adopts set theory it becomes part of the metamathematics.
>From now on, set theory can be used to define other formal systems via
inductive definitions. More significantly, one can now define the standard
notion of semantics for these formal systems.

(8) A consequence of not including finiteness in the formal logic is the
existence of non-standard models of arithmetic. A good argument could be
made to include finiteness in the formalized logic (relected in the
semantics) to achieve uniqueness up to isomorphism of natural number
structures.

(9) It is interesting to note that the most direct way of developing basic
arithmetic (PRA) is to do so directly in the basic metalogic using the
tools already available there. You do not loose any rigor in doing so,
since if your metalogic is defective then so will be any formal system
built on top of it.

Wayne Aitken