Abstract

The Curry–Howard correspondence, according to which propositions are types, suggests that every paradox formulable in natural deduction has a type-theoretical counterpart. I will give a purely type-theoretical formulation of Curry’s paradox. On the basis of the definition of a type |$\Gamma (A)$|⁠, Curry’s reasoning can be adapted to show the existence of an object of the arbitrary type A. This is paradoxical for several reasons, among others that A might be an empty type. The solution to the paradox consists in seeing that |$\Gamma (A)$| is not a well-defined type.

This article is published and distributed under the terms of the Oxford University Press, Standard Journals Publication Model (https://dbpia.nl.go.kr/journals/pages/open_access/funder_policies/chorus/standard_publication_model)
You do not currently have access to this article.