Variations on a Proof by Smullyan

by Matthew Fluet
2002-2003

Two weeks ago, I gave a rather hurried explaination of formalizing a seemingly straightforward proof of the existence and uniqueness of Boolean valuations as given in Raymond M. Smullyan's First-Order Logic. This week we'll explore the proof and variations thereof in more detail. Various issues will arise: interpreting an informal argument for formalization, specifications and extractions vs. explicit witnesses, etc. We hope to conclude with an elegant solution using very dependent function types.

Variations on a Proof by Smullyan

by Matthew Fluet 2002-2003

by Matthew Fluet
2002-2003