Ш.И._Галиев_МЛ_и_ТА_2004

С л у ч ай la. Пусть при заданном (выбранном)распределении истинностных значений букв Bt,B-„..,Bi формаЛ принимает значение

И. Тпгла А принимает панаш Л пА ‘~'\А, а В‘-В По ИНДУКТИВНОМ

предположению, имеем

	^В.	(4.9)
Согласно п. б) леммы 4.2 имеем:
|-B=s71s.		(4.10)
Из (4.9) и(J.10) поМР получим:
В\,В'ъ...,В\ j-Tlfl.		(4.11)
В рассматриваемом случае А=] В, А' -] А-Т\ В, тогда из (4.11)
следует i-ребуемое: В\.В\...,В‘,		[л \
Слу ч 1 й	16. Пусть В принимает значение J1, тогда В' есть
lfi, а А' совпадает с А.		По иидуктивноиу предположению
j-1В, 'сто итребовалосьполучить. и5п1В есть Л\
С л у ч ай	2. / имеет вид ЛэС. Тогда числа вхождений при­

митивных связок ь В и С меньше, чем в А. Поэтому, *«илу индуктив­ ного предположения

В \В \....B‘t	\- В\	(4.12)
8',.Яг...,В'*	(-С-.	(4,13)

С л у ч ай 2а. Л принимает значение JI, тагла, вне зависимости от значения формулы С, формула А-В=лС принимает значение И. Так как значение В есть Д то 5 ’=1 8 , в из истинностиА следует, что

Л'~Л.}1ъ соотношении (4.12) получаем
B‘i,B’i....В', 1- I л	(4-14)
Согласно п. в) леммы 4.2 имеем:
(-1»=>(B=>C).	(4.15)

Иа(4.14) и (4.15) го UP следует:

ЯиЗь-.г» Ув=>с.

Последнее иестьтребуемое, такхак В=С естьА.

Случай 26. С принимает Значение И. Следовательно, А прини­ маетмачение И и С' есть С, »А'естьЛ. Тогдаю (4.13) получим;

	(4.16)
Согласно схеме аксиомА1 имеем
|-0*(£=>С).	(4.П)
Из (4.16) и(4.17) по МРсясдуст
|-5=>С

итак кахВ=С совпадаете Л\ то (4.18) являете»требуемым.

С лучай 2D. В принимает значение И, Спринимает значение

Л.Тогда А принимав! значение Л, следовательно, А' -1 А. В‘есть 8, iCeOTblC. Такимобразом, го(4.12) и(4.13) получимсоответственно

		(4.19)
		(4.20)
Поп.е) леммы4,2имеем
		(4.21)
№ (4Л9) и(4.21) поМРследуй
S’!,0’s,..- Л	1Сэ1(Й=>С),	(422)

а из (4.20) и (4.22) по МРследует В’Л - Д , |-1(3=>С|.

Последнее 1вд«етсятребуемым, ибо T(fc>C) естьА'. Леммадоказана.
Теорема 4.5	(о полноте). Если формулаА теории I являйся!
тавилогней, то она	являетсятеоремойтеории£.	1

Доказательство. Предположим, ц Bi,Sj,...,St - пропозицаоналы

распределении исчннкос-ткых значений для бум £|,£г... £е имеем,

принимает значение И). Поэтомув случае, когдаВ; принимает значе­ ниеИ, получим

Отсюда по теореме дедукции получимсоответственно
eVB	[-В»=>Л,	<4.23>
£ 'I,S'2,...,BVI |-1£,=>Л.		(4.24)
Пс п. ж/леммы 4.2 имеем:
h<»t=>-4)=KClД^=>-4)=>^).		(0.25)
■МР из(4.23) и(4.25) получим
SVi	1-(1^=^)=^.	(0.26)
ее сном по МР из(4.26) и(4.24) следует
Таким образом, из B \B \..,B 't \а получили ii’i.B'j,		,S’ы |-А,

т.е. исключили В\. Точно также исключим В‘ы и так далее, после к

таких шагов придса к

м.

т.е. А является теоремой, чтои требовалосьдоказать.

Можно доказать и полноту в узком шмеле (ем., например, [7]). Примем бездоказательства.

Независимость аксиом. Отдельная аксиома дедуктивной тео­ рии, в том числе и исчисления выевазымшиб, является независимой,

4.6. Каждая из схем Л\, Л2 и А3 независима от

