This paper constructs a simple "propositions as types" interpretation for first-order classical propositional and first- and higher-order classical predicate logic. The idea is to study inhabited types and uninhabited types in general, which will be represented by \ (\) and \ (\) respectively, and to show that standard Boolean algebra applies to them using an interpretation of proofs as programs. Functions that inhabit \ (\), \ (\) and \ (\) are the identity function, a type instantiator function and a type modifier function, which as programs can be thought of respectively as a "no op" for the identity, a program to construct a member of a type and a program to construct a member of one type given a member of another. \ (\) is not inhabited by any function, but at the type level only there is a type destructor function which deletes all members of a non-empty type. Double negation elimination, which is equivalent to \ (\) for an inhabited type, can be thought of as an identity function applied to an inhabited type. To show how classical logic can be considered to be constructive, witness functions are produced for specific types representing logical truths, assuming a small number of identities at the type level that can be used to convert one type to another.
Andrew Powell (Tue,) studied this question.