[FOM] Concerning definition of formulas

[Vaughan Pratt]

> 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!

Good point, given that I haven't defined general resolution.  Since the 
completeness of resolution as defined for finite wffs seems to depend in 
an essential way on compactness, which is lost with infinitary logic 
(failure of Konig's lemma and all that), this would be a nontrivial 
exercise not at all in the spirit of a simple bootstrap mechanism, the 
intended application of my definition.

So if reasoning is required as part of the bootstrap process (which I 
hadn't been assuming) I guess that means my original requirement that 
all sets be finite was a good one.

In case there is something about the concept of "finite" that actually 
prevents my definition from serving its intended one-shot bootstrap 
function, an "engineering-style" solution is to limit all sets to at 
most a googol elements, or however many are required during 
bootstrapping.  A googol would permit up to eight atoms per formula 
(2^(2^8) is close to 10^{100}).

Vaughan Pratt