Парадокс Карри

Парадокс Карри — это парадокс , в котором произвольное утверждение F доказывается простым существованием предложения C , которое говорит о себе: «Если C , то F ». Парадокс требует лишь нескольких, казалось бы, безобидных правил логической дедукции. Поскольку F произвольна, любая логика, имеющая эти правила, позволяет доказать все. Парадокс может быть выражен на естественном языке и в различных логиках , включая определенные формы теории множеств , лямбда-исчисление и комбинаторную логику .

Парадокс назван в честь логика Хаскелла Карри , написавшего о нем в 1942 году. ^{[ 1 ]} Его также называют парадоксом Лёба в честь Мартина Гюго Лёба . ^{[ 2 ]} из-за его связи с теоремой Лёба .

На естественном языке

Утверждения вида «если А , то В » называются условными . Парадокс Карри использует особый вид самореферентного условного предложения, как показано в этом примере:

Если это предложение верно, то Германия граничит с Китаем.

Несмотря на то, что Германия не граничит с Китаем , приведенный пример предложения, безусловно, является предложением на естественном языке, и поэтому истинность этого предложения можно проанализировать. Из этого анализа следует парадокс. Анализ состоит из двух этапов. Во-первых, для доказательства истинности приведенного в качестве примера предложения можно использовать обычные методы доказательства на естественном языке [шаги 1–4 ниже] . Во-вторых, истинность этого предложения можно использовать для доказательства того, что Германия граничит с Китаем [шаги 5–6] :

Предложение гласит: «Если это предложение верно, то Германия граничит с Китаем» [повторите определение, чтобы нумерация шагов соответствовала формальному доказательству ]
Если предложение истинно, то оно истинно. [очевидно, т.е. тавтология ]
Если предложение верно, то: если предложение истинно, то Германия граничит с Китаем. [замените «это правда» определением предложения]
Если предложение верно, то Германия граничит с Китаем. [условие повторения контракта]
Но 4. — вот что сказано в предложении, так что это действительно правда.
Предложение истинно [по 5.] и [по 4] : если оно истинно, то Германия граничит с Китаем.
Итак, Германия граничит с Китаем. [ устанавливаю настроение ]

Поскольку Германия не граничит с Китаем, это говорит о том, что на одном из этапов доказательства была допущена ошибка. Утверждение «Германия граничит с Китаем» можно было бы заменить любым другим утверждением, и это предложение все равно было бы доказуемым. Таким образом, каждое предложение кажется доказуемым. Поскольку в доказательстве используются только общепринятые методы дедукции и ни один из этих методов не кажется неверным, эта ситуация парадоксальна. ^{[ 3 ]}

Неофициальное доказательство

Стандартный метод доказательства условных предложений (предложений вида «если А , то В ») называется « условным доказательством ». В этом методе, чтобы доказать «если А , то В », сначала А предполагается Б , а затем на основе этого предположения доказывается, что истинно.

Чтобы создать парадокс Карри, описанный в двух шагах выше, примените этот метод к предложению «если это предложение истинно, то Германия граничит с Китаем». Здесь A , «это предложение верно», относится к общему предложению, а B — «Германия граничит с Китаем». Итак, предположение A — это то же самое, что предположение «Если A , то B ». Следовательно, предполагая A , мы предполагали и A , и «Если A , то B ». Следовательно, B истинно по modus ponens , и мы доказали: «Если это предложение истинно, то утверждение «Германия граничит с Китаем» истинно». обычным способом, предположив гипотезу и сделав вывод.

Теперь, поскольку мы доказали: «Если это предложение истинно, то утверждение «Германия граничит с Китаем» истинно», мы можем снова применить modus ponens, потому что мы знаем, что утверждение «это предложение истинно» верно. Таким образом, мы можем сделать вывод, что Германия граничит с Китаем.

В формальной логике

Сентенциальная логика

В примере из предыдущего раздела использовались неформализованные рассуждения на естественном языке. Парадокс Карри также встречается в некоторых разновидностях формальной логики . В этом контексте это показывает, что если мы предположим, что существует формальное предложение ( X → Y ), где само X эквивалентно ( X → Y ), то мы можем доказать Y с помощью формального доказательства. Одним из примеров такого формального доказательства является следующий. Для объяснения логических обозначений, используемых в этом разделе, обратитесь к списку логических символов .

