Введение
Математический парадокс, названный в честь Хаскелла Карри
Оптическая иллюзия и головоломка-диссекция, созданная Полом Карри
Парадокс Карри — это парадокс, в котором произвольное утверждение F доказывается лишь из существования предложения C, утверждающего о себе: "Если C, то 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:
In simply typed lambda calculus, fixed point combinators cannot be typed and hence are not admitted.
Обсуждение
Парадокс Карри может быть сформулирован в любом языке, поддерживающем базовые логические операции и позволяющем построить саморекурсивную функцию как выражение. Два механизма, обеспечивающих построение этого парадокса, – это самоссылка (возможность ссылаться на "это предложение" внутри самого предложения) и неограниченное понимание в наивной теории множеств. Естественные языки почти всегда содержат множество возможностей для построения парадокса, как и многие другие языки. Как правило, добавление возможностей метапрограммирования в язык предоставляет необходимые функции. Математическая логика обычно не допускает явных ссылок на собственные утверждения. Однако суть теорем Гёделя о неполноте заключается в наблюдении, что можно добавить другую форму самоссылки; см. число Гёделя. Правила, используемые при построении доказательства, включают правило допущения для условного доказательства, правило сокращения и modus ponens. Эти правила входят в большинство распространенных логических систем, таких как логика первого порядка.
Последствия для некоторой формальной логики
В 1930-х годах парадокс Карри и тесно связанный с ним парадокс Клини — Россера, из которого и развился парадокс Карри, сыграли ключевую роль в доказательстве противоречивости различных формальных логических систем, допускающих саморекурсивные выражения. Аксиома неограниченного объема не поддерживается современной теорией множеств, что позволяет избежать парадокса Карри.