Re: [TYPES] System F and System T names
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Dear Neel, Thank you for the info. That is exactly what I was looking for. Kind regards, Alejandro On Fri, 6 Apr 2018 at 14:03 Neel Krishnaswami < neelakantan.krishnasw...@gmail.com> wrote: > Hello, > > 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 semiliterate 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. > > Best, > Neel > > > [1] "This means the axioms of this system (dubbed T) are nearly > the same as those of primitive recursive number theory [...]" > > On 06/04/18 12:07, Alejandro Díaz-Caro wrote: > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > Dear Type-theorists, > > > > 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. > > > > Kind regards, > > Alejandro > > > -- http://diaz-caro.web.unq.edu.ar
Re: [TYPES] System F and System T names
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Hello, 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 semiliterate 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. Best, Neel [1] "This means the axioms of this system (dubbed T) are nearly the same as those of primitive recursive number theory [...]" On 06/04/18 12:07, Alejandro Díaz-Caro wrote: [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Dear Type-theorists, 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. Kind regards, Alejandro
[TYPES] System F and System T names
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Dear Type-theorists, 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. Kind regards, Alejandro -- http://diaz-caro.web.unq.edu.ar
