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 <
[email protected]> 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