 Theorem 1.1 Let T be a theory that contains a modicum of arithmetic and let A be a \(\Pi^0_1\)-statement, i.e., one of the form \(\forall x_1\ldots\forall x_n\,P(x_1,\ldots,x_n)\) with quantifiers ranging over naturals and P a primitive recursive predicate, i.e., a predicate with a primitive recursive characteristic function. If F proves the consistency of T and T proves A, then F proves A.