08_Anahit_Chubaryan's article l=2�ì=2,÷�“*,� "%C!%“/ *,K�!…�2,*, , "/÷,“ë,2�ëü…%L 2�.…,*, 52, 66-73, 2019. 66 УДК 510.6 О количестве минимальных тавтологий и свойствах их выводов в ряде систем классической и неклассических логик Aрсен A. Aмбарцумян, Гайк А. Гаспарян, Саркис А. Ованнисян и Анаит А. Чубарян Ереванский государственный университет e-mails: hambardzumyanarsen99@gmail.com, haykgasparyan012@gmail.com, saqohovhannisyan0199@gmail.com, achubaryan@ysu.am Аннотация В настоящей работе для тавтологий заданной логики длины п доказано, что максимально возможное количество различных их минимальных тавтологий той же логики имеет экспоненциальную оценку от п, и доказано, что для каждой заданной в данной логике тавтологии существует такая минимальная тавтология, количество шагов вывода секвенциальной формы которой совпадает с наименьшим количеством шагов вывода секвенциальной формы заданной формулы в секвенциальных системах без правила сечения классической, интуиционистской, монотонной логик и логики Иогансона. Ключевые слова: минимальная тавтология; секвенциальные системы без правила сечения пропозициональных логик; количество шагов выводов; монотонность системы, строгая монотонность системы. 1. Введение Теория сложностей пропозициональных выводов является одной из активно исследуемых областей общей теории сложностей, так как доказано, что возможное существование полиномиально ограниченной теории выводов решит вопрос равенства известных классов сложностей NP и coNP [1]. В теории сложностей выводов пропозициональных систем важную роль играют минимальные тавтологии, т.е. тавтологии, которые не являются результатом подстановки в более короткие тавтологии. Традиционно считалось, что минимальные тавтологии не могут выводиться сложнее результатов подстановок в них, т.е. должна быть некоторая «естественная монотонность» выводов. Однако, оказалось, что многие «строгие» пропозициональные системы выводов двузначных и многозначных логик не монотонны ни по шагам ни по длине выводов [2,3], т.е. существуют минимальные тавтологии, которые выводятся сложнее, чем некоторые результаты подстановок в них. Тем не менее, оказалось, что у некоторых таких результатов подстановки сушествуют иные минимальные тавтологии, которые выводятся не сложнее. A. Aмбарцумян, Г. Гаспарян, С. Ованнисян и А.Чубарян 67 Таким образом возник вопрос о монотонности и строгой монотонности пропозициональных систем Подобные разновидности монотонностей исследованы для некоторых «слабых» систем выводов классической и неклассических логик в [4-6]. В связи с разнообразием множества минимальных тавтологий одной и той же тавтологии в настоящей работе 1) для тавтологий заданной логики длины п доказано, что максимально возможное количество различных минимальных тавтологий той же логики имеет экспоненциальную оценку от п, и 2) доказана монотонность пропозициональных секвенциальных систем без правила сечения для классической, интуиционистской, монотонной логик и логики Иогансона. Отметим, что строгая немонотонность этих систем, как и соответствующих систем с правилом сечения доказана в [7]. 2. Предварительные понятия Для представления основных результатов напомним некоторые понятия и обозначения. Мы пользуемся общепринятыми oпределениями пропозициональной формулы, тавтологии в данной логике, секвенции, сукцедента, антецедента, главной формулы секвенции, секвенциальных систем без сечения классических и неклассических логик, сложностей выводов [8-10]. Конкретный выбор языка для представления пропозициональной формулы, а значит, и системы доказательств, не имеет значения для наших рассмотрений, однако из технических соображений мы предполагаем, что он содержит пропозициональные переменные, логические связки ¬, &, ∨, ⊃ и пару скобок ( , ). В некоторых системах будут использованы также знаки Τ«истина» и ⏊«ложь». Длина формулы �, определяемая как количество всех вхождений в нее логических связок, обозначается через |�|. Очевидно, что линейной функцией от |�| оценивается и полная длина формулы, понимаемая как количество всех символов. 2.1. Описания рассматриваемых систем Напомним ряд определений. Секвенцией называется выражение Γ → Δ , где Γ (антецедент) и Δ (сукцедент) являются конечной (может быть пустой) последовательностью пропозициональных формул. Следуя [8], определим следующие системы. Схемой аксиом для классической системы (PC) является секвенция , Γ → , где произвольная формула, а Γ произвольная конечная (быть может пустая) последовательность формул. Для произвольных формул� , � и последовательностей формулΓиΔ, логическими правилами вывода являются: ⊃→ � ⊃ �, Γ → Δ, A � ⊃ �, B, Γ → Δ � ⊃ �, Γ → Δ →⊃ A, Γ → B, � ⊃ �, Δ Γ → � ⊃ �, Δ ∨→ �∨�, �, �→�и�∨�, �, �→� �∨�, �→� →∨ �→�, �∨�, �или�→�, �∨�, � �→�∨� О количестве минимальных тавтологий и свойствах их выводов в ряде систем логик 68 & → �&�, A, Γ → Δили�&�, B, Γ → Δ �&�, Γ → Δ → & Γ → A, �&�, ΔиΓ → B, �&�, Δ Γ → �&�, Δ ¬→ ¬�,�→ �, � ¬�, �→� → ¬ �, �→¬�, � �→¬�, � , где формулы � ⊃ �, � ∨ �, �&� и ¬� являются главными формулами секвенции. Структурным правилом является Γ→ Δ ——————, где Γ⊆Γ’ ևΔ⊆Δ’ Γ’ → Δ’ Схема аксиом пропозициональной интуиционистской системы (PI) и системы Иогансона (PM) та же. В верхней секвенции (секвенциях) правилах введения логических функций в сукцеденте для систем PI и PM отсутствует главная формула, Δ во всех правилах PI пуста или состоит из одной формулы, а для PM пуста [9]. Пропозициональную систему (PMon) для монотонной логики, где используются только монотонные формулы (формулы, строящиеся с использованием только монотонных логических функций), определим, следуя [10]. Схемами аксиом системы PMon являются p → p, ⏊ → Γ, Γ → Τ, где p – пропозициональная переменная, а Γ- конечная (быть может пустая) последовательность формул. Для любых монотонных формул� , � и любых последовательностей монотонных формул Γ, Γ�, Δ и Δ� правилами вывода являются: ��� Γ, Α, Α, Δ → Γ� Γ, Α, Δ → Γ� ��" Γ, Α, Β, Δ → Γ� Γ, Β, Α, Δ → Γ� ��$ Γ → Γ� Γ, Α → Γ� ��% Α, Β, Γ → Δ Α&Β, Γ → Δ ��& Α, Γ → ΔиΒ, Γ� → Δ� Α ∨ Β, Γ, Γ� → Δ, Δ� �'� Γ� → Γ, Α, Α, Δ Γ� → Γ, Α, Δ �'" Γ� → Γ, Α, Β, Δ Γ� → Γ, Β, Α, Δ �'$ Γ� → Γ Γ� → Γ, Α �'% Γ → Δ, Α, Β Γ → Δ, Α ∨ Β �'& Γ → Δ, A иΓ� → Δ�, Β Γ, Γ� → Δ, Δ�, Α&Β Обратим внимание, что порядок вхождения формул ни в сукцеденте, ни в антецеденте не существенен ни в одной из вышеописанных систем. Мы пользуемся общепринятым понятием вывода в указанных системах. Секвенция Γ → Δ называется C-доказуемой (I-доказуемой, M- доказуемой, Mon- доказуемой), если она выводима в системе PC (PI, PM, PMon). Формула A называется C- тавтологией (I-тавтологией, M-тавтологией), если секвенциальная форма→ A выводима в соответствующей системе PC (PI, PM). Для монотонных формул A и B формула A⊃B называется Mon- тавтологией, если ее секвенциальная форма � →B выводима в системе PMon. A. Aмбарцумян, Г. Гаспарян, С. Ованнисян и А.Чубарян 69 2.2. Некоторые характеристики минимальных тавтологий и логических систем выводов Здесь мы исследуем некоторые свойства тавтологий различных логик и вышеприведенных систем выводов на основе одной из сложностных характеристик выводов - t- сложности, определяемой как количество различных секвенций в выводе. Пусть ϕ является некоторой секвенциальной системой выводов фиксированной логики, а φ – некоторая тавтология данной логики. Через ()�φ обозначим минимально возможное значение t-сложности всевозможных выводов соответствующей секвенциальной формы тавтологии φ в системе ϕ. Определение 2.2.1: Тавтология данной логики называется минимальной, если она не может быть получена подстановкой вместо ее переменных из более короткой тавтологии этой же логики. Для произвольной минимальной тавтологии � фиксированной логики обозначим через S( � ) множество всех тавтологий этой же логики, являющихся результатом подстановки в �. Определение 2.2.2: Система выводов ϕ называется t-монотонной, если для каждой не минимальной тавтологии + этой системы существует такая минимальная тавтология φ этой же системы, что + принадлежит S(φ) и (, �+ = (, �� . Определение 2.2.3: Система выводов ϕ называется t-строго монотонной, если для каждой минимальной тавтологии φ и для каждой формулы + из S(φ) (, �� ≤(,�+ . 3. Основные результаты Здесь будут даны оценки максимального количества различных минимальных тавтологий для тавтологий длины n каждой из приведенных логик, а также будет доказана монотонность всех вышеперечисленных систем выводов. Для формулировки результатов введем несколько обозначений. Обозначим через Тϕ(n) множество тавтологий длины n системы ϕ и ∀g∊Тϕ(n) через kϕ(g) обозначим количество различных минимальных тавтологий формулы g в логике, определяемой системой ϕ. Пусть Mϕ(n) =max { kϕ(g) | ∀g∊Тϕ(n) }: Теорема 1: Если ϕ одна из систем PC, PI, PM и PMon, то log3Mϕ(n)=θ(n). Доказательство основано на получении верхних и нижних оценок Mϕ(n). Для получения нижних оценок в системах PC, PI и PM для любого n ≥ 3 рассмотрим формулы Gn = ((p11⊃p11)∨ ((p12⊃p12) ∨ (…∨ (p1k⊃p1k)...))&(...& ((pt1⊃pt1) ∨ ((pt2⊃pt2) ∨ (…∨ (ptk⊃ptk)...)), где n=2kt-1. Нетрудно убедиться, что ∀i∊ {1...t} подформула gi=((pi1⊃pi1) ∨ ((pi2⊃pi2) ∨ (…∨ (pik⊃pik)...)) имеет k штук различных минимальных, откуда следует, что количество различных минимальных формулы Gn равно k(n+1) / 2k . Если через Аn обозначим формулу p⊃Gn, где p – пропозициональная переменная, отличная от переменных формулы Gn, то количество различных минимальных формулы Аn будет О количестве минимальных тавтологий и свойствах их выводов в ряде систем логик 70 kn / 2k. Не трудно убедиться, что эта функция получает максимальное значение при k=3, а следовательно, Mϕ(n)≥ 3n / 6 для систем PC, PI и PM, в каждой из которых выводимы и сама формула Аn и все ее минимальные. Обозначим через Вn результат подстановки константы Т в формулу Аn вместо всех переменных подформулы Gn, тогда количество различных минимальных тавтологий формулы Вn, а значит и секвенции, получаемой из Вn заменой знака ⊃ на → n, и выводимой в PMon, будет равно kn / 2k. Таким образом, и для системы PMon получаем Mϕ(n)≥ 3n /6, а, следовательно, для всех перечисленных систем ϕlog3Mϕ(n)=0(n). Для получения нетривиальной верхней оценки обратимся к общепринятому представлению пропозициональной формулы в виде дерева, вершинам которого специальным образом приписываются подформулы заданной формулы. Заметим, что построение минимальных тавтологий данной тавтологии заключается в поиске максимального количества подформул, замена которых на переменные, не входящие в данную формулу, сохраняет тавтологичность в данной логике. Отметим, что если в формуле уже выбрана некая подформула, которая должна быть заменена переменной, то ни одна из входящих в нее подформул более не может быть выбрана, что на дереве отражается следующим образом: если выбрана некая вершина, соответствующая формула которой выбрана для замены переменной, то уже ни одна вершина поддерева с корнем в выбранной вершине не может быть выбрана. Если через f(n) обозначить максимально возможное количество подформул (верщин дерева), которые могут быть заменены переменными в формуле длины n (в дереве с n вершинами) и отвлечься от требования тавтологичности, то нетрудно убедиться, что для f(n) получим следующее рекуррентное соотношение: f(1) = 1 f(n) = max(f(n-1) + 1; max ((1 + f(i))(1 + f(n-i-1))). 1≤i≤n-2 Учитывая, что 2n -1 является тривиальной верхней оценкой для функции f(n), а также полученную выше нижнюю оценку, будем искать решение указанного рекуррентного соотношения в виде cαn для наименьшего α в промежутке [31/6, 2] и некоторой константы с, для которых выполнено неравенство: (1 + f(i))(1 + f(n-i-1)))≤(cαi+ 1) ・(cαn-i-1 + 1) = c2αn-1 + c(αi + αn-i-1 ) + 1≤ cαn . Методом приближения получаем f(n) =1 ((3/2)n). Так как Mϕ(n)≤f(n) в любой из выбранных логик, тоlog3Mϕ(n)=1 (n), откуда и следует утверждение теоремы 1. Теорема 2: Секвенциальные системы PC, PI, PM и PMon монотонны. Доказательство теоремы основано на следующем утверждении. Лемма 1: Пусть ϕ одна из систем PC, PI, PM и PMon, φ некоторая тавтология этой системы и + любая из ее минимальных тавтологий в этой системе, тогда вывод секвенциальной формы формулы + в системе ϕ является подвыводом одного из всевозможных выводов секвенциальной формы тавтологии φ в системе ϕ. Доказательство леммы основано на разрешающей процедуре, описанной для PC и PI в пункте (d) теоремы 56 из [7] и выполнимой для всех вышеописанных систем. Действительно, для любой данной секвенцииΓ→ Δ, составленных из пропозициональных формул, и для каждого выбора в качестве главной некоторой формулы из Γ или из Δ, содержащей логический символ, имеется только один или два несходных выбора посылок для вывода Γ→ Δ. Процедура завершается в силу свойства подформульности, которым обладают все правила выводов перечисленных систем и в силу конечного числа A. Aмбарцумян, Г. Гаспарян, С. Ованнисян и А.Чубарян 71 различных подформул выводимых секвенций. Метод доказательства позволяет также строить всевозможные минимальные тавтологии заданной тавтологии. 4. Заключение Все обладающие свойством подформульности системы, исследованные в работах [1-6] и в настоящей работе оказались монотонными, ряд систем без свойства подформульности оказались немонотонными. Заметим также, что все они не строго монотонны. Остается открытым вопрос о монотонности систем Фреге и секвенциальных систем с правилом сечения и о существовании строго монотонных систем, быть может и не полных. Исследование выполнено при финансовой поддержке Государственного комитета по науке МОН РА в рамках научного проекта № 18T-1B034. Литература [1] S. Cook, R. Reckhow, “The relative efficiency of propositional proofs systems”, Journal of Symbolic Logic, vol. 44, pp. 36-50, 1979. [2] A. Chubaryan, G. Petrosyan, “Frege systems are no monotonous”, Evolutio, Естественные науки, Вып. 3, 12-14, 2016. [3] A. Chubaryan, A. Khamisyan, G. Petrosyan, On Some Systems For Two Versions Of Many-Valued Logics and its Properties, Lambert Academic Publishing (LAP), 2017. [4] С. М. Саядян,.А. A. Чубарян, O свойстве немонотонности некоторых систем выводов классического исчисления высказываний, ДНАН РА, Т. 118. No 1, 20- 25, 2018. [5] Г. М. Зограбян, С. М. Саядян и А. А. Чубарян, Исследование свойства монотонности некоторых пропозициональных систем выводов классической и неклассических логик, ДНАН РА, т.119, №1, сс. 33-39, 2019. [6] А. А. Чубарян, С. М. Саядян и Г. М. Зограбян, О свойствах монотонности и строгой монотонности пропозициональных систем резолюций классической и неклассических логик, Sciences of Europe, Physics and Mathematics, vol 2, no. 35, pp. 74-79, 2019. [7] A. Chubaryan, A. Karabakhtsyan and G. Petrosyan, “On some properties of several proof systems for non classical propositional logics”, Вестник РАУ, no. 1, pp. 5-17, 2018. [8] S.C.Kleene, Introduction to Metamathemics, D.VanNostrand Company, INC,1952. [9] А. Чубарян и О.Болибекян, “О секвенциальных системах слабых арифметик”, ДНАН Армении, Прикладная математика, 102, т. 3, 214-218, 2002. [10] 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. О количестве минимальных тавтологий и свойствах их выводов в ряде систем логик 72 Դասական և ոչ դասական տրամաբանությունների մինիմալ նույնաբանությունների քանակի և դրանց արտածումների հատկությունների մասին Արսեն. Ա. Համբարձումյան, Հայկ Ա. Գասպարյան, Սարգիս Ա. Հովհաննիսյան և Անահիտ Ա. Չուբարյան Երևանի պետական համալսարան e-mail: hambardzumyanarsen99@gmail.com, haykgasparyan012@gmail.com, saqohovhannisyan0199@gmail.com, achubaryan@ysu.am Ամփոփում Սույն աշխատանքում ապացուցված է, որ տվյալ տրամաբանության п երկարությամբ նույնաբանությունների մինիմալ նույնաբանությունների մաքսիմալ հնարավոր քանակը կարող է լինել ցուցչային ֆունկցիա п-ից, ինչպես նաև ապացուցված է, որ դասական, ինտուիցիոնիստական, մինիմալ և մոնոտոն տրամաբանությունների յուրաքանչյուր նույնաբանության համար գոյություն ունի այնպիսի մինիմալ նույնաբանություն, որի սեքվենցիալ ձևի արտածման բարդությունը համընկնում է տրված բանաձևի սեքվենցիալ ձևի արտածման նվազագույն քայլերի հետ թվարկված տրամաբանությունների առանց հատույթի կանոնի սեքվենցիալ համակարգերում: Բանալի բառեր` մինիմալ նույնաբանություններ, ասույթային տրամաբանության արտածումների սեքվենցիալ համակարգեր առանց հատույթի կանոնի, արտածման քայլեր,մոնոտոնիկ համակարգեր, խիստ մոնոտոնիկ համակարգեր: A. Aмбарцумян, Г. Гаспарян, С. Ованнисян и А.Чубарян 73 On the Numbers of Minimal Tautologies and Properties of Their Proofs in Classical and Nonclassical Logic Arsen A.Hambardzumyan, Hayk A. Gasparyan, Sarkis A. Hovhannisyan, Anahit A. Chubaryan Yerevan State University e-mail: hambardzumyanarsen99@gmail.com, haykgasparyan012@gmail.com, saqohovhannisyan0199@gmail.com, achubaryan@ysu.am Abstract It is proved in this paper that the number of minimal tautologies for any given logic tautology of size п can be an exponential function in п, and it is also proved that for every tautology of the given logic there is some minimal tautology such that the number of its sequential form proof steps is equal to minimal steps in the proof of sequential form for the given tautology in cut-free sequent systems for classical, intuitionistic, Joganssons and monotone logics. Keywords: Minimal tautology, Cut-free sequent proof systems of propositional logic, Steps of proof, Monotonous system, Strong monotonous system. Submitted 15.06.2019, accepted 22.10.2019.