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

Аксиомы S5-S8 служат для определения операций сложения и умножения. В аксиоматике Пеано нет аксиом, соответствующих S5-S8, потому что Дедекинд и Пеано допускали использование интуитивной теории множеств, в рамках которой существование операций + и • (сложения и умножения), удовлетворяющих аксиомам S5-S8, выводимо. Доказывается, что множество формул любой теории первого порядка счетное, поэтому по схеме S9 можем получить лишь счетное множество аксиом. В аксиоме Р5 рассматривается некоторое свойство U, которым, быть может, обладают одни и не обладают другие натуральные числа, т.е. свойством и обладают элементы некоторого подмножества множества натуральных чисел. Известно, что мощность множества всех подмножеств множества натуральных чисел больше, чем мощность счетного множества. Поэтому схема аксиом S9, которая называется принципом математической индукции, не соответствует аксиоме Р5, поскольку схема аксиом S9 может иметь дело лишь со счетным множеством свойств, определяемых формулами теории S, а в аксиоме Р5 интуитивно предполагается более чем счетное множество свойств натуральных чисел. В заданной таким образом теории S (формальной арифметике) можно получить вывод всех известных теорем арифметики, например, доказать, что для любых термов t, snz имеют место: |- t+s=s+t - коммутативность сложения; |- (t+s)+z=t+(s+z) - ассоциативность сложения; \- t*s=s*t - коммутативность умножения; |-1* (s+z)=t*s+t*Z - дистрибутивность и т.п. Пе будем доказывать приведенные утверждения, а также другие арифметические теоремы. Пас прежде всего будут интересовать не арифметические теоремы, а свойства теории S (формальной арифметики) и других теорий, содержащих в себе S. § 15. Свойства теорий первого порядка Как было уже отмечено, одним из важнейших свойств дедуктивной теории является ее непротиворечивость. Для исчисления высказываний непротиворечивость была доказана сравнительно просто. Для произвольной теории первого порядка установить непротиворечивость в рамках этой же теории не удается. По в некоторых частных случаях, например, для исчисления предикатов первого порядка, удается доказать непротиворечивость. Непротиворечивость исчисления предикатов первого порядка (теории Kj). Теорема 4.8. Всякое исчисление предикатов первого порядка непротиворечиво. 126