## F in System F

What does the F stand for in System F?

Thanks,
Chris

## Comment viewing options

### Homework?

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.

Chris

### 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.

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

Chris