Загрузка...

Исчисление предикатов первого порядка


Это формальная система которая задается следующим образом
1 алфавит содержащий символы предметных констант a,b,c … с индексами или без,  символы предметных переменных с индексами или без, предикатные символы A,B,C … с индексами или без, символы: (), =>, @ и символы кванторов.
2 формулы исчисления предикатов образуются аналогично формулам логики предикатов
3 аксиомы : имеют место все 3 аксиомы высказывания и кроме того
(А4) (?t) (B(t)=>B(u)) спецификация
(А5) (( ?t)(m1=>m2))=>(m1(?tm2) m1 и m2 – формулы , а t – не является свободной переменной в m1. Аксиома (А4) утверждает, что t не не содержится свободно в U. Переменная U в этом случае становиться свободной
4 правила вывода m1, (?t)m1 , где t свободная переменная в m1 . Данное правило называется обобщением.
Квантор существования выражается через квантор всеобщности и явно не присутствует в определенном выше исчислении предикатов первого порядка.
Термин теории первого порядка означает , что действие в их формулах распространяется на предикаты от переменных
Первая теорема Геделя о полноте исчисления предикатов
В исчислении предикатов 1-го порядка все теоремы являются логически общезначимыми формулами т.е. являются истинными во всех интерпретациях .
Данная теорема аналогично т.Поста в исчислении высказываний , но в отличии от нее , это не приводит к эффективной процедуре разрешения.
Теоремы ограничения формальной системы
Т.Тарского : Существует формальные системы для которых всякая интерпретация приводит к выражениям одновременно истинным и недоказуемым , т.е. в любой интерпретации существует по крайней мере одна формула всегда интерпретируемая как истинная которая однако не является теоремой данной формальной системы.
Т.Черча Исчисление предикатов первого порядка не разрешима. Данная теорема утверждает , что существует такие формальные системы для которых невозможно построить процедуры отличающие теоремы от не теорем.
Результаты Тарского , Черча и Геделя говорят о том , что некоторые задачи неразрешимы средствами современной математики . Это относится как к людям так и к ЭВМ.
Т.О. если задача кажется сложной то необходимо сначала удостоверится , что она не относится к какому-либо известному случаю неразрешимости а затем приступать к решению .
Вывод : возможны формальные системы в которых
1) существуют формулы m , такие , что ни m ни @m не являются доказуемыми. (тГеделя)
2) во всякой интерпретации найдутся выражения истинные и недоказуемые (Тарского )
3) нет алгоритма для отличия теореме от не теоремы (Черч).

Загрузка...