Проблемы разрешимости, непротиворечивости и полноты исчисления предикатов

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

Проблема непротиворечивости исчисления предикатов заключена в доказательстве невыводимости формулы и ее отрицания. Исчисление предикатов непротиворечиво, т. к. каждая доказуемая формула является тождественно истинной формулой. Тогда ее отрицание является тождественно ложной формулой и при доказательстве в исчислении предикатов ведет к противоречию.

Из лекций:

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

Тезис Черча: Логика предикатов полуразрешима.

Логика называется непротиворечивой, если в ней нельзя вывести одновременно некоторые утверждения и его отрицание. Теорема логики предикатов непротиворечива.

Логика называется п олной, если в ней выводимо все, что истинно. Теорема о полноте исчислений предикатов полна.

Теорема Гёделя о неполноте.

Во всякой достаточно богатой теории существует такая истинная формула, что не она, не её отрицание не выводимо в этой теории.