Если предложение «Если это предложение истинно, то Луна сделана из сыра» является истинным, то из него формально следует, что Луна действительно сделана из сыра — и классическая логика не может этому возразить.
История возникновения парадокса
В 1942 году американский логик и математик Хаскелл Брукс Карри опубликовал работу, в которой описал необычную конструкцию. Карри не был новичком в мире формальных систем — он занимался комбинаторной логикой, лямбда-исчислением и основаниями математики. Его имя уже было связано с каррированием — техникой преобразования функций, которую используют программисты по сей день. Но именно парадокс, носящий его имя, стал одним из самых тревожных результатов в истории логики.
Контекст, в котором появился парадокс, был крайне напряженным. Математики первой половины XX века переживали настоящий кризис оснований. Парадокс Рассела уже разрушил наивную теорию множеств. Теоремы Гёделя о неполноте показали, что формальные системы не могут быть одновременно полными и непротиворечивыми. И вот Карри обнаружил нечто, что не укладывалось даже в эту и без того тревожную картину.
| Параметр | Детали |
|---|---|
| Автор | Хаскелл Брукс Карри (Haskell Brooks Curry) |
| Год публикации | 1942 |
| Работа | «The Inconsistency of Certain Formal Logics» |
| Область | Формальная логика, основания математики |
| Предшествующие парадоксы | Парадокс лжеца, парадокс Рассела, парадокс Ришара |
| Ключевое отличие | Не использует отрицание — работает только с импликацией |
Важно понимать: Карри не просто нашел еще одну головоломку для развлечения на семинарах. Он показал, что целый класс формальных систем — включая некоторые варианты теории типов и наивную теорию множеств — содержит фатальную уязвимость. И эта уязвимость не требует сложных конструкций. Она прячется в самых базовых правилах вывода.
В чем именно заключается противоречие
Для начала возьмем обычное предложение: «Если на улице дождь, то я возьму зонт». Это импликация — конструкция вида «если A, то B». Она привычна, понятна и безопасна. А теперь сделаем одну маленькую, почти невинную модификацию.
Построим предложение, которое ссылается само на себя:
C = «Если C истинно, то произвольное утверждение P истинно»
Пусть P — это что угодно. «Луна сделана из сыра». «2 + 2 = 5». «Все кошки — это собаки». Абсолютно любое утверждение. Теперь проследим цепочку рассуждений, каждый шаг которой безупречен с точки зрения классической логики:
- Предположим, что C истинно. Тогда, по определению C, верно высказывание «если C истинно, то P истинно».
- Но мы уже предположили, что C истинно. Значит, по правилу modus ponens (если «A → B» и «A», то «B»), получаем, что P истинно.
- Итого: из предположения «C истинно» мы вывели «P истинно». Но это и есть содержание самого C! Значит, мы только что доказали, что C истинно.
- Раз C истинно (мы это доказали на шаге 3), и C утверждает «если C, то P», то снова по modus ponens получаем: P истинно. Любое P. Вообще любое.
Остановитесь и перечитайте. Ни на одном шаге мы не использовали отрицание. Мы не говорили «это предложение ложно», как в парадоксе лжеца. Мы не строили множество всех множеств, не содержащих самих себя. Мы просто использовали самоссылку и импликацию — два фундаментальных инструмента логики.
Попробуйте найти ошибку в рассуждении выше. Каждый шаг использует только стандартные правила классической логики. Если вы не видите ошибки — это и есть парадокс. Ошибки нет. Проблема заключается в самой системе.
Вот что делает парадокс Карри по-настоящему пугающим. Парадокс лжеца можно попытаться обезвредить, ограничив использование отрицания или понятия истины. Парадокс Рассела можно обойти, запретив определенные виды множеств. Но парадокс Карри бьет глубже — он показывает, что одной лишь комбинации самоссылки и правила сжатия (contraction) достаточно, чтобы из системы можно было вывести вообще что угодно.
Формальная запись
Для тех, кто предпочитает символы:
| Шаг | Формула | Обоснование |
|---|---|---|
| 1 | C ↔ (C → P) | Определение предложения C (через самоссылку) |
| 2 | Допустим C | Предположение |
| 3 | C → P | Из шага 1 и шага 2 (раскрытие определения) |
| 4 | P | Modus ponens: шаг 2 + шаг 3 |
| 5 | C → P | Введение импликации: из допущения C вывели P (шаги 2-4) |
| 6 | C | Из шага 1 и шага 5 (обратное направление эквивалентности) |
| 7 | P | Modus ponens: шаг 6 + шаг 5 |
Семь шагов — и формальная система доказывает абсолютно любое утверждение. Этот результат называют «тривиализацией» системы: если можно доказать все, то система бесполезна, потому что не различает истину и ложь.
Попытки решения
С момента публикации работы Карри логики, математики и философы предложили множество стратегий борьбы с этим парадоксом. Ни одна из них не является бесспорной — каждая требует жертв.
| Подход | Авторы / Школа | Суть решения | Чем жертвуют |
|---|---|---|---|
| Иерархия языков | Альфред Тарский (1930-е) | Запретить предложениям ссылаться на собственную истинность. Предикат истины для языка L определяется только в метаязыке L’ | Невозможность построить универсальный язык, способный говорить о собственной семантике |
| Ограничение правил сжатия | Сублинейные и субструктурные логики (с 1960-х) | Отказ от структурного правила сжатия (contraction): нельзя использовать одну и ту же посылку дважды в одном выводе | Потеря некоторых привычных теорем классической логики |
| Паранепротиворечивые логики | Грэм Прист, Ньютон да Коста (1970-е — 1980-е) | Допустить, что некоторые противоречия могут быть истинными, но не позволять из них выводить что угодно (отказ от принципа взрыва) | Интуитивная ясность понятия непротиворечивости |
| Ревизия понятия импликации | Релевантные логики: Алан Андерсон, Нуэль Белнап (1960-е — 1970-е) | Потребовать, чтобы между посылкой и заключением существовала содержательная связь, а не только формальная | Простота и элегантность материальной импликации |
| Запрет самоссылки | Различные формальные теории (теория типов Рассела, ZFC) | Построить систему так, чтобы конструкция вида C = «если C, то P» была просто невозможна синтаксически | Выразительная мощность системы |
| Ревизионная теория истины | Аниль Гупта, Нуэль Белнап (1993) | Истина определяется через бесконечный итеративный процесс пересмотра; парадоксальные предложения не получают стабильного значения | Классическое понимание истины как статического свойства |
Особого внимания заслуживает подход субструктурных логик. В классической логике есть несколько «структурных правил», которые кажутся настолько очевидными, что обычно их даже не формулируют явно. Одно из них — правило сжатия: если у вас есть посылка A, вы можете использовать ее сколько угодно раз. Именно это правило позволяет на шаге 4 использовать C одновременно как посылку modus ponens и как элемент, из которого извлекается импликация C → P. Без сжатия вывод разваливается.
Грег Рестолл, Зак Вебер, Энтони Крисс и другие современные логики активно работают в этом направлении. Линейная логика Жана-Ива Жирара (1987) — один из наиболее известных примеров системы без правила сжатия. В ней ресурсы (посылки) расходуются: использовав посылку один раз, вы не можете использовать ее снова, если она не была явно дублирована.
Где парадокс встречается в реальной жизни, науке и математике
Парадокс Карри — не абстрактная игрушка для философов. Он обнаруживается в самых неожиданных местах.
Наивная теория множеств
В наивной теории множеств можно определить множество:
S = {x : если x ∈ x, то P}
Далее задаем вопрос: принадлежит ли S самому себе? Если S ∈ S, то по определению верно «если S ∈ S, то P», и по modus ponens получаем P. Значит, S ∈ S → P. Но это и есть условие членства в S, значит, S ∈ S. Применяем modus ponens еще раз — и доказываем произвольное P. Именно поэтому наивная теория множеств была заменена аксиоматическими системами вроде ZFC, где подобные конструкции запрещены схемой аксиом выделения.
Информатика и теория типов
Парадокс Карри имеет прямое отношение к проектированию языков программирования. Через соответствие Карри-Ховарда типы соответствуют высказываниям, а программы — доказательствам. Если система типов допускает нетипизированную рекурсию (аналог самоссылки), в ней можно построить «доказательство» любого типа, то есть программу, которая якобы возвращает значение любого типа, но на самом деле зацикливается или вызывает ошибку.
- Нетипизированное лямбда-исчисление допускает аналог парадокса Карри через омега-комбинатор и Y-комбинатор. Именно поэтому нетипизированное лямбда-исчисление не подходит как основание для логики.
- Языки с зависимыми типами (Coq, Agda, Lean) специально запрещают общую рекурсию и требуют доказательства завершимости функций — во многом именно для того, чтобы избежать парадоксов типа Карри.
- Парадокс Жирара (1972) — типо-теоретический аналог парадокса Карри — показал, что система U (System U) с типом Type : Type несовместна. Это привело к созданию иерархий универсумов в современных системах доказательств.
Представьте, что вы пишете программу и система типов гарантирует: «Эта функция всегда возвращает число». Но если в системе есть аналог парадокса Карри, такая «гарантия» ничего не стоит — можно написать код, который формально типизирован как возвращающий число, но на самом деле не возвращает ничего. Готовы ли вы доверить безопасность медицинского оборудования или ядерного реактора такой системе?
Юридические и бытовые самоссылки
Хотя формальный парадокс Карри живет в мире логики, его структура проглядывает и в повседневных ситуациях:
- Договоры с самоссылающимися условиями: «Если данный пункт договора действителен, то заказчик обязан выплатить исполнителю миллиард долларов». Юристы знают, что подобные конструкции могут создавать интерпретационные ловушки.
- Бюрократические петли: «Если вы имеете право на получение этой справки, то вам выдается допуск к секретным документам» — при условии, что право на справку определяется через наличие допуска.
- Фейковые обещания: «Если я когда-нибудь совру тебе, я подарю тебе миллион». Само по себе звучит щедро, но если встроить самоссылку, конструкция становится ненадежной.
Философия и теория истины
Парадокс Карри стал одним из ключевых аргументов в дебатах о природе истины. Дефляционные теории истины (согласно которым «P истинно» означает просто P и ничего больше) сталкиваются с серьезными проблемами при встрече с парадоксом Карри. Если предикат истины удовлетворяет T-схеме Тарского (T(⌜P⌝) ↔ P) без ограничений, то парадокс Карри немедленно тривиализирует всю теорию. Это заставило философов вроде Хартри Филда разрабатывать сложные условные конструкции, в которых импликация ведет себя иначе, чем в классической логике.
Интересные факты и связанные парадоксы
Факты, которые удивляют
- Парадокс Карри старше, чем кажется. Хотя Карри опубликовал его в 1942 году, саму идею самоссылающейся импликации обсуждал еще Лёб в контексте теорем Гёделя. Теорема Лёба (1955) является формализованным «ручным» вариантом парадокса Карри внутри арифметики Пеано.
- Без отрицания. Большинство известных логических парадоксов существенно используют отрицание. Парадокс Карри — одно из немногих исключений. Это делает его особенно коварным: системы, разработанные для борьбы с парадоксами отрицания, перед ним бессильны.
- Название языка Haskell — популярного функционального языка программирования — дано в честь того самого Хаскелла Карри. Ирония: язык, названный в честь человека, открывшего способ сломать логику, имеет одну из самых строгих систем типов, специально защищенную от подобных поломок.
- Карри доказал, а не предположил. Это не гипотеза и не открытый вопрос. Парадокс Карри — это строгий математический результат: любая формальная система, допускающая неограниченную самоссылку и стандартные правила для импликации, неизбежно тривиальна. Не «может оказаться тривиальной», а гарантированно является таковой.
Семейство родственных парадоксов
| Парадокс | Ключевой механизм | Связь с парадоксом Карри |
|---|---|---|
| Парадокс лжеца | Самоссылка + отрицание | Парадокс Карри обобщает лжеца, заменяя отрицание произвольной импликацией |
| Парадокс Рассела | Самоссылка в теории множеств + отрицание | Парадокс Карри для множеств работает без отрицания |
| Теорема Лёба | Самоссылка внутри арифметики | Формализованная версия рассуждения Карри; если система доказывает «если доказуемо P, то P», то она доказывает P |
| Парадокс Жирара | Type : Type в теории типов | Прямой аналог парадокса Карри в системе типов |
| Парадокс Монтегю | Самоссылка + предикат знания | Показывает, что предикат «x знает, что» приводит к аналогичным проблемам |
| Парадокс Йябло | Бесконечная цепочка ссылок без явной самоссылки | Попытка избавиться от самоссылки, но структура рассуждения родственна |
Философские следствия
Парадокс Карри ставит перед нами неудобный вопрос: насколько мы можем доверять формальной логике? Мы привыкли думать, что если каждый шаг рассуждения корректен, то и вывод корректен. Парадокс Карри показывает: это верно только в том случае, если сама система правил изначально «здорова». А проверить здоровье системы изнутри этой же системы — невозможно (привет, Гёдель).
Есть и более радикальная интерпретация. Некоторые философы — в частности, Грэм Прист — утверждают, что парадокс Карри (вместе с другими логическими парадоксами) свидетельствует о том, что реальность не обязана подчиняться классической логике. Возможно, мир допускает истинные противоречия. Возможно, наша привычная бинарная картина «истинно/ложно» — это упрощение, которое работает в повседневной жизни, но ломается на границах.
А может быть, урок парадокса Карри проще и практичнее: будьте осторожны с самоссылками. Каждый раз, когда система — логическая, юридическая, компьютерная или бюрократическая — позволяет объекту ссылаться на самого себя без ограничений, возникает риск коллапса. Не случайно эволюция формальных систем на протяжении XX века — это во многом история все более изощренных способов контролировать самоссылку, не отказываясь от нее полностью.