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)$| ,...
| Published in: | Philosophical Quarterly Vol. 75; no. 2; pp. 763 - 775 |
|---|---|
| Main Author: | |
| Format: | Article |
| Published: |
Oxford University Press / USA
Apr2025
|
| Subjects: | |
| Online Access: | View this record in EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=184192882&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 184192882 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00318094 PHQ jtl: Philosophical Quarterly issn: 00318094 maglogo: N pubinfo: dt: Apr2025 vid: 75 iid: 2 pid: 622 pub: Oxford University Press / USA artinfo: ui: 184192882 10.1093/pq/pqaf019 ppf: 763 ppct: 12 formats: fmt: – @attributes: type: T – @attributes: type: P size: 277KB tig: atl: A type-theoretical Curry paradox and its solution. aug: au: Klev, Ansten affil: Institute of Philosophy, Czech Academy of Sciences, Czechia su: Paradox Proposition (Logic) Natural deduction (Logic) Reasoning Type theory sug: subj: Paradox Proposition (Logic) Natural deduction (Logic) Reasoning Type theory keyword: Curry's paradox functions inductive definitions type theory ab: 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. pubtype: Academic Journal doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y custom: © 2019 Scots Philosophical Association and the University of St. Andrews. item: Philosophical Quarterly holder: Oxford University Press / USA dt: @attributes: year: 2025 holdings: @attributes: islocal: N |
|---|