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$ [footnote 1 on pg. 2 of Enayat and Pakhomov's arXiv preprint, "Truth, Disjunction, and Induction (arXiv:1805.09890v1 [math.LO] 24 May 2018) seems to be a restatement of this-- my comment].

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)?

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$ [footnote 1 on pg. 2 of Enayat and Pakhomov's arXiv preprint, "Truth, Disjunction, and Induction" (arXiv:1805.09890v1 [math.LO] 24 May 2018) seems to be a restatement of this-- my comment].

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)?

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)?

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$ [footnote 1 on pg. 2 of Enayat and Pakhomov's arXiv preprint, "Truth, Disjunction, and Induction (arXiv:1805.09890v1 [math.LO] 24 May 2018) seems to be a restatement of this-- my comment].

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)?