Мат_Логика(лекции)

Определение языка математической теории.

II. Аксиомы формальной теории. Система аксиом формальной теории состоит из логических и специальных аксиом.

Логическими аксиомами являются аксиомы исчисления предикатов. Небольшое отличие имеется только в группе II аксиом исчисления предикатов, а именно, группа II аксиом пишется так:

II. 1) XA(X)→A(t), II. 2) A(t)→XA(X), где t – терм, свободный для X в A(X) (т.е. не содержащий переменной X).

Для каждой теории определяются различные теории специальных аксиом. Они описывают свойства объектов именно данной теории; так как логические аксиомы одинаковы для всех формализованных теорий, то при определении теории их не указывают.

III. Правила доказуемости те же, что в исчислении предикатов.

IV. Определение доказуемых формул (теорем) то же, что в исчислении предикатов.

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

Рассмотрим пример формальной математической теории - теорию групп.

Теория групп определяется следующим образом.

Алфавит (достаточно указать только группы символов 1, 3 и 4).

1.Предметные переменные: X, Y, Z, ... и одна предметная константа: e.

2.Один предикатный символ: "=".1

3.Один функциональный символ: .

Специальные аксиомы:

1.X Y Z(X (Y Z) = (X Y ) Z);

2.X(e X = X);

3.X Y (X Y = e);

4.X Y Z((X = Y ) → ((X Z = Y Z) (Z X = Z Y )));

5.X(X = X);

6.X Y ((X = Y )→(Y = X));

7.X Y Z((X = Y )→((Y = Z)→(X = Z))).

В формальных теориях также могут решаться вопросы о непротиворечивости, полноте, разрешимости, независимости.

Объявленная Гильбертом цель спасти классическую математику от парадоксов с помощью доказательства ее непротиворечивости предполагала создание формальных систем, охватывающих арифметику (теория натуральных чисел), анализ и более широкие разделы

1Символ "=" также причисляют к логическим символам. Его смысл в содержательных интерпретациях обычно таков: отношение "a = b"означает, что a и b являются именами одного и того же объекта.

31

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

Причина неудачи была открыта Г¨еделем. Им была доказана теорема, которая теперь называется теоремой Г¨еделя о неполноте. Смысл этой теоремы заключается в том, что непротиворечивость формальной арифметики невозможно доказать с помощью этой теории, т.е. средство этой теории недостаточно для доказательства ее непротиворечивости. Смысл теоремы Г¨еделя можно сформулировать так: формальная математическая теория, если она непротиворечива, не может быть достаточно богата; если достаточно богатая математическая теория непротиворечива, то она не может быть полностью формализована. Поэтому та цель, которую ставил Гильберт, не достижима.

Однако непротиворечивость формальной арифметики может быть доказана с помощью некоторых дополнительных средств, с использованием так называемых нефинитных методов. Вопрос о том, можно ли использовать эти методы или нет, вызывает разногласие среди математиков.

Непротиворечивость формальной арифметики с использованием нефинитных методов была впервые доказана Генценом.

32