Страница 86

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). Данным свойством классическая логика не обладает. Интуиционистская логика — единственная логика среди континуума логик с тем же языком, что и классическая, для которой выполнены все эти свойства. Таким образом, она может служить основой для содержательных математических теорий, поскольку в ней интуитивная определимость совпадает с формальной. Хотя множества теорем и доказательств интуиционистской логики по объему уже соответствующих множеств классичес-