Математическая логика и теория алгоритмов

в отличие от исчисления высказываний, исчисление предикатов оказывается неполным в узком смысле. Это означает, что множество теорем теории к\ (множество тк\) можно некоторым образом расши­ рить и при этом тк\ не покроет все множество формул теории к\. О разрешимости исчисления предикатов. Имеет место сле­ дующая теорема. Теорема 4.9 (теорема Чёрча). Исчисление предикатов первого порядка является неразрешимой теорией. Следовательно, не существует метода, позволяющего для про­ извольной формулы а логики предикатов за конечное число действий выяснить: а - теорема или нет. Можно привести примеры гораздо более богатых теорий, чем исчисление предикатов первого порядка, для которых оказалось воз­ можным дать строгое доказательство непротиворечивости и полноты в широком смысле. Примером может служить арифметическая систе­ ма натуральных чисел с одной операцией сложения (без операции ум­ ножения). Но для теорий, содержащих уже всю арифметику натураль­ ных чисел, картина качественно меняется. Знаменитые и валснейшие теоремы Геделя посвящены исследо­ ванию возможностей формальных аксиоматических теорий и выясне­ нию их непротиворечивости. Первая теорема Геделя. Первая теорема Геделя утверждает, что каждая формальная аксиоматическая теория К, содержащая фор­ мальную арифметику, такова, что если К непротиворечива, то К суще­ ственно неполна, т.е. содержит некоторую формулу, что в к ее нельзя ни доказать, ни опровергнуть, хотя с помощью дополнительных средств, выходящих за рамки этой теории к, можно показать ее ис­ тинность. Более того, даже если дополнить аксиомы теории к так, чтобы известные истинные формулы были доказуемы, все равно и для такой расширенной системы всегда существует истинная, но не раз­ 176