Энциклопедия эпистемологии и философии науки

ИНТУИЦИОНИСТСКАЯ ЛОГИКА

ИНТУИЦИОНИСТСКАЯ ЛОГИКА— первоначально появилась как логика интуиционистской математики, но затем область ее применения чрезвычайно расширилась. Неформально И.л. начал развивать Л. Брауэр в 1907; первую интерпретацию, независимую от интуиционистской математики, дал А.Н. Колмогоров; первую формализацию построил А. Гейтинг.

Язык И. л. совпадает с языком классической логики. Правила естественного вывода для всех связок, кромеотрицания,также можно оставить неизменными. Для отрицания правило снятия двойного отрицания ослабляется до правила «Из лжи следует все что угодно».

В И. л. все связки независимы. В ней нет стандартных форм, аналогичных классическим. Как правило, преобразования, связанные с законами формулировки отрицаний и приведения к предваренной форме, действуют лишь в одну сторону. Так, напр., верно-AW-B-,A8LB),а-А & В)=&GT; -Av -£ выполнено не всегда.

Слабыйзакон исключенного третьего «Аи его отрицание не могут быть одновременно ложны» сохраняется и в И.л. в форме —1—I (АV—А),отвергается как логический закон лишь(Av-А).Поэтому неправильно трактовать И. л. как вводящую дополнительные истинностные значения; она, скорее, отвергает саму концепцию логических значений. И. л. не может быть описана конечной системой логических значений.

Для И. л. выполнено свойство корректности относительно V и 3: если доказаноАVВ,то доказано либоА,либоВ;если доказаноЗхА(х),то для некоторого t доказано A(t). Данным свойством классическая логика не обладает. Классическая логика вкладывается в интуиционистскую. Первым такое погружение построил Гливенко.

И. л. имеет несколько математических интерпретаций.Исторически первой была интерпретация А. Тарского. В ней значениями истинности для предикатов являются открытые подмножества топологического пространства. Значения & v3 определяются булевым образом. Значение—Аесть внутренность дополнения значения А. Напр., несправедливостьАV—Аможно продемонстрировать следующим образом: объединение открытого единичного круга и внутренности его дополнения дает плоскость без единичной окружности. Следующей интерпретацией стала алгебраическая. Еще одна семантика И.л. берет начало от Бета и развита Крипке. Это — один из видов моделей Крипке (см.Семантика возможных миров).

Параллельно с этим развивалась линия, ведущая начало от содержательного смысла И. л. согласно Брауэру. Формулы истолковывались как задачи, логические связки — как преобразования задач, аксиомы — как задачи, для которых решения считаются известными; правила вывода — как преобразования решений задач. Данные идеи систематизировал А.Н. Колмогоров. Каждой формуле А сопоставляется множество еереализаций '.Каждая реализация считается решением задачи, соответствующей А.

Реализации элементарных формул задаются по определению. ®(А&В) -®Ах©В. ®(АVВ)= ®АФ®В. ®-пА=&LT;=&GT;®А=0. ®ЗхА(х)=Ф_аеи®А(а). РеализациямиА=&GT;Вявляются эффективные функционалы из ©А в ®В. Реализациями являются эффективные функционалы, перерабатывающие каждое aeU в реализацию А(а). Уникальным свойством И. л. является наличие двух разнородных и несводимых друг к другу классов семантик: реализуемостей и моделей Крипке.

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

Обобщения идеи Колмогорова на другие классы построений с ограниченными ресурсами показали, что идея конструктивности не является исключительной принадлежностью И. л. Другим классам построений соответствуют другиеконструктивные логики,чаще всего противоречащие как классической логике, так и И. л. Напр., в линейных логиках не принимается закон А = &GT; А & А, в нильпотентных А = &GT; А влечет -А, и т. д. Поскольку разные классы построений противоречат друг другу уже на логическом уровне, то совместное их использование приводит к грубым концептуальным противоречиям и, соответственно, к нежелательным практическим эффектам. Поэтому система конструктивных логик стала основой для системы стилей программирования, а И. л. занимает в ней место логики структурного программирования.

Аналогия между доказательствами в И. л. и построениями усилена в [1]. Замкнутые типизированные выражения в комбинаторной логике изоморфны выводам в гильбертовской формулировке импликативного фрагмента И. л. Замкнутые типизированные А. -термы изоморфны выводам в импликативном фрагменте естественного вывода. Изоморфизм между выводами и Х -термами пытались расширить на всю И. л. Но на его пути стоит препятствие, указанное еще Брауэром и явно выделенное НА. Шаниным. Выводы в И. л. соединяют построения и их обоснования. В частности, построения, проделанные при выводе -iA, нельзя вычислять, поскольку они приведут к ошибке. Такие объекты, которые нельзя или не нужно вычислять в программе, но нужно рассматривать для ее обоснования, Г. С. Цейтин назвалпризраками.НА. Шанин рассмотрел алгоритм конструктивной расшифровки, разбивающий формулу на задачу и обоснование решения, причем вторая часть может в рамках конструктивного направления в математике доказываться классически. Дан алгоритм классификации объектов вывода в И. л., отделяющий построения и призраки.

