Пред.
След.
Макеты страниц
Распознанный текст, спецсимволы и формулы могут содержать ошибки, поэтому с корректным вариантом рекомендуем ознакомиться на отсканированных изображениях учебника выше Также, советуем воспользоваться поиском по сайту, мы уверены, что вы сможете найти больше информации по нужной Вам тематике ДЛЯ СТУДЕНТОВ И ШКОЛЬНИКОВ ЕСТЬ
ZADANIA.TO
31. Конструктивный вариант теоремы Гёделя о полнотеМножество всех оценок (т. е. распределений истинностных значений) атомарных формул, выполняющих данную формулу классического исчисления предикатов первого порядка, — это борелевское множество конечного бэровского класса в канторовом пространстве. Конструктивизация теории борелевских множеств, предпринятая в предыдущем пункте, позволяет нам дать конструктивный вариант теоремы Гёделя [1] о полноте. Мы будем рассматривать формулы, построенные обычным образом из предикатных символов, функциональных символов, свободных и связанных переменных и логических связок и кванторов Конечная последовательность формул
будет называться секвенцией. Мы отождествляем секвенции, если они равны как конечные множества. Аксиома — это секвенция, построенная из атомарных формул и их отрицаний и содержащая как
Для правила Д-введения имеется обычное условие: свободная переменная а не должна входить в заключение. Зафиксируем теперь взаимно однозначную рекурсивную нумерацию атомарных формул
Используя формул
Здесь мы предположили, что
— фиксированная взаимно однозначная нумерация всех термов. Если Так как в формуле Формула Формула доказуема тогда и только тогда, когда она логически истинна. Заменим временно правило Д-введения, сформулированное выше, на бесконечное правило
Выводы в модифицированном таким образом исчислении предикатов изоморфны выводам в формальной системе для борелевских множеств, построенной в предыдущем пункте, если мы сопоставим каждой формуле то позаботимся сначала о том, чтобы переменные, связываемые при Основная теорема Генцена утверждает, что правило сечения имеет место для исчисления предикатов как производное правило вывода:
Это утверждение оказывается непосредственным следствием справедливости правила сечения для исчисления борелевских множеств (через теорему о полноте). Действительно, если
|
1 |
Оглавление
|