 Brouwer rejected the principle of the excluded middle on the basis of his philosophy, but Arend Heyting was the first to formulate a comprehensive logic of principles acceptable from an intuitionistic point of view. Intuitionistic logic, which is the logic of most other forms of constructivism as well, is often referred to as “classical logic without the principle of the excluded middle”. It is denoted by IQC, which stands for Intuitionistic Quantifier Logic, but other names occur in the literature as well. A possible axiomatization in Hilbert style consists of the principles