[FOM] Concerning definition of formulas

[Arnon Avron]

I doubt whether the replies Bhaumik has got so far could
have convinced him. Denying that a circularity
exists where obviously there is one (and great
thinkers, as Hazen admits, have worried about it)
is of little help for someone who does see the circularity
(and no good explanation except "I do not think it is 
circular" was given, at least not one that I was able to 
understand). Even less convincing is the explanation
suggested in terms of proofs in type theory. After all,
the two central notions here, that of  type and that 
of  proof, are inductively defined, so at best the
question would apply now to the notion of type
and to the notion of  proof in type theory ...

  On the other hand, it makes little sense to pretend that 
we understand basic inductive definitions only in terms
of set theory. Can anyone seriously claim that undersdanding
the notions of ancestor and descendant (which exist
in all languages used by people who have reached a minimal 
degree of civilization) implicitly involves understanding and
acceptance of set theory??

  So the real answer to the question (in the spirit of Poincare)
is that there are basic concepts which  cannot
really be defined, and can only be explained in terms of themselves 
(or some equivalent notions). There is no way to explain the quantifiers
"forall" and "exists" without using at least one of these quantifiers,
and the same applies to other logical notions (I believe that 
anybody who has taught a basic course in logic, and explained
Tarski's semantics,  has faced some student claiming: "but
you use "forall" to define the meaning of "forall"!"). Similarly,
there is no way to explain the notion of "finitely many",
or the equivalent notion of the transitive closure (of a given
relation) without using one of these notions (or something
equivalent). Now, since without understanding these notions
we cannot even understand what wffs are and whar legal
formal proofs in a given system are, understending (and accepting)
these notions is an absolute precondition for being
able to reason (or at least to reason about reasoning, which is 
what logic is about).

 As a consequence, the answer to the following question is very simple:

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

No. We do not. Moreover, you, and everybody else know very well
what is "finite", and if you don't, then nobody will be able
to explain it to you. It is a basic notion (More precisely:
"finitely many" is a basic notion, and "finite" is a derived
one. Natural language is misleading here, as in many other cases).

Arnon Avron