И. л. варьировали многими способами. В минимальной логике Иогансона отбрасывается ex falso quodlibet. Как оказалось, в прикладных теориях интуиционистское отрицание моделируется (напр., в теории натуральных чисел как А = &GT; 0=1). Г р и с предложил симметрическую И. л., в которой истина и ложь равноправны. В симметрической И. л. сохраняются обычные правила формулировки отрицаний классической логики. Отрицание в ней обычно обозначается =&GT;А, интерпретируется как задача построения контрпримера к А и называется сильным отрицанием или конструктивным опровержением. Симметрическая И. л. детально исследована в монографии И.Д. Заславского.

Н.Н. Непейвода

Лит.:Шанин Н.А.О конструктивном понимании математических суждений // Тр. матем. ин-та им. В. А. Стеклова. Т. 52;Непейвода Н.Н.О построении правильных программ // Вопросы кибернетики. Т. 46. 1978;Непейвода Н.Н., Скопин Н.Н.Основания программирования. Ижевск—Москва, 2003;Brouwer L.E.J.Over de grondslagen der wiskunde [Об основаниях знания]. Amsterdam — Leipzig, 1907;Brouwer L.E.J.De onbetrouwbaarheid der logische principes [О недостоверности логических принципов] // Tijdskrift. Wijsbegeerte. Vol. 2. 1908;HeytingA.Die formalen Regeln der intuitionistischen Logik // Sitz. Berlin, 1930;Колмогоров А.Н.Zur Deutung der intuition-istischen Logik // Math. Zeitschrift. Vol. 35. 1932;Tarski A.Der Aussagenkalkul und die Topologie // Fundamenta Mathematicae. Vol. 31. 193;Curry H.B.Combinatory Logic. Vol. 2. New York, 1968.

интуиционистская логика—форма логики предикатов См. Логика предикатов отражающая взгляд Интуиционизма на характер логических законов считающихся с его точки зрения допустимыми в применении к док...Большая Советская энциклопедия II
интуиционистская логика—ИНТУИЦИОНИСТСКАЯ ЛОГИКА логика удовлетворяющая интуиционистским требованиям к математическим рассуждениям....Большой энциклопедический словарь III
интуиционистская логика—ИНТУИЦИОНИСТСКАЯ логика логика удовлетворяющая интуиционистским требованиям к математическим рассуждениям....Большой Энциклопедический словарь V
интуиционистская логика—совокупность приемлемых с точки зрения интуиционизмаi методов доказательства утверждений. В более узком смысле под И. л. понимается интуиционистское исчисление предикатов...Математическая энциклопедия
интуиционистская логика—нтуцыйная логка...Русско-белорусский математический словарь
интуиционистская логика—нтуцонстська логка...Русско-украинский политехнический словарь
интуиционистская логика—одна из наиболее важных ветвей логики неклассической имеющая своей философской предпосылкой программу интуиционизма. Выдвигая на первый план математическую интуицию интуи...Словарь логики
интуиционистская логика—ИНТУИЦИОНИСТСКАЯ ЛОГИКА одна из наиболее важных ветвей логики неклассическойi iимеющая своей философской предпосылкой программу интуиционизмаi. iВыдвигая на первый план ...Словарь по логике
интуиционистская логика—форма логики предикатов или логики высказываний включающая лишь такие логические законы крые приемлемы с т. зр. концепции интуиционизма. Системы И. л. построенные голл. у...Советский философский словарь
интуиционистская логика—ИНТУИЦИОНИСТСКАЯ ЛОГИКА логика удовлетворяющая интуиционистским требованиям к математическим рассуждениям....Современный энциклопедический словарь
интуиционистская логика—ИНТУИЦИОНИСТСКАЯ ЛОГИКА одна из наиболее важных ветвей неклассической логики имеющая своей филос. предпосылкой программу интуиционизма. Выдвигая на первый план математич...Философская энциклопедия
интуиционистская логика—форма логики предикатов отражающая взгляд интуиционизма на характер логич. законов считающихся с его т. зр. допустимыми в применении к доказательствам суждений из тех час...Философская Энциклопедия (в 5 томах)
интуиционистская логика—ИНТУИЦИОНИСТСКАЯ ЛОГИКА логика удовлетворяющая интуиционистским требованиям к математическим рассуждениям....Энциклопедический словарь естествознания