PRL Seminars

Abstract

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.