Аналитические таблицы для пропозициональной модальной логики

Доехав до речки Рубикон, Юлий долго юлил (51—50 до Р. X.) перед нею, наконец сказал: «Жребий брошен» — и полез в воду.

Всеобщая история, обработанная «Сатириконом» (1910)

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

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

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

1) с одной стороны, каждая аналитическая таблица, входящая

в структуру аналитических таблиц, будет древесно упорядочиваться посредством правил редукции для пропозициональных переменных: [t&], [f&], [tv], [/v], [t->], [t—.], [f->] (см. ниже);

2) с другой стороны, многообразие аналитических таблиц, которое возникает при проверке на общезначимость некоторой модальной формулы, также будет древесно упорядочиваться посредством правил редукции для модальных связок ? и 0: [??], [/fa], [tO], [f0.

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

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

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

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

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

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

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

Пропозициональные правила редукции — это приведённые ниже слова:

2. Правила редукции для модальных связок

Придумать зеленое солнце легко; трудно создать мир, в котором оно было бы естественным...

Дж. Р. Р. Толкиен. Из письма.

Правила редукции для модальных связок ? и 0 формулируются следующим образом [3, с. 323—324].

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

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

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

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

Поэтому в таблицу v помещаем отмеченную формулу tA. Итак:

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

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

Замечание (для знатоков нормальных модальных систем).

В нормальных модальных системах Т, В, S4, S5 отношение достижимости рефлексивно, т. е. каждая таблица достижима сама из себя, а потому по отношению к любой таблице w всегда имеется таблица, которая уже заранее построена (такой таблицей является w).

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

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

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

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

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

/(?А) в цепи таблицы w->v | fA в новой таблице v.

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

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

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

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

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

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

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

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

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

f(0A) в цепи таблицы w

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

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

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

  • 1) Локальными правилами называются правила [/и] и [tO], т. е. правила, которые обязательно требуют конструирования новых таблиц.
  • 2) Глобальными правилами называются правила [??] и f>], т. е. правила, по которым работают с уже построенными таблицами и которые можно применять повторно по мере появления новых достижимых таблиц.

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

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

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

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

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

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

  • 1. Аналитической таблицей назовём:
    • а) аналитическую таблицу, которая начинается с отмеченной формулы (при обосновании общезначимости формулы Л);
    • б) аналитическую таблицу, начинающуюся с отмеченных формул

tA}, tA2, tAn,fB (при обосновании следования А12, ...,Ап=В).

2. Система аналитических таблиц — это множество аналитических таблиц, древесно упорядоченное с помощью отношения достижимости.

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

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

  • а) в ее составе встречаются две отмеченные формулы вида С и —? С;
  • б) в ветви среди таблиц, достижимых из данной цепи таблицы w, найдётся хотя бы одна замкнутая таблица.

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

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

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

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

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