Curry paradoks

Curry paradoks on paradoks, milles mõni meelevaldne väide F tõestatakse, kasutades lauset C, mis ütleb enda kohta "kui C, siis F". Paradoks nõuab vaid paari pealtnäha süütut tuletusreeglit. Loogika, milles need tuletusreeglid sisalduvad, võib seeläbi tõestada mida iganes. Paradoksi võib väljendada loomulikus keeles ja mitmes loogikas, sealhulgas teatud hulgateooria, lambda-arvutuse ja kombinatoorse loogika vormides.

Paradoks on nimetatud Haskell Curry järgi, kes kirjutas sellest 1942. aastal. Seda on kutsutud ka Martin Hugo Löbi järgi Löbi paradoksiks, kuna sellel on seos Löbi teoreemiga.

Loomulikus keeles

Nimetame lauseid kujul "kui A, siis B" konditsionaalideks. Curry paradoks kasutab eneseleosutavat konditsionaali, näiteks:

Kui see lause on tõene, siis Eesti asub Hiina piiril.

Et see lause on loomulikus keeles, on selle tõesust võimalik analüüsida, ning Curry paradoksi on sellest lausest võimalik tuletada. Analüüs koosneb kahest sammust. Esiteks saab läbi loomuliku keele tõestada, et näitelause on tõene [sammud 1–5]. Teiseks saab lauset kasutada selleks, et tõestada, et Eesti asub Hiina piiril [samm 6]:

1. Lause tekst on "Kui see lause on tõene, siis asub Eesti Hiina piiril."
2. Kui see lause on tõene, siis on see tõene. [ilmselge ehk tautoloogia]
3. Kui see lause on tõene, siis: kui see lause on tõene, siis asub Eesti Hiina piiril. [asenda "on see tõene" lause definitsiooniga]
4. Kui see lause on tõene, siis asub Eesti Hiina piiril. [lühenda korratud tingimust]
5. Aga 4. punkt on sama tekst nagu lause ise. Seega on see tõene.
6. Lause on 5. punkti järgi tõene, ning 4. punkti järgi: kui see on tõene, siis asub Eesti Hiina piiril.
   Seega asub Eesti Hiina piiril. [modus ponens]

Kuna Eesti ei asu Hiina piiril, võiks mõista, et ühel neist sammudest on tehtud viga. Väite "Eesti asub Hiina piiril" võib asendada mistahes muu väitega, ning seda lauset saaks siiski selle mõttekäigu abil tõestada. Niisiis paistab, et mistahes lause on tõestatav. Kuna tõestus kasutab vaid üldlevinult korrektseteks peetud deduktsioonimeetodeid, ning kuna ükski neist ei paista ebakorrektne, on see olukord paradoksaalne.

Formaalloogikas

Lauseloogikas

Curry paradoks ilmub ka teatud formaalloogika vormides. Selles kontekstis näitab see, et kui eeldame, et on olemas formaalne lause (X → Y), kus X on omakorda (X → Y), siis saame tõestada väidet Y läbi formaalse tõestuse. Üks näide sellest on järgnev formaalne tõestus:

1. X := (X → Y)	Eeldus. Samaväärne väitega "kui see lause on tõene, siis Y".'
2. X → X	Samasusseadus
3. X → (X → Y)	Asenda 2. parem külg, sest X on 1. järgi sama mis X → Y
4. X → Y	Lühendatud kuju
5. X	Asenda 4. 1. vormiga
6. Y	4. ja 5., modus ponens

Lambda-arvutus minimaalse loogikaga

Curry paradoksi on võimalik väljendada tüüpimata lambda-arvutusega, millele on lisatud implikatiivne lausearvutus. Et toime tulla lambda-arvutuse süntaktiliste piirangutega, tähendab $m$ kahe parameetriga implikatsioonifunktsiooni: $((mA)B)$ tähendab $A\to B$.

Meelevaldset väidet $Z$ on võimalik tõestada defineerides lambdafunktsiooni $N:=\lambda p.((mp)Z)$, ning termi $X:=({\textsf {Y}}N)$, kus ${\textsf {Y}}$ on Curry püsipunktikombinaator. Seega ${\textsf {Y}}$ ja $N$ definitsioonide järgi $X=(NX)=((mX)Z)$, seega saab ülaltoodud lauseloogikat arvutada nõnda:

$\vdash ((mX)X)$	Minimaalse loogika aksioom $A\to A$
$\vdash ((mX)((mX)Z))$	Kuna $X=((mX)Z)$
$\vdash ((mX)Z)$	Minimaalse loogika teoreemi $(A\to (A\to B))\vdash (A\to B)$ põhjal
$\vdash X$	Kuna $X=((mX)Z)$
$\vdash Z$	Modus ponens, $A,(A\to B)\vdash B$, kuna $X$ ja $((mX)Z)$

Lihtsalt tüübitud lambda-arvutuses ei ole võimalik püsipunktikombinaatoritele tüüpe määrata, ning seega ei saa seda paradoksi esitamiseks kasutada.