Упрощение процедуры поиска вывода в натуральных исчислениях для классической логики высказываний и силлогистических систем на базе классической логики высказываний

Кандидат философских наук, кафедра философии естественных факультетов, Московский государственный университет имени .

УПРОЩЕНИЕ ПРОЦЕДУРЫ ПОИСКА ВЫВОДА В НАТУРАЛЬНЫХ ИСЧИСЛЕНИЯХ ДЛЯ КЛАССИЧЕСКОЙ ЛОГИКИ ВЫСКАЗЫВАНИЙ И СИЛЛОГИСТИЧЕСКИХ СИСТЕМ НА БАЗЕ КЛАССИЧЕСКОЙ ЛОГИКИ ВЫСКАЗЫВАНИЙ.

Аннотация

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

Ключевые слова: натуральные исчисления, алгоритм поиска вывода, детерминированный алгоритм, сложность, структурная сложность

Keywords: natural deduction calculi, proof searching algorithm, deterministic algorithm, complexity, structural complexity.

в 2008 году [1] предложил вариант натурального исчисления высказываний для классической логики с упрощенной процедурой поиска вывода. Указанный алгоритм поиска вывода сформулирован в [4].

Приведем формулировку натурального субординатного исчисления для классической логики высказываний (сокращенно – КЛВ). Алфавит исчисления и понятие формулы задаются стандартным образом. Формулировка приводится по [3, 129]

Субординатное натуральное исчисление для КЛВ.

Непрямые правила вывода:

(1) , где С – последнее неисключенное допущение в выводе; все формулы, начиная с C и заканчивая предшественником С⊃B, должны быть исключены из дальнейшего построения вывода; обозначать исключение формул будем с помощью пунктирных линий.

(2) , где С – последнее неисключенное допущение в выводе; все формулы, начиная с C и заканчивая предшественником ØС, должны быть исключены из дальнейшего построения вывода. Исключенные формулы будем отмечать прямой вертикальной линией.

Прямые правила вывода:

(3) (4) (5) (6) (7)

(8) (9) (10)

Определим понятие вывода в указанном выше исчислении. Выводом формулы А из множества посылок Γ (Γ ⊢ А) в данном исчислении называется непустая конечная последовательность формул, удовлетворяющая следующим условиям:

·  каждая формула есть либо посылка, либо произвольное допущение, либо получена из предыдущих по одному из правил вывода; в случае применения непрямого правила вывода происходит исключение из процесса дедукции соответствующих формул;

·  последний член последовательности графически равен А.

·  в завершенном выводе (А является последней формулой вывода, согласно п.2) все допущения исключены.

Доказательством называется вывод формулы из пустого множества посылок Γ.

В исчислении, сконструированном , происходит отказ от традиционных правил введения дизъюнкции справа и слева в силу того, что такая трактовка указанного правила придает процедуре поиска вывода недетерминированность (алгоритм не «знает» точно, какой именно дизъюнкт нужно получать, и его выбор носит случайный характер, а время поиска вывода существенно увеличивается; часто это сопровождается усложнением структуры самого вывода).

