Intuitionistic Model Theory

Intuitionistic logics are extremely common in computer science, since they have direct analogues to notions of computing. In fact, most type theories have interpretations as intuitionistic logics. However, there have been results showing that there can be no complete intuitionistic semantics for intuitionistic logic.

Bob Constable and Mark Bickford have shown that with a slightly different version of completeness, this result can be avoided, and have given a complete semantics of intuitionistic logics in the intuitionistic system NuPRL. I have been working to further the theory of these semantics.