Crossposted from Math StackExchange

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.

Edit: In response to Andrej Bauer's comment, my motivation is to create a small Turing machine which halts iff $\mathsf{PA}$ is inconsistent. (This is somewhat similar to my last question, which was about weak subsystems of $\mathsf{PA}$.) My hope in writing this question is that there is a $\Pi^0_1$ statement about this rewrite system which holds iff $\mathsf{PA}$ is consistent. An example idea I had for such a statement would be if there were a type $\tau$ corresponding to absurdity, and a set of terms $\Gamma$ corresponding to the axioms of system $T$, such that $\mathsf{PA}$ is consistent iff no term of type $\tau$ is obtainable from a term in $\Gamma$ by application of the rewrite rules. (I see some statements in the literature such as strong normalization which do at least imply consistency of $\mathsf{PA}$, but I don't know of a $\Pi^0_1$ way to state strong normalization.)

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.

Crossposted from Math StackExchange

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.

Edit: In response to Andrej Bauer's comment, my motivation is to create a small Turing machine which halts iff $\mathsf{PA}$ is inconsistent. (This is somewhat similar to my last question, however there I focused on weak subsystems of $\mathsf{PA}$ and tried to avoid explicitly logical statements.) My hope in writing this question is that there is a $\Pi^0_1$ statement about this rewrite system which holds iff $\mathsf{PA}$ is consistent. An example idea I had for such a statement would be if there were a type $\tau$ corresponding to absurdity, and a set of terms $\Gamma$ corresponding to the axioms of system $T$, such that $\mathsf{PA}$ is consistent iff no term of type $\tau$ is obtainable from a term in $\Gamma$ by application of the rewrite rules. (I see some statements in the literature such as strong normalization which do at least imply consistency of $\mathsf{PA}$, but I don't know of a $\Pi^0_1$ way to state strong normalization.)

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.

Crossposted from Math StackExchange

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.

Crossposted from Math StackExchange

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.

Edit: In response to Andrej Bauer's comment, my motivation is to create a small Turing machine which halts iff $\mathsf{PA}$ is inconsistent. (This is somewhat similar to my last question, which was about weak subsystems of $\mathsf{PA}$.) My hope in writing this question is that there is a $\Pi^0_1$ statement about this rewrite system which holds iff $\mathsf{PA}$ is consistent. An example idea I had for such a statement would be if there were a type $\tau$ corresponding to absurdity, and a set of terms $\Gamma$ corresponding to the axioms of system $T$, such that $\mathsf{PA}$ is consistent iff no term of type $\tau$ is obtainable from a term in $\Gamma$ by application of the rewrite rules. (I see some statements in the literature such as strong normalization which do at least imply consistency of $\mathsf{PA}$, but I don't know of a $\Pi^0_1$ way to state strong normalization.)

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.