Финитная аппроксимируемость как достаточное условие разрешимости по допустимости для транзитивных модальных и суперинтуиционистских логик

Исследование допустимых правил вывода интенсивно ведутся с 50-х годов, в первую очередь для изучения свойств интуиционистской логики H. Основным средством здесь была, как правило, алгебраическая семантика. В 60-х годах в работах М. Фиттига, С. Крипке был предложен другой мощный инструмент логических исследований – модельная семантика Крипке [Крипке 1974]. Это дало новый толчок к исследованию допустимых правил вывода, в частности, это позволило решить В.В. Рыбакову базовую проблему – о разрешимости по допустимости интуиционистских логик [Рыбаков 1984]. Но общего критерия, позволяющего однозначно определять допустимость произвольного правила вывода в заданной логике получено не было. Более того, А. Чагровым был указан пример неразрешимой по допустимости модальной логики [Chagrov A. 1997]. Вместе с тем для всех известных транзитивных модальных и суперинтуиционистских логик, обладающих свойством финитной аппроксимируемости, удавалось построить критерии допустимости правил вывода [Бабены-шев 1992; Максимова 1975; Руцкий 2006; Рыбаков 1984; Рыбаков 1984; Рыбаков 1990; Цит-кин 1974; Rutskiy 2001; Rybakov 1997]. Было естественным предположить, что наличие этих свойств в логике достаточно для ее разрешимости по допустимости.

Ранее автору удалось построить критерий допустимости правил вывода для логики S4. α m . ξ p . ζ q [Руцкий 2006]. Применив технику Рыбакова и специальные конструкции для фреймов Крипке, использованные ранее при исследовании свойств наследования правил вывода, а также обобщив ранний опыт решения проблемы, автору удалось получить исчерпывающий критерий для данного класса логик.

Основные понятия и определения

Основные понятия, определения и теоремы изложены, например, в [Rybakov 1997]. Здесь лишь кратко приведем необходимые для доказательств теоремы и построения. Фреймом Крипке F (или просто фреймом) называется пара 〈 W,R 〉 , где W – непустое множество элементов фрейма F , R – бинарное отношение на W. Если для элементов a , b ∈ W: a R b , то говорят « a достигает b » или « a видит b ». Пусть { p 1 , …, p n } – множество пропозициональных переменных, тогда означиванием V на фрейме F называется отображение, ставящее в соответствие каждой переменной p i подмножество V ( p i ) ⊆ W. Само множество переменных Dom

(V)={ p 1 , …, p n } будет образовывать область означивания V. Моделью Крипке M (или просто моделью) называется тройка 〈 W, R, V 〉 , где 〈 W, R 〉 – фрейм, а V – означивание на его элементах пропозициональных переменных.

Истинность формулы α в элементе a модели M обозначаем a ╟─ v α . Для логики λ фрейм F называется λ-фреймом или фреймом, адекватным логике λ, если ∀ α ∈ λ при любом означивании V и на любом элементе a фрейма F : a ╟─ v α . Логика λ называется финитно аппроксимируемой, если она порождается некоторым классом Fr λ λ-фреймов, т. е. ∀ α ∈ λ ∀ F ∈ Fr λ : F ╟─ α ∀ β ∉ λ ∃ F ∈ Fr λ , означивание V, ∃ b ∈ F : b ╟─ v β . Этот класс называется также классом характеристических фреймов. Правило вывода r = α 1 ( ^L ), …, α k ( ^L )/ β ( ^L ) называется допустимым в модальной логике λ, если при любой подстановке формул у⇒ ■^ из того, что α 1 ( ), …, α k ( ), ∈ λ, следует β ( ), ∈ λ. Элемент a модели M называется формульным, или определимым, если существует такая формула α , что ∀ b ∈ F b ╟─ v α ⇔ b = a . Означивание V для переменных p 1 , …, pn называется формульным, если V для каждой переменной pi существует формула α i , что ∀ b ∈ F b ╟─ v α i ⇔ b ╟─ v pi .

