PRL Seminars
Expressing and Implementing the Computational Content
Implicit in Smullyan's Account of Boolean Valuations
Abstract
In Smullyan's classic book, First-Order Logic,
the notion of a "Boolean valuation" is central in motivating
his analytical tableau proof system. Smullyan shows that these
valuations are unique if they exist, and then he sketches an
existence proof. In addition he suggests a possible computational
procedure for finding a Boolean valuation, but it is not related to
to the existence proof.
A computer scientist would like to see the obvious explicit
recursive algorithm for evaluating propositional formulas and a
demonstration that the algorithm has the properties of a Boolean
valuation. Ideally, the algorithm would be derived from the
existence proof. It turns out to be unexpectedly difficult to find
a natural existence proof from which the algorithm can be extracted,
and it turns out that the implicit computational content of
Smullyan's argument is not found where one might expect it.
We show that using the notion of a very dependent function type, it
is possible to specify the Boolean valuation and prove its existence
constructively so that the natural recursive algorithm is extracted
and is known to have the mathematically required properties by
virtue of its construction. We illustrate all of these points using
the Nuprl proof development system.
(A revised and polished account of the work presented on
May 5, 2003 at the Prl Seminar.)
|