Разрешимость по допустимости модальной логики s4.m.p.q

Допустимые правила вывода были введены в 50- х гг . К . Лоренценом как правила , применение которых не расширяет множество теорем . Традиционно исследования допустимых правил вывода имеют много аспектов – проверка разрешимости по допустимости , определения базиса допустимых правил выво да , решения логических уравнений с метапеременными , проверка истинности квазитождеств на свободных алгебрах квазимногообразий , исследование урав нений в свободных алгебрах [1; 3; 7] и др . В последние годы изучение разреши мости для допустимых правил вывода проводится также и в связи с исследова ниями свойств наследственности и строгой разрешимости ряда общих свойств для различных формальных исчислений .

В статьях Л . Л . Максимовой сформулирован ряд предположений о разреши мости по допустимости некоторых логик [2; 5]. Их подтверждение позволяет провести доказательство строгой разрешимости интерполяционного свойства модальных логик над S4 и ряда других свойств . В настоящей статье приведено доказательство разрешимости для допустимых правил вывода комбинацией части перечисленных в [2] логик , а именно S4.αm.ξp.ζq, финитно аппроксимиру емой классом транзитивных и рефлексивных фреймов . При этом внутренние сгустки этих фреймов имеют не более q элементов , максимальные сгустки име ют не более p элементов , а их число ограничено значением m. Варьируя пара метры p, m и q, мы можем получить критерии допустимости правил вывода для многих проблемных логик . Это позволяет провести доказательство строгой раз решимости интерполяционного свойства модальных логик над S4 и ряда дру гих свойств .

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

Пусть модель K основана на рефлексивном и транзитивном фрейме и не имеет бесконечно возрастающих цепей . Применив технику сжатия , изложен ную , например , в [6], получим p- морфную ей модель M , в любом сгустке кото рой нет элементов с одинаковым означиванием , а все сгустки верхнего слоя не изоморфны как подмодели . В работах [6; 3] был введен конечный и эффективно конструируемый класс формул Ω( M ) = { φ (C1,…, Cf) | Ck ∈ Sl1( M )}, обладающий свойством распознавания сгустков верхнего слоя модели :

∀ a ∈ | M | a ╟─ V φ (C1,…, Cf) ⇔ {C1,…, Cf} = S1( С ( a ) ^{R ≤}).

С помощью класса Ω( M ) выведен следующий критерий .

Теорема 1. Правило вывода r = α1(x1, …,xn), …, αl (x1, …,xn)/β(x1, …,xn)

не является допустимым в модальной логике S4.αm.ξp.ζq тогда и только тогда, когда существует модель Крипке M = = CMj c означиванием S для j переменных правила вывода r, удовлетворяющая следующим свойствам:

• (a)    модель M является (S4.αm.ξp.ζq)- моделью , модель S1( M ) – изоморфна моде ли S1(ChS4.αm.ξp.ζq( k ));

• (b)    модель М содержит не более g ( w , t )2^с элементов , здесь с = 2 ⁿ , w = S1(ChК4( n )), t = |Sub ( r )|, где g ( w , t ) – функция , определяемая формулой (1) в [4; 6], Sub ( r ) – множество подформул правила вывода r , замкнутое по отрица нию ;

• (c)    модель М обладает свойством обозрения ниже первого слоя [7] для мно жеств Y = Sub ( r ) UΩ( M ), т . е . для любой антицепи E сгустков модели M j , фрейм E^≤ которой имеет не более m максимальных сгустков , существует элемент X E из M j такой , что ◊ ( X E, Y ) = { ◊ ( y , Y ) | y ∈ E} US ( X E, Y );

• (d)    каждая модель M j – открытая подмодель модели ChS4. α m. ξ p. ζ q ( n );

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

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

Необходимость. Если правило r недопустимо в логике S4.αm.ξp.ζq, то по теореме 3.4.2 [7] для фрейма j-характеристической модели ChS4.αm.ξp.ζq (i) существует опровергающее правило r означивание W, формульное для переменных x1, …, xn. Тогда по лемме 2.4 на фрейме модели ChS4.αm.ξp.ζq (n) найдется означивание W2 с теми же свойствами. Следуя [6], n-характеристическая модель может быть представлена в виде ChS4.αm.ξp.ζq (n) =CHj , где J≤2c. В каждой компо-j∈J ненте Hj выделим для каждого подмножества Z ⊆ Sub (r) UΩ(Hj) не лежащий в максимальном сгустке элемент xZ так, чтобы S (xZ, Sub (r) UΩ(Hj)) = Z (если такой элемент в модели Hj найдется). Тогда модель Kj =    U xZR≤ будет откры-

