Интуиционистская логика - Intuitionistic logic

Интуиционистская логика , иногда более широко называемая конструктивной логикой , относится к системам символической логики, которые отличаются от систем, используемых для классической логики , более точным отражением понятия конструктивного доказательства . В частности, системы интуиционистской логики не включают в себя закон исключенного среднего и исключения двойного отрицания , которые являются фундаментальными правилами вывода в классической логике.

Формализованная интуиционистская логика была первоначально разработана Арендом Гейтингом, чтобы обеспечить формальную основу для программы интуиционизма Брауэра . С точки зрения теории доказательств , исчисление Гейтинга является ограничением классической логики, в которой были устранены законы исключенного среднего и двойного отрицания. Исключенное исключение среднего и двойного отрицания все еще может быть доказано для некоторых утверждений на индивидуальной основе, однако, но не универсально, как в случае с классической логикой.

Были изучены несколько систем семантики интуиционистской логики. Одна из этих семантик отражает классическую булевозначную семантику, но использует алгебры Гейтинга вместо булевых алгебр . Другая семантика использует модели Крипке . Это, однако, технические средства для изучения дедуктивной системы Гейтинга, а не формализации исходных неформальных семантических интуиций Брауэра. Семантические системы , называющих захватить такие интуитивные, из - за предлагая значимые понятия «конструктивной истины» (а не просто действительность или доказуемость), являются Гедель «s интерпретация Диалектика , Клини «s реализуемости , логик Юрия Медведева конечных проблем, или Джапаридзе «s логика вычислимости . Однако такая семантика постоянно вызывает логику, более сильную, чем логика Гейтинга. Некоторые авторы утверждали, что это могло быть признаком неадекватности самого исчисления Гейтинга, считая последнее неполным как конструктивную логику.

Математический конструктивизм

В семантике классической логики пропозициональным формулам присваиваются значения истинности из двухэлементного набора («истина» и «ложь» соответственно), независимо от того, есть ли у нас прямые доказательства для любого случая. Это называется «законом исключенного третьего», потому что он исключает возможность любого значения истинности, кроме «истинного» или «ложного». В отличие от пропозициональных формул в интуиционистской логике не присваивается определенное значение истинности и только считается «истинным» , когда у нас есть прямые доказательства, следовательно , доказательство . (Мы также можем сказать, вместо того, чтобы пропозициональная формула была «истинной» благодаря прямым свидетельствам, что она наполнена доказательством в смысле Карри-Ховарда .) Следовательно, операции в интуиционистской логике сохраняют обоснование по отношению к свидетельствам и доказуемости, а не оценка истины.

Интуиционистская логика - широко используемый инструмент при разработке подходов к конструктивизму в математике. Использование конструктивистской логики в целом было спорной темой среди математиков и философов (см., Например, полемику Брауэра – Гильберта ). Распространенным возражением против их использования является процитированное выше отсутствие двух центральных правил классической логики, закона исключенного среднего и исключения двойного отрицания. Они считаются настолько важными для практики математики, что Дэвид Гильберт писал о них: «Принятие принципа исключенного третьего из математика будет таким же, как запрет на использование телескопа астроному или боксеру. его кулаки. Запрещение утверждений о существовании и принципа исключенного третьего равносильно отказу от математической науки ».

Несмотря на серьезные проблемы, связанные с неспособностью использовать ценные правила исключения исключенного среднего и двойного отрицания, интуиционистская логика имеет практическое применение. Одна из причин этого заключается в том, что его ограничения производят доказательства, обладающие свойством существования , что делает его также пригодным для других форм математического конструктивизма . Неформально это означает, что если есть конструктивное доказательство того, что объект существует, это конструктивное доказательство может быть использовано в качестве алгоритма для создания примера этого объекта, принцип, известный как соответствие Карри – Ховарда между доказательствами и алгоритмами. Одна из причин, по которой этот конкретный аспект интуиционистской логики так ценен, заключается в том, что он позволяет практикам использовать широкий спектр компьютеризированных инструментов, известных как помощники по доказательству . Эти инструменты помогают своим пользователям в проверке (и создании ) крупномасштабных доказательств, размер которых обычно исключает обычную человеческую проверку, которая осуществляется при публикации и рецензировании математических доказательств. Таким образом, использование помощников по доказательству (таких как Agda или Coq ) позволяет современным математикам и логикам разрабатывать и доказывать чрезвычайно сложные системы, помимо тех, которые можно создать и проверить исключительно вручную. Одним из примеров доказательства, которое невозможно было удовлетворительно проверить без формальной проверки, является знаменитое доказательство теоремы о четырех цветах . Эта теорема ставила математиков в тупик более чем на сто лет, пока не было разработано доказательство, которое исключало большие классы возможных контрпримеров, но все же оставляло достаточно открытых возможностей, что потребовалась компьютерная программа для завершения доказательства. Это доказательство было спорным в течение некоторого времени, но позже оно было проверено с помощью Coq.