Пусть F = 〈 W,R 〉 – транзитивный фрейм, т. е. фрейм с транзитивным отношением R. Сгустком (или кластером) фрейма F называется подмножество C ∈ W, такое, что ∀ a , b ∈ C, ∀ с ∈ W: ( a R b )&( b R a ) и ( a R с )&( с R a ) ⇒ ( с ∈ C). Вырожденным сгустком называется иррефлексивный элемент C={ a }. Через C ( a ) обозначим сгусток, содержащий элемент a . Сгусток C 1 «достигает» сгусток C 2 в модели M (обозначаем C 1 RC 2 ), если ∃ a ∈ C 1 , ∃ b ∈ C 2 такие, что a R b . Фактически отношение «достигать» задает на множестве сгустков фрейма строгий частичный порядок. Сгусток C 2 называется непосредственным последователем (потомком) сгустка C 1 , если C 1 RC 2 и ∀ C (C≠C 1 )&(C 1 RC)&(CRC 2 ) ⇒ (C=C 2 ). Здесь сгусток C 1 называется непосредственным предшественником сгустка C 2 . Цепью сгустков фрейма F называется множество сгустков A, если из любых двух сгустков какой-то один «видит» другой. Длиной цепи называем количество ее сгустков. Антицепью сгустков фрейма F называется множество сгустков A, которые попарно «не видят» друг друга. Элемент a фрейма F имеет глубину n , если это максимальная длина цепи во фрейме F , начинающейся со сгустка C ( a ). Слоем глубины n фрейма F будем называть множество всех его элементов глубиной n , мы обозначим его Sl n ( F ). Сгустки фрейма F , входящие в верхний слой Sl 1 ( F ), будем называть также максимальными в F . Множество всех элементов фрейма F глубиной не больше n будем обозначать как S n ( F ).

Фрейм F = 〈 W,R 〉 называется прямой суммой семейства фреймов F i = 〈 W i ,R i 〉 , i ∈ I (при этом ∀ i ≠j W i ∩W j = ∅ ), еслиw = u_iefw; и R = V3_ieIR_t , обозначаем F = \I_1£iF, . Множество Y ^{R ≤} ={ x | x ∈ W, ∃ y ∈ Y, y R x } будем называть верхним конусом, порожденным множеством элементов       Y ⊆ W.       Аналогично определяем множество

Y ^{R ≤} ={ x | x ∈ W, ∃ y ∈ Y, y R x & (xRy)}.

Сгусток C будем называть конакрытием для антицепи сгустков A из F, если выполняется условие C ^R< = vic^croc.) . Модель M 1 = 〈 W 1 ,R 1 ,V 1 〉 называется открытой подмоделью модели M 2 = 〈 W 2 ,R 2 ,V 2 〉 , если W 1 ⊆ W 2 , R 1 ⊆ R 2 , Dom  (V 1 ) = Dom (V 2 ) и ∀ a ∈ W 1 ∀ x ∈ Dom  (V 2 )

a ╟─ V1 x ⇒ a ╟─ V2 x .

Отображение f фрейма 〈 W 1 ,R 1 〉 во фрейм 〈 W 2 ,R 2 〉 называется p -морфизмом, если ∀ a , b ∈ W 1 a R 1 b ⇒ f ( a ) R 2 f ( b ) и ∀ a , b ∈ W 1 f ( a ) R 2 f ( b ) ⇒ ∃ с ∈ W 1 ( a R 1 с )&( f ( с ) = f ( b ). Отображение f модели M 1 = 〈 W 1 ,R 1 ,V 1 〉 в модель M 2 = 〈 W 2 ,R 2 ,V 2 〉 называется p -морфным, если f осуществляет p -морфизм 〈 W 1 ,R 1 〉 во фрейм 〈 W 2 ,R 2 〉 , Dom (V 1 ) = Dom (V 2 ) и ∀ p ∈ Dom  (V 1 )

∀ a ∈ W 1 a ╟─ V1 p ⇔ f ( a )╟─ V2 p .

Модель Крипке K n называется n -характеристической для нормальной модальной логики λ, если область определения означивания V из K n будет множеством P , содержащим n различных пропозициональных переменных, и если для всякой формулы α от переменных P: α ∈ λ ⇔ K n ╟─ V1 α .

Построение n-характеристической модели Ch λ ( n ) следующее. Пусть λ – финитно аппроксимируемая модальная логика, K4 ⊆ λ, и P={ p 1 , …, p n } – множество пропозициональных букв. Пусть также S 1 – множество всевозможных сгустков со всевозможными означиваниями пропозициональных букв из P, с тем условием что в каждом сгустке нет двух элементов с одинаковыми означиваниями пропозициональных букв, а в множестве S 1 нет двух различных сгустков, изоморфных как подмодели, и каждый сгусток множества S 1 является λ-фреймом. Первый слой модели Ch λ ( n ) определяем так: Sl 1 (Ch λ ( n )):= S 1 . Если подмодель Ch λ ( m ) для некоторого m построена, то построение подмодели S m +1 (Ch λ ( n )) следующее: произвольным образом выбираем антицепь Y из подмодели S m (Ch λ ( n )), имеющей, по крайней мере, один сгусток глубиной не меньше m, и добавляем к ней любой сгусток C из множества S 1 как непосредственный предшественник сгустков из Y при условии, что:

• 1)    фрейм C ^{R ≤} будет λ-фреймом;

