 Notions such as “construction”, “presenting” and “transformation” can be understood in different ways, and indeed they have been. Similarly, there have been different ideas as to how one may justify that concrete instances of clauses H3 and H4 indeed work for any (possibly hypothetical) proof of the antecedent. Logical principles that are valid on one understanding of these notions may not be valid on another. As Troelstra and van Dalen indicate, it is even possible to understand these clauses in such a way that they validate the principles of classical logic (Troelstra &amp; van Dalen 1988: 9, 32–33; see also Sundholm 2004 and Sato 1997). In the context of the foundational programs of intuitionism and constructivism, all notions are of course understood to be effective; but even then there is room for differences of understanding. Such differences can have mathematical consequences. On some understandings, intuitionistic logic turns out formally to be a subsystem of classical logic (namely, classical logic without the Principle of the Excluded Middle). But that is not the understanding of intuitionistic mathematicians, who, in analysis, have constructed intuitionistically valid instances of the schema \(\neg \forall x(Px \vee \neg Px)\), while classically there can be none (see the section on  Strong counterexamples and the Creating Subject (3.3),  below).