Аналитические таблицы для интуиционистской логики

Джек вскочил.

  • У нас будут правила,крикнул он вдохновенно.
  • Много всяких правил. А кто их будет нарушать...

У. Голдинг. Повелитель мух

Ранее был рассмотрен метод аналитических таблиц для языка первого порядка. Этот метод позволял в определённых случаях устанавливать общезначимость формул языка первого порядка или наличие логического следования некоторой формулы В из посылок Аь А2,..., Ап.

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

Усложнение метода будет состоять в том, что при проверке общезначимости формул мы будем в общем случае иметь дело не с одной аналитической таблицей, а с некоторым упорядоченным множеством аналитических таблиц, а именно, деревом таблиц (иначе говоря, мы будем иметь дело с дважды упорядоченным деревом).

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

С другой стороны, само многообразие аналитических таблиц, которое возникает при проверке на общезначимость некоторой формулы, также будет древесно упорядочиваться посредством правил редукции для логических связок —> и —i:

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

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

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

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

Рассматривая метод аналитических таблиц, будем полагать, что аналитические таблицы — это синтаксические аналоги некоторых миров.

1. Пропозициональные правила редукции

Отметим, что так как интуиционистские системы строятся на базе пропозициональной логики, то мы без каких либо изменений принимаем все правила редукции, относящиеся к связкам & и V.

Определение (по [3, с. 194]).

Пропозициональными правилами редукции называются приведенные ниже слова:

Правила редукции для логических связок —> и -i формулируются следующим образом [3, с. 354—355].

1. Правило [t—»].

Допустим, что в некоторой цепи таблицы w содержится формула t(A —> В), утверждающая истинность формулы (А —> В) в этой цепи.

Согласно условию истинности импликации в интуиционистской логике (см. «функцию оценки формулы в возможном мире»)

это означает, что в любой таблице v, достижимой из данной цепи таблицы w (эти таблицы уже обязательно должны быть к этому моменту построены), имеет место ложность утверждения Л или истинность утверждения В.

Поэтому в таблицу v можно поместить отмеченные формулы^ и tB, расщепив таблицу на две цепи. Итак:

Замечание (важное).

В силу рефлексивности отношения достижимости в интуиционистской логике, каждая таблица достижима сама из себя, а потому по отношению к любой построенной таблице w всегда существует таблица, которая уже заранее построена (таковой является сама таблица iv).

2. Правило [/—>].

Пусть в некоторой цепи таблицы w содержится формулаДА —»В), утверждающая ложность в этой цепи таблицы w формулы —> В).

Согласно условию ложности импликации в интуиционистской логике (см. «функцию оценки формулы в возможном мире»)

это означает, что существует таблица v, в которой антецедент Л импликации является истинным утверждением, а консеквент В — ложным.

Поэтому необходимо обязательно построить новую таблицу v, с которой начинается новая ветвь аналитических таблиц, объявить ее достижимой из цепи таблицы w, и поместить в нее утверждения об истинности антецедента и ложности консеквента, т. е.

f(A —> В) в цепи таблицы w-> Л

fB в новой таблице v.

3. Правило [t—1].

Предположим, что в некоторой цепи таблицы w содержится формула t(-iA), утверждающая истинность в этой цепи формулы —А.

Согласно условиям истинности отрицания в интуиционистской логике (см. «функцию оценки формулы в возможном мире»)

это означает, что в каждой таблице v, достижимой из данной цепи таблицы w (эта таблица обязательно уже должна быть к этому моменту построена), имеет место ложность утверждения Л.

Поэтому в такую таблицу можно поместить отмеченную формулу/Л:

t(—Л) в цепи таблицы w

fA в каждой таблице v, достижимой из цепи таблицы w.

4. Правило [f-1].

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

Тогда, согласно условию ложности отрицания (см. «функцию оценки формулы в возможном мире»)

это означает, что существует таблица v, достижимая из данной цепи таблицы w, в которой формула Л является истинной.

Поэтому необходимо обязательно построить новую таблицу, с которой начинается новая ветвь аналитических таблиц, которая объявляется достижимой из цепи таблицы w ив нее помещается утверждение об истинности Л, т. е.

Д-Л) в цепи таблицы w-> | Л в новой таблице v.

Другими словами, если установлено, что формула —А в мире w является ложной, то необходимо построить новый мир v и положить, что этот мир достижим из мира w и в новом мире формула Л истинна.

Новые правила редукции подразделяются на локальные и глобальные.

Определение.

1. Локалънъши правилами называются правила [f—>] и [f-1], т. е. те правила, которые в обязательном порядке требуют конструирования новых таблиц.

