Интуиционистская логика: конструктивное доказательство и отличие от классической

Интуиционистская логика — система правил вывода, ориентированная на конструктивное понимание доказательства: чтобы принять утверждение вида «А или Б», нужно предъявить доказательство хотя бы одной из альтернатив, а не только сослаться на то, что третьей возможности нет. Она возникла в связи с математическим интуиционизмом и впоследствии стала самостоятельным объектом формальной логики. Слово «интуиционистская» не означает, что вывод принимают по догадке или по внутреннему чувству.

Проблема: достаточно ли исключить все возражения?

В классической логике общезначима схема А ∨ ¬А — закон исключённого третьего: любое высказывание либо истинно, либо ложно. В интуиционистской логике эта схема не является универсально доказуемой. Здесь важно уточнение: речь не об утверждении, будто существует «третья истинность», а о требовании к доказательству дизъюнкции. Если у нас нет конструкции, подтверждающей А, и нет конструкции, подтверждающей ¬А, то вывод «А или не-А» не считается обоснованным именно этим способом.

Рассмотрим задачу о бесконечном множестве. Высказано утверждение А: «существует число с определённым труднодоказуемым свойством». Классическое рассуждение может использовать схему А ∨ ¬А, даже когда задача ещё не решена. Конструктивный подход просит показать либо конкретный объект с нужным свойством, либо доказательство невозможности такого объекта. Само отсутствие найденного примера не доказывает отрицания; это разные логические состояния исследования.

От философии Брауэра к формальным правилам

Л. Э. Я. Брауэр связывал основания математики с конструктивной деятельностью и сомневался в безусловном переносе классических принципов на бесконечные области. Аренд Гейтинг систематизировал соответствующие логические правила; впоследствии они получили точные формальные исчисления и семантические интерпретации. Поэтому историю интуиционистской логики нельзя свести к личному мнению одного философа или к неформальной «интуиции»: это дисциплина с ясными правилами доказательства.

Типовое объяснение её связок называют интерпретацией доказательств Брауэра — Гейтинга — Колмогорова. Для утверждения А ∧ Б требуются доказательства обеих частей. Для А → Б — способ преобразовать доказательство А в доказательство Б. Для утверждения «существует x со свойством P» нужен свидетель x и доказательство P(x). Эти требования помогают понять философский смысл формул, хотя сами по себе не заменяют формального исчисления.

Две позиции и реальное расхождение

Классический взгляд

Классическая логика рассматривает закон исключённого третьего и устранение двойного отрицания как общезначимые схемы: из ¬¬А можно заключить А. Такие правила позволяют доказательства от противного, в которых невозможность отрицания используется для установления исходного тезиса. Они чрезвычайно продуктивны в классической математике.

Интуиционистский взгляд

В конструктивном прочтении из ¬¬А вообще говоря нельзя получить доказательство А: невозможно отвергнуть все возможные доказательства А — не то же самое, что построить доказательство А. При этом интуиционистская логика не отрицает закон непротиворечия и принимает многие привычные правила, включая вывод Б из А и «если А, то Б». Доказав А, можно доказать ¬¬А; обратный шаг в общем виде не допускается.

Это различие асимметрично. Любое интуиционистское доказательство в стандартном языке можно считать корректным и классически, однако не всякое классическое доказательство удовлетворяет конструктивным требованиям. Неверно говорить, что две логики одинаковы, либо что одна из них разрешает противоречие как норму.

Различают также доказуемость формулы в исчислении и истинность формулы в выбранной семантике. Фраза «исключённое третье неверно» звучит неточно: корректнее говорить, что схема не выводится как общая теорема данной логики. Для отдельных А дизъюнкция А ∨ ¬А вполне может иметь конструктивное доказательство. Формальная система тем самым фиксирует не чью-то неопределённость, а устойчивое ограничение допустимых выводов.

Значимость этой оговорки видна в работе с существованием: доказательство невозможности несуществования объекта может быть классически достаточным, но конструктивист спросит, указан ли свидетель. Разница касается не отрицания реальности объекта, а того, какие основания позволяют утверждать его существование. Поэтому не стоит представлять интуиционизм как произвольное отрицание классической математики: в определённых областях результаты и методы сосуществуют, хотя их требования к доказательствам отличаются.

Разбор конкретного вывода

Пусть А означает: «для задачи найдено решение». Исследователь доказал, что предположение «никакого решения быть не может» ведёт к противоречию. Это даёт ¬¬А. Классическая логика позволяет заключить А. Интуиционистская требует дополнительного шага: способа построить решение либо иного доказательства А, приемлемого по её правилам. Важно, что спор касается перехода в доказательстве, а не психологической уверенности исследователя.

Если же математик уже предъявил решение и проверил его, разногласия в данном примере нет: А доказано, а значит доказана и формула А ∨ ¬А. Для конкретных разрешимых задач закон исключённого третьего не создаёт проблемы; его общая схема не признаётся безусловной.

Возражение: такая логика слишком строга?

Возражение состоит в том, что требование конструктивного свидетельства может делать доказательство сложнее и запрещать привычные короткие рассуждения. Это верное наблюдение о некоторых классических методах, но из него не следует бесполезность подхода. Его достоинство — явное указание, что именно должно быть построено. Связь доказательства с вычислением используется, в частности, при обсуждении конструктивной математики и формальных систем, однако интуиционистскую логику не следует отождествлять со всяким программированием.

Итог. Интуиционистская логика меняет стандарты доказуемости отдельных схем, прежде всего исключённого третьего и устранения двойного отрицания, сохраняя строгий логический вывод. Её смысл раскрывается через вопрос «какое доказательство можно предъявить?», а не через бытовое противопоставление разума и интуиции.

Проверенные источники

• Stanford Encyclopedia of Philosophy — Intuitionistic Logic (разделы о законе исключённого третьего и доказательствах).
• Internet Encyclopedia of Philosophy — Intuitionism in Mathematics (исторический и логический контекст).
• М. М. Новосёлов, «К истории дискуссий об интуиционистской логике», ИФ РАН.