[TYPES] System F and System T names
Neel Krishnaswami
neelakantan.krishnaswami at gmail.com
Fri Apr 6 08:03:17 EDT 2018
Hello,
1. 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.
2. However, since I am semiliterate 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.
Best,
Neel
[1] "This means the axioms of this system (dubbed T) are nearly
the same as those of primitive recursive number theory [...]"
On 06/04/18 12:07, Alejandro Díaz-Caro wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear Type-theorists,
>
> 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.
>
> Kind regards,
> Alejandro
>
More information about the Types-list
mailing list