2. Глобальными правилами называются правила [t—>] и [t-О, т. е. те правила, по которым работают с уже построенными таблицами и которые можно применять повторно по мере появления новых достижимых таблиц.

При применении метода аналитических таблиц рекомендуется вначале всегда применять локальные правила.

Замечание (для знатоков модальной логики).

При применении глобальных правил необходимо помнить, что отношение достижимости обладает различными свойствами в различных логических системах:

  • а) в интуиционистской логике отношение достижимости обладает свойствами рефлексивности и транзитивности;
  • б) в модальной логике отношение достижимости может обладать следующими свойствами:
    • —рефлексивности (система Т);
    • —рефлексивности и симметричности (система Брауэра);
    • —рефлексивности и транзитивности (система S4);
    • рефлексивности, симметричности и транзитивности (система S5).

Определение.

  • 1. Принцип монотонности. Если tp в мире а и 9t(oc, (3), то tp имеет место в мире (3, где р — произвольная пропозициональная переменная.
  • 2. Обобщённый принцип монотонности. Если tA в мире

а и Э(а, (3), то tA имеет место в мире (3, где А — произвольная пропозициональная формула.

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

Определение [3, с. 324].

  • 1. Аналитической таблицей назовём:
    • а) аналитическую таблицу, которая начинается с отмеченной формулы (при обосновании общезначимости формулы Л);
    • б) аналитическую таблицу, начинающуюся с отмеченных формул tAb tA2, ...,tAnfB (при обосновании следования АЬА2, ...,Ап=В').
  • 2. Системой аналитических таблиц называется множество аналитических таблиц, древесно упорядоченное с помощью отношения достижимости Э.

Определение (по [Бочаров, Маркин,2008, с. 325]).

Будем говорить, что цепь аналитической таблицы w является замкнутой, если: а) в ее составе встречаются две отмеченные формулы вида С и -iC;

б) в ветви среди таблиц, достижимых из данной цепи таблицы w, найдётся хотя бы одна замкнутая таблица.

Определение (по [3, с. 325]).

  • 1. Будем говорить, что аналитическая таблица w является замкнутой, если все ее цепи замкнуты.
  • 2. Будем говорить, что система аналитических таблиц является замкнутой, если замкнута аналитическая таблица w0.

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

Аналогично построение замкнутой системы аналитических таблиц, используемой для проверки наличия логического следования формулы В из посылок АЛ, А2, ..., Ап, с учётом специальных свойств достижимости для интуиционистской логики, означает, что наличие данного следования в этой логике имеет место.

Работа с примерами решения некоторых типов упражнений

См. Пример 1, Пример 2.

2. Кванторные правила редукции

Вначале напомним, что замкнутым термом называется терм, не содержащий предметных переменных.

1. Правило [tV].

Пусть в некоторой цепи таблицы w содержится формула t(VxA), утверждающая истинность формулы /хА в этой цепи таблицы w.

Тогда в любой таблице v, достижимой из данной цепи таблицы w (эти таблицы уже обязательно должны быть построены), имеет место истинность утверждения (A)f, являющегося результатом подстановки замкнутого терма t вместо всех свободных вхождений переменной х: tVxA в цепи таблицы w

t(A)* в каждой таблице v, достижимой из цепи таблицы w.

2. Правило [/V].

Пусть в некоторой цепи таблицы w содержится формула/(VxA), утверждающая ложность формулы VxA в этой цепи таблицы w.

Тогда необходимо в обязательном порядке построить новую таблицу v, с которой начинается новая ветвь аналитических таблиц, объявить ее достижимой из цепи таблицы w, и поместить в нее утверждения о ложности (А)?, являющегося результатом подстановки вместо всех свободных вхождений переменной х предметной константы к, не содержащейся в данной цепи таблицы:

3. Правило [?3].

Пусть в некоторой цепи таблицы w содержится формула ?(ЗхА), утверждающая истинность формулы ЗхА в этой цепи.

Тогда в каждой таблице v, достижимой из данной цепи таблицы w (эта таблица обязательно уже должна быть построена), имеет место истинность утверждения (А)?, являющегося результатом подстановки вместо всех свободных вхождений переменной х предметной константы к, не содержащейся в данной цепи таблицы: t3xA в цепи таблицы w

t(A)? в цепи таблицы w-> t(A)? в новой таблице v.

4. Правило [/9].

Пусть в некоторой цепи таблицы w содержится формула/(НхА), утверждающая ложность формулы 3x4 в этой цепи.

Тогда в каждой таблице v, достижимой из данной цепи таблицы w (эта таблица обязательно уже должна быть построена), имеет место истинность утверждения (А)^, являющегося результатом подстановки замкнутого терма t вместо всех свободных вхождений переменной х: f(3xA) в цепи таблицы w

f(A)* в каждой таблице v, достижимой из цепи таблицы w.

Замечание (важное).

Процедура построения аналитической таблицы не является алгоритмической (в частности, процесс выбора термов в правилах для кванторов

носит творческий характер).

Работа с примерами решения некоторых типов упражнений

См. Пример 3, Пример 4.

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >