 What kind of stronger system can we have in which ∀xφ(x) is provable? We may consider second order logic in which we can define a predicate N(x) for the set of natural numbers and furthermore can prove of a new predicate symbol Tr(x) that it satisfies the inductive clauses of the truth definition of first order formulas of arithmetic, relativized to N. Then the stronger system can prove that provable first order sentences of arithmetic satisfy the predicate Tr . By the above argument, we can prove in the stronger system that ∀xφ(x) satisfies Tr. Then by adding a few lines we can prove each φ(n) satisfies Tr. Because of the nature of φ(n), this implies the stronger system has a (short) proof of φ(n). An alternative system is Peano’s axioms PA in an extended language where we have a new predicate symbol Tr and axioms stating that the predicate Tr codes the satisfaction relation for all sentences of the vocabulary not containing Tr.