# [FOM] Concerning definition of formulas

Vaughan Pratt pratt at cs.stanford.edu
Sat Oct 13 01:26:27 EDT 2007

```Arnon Avron wrote:
> Yes, but instead you take as primitive the notion of "finite"
> [...]
> 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 my previous reply to these two concerns of Arnon I merely agreed that
reinstating "finite" as a condition on my original nonrecursive
definition of "bootstrap wff" seemed like a good idea if it were
necessary to reason with such objects, as Arnon was suggesting.  On
reflection however it occurred to me that there ought to be something
better than just plain "finite" for this purpose.

There is something disturbing about a predicate like "finite" all of
whose counterexamples are mere figments of our imagination.  Poincaré
himself questioned the very existence of infinite sets, distinguishing
between potential and completed infinity.  But when none of the
incautious early believers in completed infinity were struck by
lightning, the rest threw their own caution to the wind and joined them.

And why not?  After all, surely the unit interval is sufficient visible
evidence of infinity, having all of its uncountably many points on display.

But Poincaré could point out that no matter how closely you look at an
interval, only finitely many points are discernible.  At sufficiently
close range you see the very atoms from which it is formed, and only
your imagination can then fill in the interstitial spaces with more points.

Not all second order predicates are like that.  In striking contrast the
distinction between connected and disconnected graphs is eminently
visible.  An object as small as a two-vertex graph suffices to
illustrate the distinction.

In general (second vs. first order aside) graphs are a richer source of
such "visible" predicates than sets.  A graph is a binary relation C,
with Cuv understood (for the purpose of visualization) as asserting that
vertex u is Connected to vertex v, that is, there exists an edge from u
to v.  The following elementary (first-order) properties of graphs have
very small (1-3 vertices) examples and counterexamples:
"reflexive"     (Av[Cvv]),
"discrete"      (Auv[Cuv->u=v]),
"clique"        (Auv[Cuv|Cvu]),  and
"undirected"    (Auv[Cuv->Cvu])  (aka "symmetric").
For any given number of vertices there is a unique discrete reflexive
graph, and a unique undirected clique, which is moreover a
"strong clique" (Auv[Cuv]).

But however comprehensive a library of such predicates we might
assemble, there is no getting around the upward Loewenheim-Skolem
theorem, that every first-order property of graphs holding of
arbitrarily large finite graphs holds of an infinite graph.

This is not the case with "connected" in place of "finite" and
"disconnected" in place of "infinite".  For example the property of
being a clique holds of arbitrarily large connected graphs, but not of
any disconnected graph.  Of course a fairer comparison would seem to
call for the connectedness counterpart of "arbitrarily large," something
like "arbitrarily decreasing connectivity," but how would that be defined?

If "connected" could be substituted directly for "finite", while it
wouldn't get around the basic objection of being a second order
predicate, it would seem a less objectionable predicate for the reasons
listed above: small counterexamples, and not subject to
Loewenheim-Skolem as directly as "finite" (though not completely immune
either--no elementary definition of the usual notion of "path" as a
property of graphs can rule out disconnected paths if it allows
arbitrarily long finite paths---paths are more vulnerable to
disconnection than cliques).

Has anyone defined a purely elementary notion of "pre-wff" such that the
usual inductively defined notion of finite wff, with no normalizing
assumptions at all (no prenex or disjunctive normal form for example),
is exactly a connected pre-wff?  And has (or would) that substitution of
"connected" for "finite" made (or make) the slightest difference
methodologically for anyone?  Or are all second order predicates
considered intrinsically and equally evil, the benefits claimed above
for "connected" over "finite" notwithstanding?

Vaughan
```

More information about the FOM mailing list