techrpt.pdf
(with Stuart Allen and Bob Constable; Cornell University Technical Report;
TR2004-1933)
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 di±cult 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.