System F and System T names
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 [...]"