Доказательство. № Утверждение Обоснование

Доказательство теоремы а:├ _L ┐┐А A.

№ Утверждение Обоснование

1. (┐ А ┐┐A) ((┐ А ┐A) A) А₃; { A/B, ┐ A/A },

2. ┐ А ┐A {┐ A/A },

3. (┐ А ┐┐A) А {┐ А ┐┐A/А,┐ А А/В, А/С },

4. ┐┐ А (┐ А ┐┐A) A₁; {┐┐ A/А, ┐ А/B },

5. ┐┐ А А {┐┐ А/A,┐A ┐┐А/В, А/С }.

Доказательство теоремы б: ├; _L А ┐┐ A.

№ Утверждение Обоснование

1. (┐┐┐ А ┐A) ((┐┐┐ А A) ┐A) А₃; {┐┐ A/B },

2. ┐┐┐ А ┐A a; {┐ A/A },

3. (┐┐┐ А A) ┐┐A MP; 2,1,

4. А (┐┐┐ А A) A₁; { ┐┐┐ А/B },

5. ┐┐ А А Сл. 2; {┐┐┐ А/В,

А/A, ┐┐ А/С }.

Доказательство теоремы в: ├; _L ┐ A (А В).

№ Утверждение Обоснование

1. ┐ A гипотеза,

2. А гипотеза,

3. A (┐ B A) A₁; { ┐ B/B },

4. ┐ A (┐ B ┐A) A₁; {┐ A/A, ┐ B/B },

5. ┐ B A MP; 2, 3,

6. ┐ B ┐A MP; 1, 4,

7. (┐ B ┐A) ((┐ B A) В) А₃,

8. (┐ B ┐A) B MP; 6, 7,

9. B MP; 5, 8,

10. ┐ A, ├; _L В на основании ПП 1- 9.

11. ┐ A├; _L А В теорема дедукции,

12. ├; _L ┐A (А В) теорема дедукции.

Доказательство теоремы г: ├ _L (┐В ┐A) (A В).

№ Утверждение Обоснование

1. ┐ B ┐A гипотеза,

2. A гипотеза,

3. (┐ B ┐A) ((┐ B A) В) А₃,

4. A (┐ B A) A₁; { ┐ B/B },

5. (┐ B ┐A) B MP; 1, 3,

6. A В Сл. 2; {┐ B А/В, B/С },

7. B MP; 2, 6,

8. ┐B ┐A, A ├; _L В на основании ПП 1-7,

9. ┐ B ┐A, ├; _L A В теорема дедукции,

10. ├ _L (┐В ┐A) (A В) теорема дедукции.

Доказательство теоремы д: ├ _L (A В) (В A).

№ Утверждение Обоснование

1. А В гипотеза,

2. ┐┐ А A a,

3. ┐┐ А B Сл. 2; { A/B, ┐┐ А/A, А/С },

4. ┐┐ B ┐┐B б; { B/A },

5. ┐┐А ┐┐B Сл. 2; { ┐┐ А/A, ┐┐B/С },

6. (┐┐А ┐┐B) (┐В ┐A) г; {┐ A/B, ┐ B/A },

7. ┐ В ┐A MP; 5, 6,

8. А В├ _L ┐В ┐A на основании ПП 1-7,

9. ├ _L (A В) (┐ В ┐ A) теорема дедукции.

Доказательство теоремы е: ├ _L A ┐В ┐(A B)).

№ Утверждение Обоснование

1. А гипотеза,

2. A В гипотеза,

3. В МР; 1, 2,

4. А, A В├ _L В на основании 1-3,

5. А ├ _L (A В) теорема дедукции,

6. ├ _L A ((A B) B) теорема дедукции,

1. ├ _L ((A B) B) (┐ В ┐(A B))
2. д; { A B/A },

8. ├ _L A (┐ В ┐(A B)) Сл. 2; { ((A В) B)/B,

(┐В ┐(A B))/C }.

Доказательство теоремы ж: ├; _L (A B) (┐A B)).

№ Утверждение Обоснование

1. A B гипотеза,

2. ┐ A B гипотеза,

3. (A B) (┐В ┐A) д,

4. ┐ В ┐A МР; 1, 3,

5. (┐A B) (┐В ┐┐A) д; { А/A },

6. ┐ В ┐┐A МР; 2, 5,

7. (┐В ┐┐A) (┐В ┐A) B A ₃; { А/A },

8. (┐В ┐A) B МР; 6, 7,

9. B МР; 4, 8.

10. A B, A B ├; _L B на основании ПП 1-9,

11. A ├; _L (┐A B) B теорема дедукции,

12. ├; _L (A B) ((┐A B)) теорема дедукции.

Множество теорем теории

Пусть формула A содержит переменные а₁,..., a_n, и пусть задана некоторая интерпретация I фор­мулы A, то есть приписаны истинностные значения переменным а₁,..., a_n. Обозначим

a_i, если a_i = И А, если I(А) = И

┐ a_i, если a_i = Л ┐А, если I(А) = Л

 

в данной интерпретации.

Лемма. ├; _L .

Доказательство Индукция по структуре формулы A.

1. Переменная. Пусть А = а. Тогда а├; _L а и ┐ а├; _L ┐ а.

2. Отрицание. Пусть А = ┐В.

Пусть I(B) = И. Тогда I(А) = Л и А' = ┐А = ┐┐B. По индукционному предположению ├; _L В. Но ├; _L В ┐┐B по теореме 4.12.б, следовательно, ├; _L В ┐┐B = А '.

Пусть I(В) = Л. Тогда I(А) = И и А' = А = ┐B. По индукционному предположению ├; _L В ┐B = А '.

3. Импликация. Пусть A=(B С). По индукционному предположению

├; _L и ├; _L .

Пусть I(В) = Л. Тогда, независимо от значения I(С), имеем:

I(А) = И и = ┐B, А' = А.

Но ├; _L ┐ B,├; _L┐ B (B С) по теореме 4.12.в, следовательно, ├; _L B С = А '.

Пусть I(B) = И и I(С) = И. Тогда I(А) = И и = С, А' = A = B С. Имеем: ├; _L С, ├; _L С (B С) (аксиома A ₁ с подстановкой { C/A }), следовательно, ├; _L B С = А '.

Пусть I(B) = И и I(С) = Л. Тогда А' = ┐А = ┐ (B С), В' = В и С' = ┐ С. Имеем: ├B, ├ С, ├; _L B (┐С ┐(B С)) по теореме 4.12.е. Следовательно, ├; _L ┐ (B С) = А'.

 

Теорема 4.13. Теоремами теории L являются общезначимые формулы и только они:

├; _L A — тавтология.