Спец_главы_математики

(з) ¡¡``Ã (выведение из противоречия);

(и)¡; ' ` (контрапозиция);

¡` :'

	(к)	¡ ` '	(контрапозиция);
		¡; :' `
	(л)	¡; ' ` Ã		(контрапозиция);
		¡; :Ã ` :'

(м)¡; :Ã ` :' (доказательство от противного);

¡; ' ` Ã

(н)	'0; : : : ; 'n ` Ã	(введение ^ и !);
	` (('0 ^ : : : ^ 'n) ! Ã)
(о)	` (('0 ^ : : : ^ 'n) ! Ã)	(удаление ^ и !).
	'0; : : : ; 'n ` Ã

Д о к а з а т е л ь с т в о. Допустимость правила ¡; '; ' ` Ã пока-

зывается следующим деревом:

¡; ' ` Ã

	' ` '	11;12	¡; '; ' ` Ã	7
	¡; ' ` ';		¡; ' ` ' ! Ã
				8:
		¡; ' ` Ã

Допустимость правила (а) следует из допустимости указанного правила с помощью правил 11 и 12. Допустимость правила (б) вытекает из правил (а), (ж) и (з).

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

Ясно, что секвенция ¡ ` может быть получена лишь применением правила 10. Поэтому из доказуемости секвенции ¡ ` следует доказуемость секвенций ¡ ` ' и ¡ ` :' для некоторой формулы '. Учитывая доказуемость последних секвенций, дерево

	¡ ` '		12	¡ ` :'		12
	¡; :Ã ` ';			¡; :Ã ` :'
						10
		¡; :Ã `			9
		¡ ` Ã

устанавливает доказуемость секвенции ¡ ` Ã. ¤

11

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

Например, следующее дерево устанавливает доказуемость секвенции (' ! Ã); :Ã ` :':