Z c Sub( r ) nQ ( H j )

той конечной подмоделью H j . На модели K = C K _j , также основанной на j J

(S4.αm.ξp.ζq)- фрейме , правило r будет ложным . По лемме 3.4.1 [7] для каждой компоненты K j можно построить сжимающий p - морфизм f j из K j в конечную (S4.αm.ξp.ζq)- модель M j , тогда модель M = C M _j будет удовлетворять свойствам j

• (b) и (d). При этом верхний слой этих моделей сохраняется :S1( M ) = S1(ChS4. α m. ξ p. ζ q ( n )), как и ограничение на количество элементов в сгустках верхнего слоя . По этому свойство (a) для модели M справедливо , откуда Ω( M ) = Ω( K ) = Ω(ChS4. α m. ξ p. ζ q ( n )). Поскольку при p - морфном отображении истинность формул на моделях сохраняется , то модель M свойству ( е ) также удовлетворяет .

Покажем , что модель M обладает полным свойством обозрения ниже верхне го слоя для множеств Y ⊆ Sub ( r ) UΩ( M ). Пусть E – конечная антицепь сгустков из модели M j и количество максимальных сгустков модели E ^{R ≤} не превосходит m . Обозначим через U множество представителей z ∈ CE сгустков антицепи E. В модели K j выделим f j ^{– 1} (U) множество прообразов множества U и обозначим че рез U ( f j ^–1 ) множество сгустков , содержащих элементы f j ^–1 (U). В совокупности миры множества U ( f j ^–1 ) « видят » не более m максимальных сгустков в модели H j . Действительно , пусть S1(E ^{R ≤}) = {C1, …,C b }, b ≤ m , тогда по свойству класса формул Ω( M ) [6; 3] для любого x ∈ Е имеем x ╟─ S ( Λ C j ∈ {C1, …,C b } ^┐ ρ (C j )). По выбору элемента XZ и определению p - морфизма тогда для каждого y ∈ U ( f j ^–1 ) получим y ╟─ V ( Λ C j ∈ {C1, …,C b } ^┐ ρ (C j )), что влечет {C1, …,C b } ⊆ S1(U ( f j ^–1 ) ^{R ≤}), b ≤ m . Обозначим через E ( f j ^–1 ) множество минимальных сгустков подмодели U ( f j ^{– 1} ) ^{R ≤}, и тогда

U ◊ ( y , Sub ( r ) UΩ( M )) = U ◊ ( y , Sub ( r ) UΩ( M )).

У eE( f ¹)                                        У 6U< f j ‘)

По построению в модели H j найдется элемент XE некоторого сгустка конакры - тия ( содержащего не более q элементов ) для антицепи f j ^{– 1} (U), которая видит в совокупности не более m максимальных сгустков . По построению модели K j в ней найдется элемент YE глубиной больше 1, такой , что S (XE,Sub ( r ) UΩ( M )) = S (YE, Sub ( r ) UΩ( M )). Поскольку p - морфизм f j сохраняет истинность формул , в мире f j (YE) модели M j будет справедливо :

◊ ( f j (YE), Sub ( r ) UΩ( M )) = ◊ (YE, Sub ( r ) UΩ( M )) =

• =    ◊ (XE, Sub ( r ) UΩ( M )) US ( f j (YE), Sub ( r ) UΩ( M )) =

• =    U ◊ ( y , Sub ( r ) UΩ( M )) US (XE, Sub ( r ) UΩ( M )).

