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.
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  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 [...]
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.
 "This means the axioms of this system (dubbed T) are nearly the same as those of primitive recursive number theory [...]"