In his answer to David Roberts' mathoverflow question, "$Z_2$ versus second-order $PA$" (question 97077), Prof. Ali Enayat writes (Under the subheading, "Regarding the second question)":

>One way to see this is based on an old result (noticed by a number of people, including Takeuti and Feferman) that $ACA$ is equiconsistent with an extension $PA$($T$) of $PA$ with a distinguished predicate $T$ that codes up the full truth predicate for the ambient model of arithmetic [which I will assume (for want of a better assumption) is the intended model for $PA$--my comment].  Note that $PA$($T$) includes induction in the extended language of arithmetic augmented by the predicate $T$.


If somehow Gentzen was implicitly working in $PA$($T$)(without realizing it, of course), it would explain the viewpoint expressed in the aforementioned note.


The question now remains as to whether in fact he was, which is a question to ask a historian of Gentzen's work (von Plato, perhaps)?