# [FOM] Concerning definition of formulas

Arnon Avron aa at tau.ac.il
Sun Oct 7 07:38:50 EDT 2007

```On Fri, Oct 05, 2007 at 05:57:19PM -0700, Vaughan Pratt wrote:

> No recursion or induction, either explicit, or implicit in the
> use of numbers, is involved in the definition.

Yes, but instead you take as primitive the notion of "finite"
(note that the possibility of doing so was noted already in Saurav's
original posting, in which the question "what is finite?" has
been raised too). However, once this is allowed there is no need
for your complicated definition of a wff. One can do what is
actually done in many textbooks: define wffs as  finite sequences
of certain symbols which satisfy certain simple conditions.
Alternatively, one can reproduce the inductive definition
by saying that a string A of symbols is a wff if there is a finite
sequence (of strings) ending with A such that ...
(if one wishes, the talks about finite sequences can easily
be replaced here by talks about finite sets). Indeed,
it is well known that taking "finite" as primitive and taking "and
so on" as primitive (formally: using the transitive closure operation
as primitive) are equivalent approaches (personally, I believe that our
intuition derives the first from the second, but this
is not important for the present discussion).
the finiteness condition. However, if you do so then what you will
be defining might be an interesting concept, but not the one
you were set out to define.

> are those in prenex normal form with a full DNF matrix, sufficient for
> all definitional purposes in bootstrapping up from naive set theory.

My reservation here is less important than the previous one,
but I would like to note that things are not that simple.
One of the main thing one does with
formulas is to reason with them, but the formulation of even a
basic rule like Modus Ponens is rather difficult if one
uses only wffs in prenex normal form. In fact, it seems to me
that for doing this in an acceptable way one has to identify
wffs which are not identical according to your definition of "wff".

Arnon Avron
```