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.


1 Answer 1


I posted this to TYPES, but its probably worth copying here as well:

  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 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 [...]"

  • 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
  • $\begingroup$ @AlejandroDC I don't think that is it. In this paper he defines a system Y, and then defines system F to be the subsystem consisting of closed terms. Looks like totally random to me. $\endgroup$
    – Trebor
    Feb 6 at 18:03
  • $\begingroup$ System Y looks like (modern) system F with $\forall$ and $\exists$ types. $\endgroup$
    – Trebor
    Feb 6 at 18:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.