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

Аксиомы не доказываются не потому, что могут не доказы­ ваться, а потому что не могут быть доказаны. 2. Задаются только аксиомы, а правила вывода считаются из­ вестными: а) из множества формул (правильно построенных выражений) выделяется подмножество А, элементы которого называются аксио­ мами (аксиом может быть как конечное число, так и бесконечное); б) правила вывода (методы доказательства) теорем считаются известными из опыта изучения математики. При таком задании теорем дедуктивной теории говорим, что задана полуформальная ксиоматическая теория. 3. Аксиом нет, а задается только конечное число правил выво­ дов, с помощью которых и получают теоремы. Такую дедуктивную теорию называют теориейестественного вывода. Случай, когда нет аксиом и нет правил вывода, не рассматрива­ ется в логике. Применяя один из указанных способов задания теорем, будем получать множества теорем Ти Тг и Тз соответственно. Сразу возни­ кают вопросы; когда эти множества Т\, Т2, и Гз совпадают? Когда не­ которые из Т], или Г2, или Гз дедуктивной теории В совпадают или покрывают класс "истинных" формул теории В\, при условии совпа­ дения для В и В], алфавитов и формул. Эти вопросы оказываются не всегда простыми и в рамках этого курса затрах'иваются незначительно. Разве может леопард избавиться от пятен. Английская пословица § 3, Свойства дедуктивных теорий Выберем один из трех способов задания теорем дедуктивной теории. Изменяя аксиомы или правила вывода (в. случае, когда они задаются), можно получать различные множества теорем Т. Это мно­ жество Т - множество теорем (множество доказуемых формул) явля­ ется существенной характеристикой дедуктивной теории. 139