[FOM] Concerning definition of formulas

[Saurav]

Dear Experts,

When we define formulas, i.e., well formed formulas, we use an apparent
inductive discourse like the atomic formulas are formulas, if p and q
are formulas then p\/q is a formula etc etc. But when we say that
"nothing else is a formula" or "a string is a formula if and only if it
is obtained in this way", what do we actually mean? 
Some books adopt set theoretical outlook, and I give one such:
Let L =  <V,C, R, F> where .....as usual
Define terms
T_0 = V union C
T_{n+1} = T_n union {f_m(t_1,...., t_m): where f_m \in F}

Now have T= union {T_n: n\in \omega}

Define formula:
\Phi_0 = {t=t' : t,t' in T} union {r_m(t_1,...., t_m): r_m\in R}
\Phi_{n+1} = \Phi_n union {~p : p\in T_n} union {p\/q ,p/\q,p => q: p,q
\in T_n} union {(Ex)p : x \in V, p in T_n} union {(x)p : x \in V, p\in
T_n}
....
........

Have \Phi = union {\Phi_n : n \in \omega}.

This is seemingly convincing. But as ZF is itself made of formulas, we
can not adopt this definition.

However, in the apparent, non-set-theoretical definition, we sometime
see the phrase "formulas are the strings that can be obtained by
finitely many applications of the following rules: ..."
What is finite?
Do we not need set theory to decide what is finite and what is not?

If, however, without set theory on tries to prove unique readability of
formulas, I think one would certainly fail because one is not then able
to apply "induction" on the length/complexity.

That the induction is a valid way of reasoing depends on the axiom of
infinity (am I wrong?).

So, by set theoretical tools it is not acceptable to define formulas
because we need to think about set theories as well, and without set
theoretical tools we are in this problem; then what should we do?


Thanks and regards,
Saurav Bhaumik