Доказательство. Независимость А\. Рассмотрим сле,1!ую[цую

чсний 0, 1. 2 для буи, входящих в формулу А, эта таблица позволяет най­ ти соответствующее значение формулы А Если формула А всегда принимает значение 0, то она называется выделсн-

Правшю modus pvrwm сохраняет

так как если А н принимают значение 0, т с. выделенные, то со­ гласно таблице и В принимает значение 0, следовательно, тоже выде-

тоже выделенная. Для ,43 имеем следующую таблицу, из которой гидко, что аксиома, полученная поАЗ, ялчястся выделенной. Аналогично можнопоказать выделенность.42.

Если бы /41 бша выводима в этой теории из аксиом А2 и АЗ, то она должна быть выделенной, тан как применение МР к выделенным формулам прноодкт к выделенным. Но At не является наделенной, так как формула A ^ fA i = Ai) принимает значение 2, когда Л[-|, у. А-1-1. Таким сказом, аксиома А\ не может —I быть выведена из аксиом А2 и /(3, следппа-

тельно. она независимаот них, Независимость 42. Рассмотрим

следующую таблицу.

Всякую формул), принимающую согласно этой таблице всегда значение О, назовем гротескной. Правило МР сохраняет чжгеп8нпсп>; ибо если А и А ^ В гротескны, то на приведенной таблице формула йтоже гротескна.

схеме А1 к Ai, гротескна. В гротескности Л1 убеждаемся по следую­

	A	s	(В =		А)	щей таблице. Аналогичным образом дока-
	0	0	0	0	0	етсятельно).
	1	0	0	2	1
	2	0	0	1	2			Если А2 выводима из А 1 и АЗ, то она
	0	0	1	0	0	должна бань гротескной, ибо МР, приме­
	1 0		1 2		1	ненное к гротескным формулам, дает гро­
	2	0	1	0	2	тескную. Но частный случай Л2 но являет­
	0	0	2	0	0	ся гротескным:
	1	0	2	0	1
						(А, =>И) =>4) -((/), =>Л£> => (А, =>А,))
	2 0!	2		0	2
						0	1	0	2	1	2	0	0	0	1	0	2	1,

ибо принимает значенио 2. Следовательно,Л2 иазавиенма от.41 иАЗ. Независимость -43 Пусть А - произвольная формула я h(A) - формула, полученная н?.Л удалением всех пхождений знака отрицание

165

по схемам А\ и Л2, h[A) буди тавтологией. Очевидно, чю hlA=>B)

есть КЛ'^НВУ Если ЫА^В) - h(A)^h(B) и КА) - тшггалогии, то И й(Л)-тавтология, следовательно, правшо МР сохраняет свойство А иметь а качестве h(A) тавтологию. Таким образом, вакая формула А, выводимая нз Ai, Л2 с помощью UP, иыеет ь качестве Н(А) тавтоло­

гию. Но

й((14,=>1 U,=>^,>=>,<,))-<*=>Л0=>((Л,»Л,)-Л,)

и эта последняя формула не яалгегся тавтологией, Следонагельно,

частный случайАз - формула("ki^> ^,)=?((1 Л,)=Л,) - не выво­ дима из/II и А2 спомощьюМР Теоремадоказана.

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

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

Теорема 4.7. Исчисление аыекмыганий (теория £) является разрешимой таорией.

Докаштельспю. Было доказано, что каждая теорема теории L «яляегсг тавтологиейи (обратно) каждая формула, являющаяся тавто­ логией, есть теорема. Таким образом, формула А теории L является

12.Другк« аксиоматизации исчисление выскачывянпй

Впредыдущих параграфах рассматривался пример формальной аксиоматической теории - исчисление высказываний (теория I), кото­ рая была sailalia, множеством символов, формул, аксиом и nptmn.t вы­ водаТеперь рассмотрим некоторую формсыитванную теорию С. Для

задания формализованной теории нмгбходимс задать ее символы, формулы (правильно построенные выражения) и из множества фор­ мул выделять подмножество, элементы которого считаются «истин­ ными» формулами. "Пусть формализованная творил Сзаданатак, что:

1) алфавиты теорий Lit С совпадают, те. алфавитом для Сявля­ ется следующее множество символов.' 1 =а,), !, A,,Ai:...;

2)множестваформулХи Ссовпадаюг (Ф^-Фг ,где Ф,(Фс) - мно­

жество формул теории1(C)). Таким образом, формулой в С	является
всякая пропозициональная форма, построенная на бук!	Ai. Ai, ...

спомощью связок ] и=>;

3)"истинными" формулами в теории Ссчитаются т формулы теории С, которые являются тавтологиями Пусть V<: обо­ значаетмножество "истинных” формултеорииС.

В исчислении высказыванийбыло задано Г, - множествотеорем (с помощью яксгам А1-АЗ и правила вывода МР)■При згом теорема­

ми в Z оказались тс, и только те формулы из L, которые являются тавтологиями. Следовательно, множество теорем формальной теории L совпадает о множенном “истинных" формул формализованной тео­ рии С: Ti=Vc .

