<p>I posted this to TYPES, but its probably worth copying here as well:</p>

<ol>
<li><p>In "The system F of variable types, fifteen years later", Girard
remarks  that there was no particular reason for the name F:</p>

<blockquote>
  <p>However, in [3] it was shown that the obvious rules of conversion for
   this system, called F by chance, were converging.</p>
</blockquote>

<p>There may be another explanation in his thesis, but I haven't read it
since unfortunately I am not fluent in French.</p></li>
<li><p>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:</p>

<blockquote>
  <p>Das heisst die Axiome dieses Systems (es werde T genannt) sind formal
  fast dieselben wie die der primitiv rekursiven Zahlentheorie [...][1]</p>
</blockquote>

<p>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. </p>

<p>[1] "This means the axioms of this system (dubbed T) are nearly
the same as those of primitive recursive number theory [...]"</p></li>
</ol>

CC BY-SA 3.0
2018-04-06T21:01:48.900Z
I just checked in [Girard's thesis](http://prl.ccs.neu.edu/img/g-thesis-1972.pdf): 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.
Alejandro DC
CC BY-SA 3.0
2018-04-06T21:44:39.653Z
@AlejandroDC Although that hypothesis sounds plausible, FYI that link is not the full thesis, just [bits and pieces as transcribed by Kevin Watkins](https://www.cs.cmu.edu/~kw/scans.html). (I haven't seen a copy of the original.)
Noam Zeilberger
CC BY-SA 4.0
2024-02-06T18:03:14.457Z
@AlejandroDC I don't think that is it. In [this](https://www.sciencedirect.com/science/article/pii/S0049237X08708437?via=ihub) 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.
Trebor
CC BY-SA 4.0
2024-02-06T18:04:24.403Z
System Y looks like (modern) system F with $\forall$ and $\exists$ types.
Trebor
CC BY-SA 3.0
2018-04-06T14:55:38.423Z
2018-04-06T15:38:12.257Z
2018-04-06T15:38:12.257Z
Neel Krishnaswami
<p>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.</p>

<ho.history-overview><type-systems><formal-systems>
System F and System T names
Alejandro DC
# System F and System T names

(Asked by: username_0 on 2018-04-06)

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.

**Tags:** ho.history-overview, type-systems, formal-systems

---

## 1 answers

### Answer by username_1 on 2018-04-06. Score: 9 | Accepted answer

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

> **Comments:**
> **username_0**: I just checked in [Girard's thesis](http://prl.ccs.neu.edu/img/g-thesis-1972.pdf): 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.  
> **username_2**: @AlejandroDC Although that hypothesis sounds plausible, FYI that link is not the full thesis, just [bits and pieces as transcribed by Kevin Watkins](https://www.cs.cmu.edu/~kw/scans.html). (I haven't seen a copy of the original.)  
> **username_3**: @AlejandroDC I don't think that is it. In [this](https://www.sciencedirect.com/science/article/pii/S0049237X08708437?via=ihub) 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.  
> **username_3**: System Y looks like (modern) system F with $\forall$ and $\exists$ types.  

---

