 In Brouwer’s proof of the bar theorem, the applicability of the transformation method to any demonstration of the antecedent is guaranteed by the fact that the condition on such demonstrations that he formulates is a necessary condition. Brouwer obtained this necessary condition by exploiting the fact that on his conception, mathematical objects, so in particular trees and bars, are mental objects; this opens the possibility that reflection on the way these objects and their properties are constructed in mental acts provides information on them that can be put to mathematical use, in particular if this information consists in constraints on these acts of construction. This is how Brouwer arrived at his canonical form. In effect, Brouwer’s argument for the bar theorem is a transcendental argument. On other conceptions of mathematics such considerations need not be acceptable, and indeed no proofs of the (classically valid) bar theorem are known in other varieties of constructive mathematics (where bar induction is either accepted as an axiom, a possibility that Brouwer had also suggested (Brouwer 1927B: 63n.7 [van Heijenoort 1967: 460n.7]), or not accepted, as in the Markov School).