Конструктивная математика (стр. 4 )

Правила для кванторов всеобщности

Γ |– F(v) (В∀) Γ |– ∀ v F(v)	Γ |– ∀ v F(v) (У∀) Γ |– F (t)
где v не является свободной	где t является
переменной для любой формулы в Γ	подстановочным для v в F(v)

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

3.19 (P(a) & ∀ x (P(x) ⊃ Q(x))) ⊃ Q(a).

3.20 ∀ xy P(x, y) ⊃ ∀ x P (x, x).

Правила для кванторов существования

Γ |– F(t) (В∃) Γ |– ∃ v F(v)	Γ |– ∃ v F(v) Γ ∪ { F(v) }|– C (У∃) Γ |– C
где t – подстановочный	где для C и любой формулы из Γ
для v в F(v)	v не является свободной переменной

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

3.21 (P(a) ∨ P(b)) ⊃ ∃ x P(x).

3.22 ∃ x P(x) ≡ ∀ x P(x).

Корректность и полнота логики предикатов

Множество правил вывода для логики предикатов обладает свойством корректности и полноты подобно свойствам пропозициональных выводов.

Теорема корректности. Если существует вывод замкнутой формулы F из множества формул Γ, тогда Γ влечёт F.

Теорема полноты. Для любой замкнутой формулы F и любого множества предложений Γ, если Γ влечёт F, то существует вывод F из некоторого подмножества Γ.

Полнота логики предикатов для случая счётного Γ и для другого множества правил вывода была доказана Куртом Гёделем в 1930 году.

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

Логика предикатов, определённая выше немного более ограничена, чем что обыкновенно называется ``логикой первого порядка'', и наша следующая цель – удалить эти ограничения. Во-первых, мы обобщим понятие терма. В дополнение к объектным константам и объектным переменным, мы разрешим построение термов с использованием символов для функций, ``функциональных констант''. Во-вторых, мы добавим к языку знак равенства, и уравнения будут включены как новый тип атомарных формул.

Наше наиболее общее понятие сигнатуры определяется следующим образом.

Определение 28 (Сигнатура, константы). Сигнатура – это множество символов двух типов – функциональных констант и предикатных констант – с неотрицательным целым числом, называемым арностью, связанным с каждым символом. Объектная константа – это функциональная константа арности 0. Функциональная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Пропозициональная константы, так же как унарные и бинарные предикатные константы, определены как выше.

Определение 29 (Терм). Возьмём сигнатуру σ, не включающую ни дополнительных символов, указанных в начале данной части, ни знака равенства. Множество X строк замкнуто относительно правил построения термов, если

каждая объектная константа принадлежит X, каждая объектная переменная принадлежит X, для каждой функциональной константы h арности n (n > 0) и любой строки t1, ... , tn, если t1, ... , tn принадлежит X, тогда также принадлежит h(t1, ... , tn).

Строка является термом, если она принадлежит все множествам, которые замкнуты относительно правил построения.*

3.23 Каждый терм содержит объектную константу или объектную переменную. Верно или нет?

В логике первого порядка существуют три типа атомарных формул:

пропозициональные константы, строки вида R(t1, ... , tn) где R – предикатная константа арности n (n > 0) и t1, ..., tn – термы, строки вида (t1 = t2), где t1, t2 – термы.

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

Для любых термов t1 и t2, t1 ≠ t2 обозначает формулу (t1 = t2).

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

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

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

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

Γ |– t1 = t2 Γ |– F(t1) (З=) Γ |– F(t2)

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

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

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

3.27 x = y ⊃ f(x, y) = f(y, x).

см. Решение

3.28 ∀ x ∃ y (y = f(x)).

3.29 ∃ y (x = y & y = z) ⊃ x = z.

3.30 ∃ x (x = a & P (x)) ≡ P (a).

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

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

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

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

Пример: Теория линейного порядка

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

Мы будем упрощать запись формул сигнатуры арифметики первого порядка (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) является моделью этой теории. Арифметика первого порядка имеет также другие модели, и некоторые из них совсем не похожи на систему натуральных чисел (задача 3.40).

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

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

3.34 2 ≠ 4.

3.35 x' ≠ x.

3.36 x'= x + 1.

3.37 x ≤ x.

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

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

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

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

3.39 Γ непротиворечива.

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

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

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

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

Недоказуемые теоремы для диофантовых уравнений