A type-theoretical Curry paradox and its solution.

The article focuses on a type-theoretical formulation and resolution of Curry's paradox within the framework of inductively defined types under the Curry–Howard correspondence, which identifies propositions with types. It demonstrates that defining a type |$\Gamma (A)$| in a certain circular manner leads to a paradoxical construction of an object of an arbitrary type A, including empty types, thereby implying inconsistency. The paradox arises from a vicious circularity in the definition of |$\Gamma (A)$|, where the type appears negatively as the domain of a function type in its own definition, violating well-known syntactic criteria for inductive definitions. The proposed solution denies that |$\Gamma (A)$| is a well-defined type, thereby preventing the paradoxical construction and aligning with Curry’s original insight that restrictions on the formation of propositions (types) are necessary. This analysis clarifies the conditions under which inductive definitions yield consistent types and contributes to the understanding of constructive concept formation in type theory.