dmitgu

Category:

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), который позволяет достичь нужной цели.

В качестве схем вывода, позволяющих получить новые формулы из ранее полученных, у нас имеется, наша первоначальная схема заключения <MP>

Если верно 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)

Теорема доказана.

Error

default userpic

Your reply will be screened

Your IP address will be recorded 

When you submit the form an invisible reCAPTCHA check will be performed.
You must follow the Privacy Policy and Google Terms of use.