 A finitary consistency proof is obtained once it is shown in a finitarily acceptable manner that this process of successive “repairs” terminates. If it does, all critical formulas are true formulas without epsilon-terms.