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

Доказывается, что множество формул любой теории первого порядка счетно, поэтому по схеме S9 можем получить лишь счетное множество аксиом. В аксиоме Р5 рассматривается некоторое свойство и, которым, быть может, обладают одни и не обладают другие нату­ ральные числа, т.е. свойством обладают элементы некоторого под­ множества множества натуральных чисел. Известно, что мощность мнолсества всех подмножеств множества натуральных чисел больше, чем мощность счетного множества. Поэтому схема аксиом S9, которая называется принципом математической индукции, не соответствует аксиоме Р5, поскольку схема аксиом S9 может иметь дело лишь со счетным множеством свойств, определяемых формулами теории S, а в аксиоме Р5 интуитивно предполагается более, чем счетное множе­ ство свойств натуральных чисел. В заданной таким образом теории S (формальной арифметике) можно получить вывод всех известных теорем арифметики, напри­ мер, доказать, что для любых термов t, sи г имеют место: |-t+s=s+t- коммутативность сложения; |- (H-j)+z=^+(.v+z) - ассоциативность сложения; |-1•s=s •t - коммутативность умножения; [-1 • { s + z ) - t •s+t•z — дистрибутивность и т.п. Не будем доказывать приведенные утверждения, а также другие арифметические теоремы. Нас прежде всего будут интересовать не арифметические теоремы, а свойства теории S (формальной арифме­ тики) и других теорий, содержащих в себе S. Ничто несовершенно в всехотношениях. Гораций* § 15. Свойства теорий первого порядка Как было уже отмечено, одним из важнейших свойств дедук­ тивной теории является ее непротиворечивость. Для исчисления • Римский поэт (65-8 гг. до и. э.). 173