Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Теорема 4.9 (теорема Гёделя о полноте). Каждая логически общезначимая формула из Ki является теоремой в Ki. Таким образом, исчисление предикатов первого порядка (теория Kj) является полной в широком смысле теорией. h Можно доказать, что во всяком исчислении предикатов первого порядка каждая теорема является логически общезначимой формулой. Следовательно, во всяком исчислении предикатов первого порядка теоремами являются те и только те формулы, которые логически общезначимы. Теория К считается полной в узком смысле (или в смысле Поста), если добавление к ее аксиомам любого недоказуемого в ней утверждения приводит к противоречивой теории. В отличие от исчисления высказываний, исчисление предикатов оказывается неполной в узком смысле теорией. Это означает, что множество теорем теории Ki (множество Tj^i) можно некоторым образом расширить и при этом Т]^1 не покроет все множество формул теории Ki. Оразрешимости исчисления предикатов. Имеет место: Теорема 4.10 (теорема Чёрча). Исчисление предикатов первого порядка является неразрешимой теорией. Следовательно, не существует метода, позволяющего для произвольной формулы А логики предикатов за конечное число действий выяснить: А - теорема или нет. Можно привести примеры гораздо более богатых теорий, чем исчисление предикатов 1-го порядка, для которых оказалось возможным дать строгое доказательство непротиворечивости и полноты в широком смысле. Примером может служить арифметическая система натуральных чисел с одной операцией сложения (без операции умножения). Но для теорий, содержащих уже всю арифметику натуральных чисел, картина качественно меняется. Знаменитые и важнейшие теоремы Геделя посвящены исследованию возможностей формальных аксиоматических теорий и выяснению их непротиворечивости. Первая теорема Геделя. Первая теорема Геделя утверждает, что каждая формальная аксиоматическая теория К, настолько богатая, чтобы содержать формальную арифметику такова, что если К непротиворечива, то К существенно неполна, т.е. содержит некоторую формулу, что ъ К qq нельзя ни доказать, ни опровергнуть, хотя с помощью дополнительных средств, выходящих за рамки этой теории К, можно показать ее истинность. Более того, даже если дополнить аксиомы теории К так, чтобы известные истинные 128