• 2)    если Y состоит только из одного рефлексивного сгустка C 1 , то C не будет подмоделью C 1 .

Продолжая этот процесс, мы и получаем модель Ch λ ( n ).

Приведем основные теоремы, касающиеся техники Рыбакова построения и использования семантической характеристической модели. Для упрощения работы ссылки будем приводить на единый источник.

Лемма 1 (лемма 2.5.15. [Rybakov 1997]). Пусть отображение f является p -морфизмом модели M 1 = 〈 W 1 , R 1 ,V 1 〉 в модель M 2 = 〈 W 2 , R 2 ,V 2 〉 . Тогда для любой формулы α от переменных Dom (V 1 )      справедливо утверждение:       ∀ a ∈ W 1 a ╟─ V1 α       ⇒

⇒ f ( a )╟─ V2 α .

Теорема 2 (теорема 3.3.3 [Rybakov 1997]). Пусть K n = 〈 W n , R n ,V n 〉 ( n ∈ N) – последовательность n -характеристических моделей для модальной логики λ. Правило вывода r = α 1 ( I), …, α k ( I )/ β ( 1 ) является допустимым в λ тогда и только тогда, когда для каждого n ∈ N и каждого формульного означивания S переменных из r в K n правило r истинно в модели 〈 W n , R n ,S 〉 , т. е. из S ( α 1 ) = W n , …, S ( α n ) = W n следует S ( β )= W n .

Теорема 3 (теорема 3.3.6 [Rybakov 1997]). Модель Ch λ ( n ) является n-характеристической моделью.

Теорема 4 (теорема 3.3.7 [Rybakov 1997]). Любой элемент модели Ch K4 ( k ) является формульным. Для любой нормальной модальной логики λ со свойством финитной аппроксимируемости любой элемент модели Ch λ ( k ) также является формульным.

Лемма 5 (лемма 3.4.6 [Rybakov 1997]). Пусть M – подмодель модели W, включающая модель max (Y,W,m)JS_m(W), где Y – подмножество формул. Тогда ∀ a ∈ |M|, ∀ α ∈ Y a ╟─ V α в модели W ⇔ a ╟─ V α в модели M.

Лемма 6 (лемма 3.4.2 [Rybakov 1997]). Пусть λ – финитно аппроксимируемая модальная логика, расширяющая K4, или суперинтуиционистская логика. Если существует означивание S переменных правила вывода r во фрейме некоторой p -характеристической модели Ch λ ( p ), которое опровергает правило r , тогда существует означивание S этих переменных во фрейме модели Ch λ ( k ), где k – число переменных правила вывода r , которое также опровергает правило r .

Существует перевод Геделя – Маккинси – Тарского, позволяющий устанавливать связь между суперинтуиционистскими логиками и модальными логиками решетки модальных напарников в спектрах над S4 [Максимова 1974].

Теорема 7 (теорема 3.2.2 [Rybakov 1997]). Правило вывода r является допустимым в суперинтуиционистской логике λ тогда и только тогда, когда правило Т ( r ) допустимо в наибольшем ее модальном напарнике σ(λ).

Основные результаты

Теорема 1 . Правило вывода r = α 1 ( x 1 , …, x n ), …, α s ( x 1 , …, x n ) / β ( x 1 , …, x n ) не допустимо в финитной аппроксимируемой модальной логике λ, K4 ⊆ λ тогда и только тогда, когда существует модель Крипке M = = ^ j ^M j c означиванием S для переменных правила вывода r , удовлетворяющее следующим свойствам:

• (a)    модель M является λ-моделью и модель S 1 (M) изоморфна модели S 1 (Ch λ ( n ));

• (b)    модель М содержит не более                 элементов, здесь w =

  = ||S 1 (Ch К4 ( n ))||, t = |Sub ( r )|, где g ( w , t ) – функция, определяемая формулой эффективного означивания ([Rybakov 1997]), Sub ( r ) – множество подформул правила вывода r , замкнутое по отрицанию;

