Часть 2. Логика предикатов. Теории первого порядка

Математическая логика и теория алгоритмов. Курс лекций

В.В. Гуренко

(продолжение)

§ 6. Предварённые нормальные формы.

Понятия логического следования и логической эквивалентности позволяют получить некоторые тождества – леммы теории К и всякойтеории первого порядка:

(1): "x С(x) É D º $ y (C(y) É D) | y не входит

(2): $ x С(x) É D º "y (C(y) É D) | свободно

(3): D É "x С(x) º "y (D É C(y)) | ни в C,

(4): D É $ x С(x) º $ y (D É C(y)) | ни в D!

Вместе с формулами замены кванторов:

(5): ^Ø" x C(x) º $ x ^Ø C(x)

(6): ^Ø $ x C(x) º " x ^Ø C(x)

система формул (1)…(6) с учетом правил переименования свободных и связанных переменных дает возможность для всякой формулы теории К:

§ выносить кванторы вперед;

§ заменять кванторы один другим;

§ «спускать» отрицание внутрь области действия квантора.

Опр. Формула вида:

Q₁x₁ Q₂x₂ … Q_nx_n Ф,

где Q₁, Q₂,…,Q_nx – кванторы, x_i и x_j различны для i ¹ j, Ф – формула без кванторов, называется предварённой нормальной формой (ПНФ), или предварённой формой, или формулой в предварённой форме:

Примеры ПНФ: F₁ = " x " z $ y [ ^Ø (P(y) É Q(x, y)) É ^Ø S(y, z)];

F₂ = $ y " x (P¹ É ^Ø Q²(x, y) É S²).

Примеры формулне в предварённой форме: F₃ = A²(x, z) É " x $ z [B¹(x) É A²(y, z)];

F₄ = $ y [ ^Ø" x (P¹ É Q²(x, y) É S²)];

F₅ = ^Ø" y [A(x,y) É Q(z) É ^Ø$ z (B(y,z)].

Лемма. В исчислении предикатов первого порядка для каждой формулы F существует эквивалентная ей формула F′ в предварённой форме.

Механизм приведения к ПНФ – применение к формуле тождеств (1)…(6).

Приведем доказательство леммы (1): "x С(x) É D º $ y (C(y) É D) (по E. Mendelson).

Построим вывод в теории K:

а) слева направо: если "x С(x) É D, то $ y (C(y) É D).

1. "x С(x) É D гипотеза: дано по условию.

2. ^Ø $ y (C(y) É D) гипотеза: предположение обратного следствию.

3. "y ^Ø (C(y) É D) 2, (6).

4. "y (C(y) & ^Ø D) 3 и эквивалентность: ^Ø (A É B) º A & ^Ø B.

A	B	^Ø(A É B)	A & ^ØB
Л	Л	Л	Л
Л	И	Л	Л
И	Л	И	И
И	И	Л	Л

5. " y (C(y) & ^Ø D) É C(y) & ^Ø D частный случай A ₄: " x A(x) É A(x) {C(y) & ^Ø D // A(x)}.

6. C(y) & ^Ø D 5, 4, MP.

7. C(y) 6 и тавтология A & B A.

8. " y C(y) 7, " ⁺ в частном случае: A(x) " x A(x).

9. " x C(x) 8, правило переименования связанных переменных

(по условию, С не содержит свободных вхождений y).

10. D 1, 9, MP.

11. ^Ø D 10, определение теории: отрицание формулы – формула.

12. D & ^Ø D 10, 11, определение теории: соединение двух формул

лог. связкой дает формулу.

13. "x С(x) É D, ^Ø $ y (C(y) É D) D & ^Ø D вывод 1,…,12.

14. "x С(x) É D ^Ø $ y (C(y) É D) É D & ^Ø D 13, Th. дедукции.

15. "x С(x) É D $ y (C(y) É D) 14, свойство импликации: ^Ø A É B A.

16. "x С(x) É D É $ y (C(y) É D) ■ _{в части а)} 15, Th. дедукции.

б) справа налево: если $ y (C(y) É D), то "x С(x) É D. Схема доказательства:

1. $ y (C(y) É D) гипотеза: дано по условию.

2. "x С(x) гипотеза.

3. " x C(x) É C(t) A ₄ {C // A}.

4. C(t) 3, 2, MP

… (получить C(t) É D,

далее D,

дважды Th. дедукции,

$ y (C(y) É D) É "x С(x) É D). ■ _{в части б)}

Доказанность в обе стороны доказывает эквивалентность:

"x С(x) É D º $ y (C(y) É D) ■.

Примечание. (P É Q) & (Q É P) P º Q.

Доказательство. (P É Q) & (Q É P) = «И» тогда и только тогда, когда

Это возможно во всех случаях, кроме:

Следовательно, P и Q должны принимать одинаковые истинностные

значения, то есть P º Q ■.

Примеры приведения к ПНФ.

(1): "x С(x) É D º $y (C(y) É D) (2): $x С(x) É D º "y (C(y) É D) (3): D É "x С(x) º "y (D É C(y)) (4): D É $x С(x) º $y (D É C(y)) (5): ^Ø"x C(x) º $x ^ØC(x) (6): ^Ø $x C(x) º "x ^ØC(x)

Пример 1. " x [A(x) É " y (B(x, y) É ^Ø" z C(y, z))]

1. " x [A(x) É " y (B(x, y) É $ z ^Ø C(y, z))] (5) по z

2. " x [A(x) É " y $ u (B(x, y) É ^Ø C(y, u))] (4), z®u

3. " x " v [A(x) É $ u (B(x, v) É ^Ø C(v, u))] (3), y®v

4. " x " v $ w [A(x) É (B(x, v) É ^Ø C(v, w))] (4), u®w

Все переменные в исходную формулу входят связанно. Согласно правилу переименования связанных переменных, можно возвратить имена переменным:

v®y, w®z:

5. " x " y $ z [A(x) É (B(x, y) É ^Ø C(y, z))] ■

Пример 2. A²(x, y) É $ y [A¹(y) É ($ x A¹(x) É B(y))]

1. A²(x, y) É $ y [A¹(y) É " u (A¹(u) É B(y))] (2), x®u (в области действия квантора!!!)

2. A²(x, y) É $ y " v [A¹(y) É (A¹(v) É B(y))] (3), u®v

3. $ w {A²(x, w) É " v [A¹(w) É (A¹(v) É B(w))]} (4), y®w

4. $ w " z {A²(x, w) É [A¹(w) É (A¹(z) É B(w))]} (3), v®z

В исходную формулу обе переменные – как x, так и y входят и свободно, и связанно. Обратное переименование z, w в x, y невозможно! ■

Дата добавления: 2014-01-20