Does anyone know where do the names System "F" and System "T" comes from? I am not asking who introduced those names (Girard System F, and Gödel System T), but what the "F" and the "T" means.
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
I posted this to TYPES, but its probably worth copying here as well:
In "The system F of variable types, fifteen years later", Girard remarks that there was no particular reason for the name F:
However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging.
There may be another explanation in his thesis, but I haven't read it since unfortunately I am not fluent in French.
However, since I am semi-literate in German, I did take a look at Gödel's paper "Über eine noch nicht benüzte Erweiterung des finiten Standpunktes", where System T (and the Dialectia interpretation for it) was introduced. He names this system in a parenthetical aside:
Das heisst die Axiome dieses Systems (es werde T genannt) sind formal fast dieselben wie die der primitiv rekursiven Zahlentheorie [...][1]
However, the previous page and a half were spent talking about the type structure of system T, so it is reasonable to guess that T stands for "types". But, no explicit reason is given in print.
[1] "This means the axioms of this system (dubbed T) are nearly the same as those of primitive recursive number theory [...]"
answered Apr 6, 2018 at 14:55
-
2$\begingroup$ I just checked in Girard's thesis: He speaks about "système fonctionnel" (functional system), but never mentions "System F". So, what probably happened is that he has shorten the name latter. $\endgroup$ Apr 6, 2018 at 21:01
-
3$\begingroup$ @AlejandroDC Although that hypothesis sounds plausible, FYI that link is not the full thesis, just bits and pieces as transcribed by Kevin Watkins. (I haven't seen a copy of the original.) $\endgroup$ Apr 6, 2018 at 21:44