Наименование: | Интуиционистская логика. |
Определение: | Интуиционистская логика — это раздел современной математической логики, имеющий своей логико-философской предпосылкой программу интуиционизма, которая рассматривает математику как совокупность «интуитивно убедительных» умственных построений. |
Раздел: | Концепты философского дискурса Концепты научного дискурса |
Дискурс: | Философия Наука |
Субдискурс: | Логика Логика математическая Конструктивизм математический |
Связанные концепты: | Программа интуиционизма Логика конструктивная |
Текст статьи: © Η. Η. Непейвода. Подготовка электронной публикации и общая редакция: © Центр гуманитарных технологий. Ответственный редактор: А. В. Агеев. Информация на этой странице периодически обновляется. Последняя редакция: 29.07.2025. | |
Интуиционистская логика — это раздел современной математической логики (см. Логика математическая), имеющий своей логико-философской предпосылкой программу интуиционизма (см. Интуиционизм), которая рассматривает математику как совокупность «интуитивно убедительных» умственных построений (см. Конструктивизм математический). Интуиционистская логика отражает взгляд интуиционизма на характер логических законов, считающихся с его точки зрения допустимыми в применении к доказательствам суждений из тех частей дедуктивных наук (особенно математики), которые существенно связаны с понятием математической бесконечности. Интуиционистская логика первоначально возникла как логика интуиционистской математики, получившая впоследствии более широкое применение. Неформально развивалась Язык интуиционистской логики в целом совпадает с языком классической логики (см. Логика). В соответствии с концепцией интуиционизма, в интуиционистской логике нет закона исключённого третьего (см. Закон исключённого третьего) и закона снятия двойного отрицания. Правила естественного вывода сохраняются для всех связок, кроме отрицания. Для отрицания правило снятия двойного отрицания ослабляется до правила «Из лжи следует всё, что угодно». В результате ослабляются возможности косвенного вывода — косвенно можно опровергать (по правилу reductio ad absurdum), но, вообще говоря, нельзя доказывать положительные суждения от противного. В интуиционистской логике все связки независимы. Более того, для доказательства утверждения A достаточно пользоваться лишь формулами, не содержащими связок, отсутствующих в A. В интуиционистской логике нет стандартных (нормальных) форм, аналогичных классическим. Как правило, преобразования, связанные с законами формулировки отрицаний и приведения к предварённой форме, действуют лишь в одну сторону. Так, например, верно A ∨ ¬ Β ⇒ ¬ (Α & Β), а ¬ ( Интуиционистская логика обладает рядом уникальных свойств в классе неклассических логик. Для неё выполнены теорема Крейга об интерполяции: «Если выводимо A ⇒ C, то можно построить формулу B, содержащую лишь термины, входящие и в A, и в C, такую, что выводимы A ⇒ B, B ⇒ C» и теорема Бета об определимости: «Если в сигнатуре σ выделена подсигнатура σ0, и термин Τ не принадлежит σ0, но сохраняет одно и то же значение для всех моделей теории Th, в которых совпадают значения терминов из σ0, то Τ определим через σ0 в теории Th». Эти две теоремы сохраняются лишь для малого числа неклассических логик. Более распространённым свойством является нормализуемость выводов, позволяющая в принципе устранить леммы из доказательств. Оно также выполнено для интуиционистской логики. Выполнено для неё и свойство корректности относительно ∨ и ∃: если доказано Интуиционистская логика не может быть описана никакой конечной системой логических значений, и, более того, для неё неестественно описание с помощью таблиц истинности (хотя счётно-значные таблицы истинности для неё существуют). Но она имеет несколько математических интерпретаций. Исторически первой была интерпретация А. Тарского. В ней значениями истинности для предикатов являются открытые подмножества топологического пространства. Значения &, ∨, ∃ определяются булевым образом. Значение ¬ A есть внутренность дополнения значения A. Это вызвано тем, что дополнение открытого множества часто не является открытым. Аналогично определяются значения A ⇒ B и ∀xA (x). Например, несправедливость A ∨ ¬ A можно продемонстрировать следующим образом: объединение открытого единичного круга и внутренности его дополнения даёт не всю плоскость, а плоскость без единичной окружности. Следующей интерпретацией была алгебраическая модель — алгебры Линденбаума — Тарского для интуиционистских теорий. Их называют псевдобулевыми алгебрами. Эти алгебры впервые были созданы для данной цели, но оказались распространённой и широко применимой структурой. Параллельно с этим развивалась линия, ведущая начало от брауэровского содержательного смысла интуиционистской логики. Формулы истолковывались как задачи, логические связки — как преобразования задач, аксиомы — как задачи, для которых решения считаются известными, а правила вывода — как преобразования решений задач. Данные идеи систематизировал В данном определении остаётся не уточнённым понятие эффективного функционала. Оно может уточняться Ещё одна семантика интуиционистской логики берёт начало от Э. Бет и развита С. Крипке. Это — один из видов моделей Крипке. Множество миров — частично-упорядоченное множество (достаточно рассматривать дерево), истинность элементарных формул сохраняется при подъёме, универсумы не уменьшаются при подъёме, значения &, ∨, ∃ определяются локально, w ⊧ Уникальным для неклассических логик является наличие у интуиционистской логики двух разнородных и несводимых друг к другу классов семантик: реализуемостей и моделей Крипке. Аналогия между доказательствами в интуиционистской логике и построениями усилена Изоморфизм между выводами и Н. А. Шанин рассмотрел алгоритм конструктивной расшифровки, разбивающий формулу на задачу и обоснование решения, причём вторая часть могла доказываться классически. Его решение имеет место для рекурсивной реализуемости в теории, пополненной принципом Маркова: ∀x(A (x) ∨ ¬ A (x)) & ¬ ¬ ∃xA (x) ⇒ ∃xA(x). Содержательный смысл данного принципа раскрывается изречением «Ищите и обрящете»: если известны критерии проверки правильности решения и доказано его существование, то его может найти машина полным перебором. Интуиционистскую логику пытались варьировать многими способами. Первой вариацией была минимальная логика Иогансона, получающаяся отбрасыванием ех falso sequitur quodlibet. Как оказалось, в прикладных теориях интуиционистское отрицание тем не менее моделируется (например, в любой теории, содержащей натуральные числа, как A ⇒ | |
Библиография | |
---|---|
| |