F in System F

What does the F stand for in System F?


Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


Is this a homework problem?

No, this is not a homework

No, this is not a homework problem.

My goal is to prove strong normalization of System F in the Isabelle theorem prover.

However, no description of System F that I have found says what the "F" stands for, and I was just curious.


Well, I also can't provide

Well, I also can't provide an answer off the top of my head. You may need to look up some papers by John Reynolds or Jean-Yves Girard who both independently developed System F (1974 and 1972 respectively). Reynolds, I know, has written several papers about it.

My guess

It is probably because of the [F]orall quantifier. I checked in Proofs and Types and The Blind Spot and I could not find any explanation there.

Not a bad guess...

...as System F has to do with universal quantifiers. Other guesses might be Frege (since he had an earlier notion of system F) or Functor (since it has to do with second order logic).

But my best guess would be none of the above. It probably means no more then lambda does. System F was probably just chosen to differentiate itself from Goedel's System T.

I sent an e-mail to Dr.Reynolds

I sent an e-mail to John Reynolds. Perhaps he'll get back to us with a definitive answer.

Système fonctionnel?

Look at the introduction (pp2-12) of Girard's thesis, Interprètation fonctionnelle et èlimination des coupures de l'arithmètique d'ordre supèrieur [PDF: fragment only], where the term is introduced by explicit contrast to Gödel's System T, which —being Girard— he doesn't refer to System T there directly as such but as "le système de Gödel OF_1", ie. the order-functional-one system of Gödel. I have heard that Girard delights in the carefully obscure, but I think this is where System F is named.

Postscript: For completeness sake, Gödel described his System T in his 1958 Dialectica paper, which was later translated into english under the title On a Hitherto Unexploited Extension of the Finitary Standpoint. I have the idea that the T stands for "type", as in "primitive recursive functionals of finite type", cf. Avigad & Feferman's Gödel’s Functional (“Dialectica”) Interpretation, although, as for F, I am not quite sure.

Thanks! Just what I was

Thanks! Just what I was looking for.