У 6U( f,' )

Таким образом , свойство (c) также выполняется .

Достаточность. Рассмотрим модель ChS4.αm.ξp.ζq (n) = CHj . Согласно свой-J ствам (a) и (d) каждая модель Mj является открытой подмоделью Hj и фреймы, образованные подмоделями S1(Hj) и S1(Mj), изоморфны. Поэтому мы можем рас- сматривать все элементы модели M как некоторые элементы модели ChS4.αm.ξp.ζq (n). По теореме 3.3.7 [7], каждый элемент модели ChS4.αm.ξp.ζq (n) является формульным. Поэтому на фрейме модели M, как на подфрейме фрейма модели ChS4.αm.ξp.ζq (n), можно построить означивание V для переменных правила r, которое будет совпадать с означиванием S модели M. В дальнейшем будем подразумевать под Mch = ( W,R,V = C Mcjh именно такую подмодель модели ChS4.αm.ξp.ζq j-J

( n ), полагая | M ^ch | ⊆ | ChS4. α m. ξ p. ζ q ( n ) |.

Доопределим означивание V на весь фрейм модели ChS4. α m. ξ p. ζ q ( n ), для чего на каждом компоненте H j построим последовательность возрастающих подмножеств ∑ ( x , t ) для ∀ x ∈ | M ^c _j ^h |, ∀ t : 0 ≤ t ≤ m 1, где m 1 – количество миров в модели M ^c _j ^h .

Последовательность будет удовлетворять следующим свойствам :

(a1) ∀x∈| Mcjh |, ∑(x, t) ⊆ ∑(x, t +1), причем ∀xi, xk ∈| Mcjh |, xi ≠xk ⇒ ∑(xi, t)∩∑(xk, t) = ∅;

(b1) каждое подмножество ∑ ( x , t ) формульно при означивании V в модели H j , т . е . ∀ x ∈ | M ^c _j ^h |, ∀ t 0 ≤ t ≤ m 1, найдется формула α( x , t ) такая , что ∀ y ∈ | H j | y ╟─ V α( x , t ) ⇔ y ∈ ∑ ( x , t );

(c1) ∀t 0 ≤ t ≤ m1, фрейм U ∑(xi, t) образует открытый подфрейм фрейма мо-x, elMchi ij дели Hj;

• (d1) если означивание V для переменных правила вывода r на фрейме U ∑ ( x i , t ) будет таким , что ∀ p ∈ Var( r ) V( p ) = U   { ∑ ( x i , t ) | x i ╟─ V p },

Xi eMjh                                                                      xieMchl тогда ∀β∈Sub (r) UΩ(Mj), ∀x∈| Mcjh |, ∀a∈∑(x, t) a╟─V β ⇔ x╟─V β;

(e1) ∀t 0 ≤ t ≤ m1 ∀y∈| Hcjh |, если y∉ V (p) = U {∑(xi, t) | xi╟─Vp}, то найдется x, elMchi ij подмножество W: такое, что | W | = t+1, W⊆| Mcjh | и ∀x∈| W | yR<∩∑(x, t) ≠∅.

Конструкцию последовательности подмножеств ∑ ( x , t ) опишем индукцией по значению параметра t . Подмножество ∑ ( x ,0) определим так : ∀ x ∈ | M ^c _j ^h | ∑ ( x ,0) = { x }. Пусть для элемента ∀ x ∈ | M ^c _j ^h | построены подмножества ∑ ( x , g ) для g ≤ t . Возьмем произвольное t +1 элементное подмножество D элементов модели | M ^c _j ^h |, такое , что фрейм [D] ^{R ≤} имеет не более m максимальных сгустков . Пусть ED – множество представителей всех минимальных сгустков для подфрейма [D] ^{R ≤} модели M ^c _j ^h ( по одному представителю от каждого сгустка ), тогда очевидно :

U ◊ ( y , Sub ( r ) UΩ( M j)) = U ◊ ( y , Sub ( r ) UΩ( M j)).

У ^gEd                                 У ^GD

Для антицепи ED фиксируем элемент XE, удовлетворяющий свойству (c):

• ◊ (XE, Sub ( r ) UΩ( M j)) = U ◊ ( y , Sub ( r ) UΩ( M j)) US (XE, Sub ( r ) UΩ( M j)).

y ^gEd

Для такого элемента XE построим формулы q (D) и χ(D):

q (D) = ( Л ◊α(x,t))Λ( Л ┐◊α(x,t))Λ┐( V α(x,t)), x D                  x D,                     xelMchi x ^MJhl

χ(D) = q (D)Λ□( Л ┐α(x,t) → ◊q (D))Λ( V α(x,t) Vq (D)). xelMchi                                     x DI где α(x,t) – формулы для множеств ∑(x, t), удовлетворяющие свойству (b1). Тогда множество ∑(x, t+1) строим следующим образом:

∑ ( x , t +1) = ∑ ( x , t ) U ( U V (χ(D))),

X_E = x

Нетрудно убедиться, что U ∑(x, t) = Hj. При таком расширении означива-xi elMchi, 0 tt m, ния V из модели Mch на весь фрейм модели ChS4.αm.ξp.ζq (n) получим, что на полученной модели формулы из посылки α1(x1, …,xn), …, αl (x1, …,xn) правила r будут истинны. С другой стороны, формула β(x1, …,xn) будет ложной в некотором элементе h∈| Mcjh | ⊆ |ChS4.αm.ξp.ζq (n)|. Таким образом, при построенном означивании V фрейма модели ChS4.αm.ξp.ζq (n) правило вывода r опровергается также. ◻

Следствие 1. Модальная логика S4.αm.ξp.ζq разрешима по допустимости .