-
Views
-
Cite
Cite
Ansten Klev, A type-theoretical Curry paradox and its solution, The Philosophical Quarterly, Volume 75, Issue 2, April 2025, Pages 763–774, https://doi.org/10.1093/pq/pqaf019
- Share Icon Share
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.
© The Author(s) 2025. Published by Oxford University Press on behalf of The Scots Philosophical Association and the University of St Andrews.
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)
Issue Section:
DISCUSSION NOTE
You do not currently have access to this article.