A type-theoretical Curry paradox and its solution.
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)$| ,...
| Publicado en: | Philosophical Quarterly Vol. 75; no. 2; pp. 763 - 775 |
|---|---|
| Autor principal: | |
| Formato: | Artículo |
| Publicado: |
Oxford University Press / USA
Apr2025
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| Sumario: | 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. |
|---|