Premium
A proof of the normal form theorem for the closed terms of Girard's system F by means of computability
Author(s) -
Valentini Silvio
Publication year - 1993
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19930390155
Subject(s) - computability , mathematics , discrete mathematics , calculus (dental) , pure mathematics , medicine , dentistry
In this paper a proof of the normal form theorem for the closed terms of Girard's system F is given by using a computability method à la Tait. It is worth noting that most of the standard consequences of the normal form theorem can be obtained using this version of the theorem as well. From the proof‐theoretical point of view the interest of the proof is that the definition of computable derivation here used does not seem to be well founded. MSC: 03F05, 03B15.