Crossposted to MathOverflow
Page 2 of Dowek's "Gödel's system $T$ as a precursor of modern type theory" gives a presentation of system $T$ as a set of terms with a rewrite relation:
The modern definition of the system $T$, as a set of terms, has been given later by Tait: the fact that Gödel system $T$ can express natural numbers is replaced by the fact that it contains the symbols $0$ and $\operatorname{Succ}$, the fact that it allows explicit definitions is replaced by the fact that it contains typed combinators $S$ and $K$ in the style of Curry and the fact that it allows definitions by induction is replaced by a combinator $R$.
This language contains no predicate symbols, thus there are no formulae and no truth judgments, but reduction rules allowing to compute with terms \begin{align*} Kxy & \rightarrow x \\ Sxyz & \rightarrow xz(yz) \\ Rxf 0 & \rightarrow x \\ Rxf (\operatorname{Succ} y) & \rightarrow f y(Rxf y) \end{align*} The termination of this rewrite system has been proved by Tait in 1967 ...
(The combinators of this system must be typed, since if they were not, we would have the nonterminating term $SII(SII)$, where $I = SKK$.)
I think that this formula-free presentation is interesting, and I am having trouble finding more details on it. I would like to ask for a reference on system $T$ which defines the system as done above, as a set of terms and with no formulas.
Here are a couple places that I've looked.
In Tait's 1967 paper ("Intensional Interpretations of Functionals of Finite Type I"), I see these combinators introduced on page 201 for defining the terms of his theory $T_0$ (I think he refers to these as i.p.r. terms), but on page 207, he seems to define his theory $T_0$ to have formulas, featuring logical connectives and a relation symbol $=$.
In another modern presentation "Gödel's Functional ('Dialectica') Interpretation" by Avigad and Feferman, system $T$ is defined to have formulas and an equality relation on page 9.
