[FOM] Concerning definition of formulas

[Arnon Avron]

On Sun, Oct 07, 2007 at 09:20:16PM -0700, Vaughan Pratt wrote:

> Arnon Avron wrote:
> > One can do what is
> > actually done in many textbooks: define wffs as  finite sequences
> > of certain symbols which satisfy certain simple conditions.
> 
> Those conditions, simple though they may seem, ...

Since I had suspected that you might say something like this,
and I didn't want to enter into a debate which definition
is simpler, I gave another option: reproducing the inductive
definition of wffs by using the concept of "finite set".
My main point was (and is) that using one concept rather than other
does not solve the problem, and that one of them should
be taken as PRIMITIVE.

> >   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.
> 
> In what sense is it not the one I set out to define?  If you start with 
> a definition of vector space that restricts to finite dimension, and 
> later drop finiteness, are the finite-dimensional vector spaces any 
> different now?  

If you are interested only (or mainly) in finite vector spaces,
and prove theorems peculiar to them, than you should somehow
be able to distinguish them from arbitrary vector spaces. To 
give another example: suppose you start with a definition of 
a finite matrix, and later drop finiteness. Than the finite 
matrices are not any different, but the crucial notions of
determinant, characteristic polynomial, etc become meaningless
(for "general matrices"). Similarly, the most important theorems 
of logic: completeness, incompleteness, compacteness etc are valid
only for real wffs, and you have to understand what real wffs
are in order to formulate, prove, and understand them.
    In any case, the main point is that it is an essential feature
of PA, ZFC etc  that they involve only REAL formulas (i.e. finite
formulas) - and it is this concept that we were asked to define.
Moreover: when it comes to FOM it is obligatory to restrict ourselves
to real ("finite") formulas (if you think otherwise than we 
have reached the point that we should agree not to agree).

>  and now everything is ready to begin a resolution proof chaining 
> backwards from the allegedly unsatisfiable negated formula to a 
> contradiction.

I wonder: are you going now to define general (not necessarily
finite) resolution proof chaining and suggest that it is not
necessary to use just finite ones or to define them? And will
you here too try to give a "non-inductive" definition?? After
all, the term "chaining" is only a variant of the "so on" I keep
talking about!

  Arnon Avron