Логика интуиционистская

Интуиционистская логика — это раздел современной математической логики (см. Логика математическая), имеющий своей логико-философской предпосылкой программу интуиционизма (см. Интуиционизм), которая рассматривает математику как совокупность «интуитивно убедительных» умственных построений (см. Конструктивизм математический). Интуиционистская логика отражает взгляд интуиционизма на характер логических законов, считающихся с его точки зрения допустимыми в применении к доказательствам суждений из тех частей дедуктивных наук (особенно математики), которые существенно связаны с понятием математической бесконечности. Интуиционистская логика первоначально возникла как логика интуиционистской математики, получившая впоследствии более широкое применение. Неформально развивалась Л. Э. Я. Брауэром с 1907 года. Первые формальные логические системы построены В. Гливенко и А. Гейтингом в 1930 году.

Язык интуиционистской логики в целом совпадает с языком классической логики (см. Логика). В соответствии с концепцией интуиционизма, в интуиционистской логике нет закона исключённого третьего (см. Закон исключённого третьего) и закона снятия двойного отрицания. Правила естественного вывода сохраняются для всех связок, кроме отрицания. Для отрицания правило снятия двойного отрицания ослабляется до правила «Из лжи следует всё, что угодно». В результате ослабляются возможности косвенного вывода — косвенно можно опровергать (по правилу reductio ad absurdum), но, вообще говоря, нельзя доказывать положительные суждения от противного.

В интуиционистской логике все связки независимы. Более того, для доказательства утверждения A достаточно пользоваться лишь формулами, не содержащими связок, отсутствующих в A. В интуиционистской логике нет стандартных (нормальных) форм, аналогичных классическим. Как правило, преобразования, связанные с законами формулировки отрицаний и приведения к предварённой форме, действуют лишь в одну сторону. Так, например, верно A ∨ ¬ Β ⇒ ¬ (Α & Β), а ¬ (A & B) ⇒ ¬ Α ∨ ¬ Β выполнено не всегда. Сильный закон исключённого третьего (tertium non datur) отвергается, но его слабая форма «A и его отрицание не могут быть одновременно ложны» ¬ (Α ∨ ¬ Α), сохраняется. Поэтому неправильно трактовать интуиционистскую логику как вводящую дополнительные истинностные значения, она скорее отвергает саму концепцию логических значений.

Интуиционистская логика обладает рядом уникальных свойств в классе неклассических логик. Для неё выполнены теорема Крейга об интерполяции: «Если выводимо A ⇒ C, то можно построить формулу B, содержащую лишь термины, входящие и в A, и в C, такую, что выводимы A ⇒ B, B ⇒ C» и теорема Бета об определимости: «Если в сигнатуре σ выделена подсигнатура σ₀, и термин Τ не принадлежит σ₀, но сохраняет одно и то же значение для всех моделей теории Th, в которых совпадают значения терминов из σ₀, то Τ определим через σ₀ в теории Th».

Эти две теоремы сохраняются лишь для малого числа неклассических логик. Более распространённым свойством является нормализуемость выводов, позволяющая в принципе устранить леммы из доказательств. Оно также выполнено для интуиционистской логики. Выполнено для неё и свойство корректности относительно ∨ и ∃: если доказано A ∨ B, то доказано либо A, либо B; если доказано ∃xA (x), то для некоторого t доказано A(t). Данным свойством классическая логика не обладает. Интуиционистская логика — единственная логика среди континуума логик с тем же языком, что и классическая, для которой выполнены все эти свойства. Таким образом, она может служить основой для содержательных математических теорий, поскольку в ней интуитивная определимость совпадает с формальной. Хотя множества теорем и доказательств интуиционистской логики по объёму уже соответствующих множеств классической, последняя вкладывается в интуиционистскую. Первым такое погружение осуществил Гливенко. Таким образом, выразительные возможности интуиционистской логики сильнее классической. В свою очередь, К. Гёдель показал, что интуиционистская логика вкладывается в модальную логику S4. При этом погружении связки &, ∨, ∃ остаются без изменения, а на элементарные формулы и на результаты применения остальных связок «навешивается» модальность (см. Модальность).

