Moto-o Takahashi “Simple Type Theory of Gentzen Style with the Inference of Extensionality,” in: Proceedings of the Japan Academy, vol.44 , no.2, 1968 Moto-o Takahashi “A Proof of Cut-Elimination Theorem in Simple Type-Theory,” in: Journal…

Hartry Field Saving Truth From Paradox, Oxford University Press, 2008