Икс := ( Икс → Y )
предположение , отправная точка, эквивалентная «Если это предложение истинно, то Y »
Икс → Икс
закон идентичности
Икс → ( Икс → Y )
замените правую часть 2 , так как X эквивалентно X → Y на 1
Х → Y
от 3 путем сокращения
Х
заменить 4 на 1
И
от 5 и 4 по модусу поненсу

Альтернативное доказательство — закон Пирса . Если X знак равно X → Y , то ( → Y ) → X. X Это вместе с законом Пирса (( X → Y ) → X ) → X и modus ponens подразумевает X , а затем Y (как в доказательстве выше).

Приведенный выше вывод показывает, что если Y не существует утверждения X является недоказуемым утверждением в формальной системе, то в этой системе такого, что X эквивалентно импликации ( X → Y ). Другими словами, шаг 1 предыдущего доказательства терпит неудачу. Напротив, в предыдущем разделе показано, что в естественном (неформализованном) языке для каждого утверждения Y естественного языка существует утверждение Z естественного языка такое, что Z эквивалентно ( Z → Y ) на естественном языке. А именно, Z — это «Если это предложение истинно, то Y ».

Наивная теория множеств

Даже если лежащая в основе математическая логика не допускает никаких самореферентных предложений, некоторые формы наивной теории множеств все еще уязвимы для парадокса Карри. В теориях множеств, допускающих неограниченное понимание , мы можем доказать любое логическое утверждение Y , исследуя множество. $X\ {\stackrel {\mathrm {def} }{=}}\ \left\{x\mid (x\in x)\to Y\right\}.$ Тогда легко показать, что утверждение $X\in X$ эквивалентно $(X\in X)\to Y$ . Из этого, $Y$ можно вывести аналогично доказательствам, приведенным выше. (« $X\in X$ " означает "это предложение".)

Следовательно, в последовательной теории множеств множество $\left\{x\mid (x\in x)\to Y\right\}$ не существует для ложного Y . Это можно рассматривать как вариант парадокса Рассела , но он не идентичен. Некоторые предложения по теории множеств пытались справиться с парадоксом Рассела не путем ограничения правила понимания, а путем ограничения правил логики, чтобы она допускала противоречивую природу множества всех множеств, которые не являются членами самих себя. Существование доказательств, подобных приведенному выше, показывает, что такая задача не так уж проста, поскольку хотя бы одно из правил вывода, использованных в приведенном выше доказательстве, должно быть опущено или ограничено.

Лямбда-исчисление с ограниченной минимальной логикой

Парадокс Карри может быть выражен в нетипизированном лямбда-исчислении , обогащенном импликативным исчислением высказываний . Чтобы справиться с синтаксическими ограничениями лямбда-исчисления, $m$ будет обозначать функцию импликации, принимающую два параметра, то есть лямбда-член $((mA)B)$ должно быть эквивалентно обычной инфиксной записи $A\to B$ .

Произвольная формула $Z$ можно доказать, определив лямбда-функцию $N:=\lambda p.((mp)Z)$ , и $X:=({\textsf {Y}}N)$ , где ${\textsf {Y}}$ обозначает комбинатор Карри с фиксированной точкой . Затем $X=(NX)=((mX)Z)$ по определению ${\textsf {Y}}$ и $N$ , следовательно, приведенное выше доказательство сентенциальной логики можно продублировать в исчислении: ^{[ 4 ]}^{[ 5 ]}^{[ 6 ]}

${\begin{array}{cll}\vdash &((mX)X)&{\mbox{ by the minimal logic axiom }}A\to A\\\vdash &((mX)((mX)Z))&{\mbox{ since }}X=((mX)Z)\\\vdash &((mX)Z)&{\mbox{ by the theorem }}(A\to (A\to B))\vdash (A\to B){\mbox{ of minimal logic }}\\\vdash &X&{\mbox{ since }}X=((mX)Z)\\\vdash &Z&{\mbox{ by modus ponens }}A,(A\to B)\vdash B{\mbox{ from }}X{\mbox{ and }}((mX)Z)\\\end{array}}$

В просто типизированном лямбда -исчислении комбинаторы с фиксированной точкой не могут быть типизированы и, следовательно, не допускаются.

Комбинаторная логика

Парадокс Карри также может быть выражен в комбинаторной логике , которая имеет эквивалентную выразительную силу лямбда-исчислению . Любое лямбда-выражение можно перевести в комбинаторную логику, поэтому перевода реализации парадокса Карри в лямбда-исчислении будет достаточно.

Вышеупомянутый термин $X$ переводится на $(r\ r)$ в комбинаторной логике, где $r={\textsf {S}}\ ({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))\ ({\textsf {K}}Z);$ следовательно ^{[ 7 ]} $(r\ r)=((m(rr))\ Z).$

Обсуждение

Парадокс Карри можно сформулировать на любом языке, поддерживающем основные логические операции, который также позволяет создавать саморекурсивную функцию в виде выражения. Двумя механизмами, поддерживающими построение парадокса, являются самореференция (способность ссылаться на «это предложение» изнутри предложения) и неограниченное понимание в наивной теории множеств. Естественные языки почти всегда содержат множество особенностей, которые можно использовать для построения парадокса, как и многие другие языки. Обычно добавление в язык возможностей метапрограммирования добавляет необходимые функции. Математическая логика обычно не допускает явных ссылок на собственные предложения; однако в основе теорем Гёделя о неполноте лежит наблюдение о том, что можно добавить другую форму ссылки на себя — см. число Гёделя .

Правила, используемые при построении доказательства, — это правило предположения для условного доказательства, правило сокращения и modus ponens . Они включены в большинство распространенных логических систем, таких как логика первого порядка.

Следствия для некоторой формальной логики

В 1930-х годах парадокс Карри и связанный с ним парадокс Клини-Россера , на основе которого был разработан парадокс Карри, ^{[ 8 ]}^{[ 1 ]} сыграл важную роль в демонстрации того, что различные формальные логические системы, допускающие саморекурсивные выражения, несовместимы .

Аксиома неограниченного понимания не поддерживается современной теорией множеств , и таким образом удается избежать парадокса Карри.

См. также

Ссылки

^ Перейти обратно: ^а ^б Карри, Хаскелл Б. (сентябрь 1942 г.). «Непоследовательность некоторых формальных логик». Журнал символической логики . 7 (3): 115–117. дои : 10.2307/2269292 . JSTOR 2269292 . S2CID 121991184 .
^ Барвайз, Джон ; Этчеменди, Джон (1987). Лжец: эссе об истине и цикличности . Нью-Йорк: Издательство Оксфордского университета. п. 23. ISBN 0195059441 . Проверено 24 января 2013 г.
^ Параллельный пример объясняется в Стэнфордской энциклопедии философии. Видеть Шапиро, Лайонел; Билл, Джей (2018). «Парадокс Карри» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
^ Именование здесь соответствует доказательству сентенциальной логики, за исключением того, что Z » используется « вместо « Y », чтобы избежать путаницы с комбинатором Карри с фиксированной точкой. ${\textsf {Y}}$ .
^ Жерар Юэ (май 1986 г.). Формальные структуры для вычислений и дедукции . Международная летняя школа по логике программирования и расчетам дискретного проектирования. Марктобердорф. Архивировано из оригинала 14 июля 2014 г. {{cite book}}: CS1 maint: отсутствует местоположение издателя ( ссылка ) Здесь: стр.125
^ Хаскелл Б. Карри ; Роберт Фейс (1958). Комбинаторная логика И. Исследования по логике и основам математики. Том. 22. Амстердам: Северная Голландия. ^{[ нужна страница ]}
^ $(rr)$ $=$ $({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))$ $\to$ $({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}})({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {K}}Z({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))$ $\to$ $({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}})({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))Z)$ $\to$ $({\textsf {K}}m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $\to$ $(m({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $\to$ $(m({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))Z)$ $\to$ $(m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))Z)$ $\to$ $(m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $=$ $((m(rr))\ Z)$
^ Карри, Хаскелл Б. (июнь 1942 г.). «Комбинаторные основы математической логики». Журнал символической логики . 7 (2): 49–64. дои : 10.2307/2266302 . JSTOR 2266302 . S2CID 36344702 .

Внешние ссылки

Билл, Дж. К. «Парадокс Карри» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
Кантини, Андреа. «Парадоксы и современная логика» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
Пингвины правят Вселенной: Доказательство того, что пингвины правят Вселенной , краткое и занимательное обсуждение парадокса Карри.

[:0-1] Перейти обратно: ^а ^б Карри, Хаскелл Б. (сентябрь 1942 г.). «Непоследовательность некоторых формальных логик». Журнал символической логики . 7 (3): 115–117. дои : 10.2307/2269292 . JSTOR 2269292 . S2CID 121991184 .

[2] Барвайз, Джон ; Этчеменди, Джон (1987). Лжец: эссе об истине и цикличности . Нью-Йорк: Издательство Оксфордского университета. п. 23. ISBN 0195059441 . Проверено 24 января 2013 г.

[3] Параллельный пример объясняется в Стэнфордской энциклопедии философии. Видеть Шапиро, Лайонел; Билл, Джей (2018). «Парадокс Карри» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .

[4] Именование здесь соответствует доказательству сентенциальной логики, за исключением того, что Z » используется « вместо « Y », чтобы избежать путаницы с комбинатором Карри с фиксированной точкой. ${\textsf {Y}}$ .

[5] Жерар Юэ (май 1986 г.). Формальные структуры для вычислений и дедукции . Международная летняя школа по логике программирования и расчетам дискретного проектирования. Марктобердорф. Архивировано из оригинала 14 июля 2014 г. {{cite book}}: CS1 maint: отсутствует местоположение издателя ( ссылка ) Здесь: стр.125

[6] Хаскелл Б. Карри ; Роберт Фейс (1958). Комбинаторная логика И. Исследования по логике и основам математики. Том. 22. Амстердам: Северная Голландия. ^{[ нужна страница ]}

[7] $(rr)$ $=$ $({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))$ $\to$ $({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}})({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {K}}Z({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))$ $\to$ $({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}})({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))Z)$ $\to$ $({\textsf {K}}m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $\to$ $(m({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $\to$ $(m({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))Z)$ $\to$ $(m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))Z)$ $\to$ $(m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $=$ $((m(rr))\ Z)$

[8] Карри, Хаскелл Б. (июнь 1942 г.). «Комбинаторные основы математической логики». Журнал символической логики . 7 (2): 49–64. дои : 10.2307/2266302 . JSTOR 2266302 . S2CID 36344702 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

v т и Известные парадоксы
Philosophical	Analysis Buridan's bridge Dream argument Epicurean Fiction Fitch's knowability Free will Goodman's Hedonism Liberal Meno's Mere addition Moore's Newcomb's Nihilism Omnipotence Preface Rule-following Sorites Theseus' ship White horse Zeno's
Logical	Barber Berry Bhartrhari's Burali-Forti Court Crocodile Curry's Epimenides Free choice paradox Grelling–Nelson Kleene–Rosser Liar Card No-no Pinocchio Quine's Yablo's Opposite Day Paradoxes of set theory Richard's Russell's Socratic Hilbert's Hotel Temperature paradox Barbershop Catch-22 Chicken or the egg Drinker Entailment Lottery Plato's beard Raven Ross's Unexpected hanging "What the Tortoise Said to Achilles" Heat death paradox Olbers's paradox
Economic	Allais Antitrust Arrow information Bertrand Braess's Competition Income and fertility Downs–Thomson Easterlin Edgeworth Ellsberg European Gibson's Giffen good Icarus Jevons Leontief Lerner Lucas Mandeville's Mayfield's Metzler Plenty Productivity Prosperity Scitovsky Service recovery St. Petersburg Thrift Toil Tullock Value
Decision theory	Abilene Apportionment Alabama New states Population Arrow's Buridan's ass Chainstore Condorcet's Decision-making Downs Ellsberg Fenno's Fredkin's Green Hedgehog's Inventor's Kavka's toxin puzzle Morton's fork Navigation Newcomb's Parrondo's Preparedness Prevention Prisoner's dilemma Tolerance Willpower
List Category