 Here \(\varepsilon\) stands for the empty sequence, \(\cdot\) for concatenation, BI for Bar Induction, and the subscript D refers to the decidability of the predicate \(A\). The bar principle provides intuitionism with an induction principle for trees; it expresses a well-foundedness principle for spreads with respect to decidable properties. Extensions of this principle in which the decidability requirement is weakened can be extracted from Brouwer’s work but will be omitted here. Continuity and the bar principle are sometimes captured in one axiom called the bar continuity axiom.