Alguém sabe de onde vêm os nomes Sistema "F" e Sistema "T"? Não estou perguntando quem apresentou esses nomes (Sistema Girard F e Sistema Gödel T), mas o que significa "F" e "T".
Publiquei isso no TYPES, mas provavelmente vale a pena copiar aqui também:
Em "O sistema F de tipos de variáveis, quinze anos depois", Girard observa que não havia um motivo específico para o nome F:
No entanto, em [3] foi demonstrado que as regras óbvias de conversão para esse sistema, chamadas F por acaso, estavam convergindo.
Pode haver outra explicação em sua tese, mas não a li desde que, infelizmente, não sou fluente em francês.
No entanto, como sou semi-alfabetizado em alemão, dei uma olhada no artigo de Gödel "Über eine noch nicht benüzte Erweiterung des finiten Standpunktes", onde foi introduzido o Sistema T (e a interpretação Dialectia). Ele nomeia esse sistema entre parênteses:
O primeiro sistema Axiome Dieses Systems (é o T genannt) é um serviço rápido e formal de diesel, como é o caso da recuperação primitiva Zahlentheorie [...] [1]
No entanto, a página e meia anterior foram gastas conversando sobre a estrutura de tipos do sistema T, portanto, é razoável supor que T represente "tipos". Mas, nenhuma razão explícita é fornecida na impressão.
[1] "Isso significa que os axiomas deste sistema (apelidado de T) são quase os mesmos da teoria dos números recursivos primitivos [...]"