4. Приложение. Логика теорий первого порядка с равенством
. К оглавлению . Показать весь текст .
В данном разделе приведены аксиомы логики исчисления предикатов, аксиомы равенства и сведения о некоторых базовых теоремах логики. Использована аксиоматика из книги Д. Гильберт, П. Бернайс «Основания математики. Логические исчисления и формализация арифметики». Далее кратко «Основания математики».
Выбранная аксиоматика представляется наиболее интуитивно понятной и удобной для построения логических выводов среди известных мне. К тому же опора на общеизвестный классический труд в значительной мере страхует от каких-то незамеченных читателями неточностей.
«Основания математики», Глава III. Исчисление высказываний. Параграф 3. Дедуктивная логика высказываний. Подпараграф 2. Одна система исходных формул для дедуктивной логики высказываний: полнота этой системы.
I. Формулы для импликации:
1) A ⇒ (B ⇒ A)
2) (A ⇒ (A ⇒ B)) ⇒ (A ⇒ B)
3) (A ⇒ B) ⇒ ((B ⇒ C) ⇒ (A ⇒ C))
II. Формулы для конъюнкции:
1) A ∧ B ⇒ A
2) A ∧ B ⇒ B
3) (A ⇒ B) ⇒ ((A ⇒ C) ⇒ (A ⇒ B ∧ C))
III. Формулы для дизъюнкции:
1) A ⇒ A ∨ B
2) B ⇒ A ∨ B
3) (A ⇒ C) ⇒ ((B ⇒ C) ⇒ (A ∨ B ⇒ C))
IV. Формулы для эквивалентности:
1) (A ⇔ B) ⇒ (A ⇒ B)
2) (A ⇔ B) ⇒ (B ⇒ A)
3) (A ⇒ B) ⇒ ((B ⇒ A) ⇒ (A ⇔ B)
V. Формулы для отрицания:
1) (A ⇒ B) ⇒ (¬ B ⇒ ¬ A)
2) A ⇒ ¬ ¬ A
3) ¬ ¬ A ⇒ A
«Основания математики», Глава IV. Формализация процесса вывода II: Исчисление предикатов. Параграф 2. Связанные переменные и правила для кванторов. Подпараграф 4. Окончательная формулировка правил исчисления предикатов; изображение форм категорических суждений; случай пустой индивидной области.
В качестве исходных формул разрешается брать тождественные формулы исчисления высказываний. К ним мы добавляем обе основные формулы:
(a) ∀ x A(x) ⇒ A(a)
(b) A(a) ⇒ ∃ x A(x)
Тут я от себя добавлю пояснение, что аксиома (b) - это бесконечное множество импликаций. И мы можем выбирать ту, которая удобна нам. Например, при доказательстве существования для (5.3) в подразделе II раздела 2 мы взяли как бы A(l_ChrLim ′), за счёт чего воспользовались правилом силлогизма и эта посылка исчезла из итоговой формулы. Но за счёт аксиомы (b) мы получаем возможность выбрать путь (значение переменной a), который позволяет достичь нужной цели.
В качестве схем вывода, позволяющих получить новые формулы из ранее полученных, у нас имеется, наша первоначальная схема заключения
Если верно U и верно U ⇒ R, то верно R.
И кроме того, две новые схемы:
(α) Если верно U ⇒ B(a), то верно U ⇒ ∀ x B(x)
и
(β) Если верно B(a) ⇒ U, то верно ∃ x B(x) ⇒ U
Обе они могут применяться лишь тогда, когда в первой формуле схемы переменная a встречается лишь на местах, указанных в качестве аргумента, а x не входит в B(a).
«Основания математики», Глава V. Исчисление предикатов с равенством. Полнота одноместного исчисления предикатов:
(J_1) a = a
(J_2) a = b ⇒ ( A(a) ⇒ A(b) )
Где A(a) представляет собой любую логически корректную формулу, построенную из функциональных букв, предикатных букв теории, кванторов (в область действия которых не попадают a, b) и логических связок. При этом заменять a на b можно как везде, где написано a, так и в некоторых (произвольно выбранных) местах написания переменной a.
Теперь перечислим некоторые ключевые теоремы про логику первого порядка с равенством.
VI. Ключевые теоремы
1) Теорема дедукции
Простой вариант:
Если при добавлении к теории T утверждения A можно вывести утверждение B без использования правил вывода (α) и (β), то в теории T без добавления утверждения A можно вывести утверждение A ⇒ B.
Но мы использовали и более тонкий вариант этой теоремы:
Использовать правила вывода (α) и (β) можно, но только так, чтобы при этом не связывалась на одна свободная переменная утверждения A.
Или, записывая более формально:
Если есть вывод T, A ⊢ B без использования (α) и (β) в отношении свободных переменных утверждения A, то есть вывод T ⊢ A ⇒ B.
2) Вложенные посылки эквивалентны конъюнкции посылок
Утверждение:
A_1 ⇒ (A_2 ⇒ … ⇒ (A_N ⇒ B)…)
Эквивалентно утверждению:
(A_1 ∧ A_2 ∧ … ∧ A_N) ⇒ B
Поэтому последовательность посылок во вложенных импликациях можно менять произвольным образом.
3) Правило C. Смотри, например, Э. Мендельсон, «Введение в математическую логику», Глава 2. Теория первого порядка. Раздел 7. Правило C.
Если у нас в теории T имеется истинное утверждение вида ∃ x A(x), то есть, имеется вывод:
T ⊢ ∃ x A(x))
И имеется ещё такой вывод:
T, A(u) ⊢ B, без использования (α) и (β) по u,
То найдётся вывод:
T ⊢ B
4) Определение равенства. Смотри, например, Э. Мендельсон, «Введение в математическую логику», Глава 2. Теории первого порядка. Раздел 8. Теория первого порядка с равенством. Предложение 2.26. <критерий того, что в теории первого порядка истинны аксиомы равенства>
Если в аксиомах теории есть только функциональные буквы и знак равенства, то аксиомы равенства (J_1) и (J_2) для неё будут выполнены тогда и только тогда, когда
a. Для каждой функциональной буквы f_n() с аргументами x_1, … x_m (где m - количество аргументов функции f_n(x_1, … x_m)) истинно:
(x_1=y_1 ∧ … ∧ x_m=y_m) ⇒ (f_n(x_1, … x_m) = f_n(y_1, … y_m))
b. Для знака равенства истинна рефлексивность:
x = x
c. Для знака равенства истинна транзитивность:
x = y ⇒ (z=x ⇒ z=y)
5) Введение новых функциональных букв и предметных констант. Смотри, например, Э. Мендельсон, «Введение в математическую логику», Глава 2. Теории первого порядка. Раздел 9. Введение новых функциональных букв и предметных констант. Следствие 3.3.
Если для формулы A(u, x_1, … x_m) выполнено:
∃_1 u A(u, x_1, … x_m)
То можно аксиоматизировать функцию f(x_1, … x_m) следующей формулой:
A(f(x_1, … x_m), x_1, … x_m)
И добавление данной аксиомы к теории не добавляет никакой дополнительной логики, кроме нового обозначения. В частности, такая функция будет соответствовать аксиомам равенства, если данная теория до введения этого обозначения была теорией первого порядка с равенством.
Напоминание - обозначение «существует и единственно»
∃_1 u A(u, x_1, … x_m) означает выполнение 2 условий:
a. ∃ u A(u, x_1, … x_m)
b. A(u_1, x_1, … x_m) ∧ A(u_2, x_1, … x_m) ⇒ u_1 = u_2
6) Эквивалентные формулы логики высказывания взаимозаменяемы внутри любых формул логики. Например, если доказана формула
A ⇒ (¬ B ∨ C)
И при этом верно:
B ⇔ D
То будет доказана и формула:
A ⇒ (¬ D ∨ C)
7) ¬ ∀ n ¬ A(n) ⇔ ∃ n A(n)
Доказательство.
Ветка 1
∀ n ¬ A(n) ⇒ ¬ A(i), по (a) ∀ x A(x) ⇒ A(a)
A(i) ⇒ ¬ ∀ n ¬ A(n), из предыдущего, контрапозиция
∃ n A(n) ⇒ ¬ ∀ n ¬ A(n), из предыдущего по (β) Если верно B(a) ⇒ U, то верно ∃ x B(x) ⇒ U
Ветка 2
¬ A(i) ⇒ ∃ n ¬ A(n), по (b) A(a) ⇒ ∃ x A(x)
¬ ∃ n ¬ A(n) ⇒ A(i), из предыдущего, контрапозиция
¬ ∃ n ¬ A(n) ⇒ ∀ n A(n), из предыдущего по (α) Если верно U ⇒ B(a), то верно U ⇒ ∀ x B(x)
¬ ∀ n A(n) ⇒ ∃ n ¬ A(n), из предыдущего, контрапозиция
¬ ∀ n ¬ A(n) ⇒ ∃ n A(n), из предыдущего, заменяя A(n) на ¬ A(n) и ¬ (¬ A(n)) на A(n) в соответствии с п.6)
Соединяя ветку 1 и 2 получим:
¬ ∀ n ¬ A(n) ⇔ ∃ n A(n)
8) ∀ i (B ∨ A(i)) ⇔ B ∨ ∀ i (A(i))
Доказательство
Ветка 1.
A(n) ⇒ ∃ i A(i)
B ∧ A(n) ⇒ B ∧ ∃ i A(i)
∃ i (B ∧ A(n)) ⇒ B ∧ ∃ i A(i)
¬ B ∨ ¬ ∃ i A(i) ⇒ ¬ ∃ i (B ∧ A(n))
¬ B ∨ ∀ i ¬ A(i) ⇒ ∀ i ¬ (B ∧ A(n))
¬ B ∨ ∀ i ¬ A(i) ⇒ ∀ i (¬ B ∨ ¬ A(n))
B ∨ ∀ i A(i) ⇒ ∀ i (B ∨ A(n))
Ветка 2.
∀ i (B ∨ A(i)) ⇒ (B ∨ A(n))
∀ i (B ∨ A(i)) ⇒ (¬ B ⇒ A(n))
[¬ B ∧ ∀ i (B ∨ A(i))] ⇒ A(n)
[¬ B ∧ ∀ i (B ∨ A(i))] ⇒ ∀ i A(i)
∀ i (B ∨ A(i)) ⇒ (¬ B ⇒ ∀ i A(i))
∀ i (B ∨ A(i)) ⇒ (B ∨ ∀ i A(i))
Доказано.
9) ∃ i (B ∨ A(i)) ⇔ B ∨ ∃ i A(i)
Доказательство.
Ветка 1.
∀ i A(i) ⇒ A(n)
B ∧ ∀ i A(i) ⇒ B ∧ A(n)
B ∧ ∀ i A(i) ⇒ ∀ i (B ∧ A(i))
¬ ∀ i (B ∧ A(i)) ⇒ ¬ B ∨ ¬ ∀ i A(i)
∃ i ¬ (B ∧ A(i)) ⇒ ¬ B ∨ ∃ i ¬ A(i)
∃ i (¬ B ∨ ¬ A(i)) ⇒ ¬ B ∨ ∃ i ¬ A(i)
∃ i (B ∨ A(i)) ⇒ B ∨ ∃ i A(i)
Ветка 2.
A(n) ⇒ B ∨ A(n)
B ⇒ B ∨ A(n)
B ∨ A(n) ⇒ ∃ i (B ∨ A(i))
A(n) ⇒ ∃ i (B ∨ A(i))
B ⇒ ∃ i (B ∨ A(i))
∃ i A(u) ⇒ ∃ i (B ∨ A(i))
B ∨ ∃ i A(u) ⇒ ∃ i (B ∨ A(i))
Доказано.
10) (A ∨ B) ⇔ (A ∨ (¬ A ∧ B))
Пояснение.
Данная эквивалентность часто используется, когда доказываются импликации вида:
(A_1 ∨ A_2 ∨ … ∨ A_n) ⇒ D
Для доказательства тогда надо доказывать импликации вида:
A_1 ⇒ D
A_2 ⇒ D
…
A_n ⇒ D
А после этого использовать аксиому III.3) (A ⇒ C) ⇒ ((B ⇒ C) ⇒ (A ∨ B ⇒ C)) несколько раз.
Но зачастую в приведённой цепочке импликаций вместо импликации A_n ⇒ D доказывают импликацию:
(¬ A_1 ∧ ¬ A_2 ∧ … ∧ A_n) ⇒ D
И то, что стоит слева от A_n в последней импликации - это как раз ¬ A, если считать, что (A_1 ∨ A_2 ∨ … A_{n-1}) - это A, а A_n - это B из доказываемой нами формулы VI.10. Поэтому и происходит подмена этого B в импликации B ⇒ D на (¬ A ∧ B), что вместо исходной посылки:
(A_1 ∨ A_2 ∨ … ∨ A_n)
Можно заменить её на эквивалентную:
(A_1 ∨ A_2 ∨ … ∨ (¬ A_1 ∧ ¬ A_2 ∧ … ∧ A_n))
И такая замена оказывается возможной как раз благодаря данной теореме VI.10.
Данную импликацию VI.10 можно проверить по таблицам истинности, можно дать логический вывод, но поясню, почему эта эквивалентность истинная - третьим способом - через «булеву алгебру».
A ∨ B эквивалентно A ∨ (¬ A ∧ B) по следующей причине:
B ⇔ (A ∨ ¬ A) ∧ B ⇔ (A ∧ B) ∨ (¬ A ∧ B)
Поэтому:
(A ∨ B) ⇔ A ∨ (A ∧ B) ∨ (¬ A ∧ B)
Но так как для A тоже верно:
A ⇔ (A ∧ B) ∨ (A ∧ ¬ B)
То
A ⇔ A ∧ (A ∧ B)
Ведь A ∨ (A ∧ B) ничем не отличается от (A ∧ B) ∨ (A ∧ ¬ B) ∨ (A ∧ B), где последний член просто повторяет первый, а дизъюнкция первых двух - эквивалентна A.
А в силу последней эквивалентности верно:
A ∨ (A ∧ B) ∨ (¬ A ∧ B) ⇔ A ∨ (¬ A ∧ B)
Откуда и получаем искомое:
(A ∨ B) ⇔ A ∨ (¬ A ∧ B)
Теорема доказана.