Синтаксис

Rieger-Нисимура решетки . Его узлами являются пропозициональные формулы одной переменной с точностью до интуиционистской логической эквивалентности , упорядоченные интуиционистской логической импликацией.

Синтаксис формул интуиционистской логики аналогична логике высказываний или логики первого порядка . Однако интуиционистские связки не могут быть определены в терминах друг друга так же, как в классической логике , поэтому их выбор имеет значение. В интуиционистской логике высказываний (IPL) принято использовать →, ∧, ∨, ⊥ в качестве основных связок, трактуя ¬ A как сокращение от ( A → ⊥) . В интуиционистской логике первого порядка необходимы оба квантора ∃, ∀.

Слабее классической логики

Интуиционистскую логику можно понимать как ослабление классической логики, означающее, что она более консервативна в том, что позволяет рассуждающему делать выводы, но не допускает никаких новых выводов, которые не могли быть сделаны в рамках классической логики. Каждая теорема интуиционистской логики - это теорема классической логики, но не наоборот. Многие тавтологии в классической логике не являются теоремами в интуиционистской логике - в частности, как было сказано выше, одна из главных целей интуиционистской логики состоит в том, чтобы не утверждать закон исключенного третьего, чтобы свести на нет использование неконструктивного доказательства посредством противоречия , которое может использоваться для предоставления утверждений о существовании без предоставления явных примеров объектов, которые он доказывает. Мы говорим «не подтверждать», потому что, хотя это не обязательно верно, что закон соблюдается в любом контексте, нельзя привести никакого контрпримера: такой контрпример был бы выводом (предполагающим отрицание закона для определенного утверждения), недопустимым согласно классическим правилам. логика и, следовательно, не допускается в строгом ослаблении, как интуиционистская логика. Действительно, двойное отрицание закона сохраняется как тавтология системы: то есть это теорема, которая независимо от предложения .

Последовательное исчисление

Герхард Генцен обнаружил, что простое ограничение его системы LK (его секвенциальное исчисление для классической логики) приводит к системе, которая является надежной и полной по отношению к интуиционистской логике. Он назвал эту систему ЖЖ. В LK разрешается использовать любое количество формул в конце секвенции; в отличие от этого LJ допускает не более одной формулы в этой позиции.

Другие производные от LK ограничиваются интуиционистскими выводами, но все же позволяют делать несколько выводов подряд. LJ '- один из примеров.

Исчисление в стиле Гильберта

Интуиционистскую логику можно определить с помощью следующего исчисления в стиле Гильберта . Это похоже на способ аксиоматизации классической логики высказываний.

В логике высказываний правилом вывода является modus ponens.

  • МП: от и вывести

и аксиомы

  • ТО-1:
  • ТО-2:
  • И-1:
  • И-2:
  • И-3:
  • ИЛИ-1:
  • ИЛИ-2:
  • ИЛИ-3:
  • ЛОЖНЫЙ:

Чтобы сделать это системой логики предикатов первого порядка, правила обобщения

  • -GEN: из логического вывода , если не свободен в
  • -GEN: из логического вывода , если не свободен в

добавляются вместе с аксиомами

  • PRED-1:, если термин свободен для замены переменной в (т. Е. Если ни одна из переменных в не становится связанной )
  • ПРЕД-2:, с тем же ограничением, что и для ПРЕД-1

Необязательные связки

Отрицание

Если кто-то желает включить связку для отрицания, а не рассматривать ее как сокращение , достаточно добавить:

  • НЕ-1 ':
  • НЕ-2 ':

Если кто-то хочет опустить связку (ложь) , существует ряд альтернатив . Например, можно заменить три аксиомы ЛОЖЬ, НЕ-1 'и НЕ-2' двумя аксиомами

  • НЕ-1:
  • НЕ-2:

как в исчислении высказываний § Аксиомы . Альтернативами НЕ-1 являются или .

Эквивалентность

