The Unintended Interpretations of Intuitionistic Logic

Abstract

We present an overview of the unintended interpretations of intuitionistic logic that arose after Heyting formalized the "observed regularities" in the use of formal parts of language, in particular, first-order logic and Heyting Arithmetic. We include unintended interpretations of some mild variations on "official" intuitionism, such as intuitionism, such as intuitionistic type theories with full comprehension and higher order logic without choice principles or not satisfying the right choice sequence properties. We conclude with remarks on the quest for a correct interpretation of intuitionistic logic.