ПРИКЛАДНАЯ  МАТЕМАТИКА

УДК 621.39.1:519.34

А. А. Чубарян

О нижних оценках выводов в системах Фреге с подстановками

(Представлено академиком Ю. Г. Шукуряном 20/IV 2000)

   В работе доказывается, что существуют тавтологии (твт) длины n, для которых и в системах Фреге Б, и в системах Фреге с подстановками SБ оценки количества формул и общей длины выводов имеют порядок n и n2 соответственно.

   1. Введение. В работах [1] и [2] обсуждается вопрос получения нижних оценок количества шагов выводов в систeмах Фреге с подстановками. В частности, Басс [1] указывает в качестве открытой проблему получения суперлогаритмической нижней оценки количества шагов выводов в SБ. Ургарт в [2] доказал, что существуют формулы с длиной O(n), количество шагов выводов которых в SБ не менее O(n / logn). Однако еще в 1981 г. в качестве некоего вспомогательного результата нами была получена линейная нижняя оценка для количества шагов выводов в классической, интуиционистской и минимальной системах с простыми подстановками исчисления высказываний гильбертовского типа [3]. Эти оценки были получены с использованием введенного в [4] понятия t-множества, непосредственное применение которого в системах Фреге представляется затруднительным. В настоящей работе для произвольной твт вводится понятие множества существенных подформул, и на его основе доказывается существование последовательности формул длины n, для которых в обеих системах Б и SБ количество шагов и длина выводов оцениваются соответственно функциями порядка n и n2 соответственно.

    2. Основные понятия и определения. Напомним общепринятые понятия систем Фреге, выводов в них и сложностных характеристик выводов.
   Каждая система Фреге Б использует некоторое конечное, функционально полное множество пропозициональных связок. Б определяется конечным множеством схематически заданных правил вывода [(A1 A2 јAk)/(B)] (при k=0 соответствующее правило определяет схему ксиом). Б непротиворечива, т. е. для каждого правила вывода, если при некотором истинностном значении переменных все Ai(1 Ј i Ј k) принимают значение "истина", то и B принимает значение "истина". Б полна, т. е. всякая тавтология выводима в Б. Система Фреге с подстановкой SБ получается из Б добавлением правила простой подстановки [(A)/(As)], где s - отображение, ставящее в соответствие переменной формулы A некоторую формулу (в частности переменную), и As - результат повсеместной замены этой переменной в A на соответствующую формулу.
   В дальнейшем мы будем считать зафиксированными некоторую систему Фреге Б и соответствующую систему с подстановкой SБ. Результат настоящей работы не зависит от выбора системы, однако для упрощения рассматриваемого примера мы будем предполагать, что в числе прочих язык Б содержит логические связки ® и Щ.
   Мы будем пользоваться общепринятым определением вывода в данной системе как последовательности формул, каждая из которых является аксиомой данной системы или получается из предыдущих по одному из правил вывода данной системы. Вывод в системе Б будем называть Б-выводом, а в системе SБ - соответственно SБ-выводом.
   Длину формулы F, понимаемую как количество всех символов в F, будем обозначать через (F).
   В качестве сложности вывода зафиксируем два понятия: количество различных формул (шагов) в выводе и суммарную длину всех формул вывода.
   Через Sf(F) обозначим множество всех неэлементарных подформул формулы F. Для каждой формулы F, каждой подформулы j ОSf(F) и произвольной переменной p через (F)pj обозначим результат повсеместной замены в F подформулы j на переменную p. При этом если j ПSf(F), то (F)pj=F.
   Множество различных переменных формулы F обозначим через Var(F).

   Определение. Пусть для некоторой твт F p - некоторая переменная такая, что p П Var(F) и j О Sf(F). Подформулу j назовем существенной для F, если (F)pj не является тавтологией.
   Множество существенных для твт F подформул обозначим через Essf(F).
   Очевидно, что если F является минимальной твт, т. е. не может быть получена подстановкой из более короткой твт, то Essf(F)=Sf(F).
   Если формулы не могут быть получены по правилу подстановки из одной и той же существенной подформулы некоторой твт, то будем говорить, что эти формулы несравнимы.
   Для каждого правила вывода [(A1A2 јAk)/(B)] (k і 1) определяющей назовем любую из существенных подформул формулы A1Щ(A2Щ(јЩ(Ak-1ЩAk)ј))®B. Множество определяющих подформул будем обозначать через Dsf(A1, A2, ј, Ak, B).
   Формулу j назовем важной в Б-выводе (SБ-выводе), если j или является существенной для некоторой аксиомы этого вывода, или является определяющей для некоторого Б-правила, примененного в выводе.*

   3. Основные результаты. Здесь будет описан класс формул длины n, нижние оценки количества шагов и длины выводов которых имеют порядок n и n2 соответственно и в Б и в SБ. В основе доказательства этого результата лежит следующее свойство существенных подформул.
   Лемма. 1)   Для   каждого  Б-правила     [(A1A2 јAk)/(B)]    (k і 1)     Essf(B) Н Н

                      2) Для правила подстановки [(A)/(As)]  Essf(As) Н { js/j О Essf(A)} .

    Доказательство пункта 1) основано на непротиворечивости Б-правил.

   Доказательство пункта 2) следует из того, что если для некоторых p, j, A и s  является твт, то также твт, а значит если не является твт, то также не твт.

   Следствие. Пусть F - некоторая твт и j О Essf(F), тогда
   1) в каждом Б-выводе формулы F формула j должна быть важной;
   2) если правилами подстановки, использованными в некотором SБ-выводе формулы F, являются [(A1)/(A1s1)], [(A2)/(A2 s2)],ј,[(Am)/(Amsm)], то j должна быть или важной формулой этого вывода, или результатом последовательных подстановок si1, si2,ј,siS для 1 Ј i1, i2,јiS Ј m в одну из важных формул.

   Доказательство очевидным образом следует из утверждения леммы.
 

   Теорема 1. Для достаточно больших n, если Fn твт такая, что |Fn|=O(n) и для некоторого l=O(n) существуют подформулы j1, j2, ј, jl такие, что
   a) { j1, j2, ј, jl } О Essf(Fn),
   б) формулы ji и jj  (1 Ј i < j Ј l) попарно несравнимы,
   в) |j1| < |j2| < ј < |jl| и |jl|=O(n),