Соединительно эквивалентности может рассматриваться как аббревиатура, с стоять в течение . В качестве альтернативы можно добавить аксиомы

  • МКФ-1:
  • МКФ-2:
  • МКФ-3:

IFF-1 и IFF-2 при желании можно объединить в единую аксиому с помощью конъюнкции.

Отношение к классической логике

Система классической логики получается добавлением любой из следующих аксиом:

  • (Закон исключенной середины. Также можно сформулировать как .)
  • (Устранение двойного отрицания)
  • ( Закон Пирса )
  • (Закон противопоставления)

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

Другое отношение задается отрицательным переводом Гёделя – Генцена , который обеспечивает вложение классической логики первого порядка в интуиционистскую логику: формула первого порядка доказуема в классической логике тогда и только тогда, когда ее перевод Гёделя-Генцена доказуем интуиционистски. Следовательно, интуиционистскую логику вместо этого можно рассматривать как средство расширения классической логики конструктивной семантикой.

В 1932 году Курт Гёдель определил систему логики, промежуточную между классической и интуиционистской логикой; Логики Гёделя одновременно известны как промежуточные логики .

Неопределимость операторов

В классической логике высказываний, можно взять одну из совокупности , дизъюнкции , или косвенно , как примитивные, и определить два других с точки зрения его вместе с отрицанием , например, в Лукасевич «s трех аксиом логики . Можно даже определить все четыре в терминах единственного достаточного оператора, такого как стрелка Пирса (NOR) или штрих Шеффера (NAND). Точно так же в классической логике первого порядка один из кванторов может быть определен в терминах другого и отрицания.

Это фундаментальные следствия закона бивалентности , который делает все такие связки просто булевыми функциями . В интуиционистской логике не требуется соблюдения закона бивалентности, только закона непротиворечия . В результате нельзя обойтись без основных связок, и все вышеперечисленные аксиомы необходимы. Большинство классических тождеств - это только теоремы интуиционистской логики в одном направлении, хотя некоторые - теоремы в обоих направлениях. Вот они:

Конъюнкция против дизъюнкции:

Соединение против импликации:

Дизъюнкция против импликации:

Универсальная и экзистенциальная количественная оценка:

Так, например, «a или b» - более сильная пропозициональная формула, чем «если не a, то b», тогда как они классически взаимозаменяемы. С другой стороны, «не (а или б)» эквивалентно «не а, а также не б».

Если мы включим эквивалентность в список связок, некоторые из связок станут определяемыми из других:

В частности, {∨, ↔, ⊥} и {∨, ↔, ¬} являются полными базами интуиционистских связок.

Как показал Александр В. Кузнецов, любая из следующих связок - первая тернарная, вторая - пятеричная - сама по себе функционально завершена : любой из них может выполнять роль единственного достаточного оператора для интуиционистской логики высказываний, образуя аналог от инсульта Шеффера от классической логики:

Семантика

Семантика несколько сложнее, чем в классическом случае. Теория моделей может быть дана алгебрами Гейтинга или, что то же самое, семантикой Крипке . Недавно Боб Констебл доказал полноту теории модели, подобной Тарскому , но с другим понятием полноты, чем в классическом.

Недоказанным утверждениям в интуиционистской логике не придается промежуточное значение истинности (как иногда ошибочно утверждают). Можно доказать, что такие утверждения не имеют третьей ценности истинности, результат восходит к Гливенко в 1928 году. Вместо этого они сохраняют неизвестную ценность истинности до тех пор, пока они не будут доказаны или опровергнуты. Утверждения опровергаются путем вывода из них противоречия.

Следствием этой точки зрения является то, что интуиционистская логика не имеет интерпретации ни как двузначная логика, ни даже как конечно-значная логика в привычном смысле. Хотя интуиционистская логика сохраняет тривиальные утверждения классической логики, каждое доказательство пропозициональной формулы считается действительной пропозициональной ценностью, таким образом, в соответствии с понятием пропозиций-как-множеств Гейтинга пропозициональные формулы являются (потенциально не конечными) наборами своих доказательств.

Семантика алгебры Гейтинга

В классической логике мы часто обсуждаем значения истинности, которые может принимать формула. Значения обычно выбираются как члены булевой алгебры . Встречается и присоединиться к операции в булевой алгебре идентифицируется с ∧ и ∨ логическими связками, так что значение формулы вида ∧ B является пересечением стоимости A и значения B в булевой алгебре. Тогда у нас есть полезная теорема о том, что формула является действительным предложением классической логики тогда и только тогда, когда ее значение равно 1 для каждой оценки, то есть для любого присвоения значений ее переменным.

