Skip to main content
1 of 3
Thomas Benjamin
  • 6.1k
  • 1
  • 25
  • 39

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

Thomas Benjamin
  • 6.1k
  • 1
  • 25
  • 39