' ` ' (' ! Ã) ` (' ! Ã) (' ! Ã); ' ` ';11;12 (' ! Ã); ' ` (' ! Ã)12

				8
	(' ! Ã); ' ` Ã		л
		(' ! Ã); :Ã ` :':

Правило называется равносильным, если доказуемость (единственной) секвенции, стоящей над чертой, равносильна доказуемости секвенции, стоящей под чертой. Из предложения 1.2.2 вытекает, что следующие правила равносильны: 9, 11, (г), (д), (ж), (и), (к), (л), (м), (н), (о).

Пусть V = fPi j i 2 !g множество всех пропозициональных переменных ИС, F множество всех формул ИС. Любая функция s : V ! F называется подстановкой пропозициональных переменных. Для любой формулы ' 2 F обозначим через s(') формулу, получающуюся из ' заменой всех пропозициональных переменных P , входящих в ', на формулы s(P ).

П р и м е р 1.2.2. Если s(P0) = P1 _ :P2, s(P1) = P1 ! :P3, ' =

:P0 ^ P1, то s(') = :(P1 _ :P2) ^ (P1 ! :P3). ¤

Для любой секвенции (последовательности формул) R обозначим через s(R) секвенцию (последовательность формул), получающуюся из R заменой всех пропозициональных переменных P , входящих в R, на формулы s(P ).

Таким образом, отображение s естественным образом расширяется на множество всех выражений исчисления ИС.

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

Теорема 1.2.3. (теорема о подстановке). Если s подстановка,

R секвенция, то s(RR) допустимое правило. ¤

12

§ 1.3. Эквивалентность формул

Для любых формул ' и Ã ИС обозначим через (' $ Ã) формулу ИС ((' ! Ã) ^ (Ã ! ')). Напомним, что таблица истинности последней формулы совпадает с таблицей истинности формулы алгебры логики (' $ Ã).

Лемма 1.3.1. Секвенция ¡ ` (' $ Ã) доказуема тогда и только тогда, когда доказуемы секвенции ¡; ' ` Ã и ¡; Ã ` '.

Д о к а з а т е л ь с т в о. Предположим, что секвенция ¡ ` (' $ Ã) доказуема. Тогда доказуемость секвенции ¡; ' ` Ã устанавливается следующим деревом:

' ` ' ¡ ` (' ! Ã) ^ (Ã ! ')

				11;12				2
	¡; '	`	';		¡`'!Ã		12
						¡;'`'!Ã			8
					¡; ' ` Ã

Доказуемость секвенции ¡; Ã ` ' показывается аналогично. Установим теперь доказуемость секвенции ¡ ` (' $ Ã), предпола-

гая, что секвенции ¡; ' ` Ã и ¡; Ã ` ' доказуемы:

	¡; ' ` Ã	7	¡; Ã ` '	7
	¡ ` ' ! Ã;		¡ ` Ã ! '
				1: ¤
	¡ ` (' ! Ã) ^ (Ã ! ')

Формулы ' и Ã называются эквивалентными (обозначается ' ´ Ã), если в ИС доказуемы секвенции ' ` Ã и Ã ` '.

В силу леммы 1.3.2 условие ' ´ Ã равносильно доказуемости секвенции ` (' $ Ã). Покажем, что отношение ´ образует отношение эквивалентности на множестве формул.

Лемма 1.3.2. Для любых формул ', Ã и Â исчисления ИС справедливы следующие утверждения:

(а) ' ´ ';

(б) если ' ´ Ã, то Ã ´ ';

(в) если ' ´ Ã и Ã ´ Â, то ' ´ Â.

Д о к а з а т е л ь с т в о. В пункте (а) доказывать нечего, поскольку ' ` ' аксиома. Пункт (б) следует из симметричности в определении отношения ´. Пункт (в) вытекает из правила сечения (предложение 1.2.2, в). ¤

Установим, что эквивалентность формул сохраняется под действием операций :, ^, _ и !.

Лемма 1.3.3. Если '1 ´ Ã1 и '2 ´ Ã2, то :'1 ´ :Ã1, ('1 ^ '2) ´ (Ã1 ^ Ã2), ('1 _ '2) ´ (Ã1 _ Ã2) и ('1 ! '2) ´ (Ã1 ! Ã2).

13

Д о к а з а т е л ь с т в о. В силу симметричности отношения ´ до-

статочно доказать секвенции :'1 ` :Ã1, ('1 ^ '2) ` (Ã1 ^ Ã2), ('1 _ '2) ` (Ã1 _ Ã2) и ('1 ! '2) ` (Ã1 ! Ã2), а доказуемость этих секвенций устанавливается следующими деревьями:

¡; Ã1 ` '1 (контрапозиция);

¡; :'1 ` :Ã1

'1 ^ '2 ` '1 ^ '2

'1 ` Ã1

'1 ^ '2 ` '1 ^ '2

'2 ` Ã2

'1 ^ '2 ` '1;

` '1 ! Ã1

'1 ^ '2 ` '2;

` '2 ! Ã2

'1 ^ '2 ` Ã1;

'1 ^ '2 ` Ã2

;

'1 ^ '2 ` Ã1 ^ Ã2

'1`Ã1

'2`Ã2

'1 _ '2

` '1 _ '2

;

'1`Ã1_Ã2;

'2`Ã1_Ã2;

'1 _ '2 ` Ã1 _ Ã2

Ã1 ` '1; '1 ! '2 ` '1 ! '2

'2 ` Ã2

'1 ! '2; Ã1 ` '2;

` '2 ! Ã2

: ¤

'1 ! '2; Ã1 ` Ã2

'1 ! '2 ` Ã1 ! Ã2

Формула Ã исчисления ИС называется подформулой формулы ' исчисления ИС, если Ã является подсловом слова '. Место, которое занимает подформула Ã в формуле ', называется вхождением Ã в формулу '.

П р и м е р 1.3.1. Формула A имеет два вхождения в формулу ', имеющую вид A _ (A ! B ^ C) ! D. Следующие формулы образуют множество всех подформул формулы ': A, B, C, D, B ^C, A ! B ^C,

A _ (A ! B ^ C), '. ¤

Теорема 1.3.4. (теорема о замене). Пусть ' формула исчисления ИС, Ã ее подформула, а формула '0 получается из ' заменой некоторого вхождения Ã на формулу Ã0. Тогда если Ã ´ Ã0, то

'´ '0.

До к а з а т е л ь с т в о. Если ' = Ã, то доказывать нечего. Если

'6= Ã, то используем индукцию по числу шагов построения формулы '. Предполагая, что ' пропозициональная переменная, снова получаем ' = Ã. Индукционный переход осуществляется рассмотрением

четырех случаев: ' = :'1, ' = '1 ^ '2, ' = '1 _ '2, ' = '1 ! '2. В каждом из этих случаев формула Ã входит в '1 или '2. Поэтому

эквивалентность ' ´ '0 вытекает из индукционного предположения и леммы 1.3.3. ¤

14

§1.4. Нормальные формы

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

Лемма 1.4.1. Пусть ', Ã и Â формулы ИС. Тогда справедливы следующие эквивалентности:

(а) ('^Ã)^Â ´ '^(Ã^Â), ('_Ã)_Â ´ '_(Ã_Â) (ассоциативность ^ и _);

(б) ' ^ Ã ´ Ã ^ ', ' _ Ã ´ Ã _ ' (коммутативность ^ и _);

(в) ' ^ ' ´ ', ' _ ' ´ ' (идемпотентность ^ и _);

(г) ' ^ (Ã _ Â) ´ (' ^ Ã) _ (' ^ Â), ' _ (Ã ^ Â) ´ (' _ Ã) ^ (' _ Â)

(законы дистрибутивности);

(д) ' ^ (' _ Ã) ´ ', ' _ (' ^ Ã) ´ ' (законы поглощения);

(е) :(' ^ Ã) ´ :' _ :Ã, :(' _ Ã) ´ :' ^ :Ã (законы де Моргана);

(ж) ::' ´ ' (закон двойного отрицания);

(з) ' ! Ã ´ :' _ Ã.

Д о к а з а т е л ь с т в о. Мы приведем доказательства эквивалентностей ' ^ (Ã _ Â) ´ (' ^ Ã) _ (' ^ Â) и ' ! Ã ´ :' _ Ã, оставив остальные утверждения читателю в качестве упражнения:

'^(Ã_Â)`'; Ã`Ã

'^(Ã_Â)`'; Â`Â

'^(Ã_Â);Ã`'^Ã

'^(Ã_Â);Â`'^Â

' ^ (Ã _ Â) ` Ã _ Â

'^(Ã_Â);Ã`('^Ã)_('^Â);

'^(Ã_Â);Â`('^Ã)_('^Â);

;

' ^ (Ã _ Â) ` (' ^ Ã) _ (' ^ Â)

'^Ã`';

'^Ã`Ã

'^Â`';

'^Â`Â

'^Ã`Ã_Â

'^Â`Ã_Â

('^Ã)_('^Â)`('^Ã)_('^Â)

'^Ã`'^(Ã_Â);

'^Â`'^(Ã_Â);

;

(' ^ Ã) _ (' ^ Â) ` ' ^ (Ã _ Â)

' ` '; ' ! Ã ` ' ! Ã

:' ` :'

'

' ! Ã; ' ` Ã

Ã;

`

'

_ :

'

!

Ã; '

` :

'

_

:

'

` :

'

_

Ã;

;

' ! Ã ` : ' _ Ã

' ` '; :' ` :'

'; :' `

Ã

`

Ã;

'

Ã

` :

'

_

Ã

';

:

'

`

Ã;

: _

: ¤

:' _ Ã; ' ` Ã

:' _ Ã ` ' ! Ã

15

Напомним, что литерой называется любая атомарная формула A, обозначаемая через A1, или ее отрицание :A, которое обозначается через A0. Конъюнктом (дизъюнктом) называется литера или конъюнкция (соответственно дизъюнкция) литер. Конъюнкт или дизъюнкция конъюнктов называется дизъюнктивной нормальной формой (ДНФ), а дизъюнкт или конъюнкция дизъюнктов конъюнктивной нормальной формой (КНФ).

Следующая теорема является аналогом теоремы о приведении формул алгебры логики к дизъюнктивным и конъюнктивным нормальным формам.

Теорема 1.4.2. Любая формула ИС эквивалентна некоторой ДНФ и некоторой КНФ.

Алгоритм приведения формулы ИС к ДНФ аналогичен алгоритму приведения формул алгебры логики к ДНФ и опирается на лемму 1.4.1.

1.Выражаем согласно пункту (з) леммы 1.4.1 все импликации, участвующие в построении формулы, через дизъюнкции и отрицания.

2.Используя законы де Моргана (лемма 1.4.1, п. (е)), переносим все отрицания к переменным и сокращаем двойные отрицания по закону двойного отрицания (лемма 1.4.1, п. (ж)).

3.Используя закон дистрибутивности ' ^ (Ã _ Â) ´ (' ^ Ã) _ (' ^ Â), преобразуем формулу так, чтобы все конъюнкции выполнялись раньше дизъюнкций.

В результате применения пп. 1–3 получается ДНФ данной формулы.

Приведение формулы к КНФ производится аналогично приведению

еек ДНФ c применением закона дистрибутивности ' _ (Ã ^ Â) ´ (' _

Ã) ^ (' _ Â). ¤

§ 1.5. Семантика исчисления секвенций

Пусть X некоторое множество, fX отображение, которое каждой пропозициональной переменной ставит в соответствие некоторое подмножество множества X. Расширим по индукции отображение fX до отображения множества формул ИС в булеан P(X) множества X согласно следующим соотношениям:

fX(:') = X n fX('),

fX(' ^ Ã) = fX(') \ fX(Ã), fX(' _ Ã) = fX(') [ fX(Ã), fX(' ! Ã) = fX(:') [ fX(Ã).

16

Любое такое отображение fX, действующее на множестве формул ИС, называется интерпретацией ИС в X.

Каждой секвенции S следующим образом ставится в соответствие некоторое утверждение fX(S) о подмножествах X:

fX('1; : : : ; 'n ` Ã) , fX('1) \ : : : \ fX('n) µ fX(Ã), fX(` Ã) , fX(Ã) = X,

fX('1; : : : ; 'n `) , fX('1) \ : : : \ fX('n) = ?, fX(`) , X = ?.

Теорема 1.5.1. Для любой интерпретации fX ИС и любой доказуемой в ИС секвенции S справедливо утверждение fX(S).

Д о к а з а т е л ь с т в о. Если S аксиома ' ` ', то истинность утверждения fX(S), имеющего вид fX(') µ fX('), очевидна. В общем случае достаточно доказать, что при переходе по любому из 12 правил вывода из справедливости утверждений fX от секвенций над чертой следует истинность утверждения fX от секвенции под чертой. Покажем, как проверяются указанные переходы на примере первого правила вывода

¡` '; ¡ ` Ã;

¡` (' ^ Ã)

где ¡	= '1; : : : ; 'n. Итак, по условию имеем	n	fX('i) µ fX(') и
		=1
n	n	iT
T	T
i=1 fX	('i) µ fX(Ã). Тогда i=1 fX('i) µ fX(') \ fX(Ã). Следовательно,

Tn fX('i) µ fX(' ^ Ã), т.е. справедливо утверждение fX(¡ ` (' ^ Ã)).

i=1

Проверка остальных переходов аналогична и предоставляется читателю. ¤

Следствие 1.5.2. Исчисление ИС непротиворечиво.

Д о к а з а т е л ь с т в о. Пусть X непустое множество, fX произвольная интерпретация ИС, A некоторая атомарная формула. Покажем, что формула A ^ :A не доказуема в ИС. Действительно,

fX(A ^ :A) = fX(A) \ (X n fX(A)) = ?, откуда с учетом непустоты множества X следует, что утверждение fX(` A^:A) ложно. Тогда по

теореме 1.5.1 секвенция ` A ^ :A не доказуема. ¤

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

17

Определим теперь так называемую главную интерпретацию ИС , которая позволяет составлять таблицы истинности формул. Возьмем в качестве множества X одноэлементное множество f?g. Тогда для любой атомарной формулы A значение fX(A) равно ?, т.е. fX(A) = 0,

или fX(A) равно f?g, т.е. fX(A) = 1 (напомним, что 0 = ?, а 1 = f?g). Придавая переменным x и y значения ff?g(x) ff?g(y) из множе-

ства f0; 1g, получаем таблицы истинности для логических операций

^, _, ! и :.

x	y	(x ^ y)	(x _ y)	(x ! y)	: x
0	0	0	0	1	1
0	1	0	1	1	1
1	0	0	1	0	0
1	1	1	1	1	0

Пусть A1; : : : ; Ak пропозициональные переменные, f отображение множества элементарных формул в f0; 1g. С помощью таблиц истинности логических связок функция f однозначно продолжается на множество формул '(A1; : : : ; Ak), которые строятся из пропозициональных переменных A1; : : : ; Ak и логических связок. При этом для любой формулы ', равной '(A1; : : : ; Ak), значение f(') снова равно 0 или 1. Если f(') = 1 (f(') = 0), то говорят, что формула ' истинна

(ложна) на наборе (f(A1); : : : ; f(Ak)).

Функция f' : f0; 1gk ! f0; 1g, которая каждому набору (±1; : : : ; ±k) 2 f0; 1gk сопоставляет значение истинности формулы ', называется истинностной функцией формулы '. Очевидно, что таблица истинности функции f' совпадает с таблицей истинности формулы '.

Напомним, что формула ' называется тождественно истинной (тождественно ложной), если функция f' тождественно равна единице (тождественно равна нулю).

Секвенция ¡ ` ' называется истинной на наборе (±1; : : : ; ±k) 2 f0; 1gk, если на этом наборе хотя бы одна формула из ¡ ложна или формула ' истинна. Секвенция ¡ ` называется истинной на наборе (±1; : : : ; ±k) 2 f0; 1gk, если на этом наборе некоторая формула из ¡ ложна. Секвенция ` по определению ложна на любом наборе, а истинность секвенции ` ' совпадает с истинностью формулы '.

Секвенция S называется тождественно истинной, если S истинна на любом наборе (±1; : : : ; ±k) значений истинности переменных A1; : : :

: : : ; Ak, среди которых содержатся все переменные, входящие в формулы из S.

18

Теорема 1.5.3. (теорема о полноте). 1. Формула ' ИС доказуема

вИС тогда и только тогда, когда ' тождественно истинна.

2.Секвенция S ИС доказуема в ИС тогда и только тогда, когда S тождественно истинна.

По теореме о полноте для того чтобы установить, доказуема ли секвенция '1; : : : ; 'n ` Ã (или '1; : : : ; 'n `), достаточно составить таблицу истинности формулы '1 ! ('2 ! : : : ! ('n ! Ã) : : :) (или

'1 ! ('2 ! : : : ! ('n ! A0 ^ :A0) : : :)) и проверить ее тождественную истинность. Как известно, существует единый алгоритм построе-

ния таблиц истинности, и, значит, ИС разрешимо.

Следствие 1.5.4. Тогда и только тогда выполняется ' ´ Ã, когда равны истинностные функции f' и fÃ.

Д о к а з а т е л ь с т в о. Предположим, что ' ´ Ã. Тогда по лемме 1.3.2 доказуема формула (' $ Ã). По теореме о полноте получаем тождественную истинность этой формулы, что равносильно соотноше-

нию f' = fÃ.

Обратно, из равенства f' = fà следует тождественная истинность секвенций ' ` à и à ` '. По теореме о полноте эти секвенции доказуемы, и, значит, справедливо ' ´ Ã. ¤

Из следствия 1.5.6 вытекает, что отношение эквивалентности » на формулах алгебры логики и отношение эквивалентности ´ совпадают:

'» Ã , ' ´ Ã:

Пр и м е р 1.5.1. Так как '^Ã » :(:'_:Ã), то '^Ã ´ :(:'_:Ã).

Замечание 1.5.5. Пусть © множество всех формул ИС с пропозициональными переменными из множества I. Рассмотрим алгебру F = h©; ^; _; :; A^:A; A_:Ai, где A некоторая фиксированная переменная. Тогда фактор-алгебра F= ´ является булевой алгеброй, называемой алгеброй Линденбаума для ИС.

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

Теорема 1.5.6. Исчисление ИС независимо. ¤

19

§1.6. Исчисление высказываний гильбертовского типа

Вэтом параграфе мы построим исчисление ИВ, в котором в отличие от ИС не используется понятие секвенции, правило вывода одно, а схем аксиом несколько.

Формулами ИВ называются формулы ИС.

Аксиомами ИВ являются следующие формулы для любых формул

', Ã, Â:

1)' ! (Ã ! ');

2)(' ! Ã) ! ((' ! (Ã ! Â)) ! (' ! Â));

3)(' ^ Ã) ! ';

4)(' ^ Ã) ! Ã;

5)(' ! Ã) ! ((' ! Â) ! (' ! (Ã ^ Â)));

6)' ! (' _ Ã);

7)' ! (Ã _ ');

8)(' ! Â) ! ((Ã ! Â) ! ((' _ Ã) ! Â));

9)(' ! Ã) ! ((' ! :Ã) ! :');

10)::' ! '.

Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.

Единственным правилом вывода в ИВ является правило заключения (modus ponens): если ' и ' ! Ã выводимые формулы, то Ã также выводимая формула. Символически это записывается так:

'; ' ! Ã:

Ã

Например, если высказывания A^B и A^B ! (A ! C) выводимы, то высказывание A ! C также выводимо согласно правилу заключения.

Говорится, что формула ' выводима из формул '1, : : :, 'm (обозначается '1, : : :, 'm ` '), если существует последовательность формул Ã1, : : :, Ãk, ', в которой любая формула либо является аксиомой, либо принадлежит списку формул '1, : : :, 'm, называемых гипотезами, либо получается из предыдущих по правилу вывода. Выводимость формулы ' из ? (` ') равносильна тому, что ' теорема ИВ.

П р и м е р 1.6.1. Покажем, что формула ' ! ' выводима в ИВ. Для этого построим вывод данной формулы:

1) в схеме аксиом 2 формулу Ã заменим на ' ! ', Â на '. Получаем аксиому (' ! (' ! ')) ! ((' ! ((' ! ') ! ') ! (' !

'));

20