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

1) натуральное число 0 обладает двойством Uи 2) для всякого натурального числа $ изтощ 'пол обладает свойcmou U следует, что

и натуральное число х' обладает свойством С/, то июйстпом О обла­ дают сс* натуральные тасла (принцип математечикой индукции).

Заметим, что икота аксиома Р1 формулируется иначе: 1 - есть натуральное число. В этом случав легко видеть, что аксиоматика

•единственную предтнкатиугабукву А] ,

•единственную предметную постоишуюОь

» три функциональныебуквы /! , / ' f\,

кроме того, очевидно, ее символами являются !,= > ,),(, ’ , * х2,. ,V*llVje2,...,3a:i,3

Чтобы и:погткэоват1, привычныедтинас записи, обозначим

Af(f,sJ через !-.г,

/|(!) черв!г ; /?((,.О черезг+т;

f \ (г-*)- чере! понимаетсякак гнак ушожешш)

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

51; 4 =^2=>C(*i“ *:>*( *j“ »));

S1: Si: 0

Si: x,‘=jfj'=MTI=xa; Si: *1+0-»;

S6:

,77; *rU=0; SB.

59 Л ф ^ У Ц Л (х ,)= > А (х ,MW). гдеА(д)~ произвольна» формулатеории 5,

Напомним, >гго правилами вывода любой теории первого поряд­ ка являются правила МР и Gen.

Рассмотрим Собственные аксиомы теории S и сравним их с ак-

Замегим, что аксиомы Л1 - Я являются конкретными формула­ ми, в то время как 59 представляет собой схему аксиом, порождаю­ щую бесконечное мпсйсесттоаксиом

сиа равенства, которые Дедехикдом и Пеано предполагались как ин-

Аксиоиы .93 и SA соответствуют аксиомам РЗ и Р4 системы аксиом Псаии. Аксиомы Р\ и П леановегок системы обеспечивают существование 0 (нуля) и операции "непосредственно следующий", которым л теория S соответствуют предмечная константе а, и функ-

Аксиомы £5 - S8 служат для определения операций сло*енюг и умножения. В аксиоматике Пеано нет аксиом, соответствующих S5S8, потому что Дедеккнс и Пешо вопуслали использование интуи­ тивнойтеории множеств, г рачках которой существование операций+ и • (сложения и умнойенш), удовлетворяющих аксиомам SS-SS,

:т2

Доказывается, что множество формул любой теории первого порядка счетно, поэтому го схеме .99 можем получит лишь счетное множество аксиом. В аксиоме Р5 рассматривается некоторое свойство U, которым, (тьгпможет, оИтадают один и 1¾ обладаг ггдругие катуральные числа, т.е, свойством U обладают элементы : которого подмножества множества натуральных чисел. Известно, чго мощность множества see* подмножеств множества натуральных чисел больше, чем мощность счетного множества. Поэтому схемаакс ом59, которая наливается принципом мятематшеско# индукции, не соответствует аксиоме PS, поскольку схема аксиом 59 может им ть дело лигиь со счетным множеством свойств, определяемых форм. ламп теории S, а в аксиоме PS интуитивно предполагается более, чем четное мно*в- C-IBO свойств натуральных чисел.

В заданной таким образом теории S (формальной арифметике) можно получить вывод всех известных теорем арифметики, например, доказать, что для любых термов /, J иг имеют место:

(■/+.;=?+( - коммутативность сложения;

|- (i+i)+2=t+{«+3) - ассоииамвность сложения; / • j=j 1 - коммутативность умножения;

|-l -(з+г)~1 • ■з - дистрибутивность ит.п.

Не будем аокизьгеать приведенные утверждения, а также другие арифметические теоремы. Hie прежде всего будут интересовать не арифметические теоремы, а свойства теории S (формальной арифме­ тики) идругих теорий, содержащих всебеS.

§ 15. Свойства теорий первого порядка

было уже отмечено, одним ю важнейших свойств дедукеории является ее непротиворечивость. Для исчишения

173

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

Непротиворечивость исчисления предикатов первого порядка (,торчи KJ.

Теорема 4,Я. Всякое исчисление предикатов первого порядка

(непротиворечиво.	|
Докачигелыпво	Для произвольной формулы А обозначим

через h{A) выражение, получающееся в результате следующего преоб­ разования формулы А: в А спускаются все кванторы я термы (вмосте с соответствующими скобками изапятыми).

Например, ft(Vxj,4J| (Х|, х;)” А \ (л;>)есть A'': ; AllV-ti/lVxi.oi, 11)=3^ 5((¾)¾^1^ ] ) есть ~[A:\^>A'i=>A'i..

По существу h(A) всегда является пропозициоиалыюй формой, в ко­ торой роль пропозициональных букв играют симвшыа \ .

Ясно, что имеют мссто

Ы\Л)=ЛЫА\ h(A^Bf=h\AJ*KB).

кой-кибудь до схемA 1-/(5, является тлетологней. Для/И, AZA3 это очевидно.

Всякий частный случай Ai Vx,A(x,)^>A(t) преобрпзуетт:* оиера-

Ух,(А^В)=з{А=$'}х£)-в тавтологию вида(С=?Я)=4>(С=*0).

Далее: 1) пусть h(A) и ЫА->!1)-к(4)^>1\(3:) гавгологии, тогда h{B) - тоже тавтология;

2) если Ы.А)- тавтология, то WVa-4) - тавтология, ибо резуль ты применения операции h к А и к Чх,А совпадают.

174

5 отличие от исчисления высказываний, исчисление предикатов оказывается неполным в узком смысле. Эго означает, что множество теорем теории К\ (множество Тщ) можно некоторым образом расши­ рить и при этом Тщ непокроет все множество формул теории JTi.

дующая теорема

Теорема 4.9 (теорема Чёрча). Исчисление предикатов первого порядка является неразрешимойтеорией.

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

Можно привести примеры гораздо более богатых теорий, чем исчисление предикатов первого порядка, дли которых оказалось воз­ можным дать строгое доказательство непротиворечивости и полноты R широком смысла. Примером может служить арифметическая систе­ ма натуральны* чисел с одной операцией сложения (без операции ум­ ножения). Но для теорий, содержащих уже всю арифметику натураль­ ных чисел, картина качественноменяется.

Знаменитые и важнейшие теоремы Геделя посвящены жследованию возможностей формальных аксиоматических теорий и вьзяене-

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

176

решимая (нельзя НК доказать, ни опровергнуть) формула. Теорема Гелем утверждает, что такое расширение теории не может сделатьее полной.

Теорема Геделя показывает, что множество теорем теории (множество Т.) содержит! во чтжестпе всех истинных арифметиче­ ских формул V, (?', с /,) и в то >№врем* нельм построить непротиво­ речивое эффективно аксиоматизированное расширение для £так, чюбы полученное множество теоремпокрыло все V,.

Отсюда следует, что формальный аксиоматический подход

истинных арифметических суждений (формул). Таким обрцом, результат Геделв указывает на некоторую принципиальную ограни­ ченность возможностей аксиоматическогометода.

Вторив теорема Геаеля. В этой теореме Гедель показал, что никакое предложение, которое можно точным образом интерпретиро­ вать как выражающее непротиворечивость какой-либо непротиворе­ чивой формальной аксиоматической теории К, содержащей арифме­ тику, не может быть доказано вэтой теорииК.

Более вольно излагая эгу теорему, можно сказать, что «если теорий К, содержащая орифметнку, непротиворечива, то непротиваре-

Конечно, неплохо, «ия получим доказате/гьетво иаоснове более богатой теории. Но нам нужно чнать, непротиворечива ли зга более богатая теории. Теорема Гглеля утверждает, что еслиона непротиво­ речива, то нЕпро1Яворе'Шво<.-1ъ ев нельзя доказать средствами самой теории, т.е. придется привлекал еще более богатуютеорию, непротаBupe'iHiocTi. которой тоне нельэидоказать в ней самой, и т.д.

Доказательство непротиворечивости арифметики натуральны* чисел с привлечением новых правил вывода было впервые получено

казательств. Эти доказательства имеют относительную ценность. Они

177

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

§ 16. Значение аксиоматического метода

ГоВС^м об ограниченности аксиоматических подходов, нельзя умолчать о достоинствах и большом значении аксиоматического под-

Аксиоматизация теории позволяет: 1) систематизировать науч­ ный материал;2)обеспечнеать определенную организацию научного знания; 3) исследовать структуру рамлчных теорий и их взаимоотно­ шение; 4) обеспечивать необходимуюстрогостьрассуждеиий.

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

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

С проблемой формализации неразрывно связано создание раз­ личных научных или формализованных лаыкив Основная цель, кото­

рая trpJi >гом преследуется, состоит в том, чгож построить язык, «обидный от недос/агков обычного лзыка. Благодаря точности и од­ нозначности формализованные азыки нвходтг применение там, гдв

Д. ГкльЕгрт писал: "Подзнаком акеиолитичесхгко иемаоа ма­ тематика проявляет сеп№ руководящуюрпяь в науке вообще".

1 17. Теория естественного вывода

Естественный вывоз является югтгресныч подходом к заданию дедуктивной теории. Здесь, хав и в любой дедуктивной теории, зада­ ются алфавит, формулы (правильно построенные выражения), но нет ахеиом, есть только правила вывода. Окалывается, что задание только правил выводоа позволяв! выделить из множества всех формул неко­ торое подмножество формул, элементы которого и называются тсоре-

теорсмы.

Рассмотри задание исчисления высказываний в виде теории

Пус1ъ символамиявляются l,&,v, 4 ,(,), АиAh .... а формула­ мипропозициональные формы, образованные изА\,Лъ.~ с почощью '|. &. V. 4 .

Пусть А, В, С - произвольные формулы. Правила вывод» зада­ ются следующим образом. В каждом правиле вывода справа стоит символ в качестве имени этого правила Например, одно из лрзенл

означает, что ичА можно вывестиA'JB где В - произвольная форму­ ла. Точно так же в каждом правиле рьтода в "числителе'1записывают­

ся гипотезы (посылки), a t		"знаменателе" то, что выаолитса из зтих
гипотез.
Все правила вывода подразделяются на правиле введения и ttpa-
А&П * ’	В&А	AvB	V’ ПчА V ’
4 М = - ;
а=>в	~\л
а правилами исключения (удаления):
		&: А |-С.В	\-C.AvB у

ILL I;

Tax как в естественном еикаде нет аксиом, то доказательство должно основываться на правиле введения импликации, которое гово­ рит, что или й может быть выведена из А по правшам вывода, то А-^>В доказано. В формальной аксиоматической теории всякая формула вывода является либо аксиомой, либо непосредственным следствием по правилам вывода из предыдущих формул этого вывода. В доказательстве естественного вывода начинаем с гипотез (т.е. с недокаяаннвд предложений), исследуем гледегпия, получаю­ щиеся по правилам вывода, и загем используем информацию вкиа A |-б для того, чтобы заключитьо доказуемостипредложении

Например, докажем, что для любой формулыА формула Т1 *=>А является теоремой, Это моментально следует, если применить прави­ ло исключекия отрицания

Ik-1,