Кіріспе
Хаскелл Кэрри есімімен аталатын математикалық парадокс. Пол Кэрридің оптикалық иллюзиясы және бөлу жұмбағы. Кэрридің парадоксы – өзі туралы «Егер С болса, онда F» дегенді айтатын С деген сөйлемнің бар болуынан кез келген F тұжырымының дәлелденуіне әкелетін парадокс. Парадокс үшін тек бірнеше сырттай зиянсыз көрінетін логикалық дедукция ережелері ғана қажет. F кездейсоқ болғандықтан, осы ережелерге ие кез келген логикада кез келген нәрсені дәлелдеуге болады. Парадокс табиғи тілде де, әртүрлі логика түрлерінде де, соның ішінде жиын теориясының белгілі бір түрлерінде, лямбда-есептеуде және комбинаторлық логикада да көрсетілуі мүмкін. Парадокс 1942 жылы осы парадокс туралы жазған логик Хаскелл Кэрридің есімімен аталған, себебі ол Лёб теоремасымен байланысты.
Paul Curry's optical illusion and dissection puzzle
Curry's paradox is a paradox in which an arbitrary claim F is proved from the mere existence of a sentence C that says of itself "If C, then F". The paradox requires only a few apparently innocuous logical deduction rules. Since F is arbitrary, any logic having these rules allows one to prove everything. The paradox may be expressed in natural language and in various logics, including certain forms of set theory, lambda calculus, and combinatory logic. The paradox is named after the logician Haskell Curry, who wrote about it in 1942. due to its relationship to Löb's theorem.
Наивтік жиынтық теориясы
Тіпті математикалық логика өзіне-өздік анықтамалық сөйлемдерге жол бермесе де, наивтік жиын теориясының кейбір түрлері Керридің парадоксына осал болып қалады. Шешілмеген түсініктілікке рұқсат ететін жиын теорияларында, кез келген логикалық Y-мәлімдемесін жиынды қарастыру арқылы дәлелдеуге болады. Содан кейін мәлімдеме эквивалентті екені оңай көрсетіледі. Осыдан, жоғарыда көрсетілген дәлелдерге ұқсас түрде, шығаруға болады. ("" дегені – "осы мәлімдеме" дегенді білдіреді.) Сондықтан, дұрыс жиын теориясында, жалған Y үшін жиын болмайды. Бұл Расселдің парадоксының бір түрі ретінде қарастырылуы мүмкін, бірақ толықтай сәйкес емес. Жиын теориясының кейбір ұсыныстары Расселдің парадоксын түсініктілік қағидасын шектеу арқылы емес, логика қағидаларын шектеу арқылы, өзіне мүше болмайтын жиындардың барлық жиынының қарама-қайшылығын қабылдау арқылы шешуге тырысты. Жоғарыдағыдай дәлелдердің болуы мұндай міндеттің оңай еместігін көрсетеді, себебі жоғарыда көрсетілген дәлелде қолданылған кем дегенде бір шешілім қағидасын жою немесе шектеу қажет.
One then shows easily that the statement is equivalent to From this, may be deduced, similarly to the proofs shown above. ("" stands for "this sentence".) Therefore, in a consistent set theory, the set does not exist for false Y. This can be seen as a variant on Russell's paradox, but is not identical. Some proposals for set theory have attempted to deal with Russell's paradox not by restricting the rule of comprehension, but by restricting the rules of logic so that it tolerates the contradictory nature of the set of all sets that are not members of themselves. The existence of proofs like the one above shows that such a task is not so simple, because at least one of the deduction rules used in the proof above must be omitted or restricted.
Шектелген минималды логикалы Ламбда-саны
Керридің парадоксы типтелмеген ламбдалық есептеуде, шектелген минималды логикамен толықтырылып, көрсетілуі мүмкін. Ламбдалық есептеудің синтаксистік шектеулерін еңсеру үшін, екі параметрді қабылдайтын импликация функциясын білдірейік, яғни, ламбдалық термин әдеттегі инфикс жазу түрімен тең болады. Кез келген формула ламбдалық функцияны анықтау арқылы дәлелденуі мүмкін, яғни және , мұнда – Керридің тұрақты нүкте комбинаторын білдіреді. Содан кейін , анықтама бойынша және , демек, жоғарыдағы сөйлемдік логикалық дәлелді есептеуде дубликаттауға болады:
An arbitrary formula can be proved by defining a lambda function , and , where denotes Curry's fixed point combinator. Then by definition of and , hence the above sentential logic proof can be duplicated in the calculus:
Жай типтелген ламбдалық есептеуде, тұрақты нүкте комбинаторларын типтеу мүмкін емес, сондықтан олар қабылданбайды.
Талқылау
Керридің парадоксы негізгі логикалық операцияларды қолдайтын және өзіндік рекурсивті функцияны өрнек ретінде құруға мүмкіндік беретін кез келген тілде тұжырымдалады. Парадокс құрастыруға көмектесетін екі механизм – өзіне сілтеме жасау (сөйлем ішінде "осы сөйлемге" сілтеме жасау қабілеті) және наивтік жиын теориясындағы шектеусіз түсінік. Табиғи тілдер, сондай-ақ көптеген басқа тілдер парадокс құру үшін қолданылатын көптеген мүмкіндіктерге ие. Әдетте, тілге метабағдарламалау мүмкіндіктерін қосу қажетті мүмкіндіктерді ұсынады. Математикалық логика, әдетте, өзінің сөйлемдеріне тікелей сілтеме жасауға рұқсат бермейді. Дегенмен, Гёдельдің толық еместік теоремаларының мәні – өзін-өзі көрсетудің басқа түрін қосу мүмкіндігінде жатыр; Гёдель нөмірін қараңыз. Дәлел құрастыруда қолданылатын ережелер – шартты дәлелдеу үшін болжам ережесі, қысқарту ережесі және modus ponens. Бұлар бірінші реттік логика сияқты көптеген таралған логикалық жүйелерге кіреді.
Кейбір формальды логиканың салдары
1930 жылдары Карри парадоксы және оған байланысты Клини-Россер парадоксы, Карри парадоксының дамуына негіз болған, өзін-өзі рекурсивті түрде бейнелейтін әр түрлі формалды логикалық жүйелердің қарама-қайшылыққа тап болатынын көрсетуде маңызды рөл атқарды. Шекарасыз түсініктің аксиомасы қазіргі заманғы жиын теориясымен қолдау таппайды, сондықтан Карри парадоксы болдырмайды.