Интуиционистская логика не может быть описана никакой конечной системой логических значений, и, более того, для неё неестественно описание с помощью таблиц истинности (хотя счётно-значные таблицы истинности для неё существуют). Но она имеет несколько математических интерпретаций. Исторически первой была интерпретация А. Тарского. В ней значениями истинности для предикатов являются открытые подмножества топологического пространства. Значения &, ∨, ∃ определяются булевым образом. Значение ¬A есть внутренность дополнения значения A. Это вызвано тем, что дополнение открытого множества часто не является открытым. Аналогично определяются значения A ⇒ B и ∀xA (x). Например, несправедливость A ∨ ¬ A можно продемонстрировать следующим образом: объединение открытого единичного круга и внутренности его дополнения даёт не всю плоскость, а плоскость без единичной окружности.

Следующей интерпретацией была алгебраическая модель — алгебры Линденбаума — Тарского для интуиционистских теорий. Их называют псевдобулевыми алгебрами. Эти алгебры впервые были созданы для данной цели, но оказались распространённой и широко применимой структурой.

Параллельно с этим развивалась линия, ведущая начало от брауэровского содержательного смысла интуиционистской логики. Формулы истолковывались как задачи, логические связки — как преобразования задач, аксиомы — как задачи, для которых решения считаются известными, а правила вывода — как преобразования решений задач. Данные идеи систематизировал А. Н. Колмогоров. Каждой формуле A сопоставляется множество её реализаций (r). Каждая реализация считается решением задачи, соответствующей A. Реализации элементарных формул задаются по определению. (r) (A & B) = (r) A × (r) B, где (r) (A & B) это пара реализаций 〈(r) А (r) В 〉 (r) (A ∨ B) = (r) A ⊕ (r) B, где (r) (A ∨ B) — реализация A или B с указанием, какая из подзадач решена; (r) ¬ A = ¬ 0 ⇔ (r) A = ∅, где (r) ¬ A — это стандартный элемент, например 0, при условии, что задача A неразрешима; (r) ∃xA (x) = ⊕ α ∈ U (r) A (α), где (r) ∃xA (x) — это пара из значения x₀ и решения A (x₀). Реализациями A ⇒ B являются эффективные функционалы из (r) A в (r) B. Реализациями ∀xA (x) являются эффективные функционалы, перерабатывающие каждое α ∈ U в реализацию Α (α).

В данном определении остаётся не уточнённым понятие эффективного функционала. Оно может уточняться по-разному, в частности, если взять в качестве эффективных функционалов все классические функции, то логика превращается в классическую. С. К. Клини построил первый точный вариант реализуемости, взяв в качестве эффективных операторов алгоритмы и кодируя программы алгоритмов натуральными числами, обходя таким образом сложности с операторами высших типов (клиниевская реализуемость). Он показал, что из доказательства в интуиционистской арифметике извлекается клиниевская реализация доказанной теоремы, и, таким образом, если мы доказали ∃xA (x), то имеется такое n, что доказано A (n). Это точно обосновало тезис Брауэра о том, что интуиционистские доказательства дают, в отличие от классических, построения.

Ещё одна семантика интуиционистской логики берёт начало от Э. Бет и развита С. Крипке. Это — один из видов моделей Крипке. Множество миров — частично-упорядоченное множество (достаточно рассматривать дерево), истинность элементарных формул сохраняется при подъёме, универсумы не уменьшаются при подъёме, значения &, ∨, ∃ определяются локально, w ⊧ A ⊃ B ⇔ ∀v ≥ w (v ⊧ A ⇒ v ⊧ B), w ⊧ ¬ A ⇔ ∀v ≥ w (¬ v ⊧ A), w ⊧ ∀xA (x) ⇔ ∀v ≥ w (∀a ∈ U_v ν ⊧ A (a)), где v и  w — это «переменные по мирам». Данные пункты практически повторяют на семантическом уровне гёделево погружение интуиционистской логики в S4. Модели Крипке изоморфны алгебраическим и топологическим моделям (порядок определяет псевдобулеву алгебру верхних отрезков множества миров и топологию, в которой окрестностями служат верхние отрезки).

