Парадокс Карри - это парадокс, в котором произвольное утверждение F доказывается простым существованием предложения C, которое говорит о себе «Если C , то F », требуя лишь нескольких, казалось бы, безобидных правил логической дедукции. Поскольку F произвольно, любая логика, имеющая эти правила, позволяет доказать все. Парадокс может быть выражен на естественном языке и в различных логиках , включая определенные формы теории множеств , лямбда-исчисления и комбинаторной логики .
Парадокс назван в честь логика Хаскелла Карри . Он также был назван парадоксом LOB в после Мартина Уго LOB , [1] из - за его связь с теоремой лёба .
На естественном языке
Претензии вида «если А, то Б» называются условными . В парадоксе Карри используется особый вид условных предложений с указанием самих себя, как показано в этом примере:
Несмотря на то, что Германия не граничит с Китаем , примерное предложение определенно является предложением на естественном языке, и поэтому истинность этого предложения может быть проанализирована. Из этого анализа следует парадокс. Анализ состоит из двух этапов.
- Во-первых, можно использовать общепринятые методы доказательства на естественном языке, чтобы доказать, что приведенное в качестве примера предложение истинно.
- Во-вторых, истинность приведенного в качестве примера предложения может быть использована для доказательства того, что Германия граничит с Китаем. Поскольку Германия не граничит с Китаем, это говорит о том, что в одном из доказательств допущена ошибка.
Утверждение «Германия граничит с Китаем» может быть заменено любым другим утверждением, и приговор все равно будет доказуемым. Таким образом, каждое предложение представляется доказуемым. Поскольку в доказательстве используются только общепринятые методы дедукции, и поскольку ни один из этих методов не кажется неправильным, эта ситуация парадоксальна. [2]
Неофициальное доказательство
Стандартный метод доказательства условных предложений (предложений формы «если А, то Б») называется « условным доказательством ». В этом методе, чтобы доказать, что «если A, то B», сначала предполагается A, а затем с этим предположением B показывается истинным.
Чтобы произвести парадокс Карри, как описано в двух шагах выше, примените этот метод к предложению «если это предложение верно, то Германия граничит с Китаем». Здесь 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
- X → Yот 3 по сокращению
- Иксзаменить 4 на 1
- Yот 5 и 4 по модусу поненс
Альтернативное доказательство - через закон Пирса . Если X = X → Y, то (X → Y) → X. Это вместе с законом Пирса ((X → Y) → X) → X и modus ponens влечет X, а затем Y (как в доказательстве выше).
Следовательно, если Y - недоказуемое утверждение в формальной системе, в этой системе нет такого утверждения X, что X эквивалентно импликации (X → Y). Напротив, предыдущий раздел показывает, что в естественном (неформализованном) языке для каждого оператора Y естественного языка существует такое утверждение Z естественного языка, что Z эквивалентно (Z → Y) в естественном языке. А именно, Z - это «Если это предложение верно, то Y».
В конкретных случаях, когда классификация Y уже известна, требуется несколько шагов, чтобы выявить противоречие. Например, когда Y - «Германия граничит с Китаем», известно, что Y ложно.
- Х = (Х → Y)предположение
- X = (X → ложь)заменить известное значение Y
- X = (¬X ∨ ложь)
- Х = ¬Xличность
Наивная теория множеств
Даже если лежащая в основе математическая логика не допускает никаких самореференциальных предложений, некоторые формы наивной теории множеств по-прежнему уязвимы для парадокса Карри. В теориях множеств, допускающих неограниченное понимание , мы, тем не менее, можем доказать любое логическое утверждение Y , исследуя множество
При условии, что имеет приоритет перед обоими а также , доказательство происходит следующим образом:
- Определение X
- Замена равных наборов в членстве
- Добавление консеквента к обеим сторонам двусмысленного (из 2)
- Закон конкреции (из 1 и 3)
- Двуусловное выбывание (из 4)
- Сокращение (от 5)
- Двуусловное выбывание (из 4)
- Modus ponens (из 6 и 7)
- Modus ponens (из 8 и 6)
Шаг 4 - единственный недопустимый шаг в непротиворечивой теории множеств. В теории множеств Цермело – Френкеля потребовалась бы дополнительная гипотеза, утверждающая, что X является множеством, что недоказуемо в ZF или его расширении ZFC (с выбранной аксиомой ).
Следовательно, в непротиворечивой теории множеств множество не существует для ложного Y . Это можно рассматривать как вариант парадокса Рассела , но он не идентичен. Некоторые предложения по теории множеств пытались справиться с парадоксом Рассела не путем ограничения правила понимания, а путем ограничения правил логики, чтобы она допускала противоречивую природу множества всех множеств, которые не являются членами самих себя. Существование доказательств, подобных приведенному выше, показывает, что такая задача не так проста, потому что по крайней мере одно из правил вывода, используемых в приведенном выше доказательстве, должно быть опущено или ограничено.
Лямбда-исчисление
Парадокс Карри может быть выражен в нетипизированном лямбда-исчислении , обогащенном ограниченной минимальной логикой . Чтобы справиться с синтаксическими ограничениями лямбда-исчисления, будет обозначать функцию импликации, принимающую два параметра, то есть лямбда-член должен быть эквивалентен обычной инфиксной записи .
Произвольная формула можно доказать, определив лямбда-функцию , а также , где обозначает комбинатор Карри с фиксированной точкой . потом по определению а также , следовательно, приведенное выше доказательство сентенциальной логики может быть продублировано в исчислении: [3] [4] [5]
В просто типизированном лямбда-исчислении комбинаторы с фиксированной точкой не могут быть типизированы и, следовательно, не допускаются.
Комбинаторная логика
Парадокс Карри также может быть выражен в комбинаторной логике , которая имеет эквивалентную выразительную силу лямбда-исчислению . Любое лямбда-выражение может быть переведено в комбинаторную логику, поэтому будет достаточно перевода реализации парадокса Карри в лямбда-исчислении.
Вышеупомянутый термин переводится на в комбинаторной логике, где
следовательно
Обсуждение
Парадокс Карри может быть сформулирован на любом языке, поддерживающем базовые логические операции, который также позволяет конструировать саморекурсивную функцию как выражение. Два механизма, которые поддерживают построение парадокса, - это самоотнесение (способность ссылаться на «это предложение» изнутри предложения) и неограниченное понимание в наивной теории множеств. Естественные языки почти всегда содержат множество функций, которые можно использовать для построения парадокса, как и многие другие языки. Обычно добавление к языку возможностей метапрограммирования добавляет необходимые функции. Математическая логика обычно не допускает явных ссылок на свои собственные предложения. Однако в основе теорем Гёделя о неполноте лежит наблюдение, что можно добавить другую форму самореференции; см. число Гёделя .
Аксиома неограниченного понимания добавляет возможность построить рекурсивное определение в теории множеств. Эта аксиома не поддерживается современной теорией множеств .
Логические правила, используемые при построении доказательства, - это правило предположения для условного доказательства, правило сжатия и modus ponens . Они включены в наиболее распространенные логические системы, такие как логика первого порядка.
Последствия для некоторой формальной логики
В 1930-х годах парадокс Карри и связанный с ним парадокс Клини – Россера сыграли важную роль в демонстрации несовместимости формальных логических систем, основанных на саморекурсивных выражениях . К ним относятся некоторые версии лямбда-исчисления и комбинаторной логики .
Карри начал с парадокса Клини – Россера [7] и пришел к выводу, что основная проблема может быть выражена в этом более простом парадоксе Карри. [8] [9] Его вывод может быть сформулирован как утверждение, что комбинаторная логика и лямбда-исчисление не могут быть согласованы в качестве дедуктивных языков, но при этом допускают рекурсию.
Изучая иллятивную (дедуктивную) комбинаторную логику , Карри в 1941 [10] осознал, что парадокс подразумевает, что следующие свойства комбинаторной логики без ограничений несовместимы:
- Комбинаторная полнота . Это означает, что оператор абстракции является определяемым (или примитивным) в системе, что является требованием к выразительной мощности системы.
- Дедуктивная полнота . Это требование выводимости, а именно принцип, согласно которому в формальной системе с материальной импликацией и modus ponens, если Y доказуемо на основе гипотезы X, то существует также доказательство X → Y. [11]
разрешение
Обратите внимание, что в отличие от парадокса лжеца или парадокса Рассела, парадокс Карри не зависит от того, какая модель отрицания используется, поскольку он полностью свободен от отрицания. Таким образом, паранепротиворечивые логики все еще могут быть уязвимы для этого парадокса, даже если они невосприимчивы к парадоксу лжеца.
Нет разрешения в лямбда-исчислении
Происхождение Алонзо Черч «s лямбда - исчисления может быть,„Как вы можете решить уравнение, чтобы обеспечить определение функции?“. Это выражается в этой эквивалентности,
Это определение действительно, если есть одна и только одна функция который удовлетворяет уравнению , но в противном случае недействителен. Это суть проблемы, которую Стивен Коул Клини, а затем Хаскелл Карри обнаружили с помощью комбинаторной логики и лямбда-исчисления.
Ситуацию можно сравнить с определением
Это определение подходит, если для квадратного корня допускаются только положительные значения. В математике экзистенциально количественно определенная переменная может представлять несколько значений, но только по одному за раз. Количественная оценка существования - это дизъюнкция многих экземпляров уравнения. В каждом уравнении есть одно значение переменной.
Однако в математике выражение без свободных переменных должно иметь одно и только одно значение. Так может только представлять . Однако нет удобного способа ограничить лямбда-абстракцию одним значением или гарантировать, что значение существует.
Лямбда-исчисление допускает рекурсию, передавая ту же функцию, которая вызывается в качестве параметра. Это позволяет ситуации, когда есть несколько или нет решений для .
Лямбда-исчисление можно рассматривать как часть математики, если разрешены только лямбда-абстракции, которые представляют единственное решение уравнения. Другие лямбда-абстракции неверны в математике.
Парадокс Карри и другие парадоксы возникают в лямбда-исчислении из-за несостоятельности лямбда-исчисления, рассматриваемого как дедуктивная система . См. Также дедуктивное лямбда-исчисление .
Область терминов лямбда-исчисления
Лямбда-исчисление - последовательная теория в своей собственной области . Однако добавлять определение лямбда-абстракции в общую математику непоследовательно . Лямбда-члены описывают значения из области лямбда-исчисления. Каждый лямбда-термин имеет значение в этом домене.
При переводе выражений из математики в лямбда-исчисление область терминов лямбда-исчисления не всегда изоморфна области математических выражений. Это отсутствие изоморфизма является источником очевидных противоречий.
Разрешение на неограниченных языках
Есть много языковых конструкций, которые неявно вызывают уравнение, которое может не иметь или иметь много решений. Звуковое решение этой проблемы состоит в том, чтобы синтаксически связать эти выражения с экзистенциально количественной переменной. Переменная представляет несколько значений таким образом, который имеет смысл в обычном человеческом рассуждении, но также применим в математике.
Например, естественный язык, допускающий функцию Eval, математически несовместим. Но каждый призыв к Eval на этом естественном языке может быть последовательно переведен на математический язык. Перевод Eval (s) в математику
Итак, где s = "Eval (s) → y",
Если y ложно, то x = x → y ложно, но это ложь, а не парадокс.
Существование переменной x подразумевается в естественном языке. Переменная x создается, когда естественный язык переводится в математику. Это позволяет нам использовать естественный язык с естественной семантикой при сохранении математической целостности.
Разрешение в формальной логике
Аргумент в формальной логике начинается с допущения действительности наименования (X → Y) как X. Однако это не правильная отправная точка. Сначала мы должны установить обоснованность наименования. Следующая теорема легко доказывается и представляет собой такое именование:
В приведенном выше утверждении формула A названа как X. Теперь попытайтесь создать экземпляр формулы с (X → Y) для A. Однако это невозможно, так как область видимости находится в рамках . Порядок квантификаторов может быть изменен с помощью сколемизации :
Однако теперь создание экземпляра дает
что не является отправной точкой для доказательства и не приводит к противоречию. Для A нет других экземпляров, которые привели бы к отправной точке парадокса.
Разрешение в теории множеств
В теории множеств Цермело – Френкеля (ZFC) аксиома неограниченного понимания заменена группой аксиом, которые позволяют строить множества. Итак, парадокс Карри нельзя описать в ZFC. ZFC возникла в ответ на парадокс Рассела.
Смотрите также
- Парадокс Рассела
- Парадокс Жирара
- Парадокс Клини – Россера
- Парадокс лжеца
- Список парадоксов
- Парадокс ричарда
- Теория множеств Цермело – Френкеля.
- Комбинатор с фиксированной точкой
- Дедуктивное лямбда-исчисление
- Пусть выражение
Рекомендации
- ^ Барвайз, Джон ; Этчменди, Джон (1987). Лжец: эссе об истине и круговороте . Нью-Йорк: Издательство Оксфордского университета. п. 23. ISBN 0195059441. Проверено 24 января 2013 года .
- ^ Параллельный пример объясняется в Стэнфордской энциклопедии философии. Видеть Шапиро, Лайонел; Билл, Дж. С. (2018). «Парадокс Карри» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
- ^ Обозначение здесь следует за доказательством сентенциональной логики, за исключением того, что " Z " используется вместо " Y ", чтобы избежать путаницы с комбинатором фиксированной точки Карри..
- ^ Жерар Юэ (май 1986). Формальные структуры для вычислений и дедукции . Международная летняя школа по логике программирования и исчислениям дискретного проектирования. Марктобердорф. Архивировано из оригинала на 2014-07-14. Здесь: с.125
- ^ Хаскелл Б. Карри ; Роберт Фейс (1958). Комбинаторной логики я . Исследования по логике и основам математики. 22 . Амстердам: Северная Голландия.[ требуется страница ]
- ^
- ^ Клини, С. К. и Россер, Дж. Б. (1935). «Несостоятельность некоторых формальных логик». Анналы математики . 36 (3): 630–636. DOI : 10.2307 / 1968646 . JSTOR 1968646 .
- ^ Карри, Хаскелл Б. (июнь 1942 г.). «Комбинаторные основы математической логики». Журнал символической логики . 7 (2): 49–64. DOI : 10.2307 / 2266302 . JSTOR 2266302 .
- ^ Карри, Хаскелл Б. (сентябрь 1942 г.). «Несогласованность некоторых формальных логик». Журнал символической логики . 7 (3): 115–117. DOI : 10.2307 / 2269292 . JSTOR 2269292 .
- ^ Карри, Хаскелл Б. (1941). «Парадокс Клини и Россера» . Труды Американского математического общества . 50 (3): 454–516. DOI : 10.1090 / S0002-9947-1941-0005275-6 . Руководство по ремонту 0005275 . Проверено 24 января 2013 года .
- ^ Стенлунд, Сорен (1972). Комбинаторы, λ-члены и теория доказательства . Дордрехт: Д. Рейдел . п. 71. ISBN 978-9027703057.
Внешние ссылки
- Beall, JC "Парадокс Карри" . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
- Кантини, Андреа. «Парадоксы и современная логика» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
- Пингвины правят Вселенной: доказательство того, что пингвины правят Вселенной , краткое и занимательное обсуждение парадокса Карри.