[FOM] Concerning definition of formulas

[Vaughan Pratt]

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