Уникальным для неклассических логик является наличие у интуиционистской логики двух разнородных и несводимых друг к другу классов семантик: реализуемостей и моделей Крипке. Аналогия между доказательствами в интуиционистской логике и построениями усилена Н. В. Карри в его «Комбинаторной логике» («Combinatory Logic», 1968). Замкнутые типизированные выражения в комбинаторной логике изоморфны выводам в гилбертовской формулировке импликативного фрагмента интуиционистской логики. Замкнутые типизированные λ-термы изоморфны выводам в импликативном фрагменте естественного вывода.

Изоморфизм между выводами и λ-термами пытались расширить на всю интуиционистскую логику, обобщая λ-исчисление. Но на этом пути стоит препятствие, указанное ещё Брауэром и явно выделенное Н. А. Шаниным. Выводы в интуиционистской логике соединяют построения и их обоснования. В частности, построения, проделанные при выводе ¬A, нельзя вычислять, поскольку они приведут к ошибке. Но подобным же действием могут обладать и другие импликации, в частности, закон транзитивности ∀xyz (A (x, y) & A (y, z) ⇒ A (x, z) Здесь может привести к нежелательным последствиям вычисление y. Такие объекты, которые нельзя или не нужно вычислять в программе, но нужно рассматривать для её обоснования, ввёл Г. С. Цейтин и назвал «призраками».

Н. А. Шанин рассмотрел алгоритм конструктивной расшифровки, разбивающий формулу на задачу и обоснование решения, причём вторая часть могла доказываться классически. Его решение имеет место для рекурсивной реализуемости в теории, пополненной принципом Маркова: ∀x(A (x) ∨ ¬ A (x)) & ¬ ¬ ∃xA (x) ⇒ ∃xA(x). Содержательный смысл данного принципа раскрывается изречением «Ищите и обрящете»: если известны критерии проверки правильности решения и доказано его существование, то его может найти машина полным перебором. Н. Н. Непейвода дал алгоритм классификации объектов внутри произвольного вывода в интуиционистской логике, отделяющий действующие объекты и формулы от бездействующих, порождающих лишь обоснования и призраки.

Интуиционистскую логику пытались варьировать многими способами. Первой вариацией была минимальная логика Иогансона, получающаяся отбрасыванием ех falso sequitur quodlibet. Как оказалось, в прикладных теориях интуиционистское отрицание тем не менее моделируется (например, в любой теории, содержащей натуральные числа, как A ⇒ 0 = 1). Но минимальная логика, как и интерпретация Колмогорова, высветила аномальный статус отрицания в интуиционистской логике. Это — единственная связка, не требующая никакого построения. В связи с этим Грис предложил симметрическую интуиционистскую логику, в которой истина и ложь определяются одновременно и равноправно. В симметрической интуиционистской логике сохраняются обычные правила формулировки отрицаний классической логики, и в её натуральном варианте они даже постулируются в качестве правил вывода. Отрицание в ней обычно обозначается ~A и называется «сильным отрицанием», или «конструктивным опровержением». Оно интерпретируется как задача на построение контрпримера к A. Симметрическая интуиционистская логика детально исследована в монографии И. Д. Заславского. Ю. М. Медведев предложил рассматривать логику финитных задач и заметил, что, если функционалы всюду определены, то формула (¬A ⇒ B ∨ C) ⇒ (¬A ⇒ Β) ∨ (¬Α ⇒ C) реализуема (реализация ¬A стандартна, и её можно подставить в функционал, чтобы выявить единственного кандидата на решение среди B, C). Вслед за этим начали рассматриваться многочисленные суперинтуиционистские логики, получающиеся расширением интуиционистской логики некоторыми схемами аксиом. Почти все они либо влекут закон исключённого третьего в прикладных теориях, либо не удовлетворяют теореме Крейга об интерполяции и теореме Бета. В результате критического переосмысления основных принципов интуиционистской логики возникла конструктивная логика (см. Логика конструктивная). В целом, интуиционистская логика занимает уникальное место в классе неклассических логик, не только как старейшая из них, но и как концептуально целостная система.