137

ИНТУИЦИОНИСТСКАЯ ЛОГИКА Зафиксировав понятие вычислимой последовательности, мы сохраняем свободу при определении операторов высших типов. Первым это показал Клини, построив общерекурсивную реализуемость, при которой выполнена схема Vx(\A(x) => ЗуВ(х,у)) =>ЧхЗу(\А(х*> В(х,у)), выражающая всюду определенность всех функций. Возможность выразить формулами первого порядка те высказывания, для которых в классической логике требуются конструкции высших порядков — еще одно преимущество интуиционизма. Принцип Маркова несовместим с данной схемой во всех содержательных интуиционистских теориях, хотя оба они являются классическими тавтологиями. Э. Бишоп (1960), переопределив вычислимые функционалы, предложил вариант интуиционизма, который характеризуется принципом: «использовать лишь алгоритмы, но явно этого не говорить». Этот вариант, в дальнейшем развитый многими учеными, в том числе П. Мартин-Лёфом, соединил многие преимущества брауэровского и марковского подходов. Сам Брауэр после появления реализуемости по Клини сосредоточился на примерах вычислимости, не подходящих под понятие алгоритма. В частности, он предложил следующие новые типы последовательностей — творческую последовательность а(п) = 0, если в году п не доказана формула А, и 1, если она доказана; и беззаконную последовательность, обладающую следующим свойством: Va (А (а) => 3 n V?(Vm (m < n =* а(т) = ?(m)) =M(?))), т. е. все, что мы о них знаем, мы знаем из уже полученной информации. Трулстра (1974) доказал, что композиции алгоритмов и беззаконных последовательностей образуют интуиционистскую модель, в которой можно промоделировать творческие последовательности. Беззаконные последовательности явились первым примером позитивного использования незнания в точных науках. Возможность сформулировать незнание в виде логической формулы — еще одно достижение интуиционизма. С конца 70-х гг. развиваются идеи приложений интуиционизма к программированию, поскольку интуиционистские доказательства могут рассматриваться как полностью обоснованные программы. Как всегда, попытка лобового применения глубоких идеальных концепций оказалась неудачной. В таких случаях нужно искать обходные пути. Ими могут стать системы, основанные на более жестких принципах, не принимающие абстракции потенциальной осуществимости и дающие построения при ограниченных ресурсах. Таковы линейные логики Ж.-И. Жирара, ультраинтуиционистские системы А. С. Есенина-Вольпина и С. Ю. Сазонова, нильпотентные логики Н. Н. Непейводы и А. П. Белътюкова. Голландская школа, наоборот, рассмотрела приложения интуиционистских понятий к теории множеств, расширяющие понятие эффективной операции, и получила ряд глубоких результатов. В частности, аксиома выбора интуиционистски становится почти безвредной, так что она концептуально противоречит исключенного третьего закону, а не эффективности построений. Интуиционистские теории возникают также при категорной интерпретации логики. Интуиционизм, остро поставив вопросы оснований математики, способствовал развитию других направлений, в частности, формулировке программы Гильберта (см. Формализм). Он выдвинул на первый план понятие построения, что способствовало повороту математики в сторону приложений. Он показал важность идеальных объектов при построениях, что обосновало ущербность плоских прагматических и утилитаристских концепций и возможность рациональной альтернативы традиционному рационализму, что до сих пор как следует не использовано современной философией и системологией. Лит.: ГейтингА. Интуиционизм. М., 1969. Н. Н. Непейвода

ИНТУИЦИОНИСТСКАЯ ЛОГИКА- первоначально логика интуиционистской математики, получившая впоследствии более широкое применение. Неформально развивалась Л. Брауэром с 1907 г., первую интерпретацию, независимую от интуиционистской идеологии, дал А. Н. Колмогоров, первые формализации построили A Гливенко и А. Гейтинг. Язык интуиционистской логики совпадает с языком классической логики. Сохраняются и правила естественного вывода для всех связок, кроме отрицания. Для отрицания правило снятия двойного отрицания ослабляется до правила «Из лжи следует все, что угодно». В результате ослабляются возможности косвенного вывода — косвенно можно опровергать (по правилу reductio ad absurdum), но, вообще говоря, нельзя доказывать положительные суждения от противного. В интуиционистской логике все связки независимы. Более того, для доказательства утверждения А достаточно пользоваться лишь формулами, не содержащими связок, отсутствующих в А. В интуиционистской логике нет стандартных (нормальных) форм, аналогичных классическим. Как правило, преобразования, связанные с законами формулировки отрицаний и приведения к предваренной форме, действуют лишь в одну сторону. Так, напр., верно —[A v ~iB=> i(A&B), a ~~\(А&В) => iAv~\B выполнено не всегда. Сильный исключенного третьего закон (tertium non datur) отвергается, но его слабая форма «А и его отрицание не могут быть одновременно ложны» —|—I (A v "H/0, сохраняется. Поэтому неправильно трактовать интуиционистскую логику как вводящую дополнительные истинностные значения, она скорее отвергает саму концепцию логических значений. Интуиционистская логика обладает радом выдающихся свойств в классе неклассических логик. Для нее выполнены теорема Крейга об интерполяции: «Если выводимо А => С, то можно построить формулу В, содержащую лишь термины, входящие и в А, и в С, такую, что выводимы А => В,В=$ С» и теорема Бета об определимости: «Если в сигнатуре а выделена подсигнатура а0, и термин Т не принадлежит а0, но сохраняет одно и то же значение для всех моделей теории 77*, в которых совпадают значения терминов из о0, то Т определим через а0 в теории Th.» Эти две теоремы сохраняются лишь для малого числа неклассических логик. Более распространенным свойством является нормализуемость выводов, позволяющая в принципе устранить леммы из доказательств. Оно также выполнено для интуиционистской логики. Выполнено для нее и свойство корректности относительно v и 3 : если доказано A v В, то доказано либо А, либо В; если доказано 3 хА(х), то для некоторого t доказано Aft). Данным свойством классическая логика не обладает. Интуиционистская логика — единственная логика среди континуума логик с тем же языком, что и классическая, для которой выполнены все эти свойства. Таким образом, она может служить основой для содержательных математических теорий, поскольку в ней интуитивная определимость совпадает с формальной. Хотя множества теорем и доказательств интуиционистской логики по объему уже соответствующих множеств классичес-

138

ИНТУИЦИОНИСТСКАЯ ЛОГИКА кой, последняя вкладывается в интуиционистскую. Первым такое погружение осуществил Гливенко. Таким образом, выразительные возможности интуиционистской логики сильнее классической. В свою очередь, К. Гёдель показал, что интуиционистская логика вкладывается в модальную логику S4. При этом погружении связки &, V , 3 остаются без изменения, а на элементарные формулы и на результаты применения остальных связок навешивается модальность. Интуиционистская логика не может быть описана никакой конечной системой логических значений, и, более того, для нее неестественно описание с помощью таблиц истинности (хотя счетнозначные таблицы истинности для нее существуют). Но она имеет несколько математических интерпретаций. Исторически первой была интерпретация А. Тарского. В ней значениями истинности для предикатов являются открытые подмножества топологического пространства. Значения &, V , 3 определяются булевым образом. Значение ~i А есть внутренность дополнения значения А. Это вызвано тем, что дополнение открытого множества часто не является открытым. Аналогично определяются значения А => Вк V хА(х). Напр., несправедливость А V —\ А можно продемонстрировать следующим образом: объединение открытого единичного круга и внутренности его дополнения дает не всю плоскость, а плоскость без единичной окружности. Следующей интерпретацией была алгебраическая модель — алгебры Линденбаума-Тарского для интуиционистских теорий. Их называют псевдобулевыми алгебрами. Эти алгебры впервые были созданы для данной цели, но оказались распространенной и широко применимой структурой. Параллельно с этим развивалась линия, ведущая начало от бра- уэровского содержательного смысла интуиционистской логики. Формулы истолковывались как задачи, логические связки — как преобразования задач, аксиомы — как задачи, для которых решения считаются известными, а правила вывода — как преобразования решений задач. Данные идеи систематизировал А. Н. Колмогоров. Каждой формуле А сопоставляется множество ее реализаций ®. Каждая реализация считается решением задачи, соответствующей А. Реализации элементарных формул задаются по определению. ®(А&В) = ®А х ®В, где ®{А&В) это пара реализаций <®А®В> ®(AvB) = ®А® ®В, где ®(Av В) — реализация А или В с указанием, какая из подзадач решена; ® "~1А = 0 <=> ®А = 0, где ® —IA — стандартный элемент, например О, при условии, что задача А неразрешима; ® 3хА(х) =©aGu ®A(a), где ®3хА(х) — это пара из значения х0 и решения А(х0). Реализациями А => В являются эффективные функционалы из ®А в ®В. Реализациями V хА(х) являются эффективные функционалы, перерабатывающие каждое а е U в реализацию ^(а). В данном определении остается не уточненным понятие эффективного функционала. Оно может уточняться по-разному, в частности, если взять в качестве эффективных функционалов все классические функции, то логика превращается в классическую. С. К. Клини построил первый точный вариант реализуемости, взяв в качестве эффективных операторов алгоритмы и кодируя программы алгоритмов натуральными числами, обходя таким образом сложности с операторами высших типов (клнниевская реализуемость). Он показал, что из Доказательства в интуиционистской арифметике извлекается клиниевская реализация доказанной теоремы, и, таким образом, если мы доказали ЗхА(х), то имеется такое п, что доказано А(п). Это точно обосновало тезис Брауэра о том, что интуиционистские доказательства дают, в отличие от классических, построения. Еще одна семантика интуиционистской логики берет начало от Бета и развита Крите. Это — один из видов моделей Крип- ке. Множество миров — частично-упорядоченное множестю (достаточно рассматривать дерево), истинность элементарных формул сохраняется при подъеме, универсумы не уменьшаются при подъеме, значения &, V , 3 определяются локально, w = A Z) Во Vv>w(v = А*> V = В), w = —\А» V v >w(—\v = A),w= V xA(x)oV v> w(V aG Uvv=A(a)),me v и w — это «переменные по мирам». Данные пункты практически повторяют на семантическом уровне гёделево погружение интуиционистской логики в S4. Модели Крипке изоморфны алгебраическим и топологическим моделям (порядок определяет псевдобулеву алгебру верхних отрезков множества миров и топологию, в которой окрестностями служат верхние отрезки). Уникальным для неклассических логик является наличие у интуиционистской логики двух разнородных и несводимых друг к другу классов семантик: реализуемостей и моделей Крипке. Аналогия между доказательствами в интуиционистской логике и построениями усилена X. Б. Карри в его «Комбинаторной логике» (Combinatory Logic, 1968). Замкнутые типизированные выражения в комбинаторной логике изоморфны выводам в гилъбертовской формулировке импликативного фрагмента интуиционистской логики. Замкнутые типизированные Х-термы изоморфны выводам в импликативном фрагменте естественного вывода. Изоморфизм между выводами и X.-термами пытались расширить на всю интуиционистскую логику, обобщая ^-исчисление. Но на этом пути стоит препятствие, указанное еще Брауэром и явно выделенное Н. А. Шаниным. Выводы в интуиционистской логике соединяют построения и их обоснования. В частности, построения, проделанные при выводе i А, нельзя вычислять, поскольку они приведут к ошибке. Но подобным же действием могут обладать и другие импликации, в частности, закон транзитивности V xyz (А(х, у) &A(y,z)=>A(x,z). Здесь может привести к нежелательным последствиям вычисление у. Такие объекты, которые нельзя или не нужно вычислять в программе, но нужно рассматривать для ее обоснования, ввел Г. С. Цейтин и назвал «призраками». Н. А. Шанин рассмотрел алгоритм конструктивной расшифровки, разбивающий формулу на задачу и обоснование решения, причем вторая часть могла доказываться классически. Его решение имеет место для рекурсивной реализуемости в теории, пополненной принципом Маркова: V x(A(x)V -пА(х))&-]-\3 хА(х) => ЗхА(х). Содержательный смысл данного принципа раскрывается изречением «Ищите и обрящете»: если известны критерии проверки правильности решения и доказано его существование, то его может найти машина полным перебором. Н. Н. Непейвода дал алгоритм классификации объектов внутри произвольного вывода в интуиционистской логике, отделяющий действующие объекты и формулы от бездействующих, порождающих лишь обоснования и призраки. Интуиционистскую логику пытались варьировать многими способами. Первой вариацией была минимальная логика Иогансона, получающаяся отбрасыванием ex falso sequitur quodlibet. Как оказалось, в прикладных теориях интуиционистское отрицание тем не менее моделируется (напр., в любой теории, содержащей натуральные числа, какА=> 0=1). Но минимальная логика, как и интерпретация Колмогорова, высветила аномальный статус отрицания в интуиционистской ло-