Mario Piazza

A finite algebraic target theorem for Kreisel’s conjecture

Friedman’s Problem 34, attributed there to Kreisel, states that for Peano arithmetic formalized precisely as in Kleene, a uniform bound on the proof lengths of all numeral instances $$A(\bar{n})$$ A ( n ¯ ) entails the provability of the universal closure $$\forall x\,A(x)$$...