Weiß jemand, woher die Namen System "F" und System "T" kommen? Ich frage nicht, wer diese Namen eingeführt hat (Girard System F und Gödel System T), sondern was das "F" und das "T" bedeuten.
Ich habe dies auf TYPES gepostet, aber es lohnt sich wahrscheinlich auch, es hier zu kopieren:
In "Das System F variabler Typen, fünfzehn Jahre später" bemerkt Girard, dass es keinen besonderen Grund für den Namen F gab:
In [3] wurde jedoch gezeigt, dass die offensichtlichen Konvertierungsregeln für dieses System, zufällig F genannt, konvergierten.
Es mag eine andere Erklärung in seiner These geben, aber ich habe sie nicht gelesen, da ich leider nicht fließend Französisch spreche.
Da ich jedoch halbkundig Deutsch kann, habe ich mir Gödels Artikel "Über eine noch nicht benüzte Erweiterung des finiten Rechtees" angesehen, in dem System T (und die Dialektieninterpretation dafür) eingeführt wurde. Er nennt dieses System in Klammern:
Das heisst die Axiome dieses Systeme (es werden T genannt) sind formal schnell wie die der primitiven rekursiven Zahlentheorie [...] [1]
Auf den vorherigen anderthalb Seiten wurde jedoch über die Typstruktur des Systems T gesprochen, sodass anzunehmen ist, dass T für "Typen" steht. Im Druck wird jedoch kein expliziter Grund angegeben.
[1] "Dies bedeutet, dass die Axiome dieses Systems (genannt T) fast dieselben sind wie die der primitiven rekursiven Zahlentheorie [...]"