• (c)    для каждой антицепи E сгустков X k модели M j , допускающей в λ рефлексивное (ир-рефлексивное) конакрытие, существует элемент x ER ( x EI ) из M j такой, что

• ◊(xer, Sub (r)) = U   {◊(y, Sub (r)) US (y, Sub (r)) |yeX^ E} US (xer, Sub (r))     (1)

(или соответственно

◊ ( x ei , Sub ( r )) = U    { ◊ ( y , Sub ( r )) U S ( y , Sub ( r )) | yeX < e E});                            (2)

• (d)    каждая компонента M j является открытой подмоделью модели Ch λ ( n );

• (e)    модель M также опровергает правило вывода r.

Доказательство

Необходимость. Пусть правило r не является допустимым в логике λ, то, согласно теоремам 2, 3 и лемме 6, для фрейма n-характеристической модели Chλ(n) существует опровергающее правило r означивание W, формульное для переменных x1, …, xn. Для каждого подмножества Z ⊆ Sub (r) и каждой компоненты Hj модели Chλ(n) выделим не лежащий в максимальном сгустке элемент-представитель xZ так, чтобы S (xZ, Sub (r)) = Z (если такой элемент в модели Hj найдется). Построим модель KjZ как открытую подмодель Hj, порожден-K ную таким элементом xZ. Тогда модель K, = c ^(r) K jz также будет открытой конечной U                          U           2 5ubWl          _ подмоделью Hj, поскольку количество компонент Hj не превышает        . Очевидно, что

K объединение K = ^j K j этих компонент также опровергает правило r и также является X- фреймом. Согласно лемме 5, для произвольной компоненты Kj (которая очевидно содержат модель max (sub (r),Kj,1) US1(Kj)) можно построить сжимающий p-морфизм f из Kj в конечную λ-модель Mj с эффективным ограничением мощности (см. [Рыбаков 1984] или [Rutskiy 2001]). Как известно, при p-морфном отображении истинность формул на элементах образа сохраняется, поэтому правило r на некоторой модели Mj будет опровергаться. Верхний слой при этом отображении не будет подвергнут сжатию, поэтому S1(Mj) = S1(Kj) = S1(Hj). Точный p-морфный прообраз M j будет некоторой открытой подмоделью Kj, следовательно, сама модель M является открытой подмоделью ChX(n). Но тогда модель M = ^j M~ j обладает свойствами (a), (b), (d), (e).

Докажем теперь свойство (с). Пусть E – конечная антицепь сгустков модели Mj, допускающая рефлексивное (иррефлексивное) конакрытие в логике λ. Обозначим через U множество представителей z∈CE сгустков антицепи E. Рассмотрим в модели Kj множество прооб- разов fj – 1(U) множества U и обозначим через E (fj – 1) множество сгустков, содержащих элементы fj – 1(U). Поскольку антицепь E допускала рефлексивное (иррефлексивное) конакры-тие в X, то фрейм [- ] U {x}, полученный добавлением рефлексивного (иррефлексивного) Irr/£-1\]Я<

U

{y}, где y – аналогичное конакрытие для E ( f j ^{– 1} ). Точные прообразы сгустков E ( f j ^{– 1} ) содержатся в K j , а значит, и в компоненте n -характеристической модели H j . Согласно принципам ее построения, для них в H j должно существовать рефлексивное (иррефлексивное) конакры-тие z ER (z EI ) со свойством

◊ ( z er , Sub ( r )) = U    { О ( у , Sub ( r )) U S (y, Sub ( r )) | y e X E (f j " 1 )} U S ( z er , Sub ( r )),

(соответственно ◊ ( z ei , Sub ( r )) =

U

{ ◊ ( y , Sub ( r )) U S ( y , Sub ( r )) | y e Xe E (fj- ')}).

Согласно теореме, 2 р-морфное отображение сохраняет истинность формул на элементах-образах, следовательно,

U    { O ( y , Sub ( r )) U S ( y ,Sub ( r )) | y e X k e E ( f " 1 )} =

= U    M y , Sub ( r )) US ( y ,Sub ( r ))| e X ₍ e E}.

Согласно построению модели K j , в ней будут существовать элементы с аналогичными свойствами, что и доказывает свойство (c).

Достаточность. Пусть для логики X существует модель M = ^j M j , обладающая свойствами (a)-(e). Тогда каждую модель Mj можно воспринимать как открытую подмоделью компоненты Hj, построенную на фрейме характеристической модели Chλ(n). Будем M ch подразумевать под Mch =