устраняет данную недетерминированность за счет замены правил (4) и (5) непрямым правилом (∨'i) ,

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

Данное правило (∨') формулирует дизъюнкцию в импликативных терминах (используя классическое соотношение между дизъюнкцией и импликацией: A∨B ⇔ A⊃B и придает процедуре поиска вывода строгую детерминированность и, следовательно, понижает временную сложность алгоритма во многих (но не во всех – об исключениях будет сказано ниже) случаях, когда требуется вывести/доказать дизъюнктивную формулу.

Хотя правило (∨'i) является непрямым, оно не усложняет, а во многих случаях даже упрощает структуру вывода, например, в случае доказательства теоремы ⊢(p∨(q∨r))⊃(q∨(r∨p)). При доказательстве этой теоремы с использованием прямых правил введения дизъюнкции мы получаем следующую последовательность формул:

1.p∨(q∨r) – доп.
	2.(q∨ (r ∨p)) – доп.
	3.p – доп.
	4. p - e: 3
	5.r∨p - ∨2i: 4
	6.q∨(r ∨p) - ∨2i: 5
	7.p - i: 2, 6
	8.p - e: 7
	9.q ∨ r - ∨e: 1, 8
		10.q – доп.
		11.q - e: 10
		12.q ∨ (r ∨p) - ∨1i: 11
	13.q - i: 2, 12
	14.q - e: 13
	15.r - ∨e: 9, 14
	16.r ∨ p - ∨1i: 15
	17.q ∨ (r ∨p) - ∨2i: 16
18.(q∨ (r∨p)) - i: 2, 17
19. q∨(r∨p) - e: 18
20.( p∨(q∨r))⊃( q∨(r ∨p)) - ⊃i: 19

При доказательстве с использованием правила (∨'i) мы получаем такое доказательство:

1. p∨(q∨r) – доп.
	2. q – доп.
		3. r– доп.
			4. p– доп.
			5. q∨r - ∨e: 1, 4
			6. r - ∨e: 5, 3
		7. p - Øi: 6, 2
		8. p - Øe: 7
	9. r∨p - ∨'i: 8
10. q∨(r∨p) - ∨'i: 9
11. (p∨ (q ∨ r))⊃(q∨ (r ∨ p)) - ⊃i: 10

Очевидно, что второе доказательство является более коротким и простым.

Далее конструктивно доказывает дедуктивную эквивалентность натуральных систем с правилами (∨1) и (∨2) и (∨'i) соответственно, тем самым обосновывая правомерность такой замены.

В данной работе я приведу свою формулировку натуральных исчислений для КЛВ и силлогистических систем на базе КЛВ с непрямым правилом введения дизъюнкции, которое также сохраняет детерминированность поиска вывода в этом направлении (при обосновании/доказательстве дизъюнктивных формул), а во многих случаях дает структурно более простые выводы, чем системы с правилом (∨'i). Отмечу, что построенные мною системы являются "рабочими" и тестировались с помощью программы Syllogistic Deductio (подробное описание программы Syllogistic Deductio приведено в [2]), на репрезентативном (от фр. множестве формул.

В силу того, что программа Syllogistic Deductio позволяет в определенных пределах изменять множество дедуктивных постулатов (это доступно любому пользователю, так как множество правил вывода является внешним по отношению к программе и задается на языках логики высказываний и силлогистики в текстовых файлах, прилагающихся к программе – подробнее см. [2]), не затрагивая структуру самого алгоритма поиска вывода, перестройка систем происходит быстро и "безболезненно",без участия программиста, и пользователь может выбрать "старую" или "новую" систему для дедукции, по своему усмотрению[1].

Далее, я приведу доказательство дедуктивной эквивалентности моей системы и системы и, как следствие, традиционной системы.

Итак, для построения системы КЛВ+ (так назовем мою дедуктивную систему) мы устраняем из дедуктивных постулатов системы правила (∨1) и (∨2) (пользователь стирает соответствующие правила вывода из текстового редактора) и добавляем дополнительные аналитические правила вывода[2]: ∨e1

и ∨e2

(пользователь делает то же самое в текстовом файле).

Таким образом, вывод дизъюнктивных формул осуществляется от противного с использованием правил де Моргана. Покажем на примерах, что такая модификация процедуры поиска вывода дает выводы не длиннее, чем при использовании системы , а в значительном числе случаев не только не усложняет, но и упрощает сложность структуры самих выводов.

Примеры.

Построим вывод формулы (((p∨s)∨r)∨q)⊃(((q∨r)∨p)∨s) в системе

1. ((p∨s)∨r)∨q– доп.
	2. ((q∨r)∨p)– доп.
		3.s– доп.
			4. (q∨r) – доп.
				5. p– доп.
					6. q – доп.
						7.r – доп.
							8.((p∨s)∨r) – доп.
							9. (p∨s)∨r–e: 8
								10. (p∨s) – доп.
								11. p∨s –e: 10
								12. s–∨e: 11, 5
							13. (p∨s) –i: 12, 3
							14. (p∨s) –e: 13
							15. r –∨e: 9, 14
						16. ((p∨s)∨r) –i: 15, 7
						17. ((p∨s)∨r) –e: 16
						18. q–∨e: 1, 17
					19. r –i: 18, 6
					20. r –e: 19
				21. q∨r –∨’i: 20
			22. p–i: 21, 4
			23. p–e: 22
		24. (q∨r)∨p –∨’i: 23
	25. s –i: 24, 2
	26. s–e: 25
27. ((q∨r)∨p)∨s –∨’i: 26
p∨s)∨r)∨q)⊃(((q∨r)∨p)∨s) –⊃i: 27

Теперь построим вывод этой же формулы в системе КЛВ+.

1. ((p∨s)∨r)∨q – доп
	2. (((q∨r)∨p)∨s) – доп
	3. ((q∨r)∨p) - ∨e1: 2
	4. s - ∨e2: 2
	5. p -∨e1: 3
	6. (q∨r) - ∨e1: 3
	7. r--- ∨e2: 2
	8. q--- ∨e1: 6
		9. ((p∨s)∨r) – доп
		10. (p∨s)∨r - e: 9
			11. (p∨s) – доп
			12. p∨s - e: 11
			13. s - ∨e1: 12, 5
		14. (p∨s) - i: 4, 13
		15. (p∨s) - e: 14
		16. r - ∨e1: 1,15
	17. ((p∨s)∨r) - i: 7, 16
	18. ((p∨s)∨r) - e: 17
	19. q - ∨e1: 1,18
q∨r)∨p)∨s) - i: 8, 19
21. ((q∨r)∨p)∨s - e: 20
p∨s)∨r)∨q)⊃(((q∨r)∨p)∨s) - ⊃i: 21