Итак, формальная теория L оказалась построенной таким обра­ зом, что ее множество теорем (ГО вточности совпадает с.множеством "истинных" формул (Ус) формализованной теория С.

Из полноты в уисом смысле теории L следует, что всякая по­ пытка расширить множество '1). приводит к противоречивой теории, поэтому нельзя к А1-АЗ доВа&игь недоказуемую из них формулу, не прихо.пя при этом к противоречию, Естественно выяснить, можно ли.

167

взяв другие аксиомы и, гложетбыть, другие правила «ывдда, получить

Т:. - Гг-

Оказывается, что можно. Например, построим формальную аксиоматическую (дедуктивную) теорию /Л, которая отличается от L только тем, что вместо схем аксиом А1 -/13 здесь имеются лишь три конкре,ные аксиомы:

1)^1=>(<^2=* 4,); 2) (/,=^=^))= .((4,= -,1,)= .(,(,= *.));

3 )(1 4 ,= ^ ,)= ((1 ^ = 4 ,)= ^ ,).

но, кроме правила вывода МР (modus ponens), имеется еще одно пра­ вило вывода - праияло подстановки, разрешающее подстановку лю­ бой формулы на места все* вхождений дзннпй пропозициональной буквы в данную формулу. Приэтом мо*но показать, что Гц ” VrmT<- Оказывается, мо*но даже построить формальную аксиоматиче­ скую (дедуктивную) теорию 11 с тем же алфавитом и множеством

формул, что иI, ни всего с одной схемой акском <С4г>Б)=>(10=1 D»*£)=.((£=.4)=(C^))

и единственным п|швилом вывода - МР (modus pattern). Здесь гоие Ти = Vr -7,,. Возможны и другие заданна формальных аксиоматиче­ ских (дедуктивных) теорий гак, чтобы ее множество теорем совпадало с множеством Vc,

§ 13. Теории первого ппрндка

Теорна первого порядка (теория R") представляет собой фор­ мальную аксиоматическую теорию Следовательно, дня ее зядакня необходимо определить символы, формулы, аксиомы и конечное чис-

1. Символами всякой теории первого Пирядхаслужат: 1,= - пропозициональные связки;

168

(,),'-знаки пунктуации; ль хг,... -счстое множесшп предметных переменных;

а\, й;,... - конечное (возможно и пустое) или счетное множество предметных констант;

Л? (г,&>0) - непустое, конечное или счетное множество преди­ катных бугсв;

f k (ttel) - конечное (возможно н пустое) ил» счетное множе­ ство функциональных бука:

V*, ,3л-, (i>l) - кпанторы всеобщности и кванторы существова-

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

2.Формулы теории первого порядка опреаолжстгси точно также, как определяются формулы в логике предикатов.

3.Аксиомы теорииК разбиваются не два класса: логические ак­ сиомы и собственные аксиомы.

Логические аксиомы: каковы бы ни были формулы А, В, С тео­

рии К,	следующие формулы являются логическими аксиомами
А\:	А=,(В->А)\
А2:	(A^(B^Q)^((A^B)=i<A^C)y,
Ai:	(lB=>'i л)=>((1а=»Л)=»д);
АА:	V% A(x,)=*A(f),

здесь А(х,) ссть формула теории К и t есть терн теории К, свободный лия х, вЛ(*,);

А5: Vjc, (^^>S)»(^_jVx,B), если формула А не содержит сво-

Собстеенные женимы. Собственные аксиомы не могут быть сформулированы в общем случае, ибо меняются от чсории к теории.

169

В дальнейшей рассмотрим конкретную теорию первого порядка (формальную арифметику), для которой будут сформулированы (перечислены) собственные аксиомы

4.Правилами пыподаповсякойтеориипервого порядкаяш1якяся:

1)modus ропепз: В является непосредственным следствием А

и А=эВ;

2)праеюо обобщений (Gsn): из А стедует Vx, л, точнее Vx, А являете! непосредственным следстднем изА.

Теории первого порядна, не содержащая собсгпенних аксиом, называется исчислением предикатов трвогс пврийка и обозначается

1 14. Формальная арифметика (теория S)

Первое полуавтоматическое построение арифметики было предложено Дедекиндпч (1901), далее усовершенствовано Пеыю и извсспю под названием "систем» аксиом Пеано". Эта система форму­ лируется следующим образом;

f 1:0 - есть натуральное число;

Р2: для любого натурального числя х сушостьуот другое нату­ ральное число, обозначаемое х' и называемое непосредственно сле­ дующим за х;

РЗ. Ога;' для любого натуральногочислам;

И; если Uесть свойство, которым, быть может, обладают одни и не обладаютдругие Натуральныечисла, и если;