[FOM] Concerning definition of formulas
Vaughan Pratt
pratt at cs.stanford.edu
Wed Oct 10 00:58:02 EDT 2007
> 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
More information about the FOM
mailing list