Curry paradoks

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 ${\displaystyle m}$ kahe parameetriga implikatsioonifunktsiooni: ${\displaystyle ((mA)B)}$ tähendab ${\displaystyle A\to B}$.

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

${\displaystyle \vdash ((mX)X)}$	Minimaalse loogika aksioom ${\displaystyle A\to A}$
${\displaystyle \vdash ((mX)((mX)Z))}$	Kuna ${\displaystyle X=((mX)Z)}$
${\displaystyle \vdash ((mX)Z)}$	Minimaalse loogika teoreemi ${\displaystyle (A\to (A\to B))\vdash (A\to B)}$ põhjal
${\displaystyle \vdash X}$	Kuna ${\displaystyle X=((mX)Z)}$
${\displaystyle \vdash Z}$	Modus ponens, ${\displaystyle A,(A\to B)\vdash B}$, kuna ${\displaystyle X}$ ja ${\displaystyle ((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.