Как мы видим, второй вывод является более коротким (22 шага вместо 28) и структурно более простым: мы строим только 4 вспомогательных подвывода вместо 9. Длины самих доказательств примерно одинаковы: около 114 и 110 символов.

Следует отметить, что выводы, построенные в КЛВ+, почти всегда являются структурно более простыми, чем в системе с правилом (∨'); длина выводов обычно одинакова, как в вышеприведенном примере, или различается не слишком значительно. Однако требование структурной простоты также является существенным.

Рассмотрим, к примеру, доказательство следующей теоремы ⊢(p∨(q∨r))⊃((p∨q)∨r) в системе КЛВ+.

1. p∨(q∨r) – доп.
	2. ((p∨q)∨r) – доп.
	3. (p∨q) - ∨e1: 2
	4. r - ∨e2: 2
	5. p - ∨e1: 3
	6. q - ∨e1: 3
	7. q∨r - ∨e1: 1, 5
	8. r - ∨e1: 6, 7
9. ((p∨q)∨r) - i: 4, 8
10. (p∨q)∨r - e: 9
11. (p∨(q∨r))⊃((p∨q)∨r) - ⊃i: 10

Приведем ее доказательство в системе

1. p∨(q∨r) – доп.
	2. (p∨q) – доп.
		3. r – доп.
			4. p – доп.
				5. p – доп.
					6. q – доп.
				7. q - i: 4, 5
				8. q - e: 7
			9. p∨q - ∨’i: 8
		10. p - i: 2, 9
		11. q∨r - ∨e1: 1, 10
			12. q – доп
				13. p – доп
			14. p∨q - ∨’i: 12
		15. q - i: 2, 14
		16. r - ∨e1: 1, 5
	17. r - i: 3, 16
	18. r - e: 17
19. (p∨q)∨r - ∨’i: 18
20. (p∨(q∨r))⊃((p∨q)∨r) - ⊃i: 19

Первый вывод гораздо проще второго в структурном отношении: 2 подвывода вместо 8. Длины доказательств вновь различаются несущественно: 32 и 41 символ, соответственно.

Отметим еще раз, что структурная простота логических и математических объектов также является важной характеристикой при условии, что длина доказательств (по которой традиционно измеряется сложность алгоритмов поиска вывода) в большинстве случаев примерно одинакова или различается незначительно.

Теперь приведем доказательство дедуктивной эквивалентности системы КЛВ+ и системы По транзитивности отношения дедуктивной эквивалентности и результату , система КЛВ+ будет дедуктивно эквивалентна традиционной натуральной системе КЛВ.

Докажем, что все натуральные выводы, которые можно построить с помощью правила (∨'i), можно построить путем применения метода доказательства от противного и с помощью правил де Моргана.

Итак, пусть у нас имеется незавершенный вывод вида:

+n.ØA

.

.

n+l. B

Если бы мы могли применить правило (∨'), то мы бы, исключив из процесса вывода все формулы с номерами n – n+1, ввели бы искомую формулу A∨B. Теперь достроим данный вывод с помощью метода доказательства от противного и правил де Моргана, которые были добавлены нами в качестве новых дедуктивных постулатов системы КЛВ+.

+n.ØA – доп.

.

.

n+l. B

n+l+1. ØA⊃B - ⊃i: n+l

+n+l+2. Ø( A∨B) – доп

n+l+3. ØA – Øe1: n+l+2

n+l+4. ØB – Øe2: n+l+2

n+l+5. B - ⊃e: n+l+1, n+l+3

n+l+6. ØØ( A∨B) – Øi: n+l+4, n+l+5

n+l+7. A∨B– Øe: n+l+6

Утверждение «влево» доказано.

Теперь обоснуем обратное утверждение: все выводы, которые можно построить путем применения метода доказательства от противного и с помощью правил де Моргана, можно получить с использованием правила (∨').

Пусть у нас имеется незавершенный вывод вида:

+n.Ø(A∨B) – доп.

Если бы мы могли применить правила де Моргана Øe1 и Øe2, то, в силу того, что, по условию, мы обосновываем выводимую/доказуемую формулу, через некоторое конечное число шагов мы бы получили необходимое нам противоречие и смогли бы применить правило введения отрицания, проведя доказательство методом от противного. Теперь достроим данный вывод с помощью правила (∨').

+n.Ø(A∨B) – доп.
	+n+1.ØA– доп.
	.
	.
	n+1+l. B – формула получена с помощью допущения ØA (№ n+1) и соответствующих правил вывода прямо, без введения новых допущений или она уже была в выводе до введения допущения ØA; в последнем случае l = 1.
	n+l+2. A∨B – ∨’i: n+l+1
	n+l+3. ØØ( A∨B) – Øi: n, n+l+2
	n+l+4. A∨B – Øe: n+l+3.

В случае, когда мы получаем формулу B методом от противного, вывод будет выглядеть следующим образом:

+n.Ø(A∨B) – доп.
	+n+1.ØA– доп.
		+n+2.ØB– доп.
		.
		.
		n+2+l. ⊥ (где ⊥ – условное обозначение для противоречия, полученного при участии формул ØA (n+1) и/или ØB (n+2)).
	n+l+3. ØØB – Øi: n+2+l.
	n+l+4. B – Øe: n+l+3
n+l+5. A∨B – ∨’i: n+l+4
n+l+6. ØØ( A∨B) – Øi: n+l+5, n
n+l+7. A∨B – Øe: n+l+6.

Утверждение «вправо» доказано.

Обе системы – КЛВ+ и система дедуктивно эквиваленты.

Используя транзитивность отношения дедуктивной эквивалентности, можем утверждать дедуктивную эквивалентность традиционной натуральной системы КЛВ куайновского типа, как она была сформулирована , , и системы КЛВ+. Доказательство данного утверждения можно провести прямо, и в силу того, что оно является несложным, мы предоставим его читателю.

Как мы видим, система КЛВ+, система и традиционная натуральная система КЛВ дедуктивно эквивалентны. Силлогистические системы, подпадающие под действие алгоритма, лежащего в основе Syllogistic Deductio, переформулируются аналогично КЛВ+, так как их пропозициональные части полностью совпадают с пропозициональной частью КЛВ+, а силлогистические части указанным преобразованием не затрагиваются. Эффективность и корректность работы Syllogistic Deductio относительно данных систем полностью сохраняется, в силу дедуктивной эквивалентности старых и новых вариантов.

Однако существует целый класс примеров, на которых различие между системой и традиционной системой КЛВ проступает особенно ярко; таким образом, на данном классе примеров недетерминированный алгоритм поиска вывода для традиционной системы КЛВ оказывается более эффективным, чем указанные детерминированные алгоритмы – и КЛВ+.

Такими «парадоксальными» примерами являются формулы вида: p⊃(p∨(q∨(r∨(p1∨p2)))) и т. п. (чем больше дизъюнктов, тем «хуже»); (p&((q&r)&p1))⊃(p∨(q∨(r∨(p1∨p2)))) и тому подобные формулы, где литерал, по которому вводится дизъюнкция, запрятан не слишком глубоко в антецеденте и поэтому не может создать проблем недетерминированному (по введению дизъюнкции) алгоритму поиска вывода.

Продемонстрируем данный факт. Построим доказательство формулы: p⊃(p∨(q∨(r∨(p1∨p2)))) в традиционной системе КЛВ (с помощью соответствующего алгоритма поиска вывода), а затем соответствующие доказательства в системах Маркина и КЛВ+.

Вывод в традиционной системе КЛВ:

1. p – доп.

2. p∨(q∨(r∨(p1∨p2))) - ∨1i: 1

3. p⊃(p∨(q∨(r∨(p1∨p2)))) - ⊃i: 2

Вывод в системе КЛВ+:

1. p – доп.
	2. (p∨(q∨(r∨(p1∨p2)))) – доп.
	3. p - ∨e1: 2
	4. (p∨(q∨(r∨(p1∨p2)))) - i: 1, 3
	5. p∨(q∨(r∨(p1∨p2))) - e: 4
	6. p⊃(p∨(q∨(r∨(p1∨p2)))) - ⊃i: 5

Вывод в системе :

1. p – доп
	2. p – доп
		3. q – доп[3]
			4. r – доп
				5. p1 – доп
					6. p2 – доп
				7. p2 - i: 1, 2
				8. p2 - e: 8
			9. p1∨p2 - ∨’i: 8
		10. r∨(p1∨p2) - ∨’i: 9
	11. q∨(r∨(p1∨p2)) - ∨’i: 10
12. p∨(q∨(r∨(p1∨p2))) - ∨’i: 11
14. p⊃(p∨(q∨(r∨(p1∨p2)))) - ⊃i: 12

Как мы видим, «традиционное» не только является существенно более коротким (и менее сложным), но и структурно более простым, чем доказательства в системах без прямого правила введения дизъюнкции. Кроме того, работа со списком целей, проводимая алгоритмом при доказательстве подобных теорем, также минимальна: взятие первого дизъюнкта в качестве цели сразу же приводит к успеху и алгоритм не «петляет». Так же дело обстоит и с примерами вида (p&((q&r)&p1))⊃(p∨(q∨(r∨(p1∨p2)))) и др. Доказательство для КЛВ+ является структурно существенно более простым (2 допущения вместо 6), чем для системы ; сложность, измеряемая числом знаков доказательства, абсолютно одинакова.

Таким образом, мы видим, что все предложенные выше стратегии поиска вывода не являются универсальными для решения задачи доказательства теорем КЛВ: на каких-то примерах одни стратегии работают лучше, а другие – хуже, и наоборот; выбор между ними, скорее всего, должен осуществляться по числу классов задач, которые данная стратегия решает наиболее эффективно. Однако тезис о неравенстве классов P и NP пока не опровергнут.

Литература

1.  Маркин классического натурального исчисления высказываний с упрощенной процедурой поиска вывода: Материалы X Общероссийской научной конференции "Современная логика: проблемы теории, истории и применения в науке". Стр. 289 – 293 / Издательство СПбГУ, С-Пб, 2008. – 501 с.

2.  Красненкова поиска вывода для систем негативной силлогистики. Диссертация на соискание ученой степени кандидата философских наук. Специальность 09.00.07 – Логика. М., 2009. На правах рукописи.

3.  , Маркин логики. Учебник. ИНФРА-М, М., 2002. – 296 с.

4.  , , – Алгоритм поиска вывода в классической пропозициональной логике / Труды научно-исследовательского семинара логического центра института философии РАН. Издательство ИФРАН, М., 1996 г. – 109 с.

[1]Таким образом, при указанных преобразованиях «жесткое ядро» алгоритма и, соответственно, программы остается неизменным.

Если бы мы попытались сформулировать новую дедуктивную систему с непрямым правилом введения дизъюнкции (∨'i), используя алгоритм, предложенный в [2], то нам пришлось бы изменять «жесткое ядро» алгоритма, определенным образом перестраивать его, так как заложенная в нем концепция работы с непрямыми правилами вывода не позволяет задавать их так, как это делает : его «расширение» понятия непрямого правила вывода оказывается критическим для нашего алгоритма.

[2] Под аналитическими правилами вывода будем понимать, в соответствии с соглашениями, принятыми в [2], такие правила вывода, в которых пропозициональная (либо терминная, в случае силлогистических правил вывода) сложность заключения нестрого меньше сложности большей посылки. Т. е. при применении аналитических правил вывода у нас не происходит приращения сложности.

[3] Если требуемый правый дизъюнкт, в свою очередь, сам является дизъюнктивной формулой, то мы должны получать его именно как дизъюнктивную формулу, через правило ∨’i, а не от противного.