Лекция №19

Тема: СВОЙСТВА ТЕОРИЙ ПЕРВОГО ПОРЯДКА

Основные вопросы, рассматриваемые на лекции:

1. Теорема истинности

2. Непротиворечивые теории

3. Полные (в широком и узком смысле) теории

4. Две формулировки теоремы Гёделя о полноте теорий

5. Формальная теория арифметики

6. Две теоремы Гёделя о неполноте теорий

Краткое содержание лекционного материала

Вычисление значения (a_x [ t ]) ^I терма a_x [ t ] и истинностного значения (A_x [ t ]) ^I формулы A_x [ t ] не зависит от порядка вычисления

Строго доказывается индукцией по термам и формулам

Лемма 1. Формула " xA Þ A_x [ t ] является логически общезначимой.

Лемма 2. Если переменная x не свободна в формуле A, то из формулы A Þ B логически следует формула A Þ" xB.

Формула теории первого порядка T называется истинной в теории T, если она истинна в любой модели теории T.

Теорема истинности. Любая теорема теории первого порядка T является истинной в теории T.

Доказательство индукцией по теоремам. Логические аксиомы являются логически общезначимыми формулами: аксиомы (A ₁)-(A ₃) как частные случаи тавтологий, а аксиома (A ₄) в силу леммы 1. Если T – теория с равенством, то истинностное значение формулы t = u, где t, u – термы, определяется следующим образом: (t = u) ^I ºИ, если t^I = u^I. Аксиомы (A ₅)-(A ₇) в любой интерпретации выражают основные свойства равенства, и поэтому будут логически общезначимыми. Следовательно, аксиомы (A ₁)-(A ₇) истинны в любой интерпретации языка теории T, в частности, в любой модели теории T, т.е. истинны в теории T.

Нелогические аксиомы истинны в теории T по определению модели теории T. Следовательно, все аксиомы теории T истинны в теории T.

Основные правила вывода являются логическими следствиями: правило (MP) – как тавтологическое следствие, а правило (") в силу леммы 2. Это значит, что если посылки (MP) и (") истинны в теории T, то их заключения тоже истинны в теории T.

Теория T называется (не)противоречивой, если в теории T (не) выводимо противоречие. Из теоремы истинности следует, что если теория T имеет модель, то она непротиворечива. В самом деле, если теория T имеет модель M, а противоречие A ÙØ A выводимо в теории T, то по теореме истинности формула A ÙØ A истинна в теории T, чего не может быть.

Теория T обладает свойством полноты в широком смысле, если каждая формула A теории T, истинная в теории T, является теоремой теории T.

Теория T обладает свойством полноты в узком смысле, если теория T непротиворечива и для каждой замкнутой формулы A теории T, не являющейся теоремой теории T, теория T [Ø A ] будет противоречивой. При этом теория T называется полной теорией. Легко увидеть, что в полной теории T для каждой замкнутой формулы A теории T, в точности одна из двух формул A и Ø A является теоремой теории T.

Из свойства полноты в узком смысле следует свойство полноты в широком смысле. Пусть T – полная теория, формула A теории T истинна в теории T. Тогда предположим, что формула A не является теоремой теории T. Тогда по определению полной теории T теория T [Ø A *] противоречива. По теореме редукции формула Ø A является теоремой теории T. По теореме истинности формула Ø A истинна в теории T,а формула A ложна в теории T. Получается противоречие: формула A истинна и ложна в теории T. Значит, формула A является теоремой теории T.

В теореме Гёделя о полноте для произвольных теорий первого порядка утверждается свойство полноты в широком смысле. Приведем две эквивалентные формулировки теоремы Гёделя о полноте.

I. Любая формула А теории Т является теоремой теории Т Û формула А истинна в теории Т.

II. Теория Т непротиворечива Û теория Т имеет модель.

В первой теореме Гёделя о неполноте для теории S опровергается свойство полноты в узком смысле.

I теорема Гёделя о неполноте. Любое непротиворечивое расширение формальной арифметики неполно.

II теорема Гёделя о неполноте. В формальной арифметике N можно построить формулу, которая интерпретируются «N непротиворечива» и которая недоказуема и неопрвержима в N.

1. Проблема разрешимости для теории T. Существует ли алгоритм, который для любой формулы A из теории T за конечное число шагов решает: формула A является теоремой из теории T или нет? При положительном решении этой проблемы теория T называется разрешимой.

2. Проблема разрешимости для множества M Í U. Существует ли алгоритм, который для любого элемента x Î U за конечное число шагов решает: x Î M или нет? При положительном решении этой проблемы множество M называется разрешимым.

3. Проблема разрешимости для функции f:U ® V. Существует ли алгоритм, который для любого элемента x Î U за конечное число шагов останавливается и выдает результат f (x)Î U при условии, что f (x) определено, и не выдает никакого результата или не останавливается при условии, что f (x) не определено? При положительном решении этой проблемы функция f называется вычислимым.

Проблема 1 – частный случай проблемы 2: достаточно принять за M множество теорем теории T и за U множество формул теории T.

Проблема 2 – частный случай проблемы 3: множество M разрешимо, если вычислима его характеристическая функция l _M:U ®{0,1}, такая, что

Теорема Черча. Любое непротиворечивое расширение формальной арифметики неразрешимо.