то количество шагов в любом Б-выводе (SБ-выводе) формулы Fn не менее, чем O(n), а длина любого Б-вывода (SБ-вывода) не менее O(n2).

   Доказательство следует из вышеприведенных утверждений и того факта, что и количество существенных подформул каждой аксиомы, и количество определяющих подформул каждого Б-правила ограничено некоторой константой.

   Пример. Нетрудно  видеть,  что  условия  теоремы  выполнены  для
Fn = (p1 ® p1) Щ ((p2 ® p2) Щ (јЩ ((pn-1 ® pn-1) Щ (pn ® pn))ј)), где ji = (pn-i ®
®  pn-i) Щ ((pn-i+1 ® pn-i+1) Щ (јЩ (pn-1 ® pn-1) Щ (pn ® pn))ј))     (0 Ј i Ј n - 1).

   Теорема 2. Для достаточно больших n существуют формулы Fn такие, что минимальные количества шагов их Б-выводов и SБ-выводов имеют порядок n, а минимальные длины их Б-выводов и SБ-выводов имеют порядок n2.
   В качестве таковых могут быть рассмотрены, например, вышеприведенные. Для них нетрудно получить одинаковые верхние оценки сложностей Б-выводов и SБ-выводов, равные по порядку нижним для обоих критериев сложностей.
   Фактически для класса формул, удовлетворяющего условиям теоремы 1, не имеет место "ускорение" выводов при переходе от Б систем к SБ системам, исследованное в работах [1, 3, 4].
   Заметим, что при мультипликативной подстановке формула Fn может быть выведена за log2n шагов, что указывает на существенное различие способов подстановки.
   Автор благодарен участникам семинара под руководством И. Заславского за полезные советы.



* Отметим, что важные в выводе формулы активны в смысле определения, введенного в [1].
 

   Ереванский государственный университет


Литература

     1. Buss S. R. - Arch. Math. Logic. 1995. V. 34. P. 377-394.
     2. Urquhart A. - Arch. Math. Logic. 1997. V. 37. P. 15-19.
     3. Чубарян А. А. - Прикл. математика. ЕГУ. 1981. N 1. С. 81-89.
     4. Г. С. Цейтин, Чубарян А. А. - Мат. вопр. кибернетики и вычисл. техники. Ереван: Изд-во АН АрмССР. 1975. С. 57-64.