Напишем:


✔ Реферат от 200 руб.
✔ Контрольную от 200 руб.
✔ Курсовую от 500 руб.
✔ Решим задачу от 20 руб.
✔ Дипломную работу от 3000 руб.
✔ Другие виды работ по договоренности.

Узнать стоимость!

Не интересно!

 

Логика - доступно для всех

  • Увеличить размер шрифта
  • Размер шрифта по умолчанию
  • Уменьшить размер шрифта

Функциональные символы и равенство: семантика

Выводы в логике первого порядка

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

Новые аксиомы выражают рефлексивность равенства и имеют вид Ж |– t = t , где t – произвольный терм. Новые правила вывода – правила замены:

G |– t1 = t2 G |– F(t1)

(З=)

G |– F(t2)

G |– t1 = t2 G |– F(t2)

G |– F(t1)

где t1 и t2 свободные для v в F(v).*

Теории первого порядка

Теория первого порядка сигнатуры s определяется с помощью аксиом. Интерпретация, при которой истинны все аксиомы теории первого порядка G, называется моделью G. Если теория первого порядка G выполнима, мы также говорим что она непротиворечива. Логические следствия теории первого порядка называется её теоремами. Доказательство предложения F в теории первого порядка G есть вывод F из подмножества аксиом из G.

Теоремы корректности и полноты выполняются для логик предикатов с функциональными символами и равенством и могут быть сформулированы в рамках теорий первого порядка следующим образом. В соответствие с теоремой корректности, если существует доказательство предложения F в теории первого порядка G, тогда F является теоремой G. В соответствие с теоремой полноты Гёделя, обратное также верно: для любой теоремы F теории первого порядка G, существует доказательство F в G.

Однако, добавление правил вывода для кванторов второго порядка ведёт к формальной системе которая корректна, но не полна.

Арифметика первого порядка

Мы будем упрощать запись формул сигнатуры арифметики первого порядка (6) введением следующего обозначения: a будет записываться как 0, s(t) как t' , f(t1, t2) как t1+t2, и g(t1, t2) как t1 · t2. Аксиомы арифметики первого порядка являются универсальным замыканием следующих формул:

x' № 0.

x'= y'Й x = y.

(F(0) & " v (F(v) Й F(v'))) Й " v F(v) для любой формулы F(v).

x + 0 = x.

x + y'= (x + y)'.

x · 0 = 0.

x · y'= x · y + x.

*

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

В следующих формулах 1 обозначает терм 0', 2 – 0'', и 4 – 0''''. Через t1 Ј t2 мы обозначаем формулу $ v(t2 = t1 + v), где v – первая объектная переменная, которая не встречается в t1, t2.

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

Нестандартные модели арифметики

Термы 0, 0', 0'', ... называются цифрами. Модель M арифметики первого порядка стандартна, если для каждого c О |M| существует цифра t такая, что tM = c.

Модель арифметики первого порядка (7) стандартна.

Существуют модели арифметики первого порядка, которые не обладают этим свойством. Чтобы доказать существование такой модели, полезно рассмотреть следующую теорию первого порядка G. Сигнатура G получается из сигнатуры арифметики первого порядка добавлением буквы b в качестве новой объектной константы. Множество аксиом G получается из множества аксиом арифметики первого порядка добавлением формул b № 0, b № 0', b № 0'', ... в качестве новых аксиом.

Арифметика первого порядка имеет нестандартную модель.

Существование нестандартных моделей арифметики следует из теоремы Сколема (1920), который обобщил раннюю работу Леопольда Лёвенхейма (1915). Возможность таких моделей резко контрастирует с результатом задачи 1.41. Разница связана с тем, что язык арифметики первого порядка является слишком ограниченным для выражения аксиомы индукции. ``Арифметика второго порядка'', в которой схема индукции заменяется по аксиоме (8), не имеет нестандартных моделей.

Теорема неполноты Гёделя

Пусть M – нестандартная модель арифметики первого порядка. Может случится что M ``не отличима'' от модели (7) в том смысле, что для любой замкнутой формулы F арифметики первого порядка F истинно при M тогда и только тогда, когда F истинно при (7). Но некоторые нестандартные модели не обладают этим свойством: может существовать предложение F такое, что при M предложение F истинно, а при (7) ¬F истинно. Так как и M и интерпретация (7) являются моделями арифметики первого порядка, значит ни F, ни ¬F не являются теоремами, а это означает, что арифметика первого порядка неполна. Этот факт, известный как теорема неполноты Гёделя, был доказан Куртом Гёделем в 1931 году.