A type-theoretical Curry paradox and its solution

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985955%3A_____%2F25%3A00641619" target="_blank" >RIV/67985955:_____/25:00641619 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1093/pq/pqaf019" target="_blank" >https://doi.org/10.1093/pq/pqaf019</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1093/pq/pqaf019" target="_blank" >10.1093/pq/pqaf019</a>

Result language
angličtina
Original language name
A type-theoretical Curry paradox and its solution
Original language description
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 G(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 G(A) is not a well-defined type.
Czech name
—
Czech description
—

Type
J<sub>SC</sub> - Article in a specialist periodical, which is included in the SCOPUS database
CEP classification
—
OECD FORD branch
60301 - Philosophy, History and Philosophy of science and technology

Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)