14_Anahit_Chubaryan's article_138-146 l=2�ì=2,÷�“*,� "%C!%“/ *,K�!…�2,*, , "/÷,“ë,2�ëü…%L 2�.…,*, 54, 138-146, 2020. 138 УДК 510.6 Об отношениях сложностей выводов в ряде систем исчисления высказываний Акоп A. Тамазян и Анаит А. Чубарян Ереванский государственный университет e-mail: tam.hak27@gmail.com, achubaryan@ysu.am Аннотация Для некоторых семейств формул сравнены количествa шагов линейных выводов в ряде систем исчисления высказываний: секвенциальной системе с правилом сечения PK, в той же системе без правила сечения PK—, в той же системе с добавлением правила подстановки SPK, в той же системе с добавлением кванторов QPK. Для одного из рассмотренных семейств формул Алессандрой Карбоне в [1] сравнены количествa шагов выводов в виде дерева в тех же системах исчисления высказываний и выявлено отличительное свойство системы QPK, а именно доказано экспоненциальное ускорение по отношению к системам SPK и PK, которые,, в свою очередь,, имеют экспоненциальное ускорение по отношению к системе PK—. Этот результат послужил толчком для бурного интереса к исследованиям системы QPK. В настоящей работе для линейных выводов получены иные сотношения количествa шагов в тех же системах: оказалось, что система QPK не имеет преимуществ по отношению к системе SPK, оказалось также, что для рассматриваемых семейств формул система PK не имеет преимуществ по отношению к системе PK—, которая, в свою очередь, не имеет преимуществ по отношению к более слабой монотонной системе PMon. Доказана также достоверность полученных результатов для ряда иных семейств формул и ряда других систем. Ключевые слова: разновидности секвенциальных систем исчисления высказываний; разновидности систем Фреге; количество щагов вывода; экспоненциальное ускорение. 1. Введение Теория сложностей выводов изучает количественные характеристики выводов, то есть насколько «просто» или «сложно» может быть доказана та или иная теорема. Толчком для бурного развития теории сложностей пропозициональных выводов явился известный результат Кука и Рекхау о неравенстве множеств �� и ���� в том и только в том случае, А.Тамазян и А.Чубарян 139 если не существует полиномиально ограниченной системы доказательств классических тавтологий [2]. За годы интенсивных исследований получено множество интересных оценок длины и количества шагов выводов в различных системах классического исчисления высказываний, на основе которых выстроена некая иерархия пропозициональных систем выводов. Некоторые из них с относительно простой стратегией поиска выводов, условно определены как «слабые» системы – системы, в которых для отдельных классов формул получены нижние экспоненциальные оценки длин выводов, а те системы, в которых ни для какого класса таковых оценок пока не найдено, считаются «сильными». К первому множеству относится, в частности, секвенциальная система без правила сечения PK—, ко второму классу относятся наиболее естественные системы выводов – системы Фреге �, системы Фреге с правилом подстановки S�, секвенциальная система с правилом сечения PK, та же система с добавлением правила подстановки SPK, а также та же система с добавлением кванторов QPK. Добавление кванторов расширило множество пропозициональных тавтологий: в частности, формула � ⊃ q� ⊃ ��p ⊃ q�&�� ⊃ ��� не является тавтологией, но формула ∃r�� ⊃ q� ⊃ ��p ⊃ q�&�r ⊃ q��� уже является тавтологией. Это обстоятельство вызвало особый интерес к изучению системы QPK, а результаты работы [1], в которой для одного из рассмотренных семейств формул выявлено отличительное свойство системы QPK, а именно доказано экспоненциальное ускорение по отношению к системам SPK и PK, которые, в свою очередь, имеют экспоненциальное ускорение по отношению к системе PK—, послужили толчком для бурного интереса к исследованиям системы QPK. Как оказалось, эта система может быть полезной для решения одной из ��-полных задач – задачи «Выполнимости». В настоящей работе исследованы соотношения количествa шагов для линейных выводов (выводов, в которых формулы не повторяются) для тех же систем, которые рассмотрены в [1]. Оказалось, что для этих более естественных выводов система QPK не имеет преимуществ по отношению к системе SPK, оказалось также, что для рассматриваемых семейств формул система PK не имеет преимуществ по отношению к системе PK—. Доказана также достоверность полученных результатов для ряда иных семейств формул и ряда других систем. 2. Предварительные понятия Для представления основных результатов напомним некоторые понятия и обозначения. Мы пользуемся общепринятыми oпределениями пропозициональной формулы, пропозициональной формулы с кванторами, свободной переменной в формуле с кванторами, тавтологии в данной логике, секвенции, сукцедента, антецедента, главной формулы секвенции, секвенциальных систем без сечения, секвенциальных систем с правилом подстановки, секвенциальных систем с кванторами, сложностей выводов [2-6]. Конкретный выбор языка для представления пропозициональной формулы, а значит, и системы доказательств, не имеет значения для наших рассмотрений, однако из технических соображений мы предполагаем, что он содержит пропозициональные Об отношениях сложностей выводов в ряде систем исчисления высказываний 140 переменные, логические связки ¬, &, ∨, ⊃ и пару скобок ( , ). В некоторых системах будут использованы также знаки Τ «истина» и ⏊ «ложь». Длина формулы �, определяемая как количество всех вхождений в нее логических связок, обозначается через |�|. Очевидно, что линейной функцией от |�| оценивается и полная длина формулы, понимаемая как количество всех символов. 2.1. Описание рассматриваемых систем. Напомним ряд определений. Секвенцией называется выражение Γ → Δ , где Γ (антецедент) и Δ (сукцедент) являются конечной (может быть пустой) последовательностью пропозициональных формул. Следуя [3,4], определим следующие системы. Схемой аксиом для классической системы PК являются секвенции p → p, → Τ, где p - произвольная пропозициональная переменная. Для произвольных формул � , и последовательностей формул Γ и Δ логическими правилами вывода являются: ⊃→ Γ → Δ, A B, Γ → Δ � ⊃ , Γ → Δ →⊃ A, Γ → B, Δ Γ → � ⊃ , Δ ∨→ A, Γ → Δ и B, Γ → Δ � ∨ , Γ → Δ →∨ Γ → A, Δ или Γ → B, Δ Γ → � ∨ , Δ & → A, Γ → Δ или B, Γ → Δ �& , Γ → Δ → & Γ → A, Δ и Γ → B, Δ Γ → �& , Δ ¬→ $→ %, & ¬', $→& → ¬ ', $→ & $→¬', & , где формулы � ⊃ , � ∨ , �& и ¬� являются главными формулами секвенции. Правило сечения $ → &,% %,$ → & $ → & . Система PK— получается из системы PK удалением правила сечения. Система SPK получается из системы PK добавлением правила подстановки: () В С�,�,$ → &,%�,� С�В�,$ → &,%�-� , где переменная р не присутствует ни в Γ, ни в Δ, В – формула, подставляемая вместо всех вхождений переменной р. Система QPK получается из системы PK добавлением правил: A�q�, Γ → Δ �∃p�A�p�, Γ → Δ �∃ →� Γ → Δ, A�B� Γ → Δ, �∃p�A�p� �→ ∃� A�B�Γ → Δ �∀p�A�p�, Γ → Δ �∀→� Γ → Δ, A�q� Γ → Δ, �∀p�A�p� �→ ∀�, где B - любая пропозициональная формула быть может с кванторами, а также выполнены следующие условия: в нижних секвенциях правил �∃ →� и �→ ∀� не должно быть А.Тамазян и А.Чубарян 141 свободных переменных, которые не свободны в верхних, и все вхождения переменной q в A(q) должны быть заменены переменной p, а в правилах �→ ∃� и �∀→� формула B не должна содержать переменные, находящиеся в области действия каких-либо кванторов. 2.2. Некоторые характеристики тавтологий и логических систем выводов. Здесь мы исследуем некоторые свойства тавтологий различных логик и вышеприведенных систем выводов на основе одной из сложностных характеристик выводов – t-сложности, определяемой как количество различных секвенций в выводе. Пусть ϕ является некоторой секвенциальной системой выводов фиксированной логики, а φ – некоторая тавтология данной логики. Через 01�φ� обозначим минимально возможное значение t- сложности всевозможных выводов соответствующей секвенции → φ в системе ϕ. Далее будут получены верхние и нижние оценки t-сложностей выводов и для их записи будут использованы следующие общепринятые обозначения: если ∃с4∃54∀6 > 54|8�6�| ≥ �4|:�6�|, то мы будем писать8�6� = Ω�:�6��, если ∃с=∃5=∀6 > 5=|8�6�| ≤ �=|:�6�|, то мы будем писать8�6� = О�:�6��. При выполнении этих обоих условий будем писать 8�6� = A�:�6��. Если для двух систем B4 и B= для одних и тех же последовательностей формул ϕn имеет место CDE ��F � = Ω�2 HIJ �KL��, то считают, что для последовательности формул ϕn система B= имеет экспоненциальное ускорение по отношению к системе B4. 2.3. Результаты А.Карбоне. В [1] дано определение некоторого класса тавтологий длины M�2= L � , для которых исследованы количество шагов выводов в виде дерева во всех вышеперечисленных системах. Для пропозициональной переменной формула N определяется по индукции следующим образом: 4 ≡ и PQ4 ≡ � P & P � для R ≥ 1 . Нетрудно проверить, что формула N содержит ровно 2N вхождений пропозициональной переменной и T различных подформул. Теорема (Карбоне): Если для достаточно больших n Fn является секвенцией → ⊃ = L , то 1. существует вывод в виде дерева секвенции Fn в системе QPK с количеством шагов О(U�; 2. количество шагов любого вывода в виде дерева секвенции Fn в системе SPK является V�2F �; 3. количество шагов любого вывода в виде дерева секвенции Fn в системе PK является V�2F �; 4. количество шагов любого вывода в виде дерева секвенции Fn в системе PK— является V�2= L �. Нам полезен вывод секвенции → ⊃ = L в системе QPK с количеством шагов О(n�. Сначала рассматривается вывод секвенции ∀��� ⊃ �X � → ∀��� ⊃ �=X � , где 5 произвольное натуральное число и �=X = ��X �X. Вывод этой секвенции не зависит от k и может быть получен за конечное число шагов следующим образом: → X → X ⊃ X , → X Об отношениях сложностей выводов в ряде систем исчисления высказываний 142 ∀��� ⊃ �X �, → X =X → =X ∀��� ⊃ �X �, X ⊃ =X , → =X ∀��� ⊃ �X �, X ⊃ =X → ⊃ =X ∀��� ⊃ �X �, ∀��� ⊃ �X � → ⊃ =X ∀��� ⊃ �X � → ⊃ =X ∀��� ⊃ �X � → ∀��� ⊃ �=X � Следует отметить, что в этом выводе нет повторяющихся секвенций, а значит этот вывод линейный. Повторяя этот вывод U раз можно получить вывод секвенции ∀��� ⊃ �=� → ∀��� ⊃ �= L �, а так как ∀��� ⊃ �=� выводится за конечное число шагов, то ∀��� ⊃ �= L �, а следовательно и → ⊃ = L выводится за M�U� шагов. 3. Основные результаты Для того же класса формул, но для линейных выводов доказана Теорема 1: Если для достаточно больших n Fn является секвенцией → ⊃ = L , то 1. существует линейный вывод секвенции Fn в системе QPK с количеством шагов О(U�; 2. существует линейный вывод секвенции Fn в системе SPK с количеством шагов О(U�; 3. количество шагов линейного вывода секвенции Fn в системе PK является A�2U� ; 4. количество шагов линейного вывода секвенции Fn в системе PK- является A�2U�. Доказательство: Доказательство пункта 1. совпадает с доказательством Карбоне с учетом замечания о линейности рассмотренного вывода. Для доказательства пункта 2. рассмотрим: Вывод в SPK Количество шагов → аксиома 1 & → & () )J 2 → & сечение 3 = → Z () )J 4 → Z сечение 5 Z → ] () )^ 6 → ] сечение 7 . . . . . . . . . А.Тамазян и А.Чубарян 143 → = LaEQ4 сечение 2�U b 1� c 3 = LaEQ4 → = LQ4 () )J LaEdE 2�U b 1� c 4 → = L Q4 сечение 2U c 3 Таким образом доказан пункт 2. Для доказательства пункта 3. верхнюю оценку порядка 2F получим на основе вывода в РК: → аксиома 1 → & → & 2 → � & �&� & � → & 3 → e → & 4 → ] → & 5 . . . . . . . . . → = Lf4 → & 2F b 1 → = L → & 2F Для получения нижней оценки напомним понятие существенной подформулы тавтологии: подформула φ тавтологии А называется сушественной, если результат ее повсеместной замены на переменную, не входящую в А, не является тавтологией. В [5] было доказано, что формулы, имеющие k штук существенных подформул, требуют как минимум k шагов выводов в системах Фреге, а значит вывод секвенции → А в системе РК также содержит как минимум k различных секвенций. В формуле Fn 2F c 1 штук сушественных подформул: сама формула и различные подформулы формулы = L . Для доказательства пункта 4. достаточно заметить, что в приведенном выше выводе в системе РК не применено правило сечения, а значит результаты, полученные для системы РК верны и для системы РК—. Теорема полностью доказана. Таким образом, для линейных выводов той же последовательности формул нет экспоненциального ускорения системы QPK по отношению к системам SPK и PK, и последняя не имеет экспоненциального ускорения по отношению к системе PK—. Замечание 1. Утверждения нашей теоремы и теоремы Карбоне верны не только для рассмотренного семейства формул Fn. Нетрудно убедиться, что если в Fn все знаки конъюкции заменить на дизъюнкции, а применения правила → & заменить на применения правила →∨, то все утверждения обеих теорем будут верны и для нового семейства. Интересно исследовать как велико множество семейств формул, для которых верны вышеприведенные утверждения, или может будут иные соотношения между сложностями выводов в тех же системах. Об отношениях сложностей выводов в ряде систем исчисления высказываний 144 Замечание 2. Если в качестве сложности выводов рассматривать вторую из основных характеристик – длину вывода, определяемую как сумму длин всех формул вывода, то нетрудно убедиться, что во всех рассмотренных выводах длины практически те же или один из них является квадратом другого, но экспоненциальный рост не наблюдается. Однако получение нижних оценок требует дополнительного изучения. Замечание 3. Отметим также, что результаты пунктов 4. обеих теорем верны для монотонного исчисления высказываний, описанного в [6], так как сами семейства секвенций → = L и для конъюнкций и для дизъюнкций монотонны и в монотонном исчислении высказываний имеются те же правила → & и →∨. 4. Заключение На основе сравнения шагов выводов некоторых множеств формул в ряде пропозициональных систем обосновано существенное различие между выводами в виде дерева и линейными выводами, что, в свою очередь, указало на «равносильность» системы с кванторами и системы с правилом подстановки для линейных выводов. Литература [1] A. Carbone, “Quantified propositional logic and the number of lines of tree-like proofs”, Studia Logica, vol.. 64, pp. 315-321, 2000. [2] S. Cook and R. Reckhow, “The relative efficiency of propositional proof systems”, Journal of Symbolic Logic, vol. 44, pp. 36-50, 1979. [3] P. Pudlák, The Lengths of Proofs, in S. Buss (ed.), handbook of proof Theory, North Holland, pp. 547-637, 1998. [4] S. C. Kleene , Introduction to Metamathemics. D.VanNostrand Company, INC, 1952. [5] Г. Цейтин и Ан.Чубарян, “Некоторые оценки длин логических выводов в классическом исчислении высказываний”, ДАН Арм. ССР, т. LV, N 1, 10-12, 1972. [6] A. Atserias, N. Galesi and R. Gavalda, “Monotone proofs of the pigeon-hole principle”, Mathematical logic quarterly, vol. 47, no. 4, pp. 461-474, 2001. А.Тамазян и А.Чубарян 145 Ասույթային հաշվի մի շարք համակարգերում արտածումների բարդության հարաբերությունների մասին Հակոբ Ա. Թամազյան և Անահիտ Ա. Չուբարյան Երևանի պետական համալսարան e-mail: tam.hak27@gmail.com, achubaryan@ysu.am Ամփոփում Բանաձևերի մի քանի ընտանիքների համար համեմատված է գծային արտածումների քայլերի քանակը ասույթային հաշվի մի քանի համակարգերում՝ հատույթի կանոնով սեկվենցիալ համակարգում – PK, առանց հատույթի կանոնի նույն համակարգում - PK—, տեղադրման կանոնով նույն համակարգում - SPK, ծավալիչների ավելացմամբ նույն համակարգում - QPK. Մեր կողմից դիտարկված բանաձևերի մեկ ընտանիքի համար Ալեսսանդրա Կարբոնեի կողմից [1]-ում համեմատված են ծառատիպ արտածումների քայլերի քանակը հիշատակված համակարգերում և հայտնաբերված է QPK համակարգի գերակայությունը՝ ապացուցված է, որ այն ունի էքսպոնենցիալ արագացում SPK և PK համակարգերի նկատմամբ, իսկ վերջինները, իրենց հերթին, ունեն էքսպոնենցիալ արագացում PK— համակարգի նկատմամբ: Այս արդյունքը առիթ հանդիսացավ QPK համակարգի հանդեպ հետազոտումների բուռն հետաքրքրությունների համար: Սույն աշխատությունում այդ նույն համակարգերի համար ստացվել են գծային արտածումների քայլերի բոլորովին այլ հարաբերություններ՝ պարզվել է, որ QPK համակարգը չունի որևէ առավելություն SPK համակարգի նկատմամբ, պարզվել է նաև, որ բանաձևերի դիտարկվող ընտանիքների համար PK համակարգը ևս չունի առավելություն PK— համակարգի նկատմամբ, որն իր հերթին չունի որևէ առավելություն առավել թուլ, մոնոտոն PMon համակարգի նկատմամբ: Ապացուցված է նաև ստացված արդյունքների իսկությունը բանաձևերի այլ ընտանիքների, ինչպես նաև այլ համակարգերի համար: Բանալի բառեր՝ ասույթային հաշվի սեկվենցիալ համակարգերի տարատեսակներ, Ֆրեգեի համակարգի տարատեսակներ, արտածման քայլերի քանակ, էկսպոնենցիալ արագացում: Об отношениях сложностей выводов в ряде систем исчисления высказываний 146 On Proof Complexities Relations in Some Systems of Propositional Calculus Hakob A. Tamazyan and Anahit A. Chubaryan Yerevan State University e-mail: tam.hak27@gmail.com, achubaryan@ysu.am Abstract The number of linear proofs steps for some sets of formulas is compared in the folowing systems of propositional calculus: PK – seguent system with cut rule, PK— - the same system without cut rule, SPK – the same system with substitution rule, QPK – the same system with quantifier rules. The number of steps of tree-like proofs in the same systems for some considered set of formulas is compared from Alessandra Carbone in [1] and some distinctive property of the system QPK is revealed: QPK has an exponential speed-up over the systems SPK and PK, which, in their turn, have an exponential speed-up over the system PK—. This result drew the heavy interest for the study of the system QPK. In this work for linear proofs steps in the same systems the other relations are received: it is showed that the system QPK has no preference over the system SPK, it is showed also that for the considered formula sets the system PK has no preference over the system PK—, which, in its turn, has no preference over the monotone system PMon. It is proved also, that the same results are reliable for some other sets of formulas and for other systems as well. Keywords: the varieties of propositional sequent systems; the varieties of Frege systems; the number of proof steps; exponential speed-up. Submitted 20.08.20, accepted 24.11.20.