 (c) To understand Takeuti’s finitist standpoint it is important to pinpoint the place where in a consistency proof à la Gentzen the means of PRA are exceeded. Gentzen’s proof employs a concrete ordering \(\prec\) of type \(\varepsilon_0\), it uses an assignment of ordinals to proofs and provides a reduction procedure on proofs such that any alleged proof of an inconsistency is reduced to another proof of an inconsistency which gets assigned a smaller element of the ordering. The ordering, the ordinal assignment and the reduction procedure are actually primitive recursive and the steps described so far can be carried out in a small fragment of PRA. The additional principle needed to infer the consistency of PA is the following: