[FOM] Concerning definition of formulas

[Arnon Avron]

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).
  There was a hint in your posting that you might be ready to discard
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