 Because of the finiteness of a natural number in contrast to, for example, a real number, many arithmetical statements of a finite nature that are true in classical mathematics are so in intuitionism as well. For example, in intuitionism every natural number has a prime factorization; there exist computably enumerable sets that are not computable; \((A \vee \neg A)\) holds for all quantifier free statements \(A\). For more complex statements, such as van der Waerden’s theorem or Kruskal’s theorem, intuitionistic validity is not so straightforward. In fact, the intuitionistic proofs of both statements are complex and deviate from the classical proofs (Coquand 1995, Veldman 2004).