Соответствующая теорема верна для интуиционистской логики, но вместо присвоения каждой формуле значения из булевой алгебры используются значения из алгебры Гейтинга , частным случаем которой являются булевы алгебры. Формула действительна в интуиционистской логике тогда и только тогда, когда она получает значение верхнего элемента для любой оценки в любой алгебре Гейтинга.

Можно показать , что признать действительные формулы, достаточно рассмотреть один Гейтингова алгебру, элементы которой являются открытыми подмножествами вещественной прямой R . В этой алгебре мы имеем:

где Int ( X ) является внутренность из X и X его дополнения .

Последнее тождество относительно AB позволяет вычислить значение ¬ A :

С такими присвоениями интуиционистски верные формулы - это как раз те, которым присваивается значение всей строки. Например, формула ¬ ( A ∧ ¬ A ) действительна, потому что независимо от того, какой набор X выбран в качестве значения формулы A , значение ¬ ( A ∧ ¬ A ) может отображаться как целая строка:

Таким образом, оценка этой формулы верна, и формула действительно действительна. Но можно показать, что закон исключенного среднего, A ∨ ¬ A , недействителен, если использовать конкретное значение набора положительных действительных чисел для A :

Интерпретация любых действительных интуиционистский формулы в бесконечной алгебре гейтинговой описана выше , приводит в верхнем элементе, представляющая правда, в качестве оценки формулы, независимо от того, каких значений из алгебры присваивается переменной формула. И наоборот, для каждой недопустимой формулы переменным присваиваются значения, которые дают оценку, отличную от верхнего элемента. Никакая конечная алгебра Гейтинга не обладает вторым из этих двух свойств.

Семантика Крипке

Основываясь на своей работе по семантике модальной логики , Сол Крипке создал другую семантику для интуиционистской логики, известную как семантика Крипке или реляционная семантика.

Семантика типа Тарского

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

Отношение к другой логике

Интуиционистская логика связана двойственностью с паранепротиворечивой логикой, известной как бразильская , антиинтуиционистская или двойная интуиционистская логика .

Подсистема интуиционистской логики с удаленной аксиомой ЛОЖЬ известна как минимальная логика .

Отношение к многозначной логике

Работа Курта Гёделя , связанная с многозначной логикой, показала в 1932 году, что интуиционистская логика не является конечнозначной логикой . (См. Выше раздел Семантика алгебры Гейтинга для бесконечнозначной логической интерпретации интуиционистской логики.)

Отношение к промежуточной логике

Любая конечная алгебра Гейтинга, не эквивалентная булевой алгебре, определяет (семантически) промежуточную логику . С другой стороны, валидность формул в чистой интуиционистской логике не привязана к какой-либо отдельной алгебре Гейтинга, но относится к любой и всем алгебрам Гейтинга одновременно.

Отношение к модальной логике

Любая формула интуиционистской логики высказываний (IPC) может быть переведена в нормальную модальную логику S4 следующим образом:

и было продемонстрировано, что переведенная формула действительна в модальной логике высказываний S4 тогда и только тогда, когда исходная формула действительна в IPC. Приведенный выше набор формул называется переводом Гёделя – МакКинси – Тарского .

Существует также интуиционистская версия модальной логики S4, называемая конструктивной модальной логикой CS4.

Лямбда-исчисление

Существует расширенный изоморфизм Карри – Ховарда между IPC и просто типизированным лямбда-исчислением .

Смотрите также

Примечания

использованная литература

  • Ван Дален, Дирк , 2001, «Интуиционистская логика», в Гобле, Лу, изд., Блэквелл: Руководство по философской логике . Блэквелл
  • Мортен Х. Соренсен, Павел Уржичин, 2006, Лекции по изоморфизму Карри-Ховарда (глава 2: «Интуиционистская логика»). Исследования по логике и основам математики об. 149, Эльзевир
  • В. А. Карнелли (совместно с А. Б. Бруннером). «Антиинтуиционизм и параконсистентность» . Журнал прикладной логики, том 3, выпуск 1, март 2005 г., стр. 161–184
  • Аренд Хейтинг , 1930, «Die formalen Regeln der intuitionistischen Logik», в трех частях, Sitzungsberichte der preussischen Akademie der Wissenschaften : 42–71, 158–169.

внешние ссылки