Формальные и неформальные аксиоматические теории

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

· были объявлены первоначальные (неопределяемые) понятия: высказывание, истина, ложь, предикат.

· все остальные понятия определялись, опираясь на неопределяемые понятия, а также на общематематические неопределяемые понятия: множество, принадлежность элемента множеству, натуральное число, и др.

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

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

· не было определено формального понятия “доказательство” и не были сформулированы явно правила рассуждений, которые допустимо использовать в доказательствах.

Все перечисленные черты присущи неформальным аксиоматическим теориям, структура которых обсуждалась в § 7 главы II.

Идя по тернистому пути к матемтической строгости, математики пытаются придать математическим теориям всё более формальный характер, чтобы исключить всякую возможность использования несанкционированных аксиомами и правилами вывода рассуждений. Программа такой формализации была выдвинута Д. Гильбертом в начале XX в., и первые её шаги вселяли уверенность в скором завершении строительства незыблемого и непоколебимого здания самой точной из всех наук – математики.

Построение формальной аксиоматической теории, в отличие от неформальной, предполагает следующие шаги:

o задание её алфавита, т.е. базовых символов аксиоматической теории, каждый из которых лишён какого-нибудь содержательного смысла.

o указываются правила построения формул теории из символов алфавита, т.е. её осмысленных предложений.

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

o формулируются правила вывода, т.е. используемые при доказательствах правила вывода одних формул из других.

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

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

На самом деле, некоторые черты построения формальных аксиоматических теорий были присущи и изложению предыдущих глав: так, например, в этих главах были определены понятия формул исчисления высказываний и формул исчисления предикатов. Однако последовательно идея формализма в жизнь не проводилась. Таким образом, наше изложение носило эклектичный характер.