Кортунов Вадим Вадимович kortunov@live.com

X. Натуральные исчисления в модальной логике

Урок X.

Натуральные исчисления в модальной логике.

 

Для натуральных исчислений в модальной логике используются все законы и правила исчисления логики высказываний. К ним прибавляются правила кванторов и специальные правила модальной логики. В этом смысле, натуральное исчисление в модальной логике является расширением натурального исчисления логики предикатов.

Итак, напомним правила логики высказываний:

 

Правила вывода первого рода:

  1. а,b ⊧ a˄b –введение ˄ — конъюнкции — (кратко: В˄)

Поясняем. Знак «⊧» означает логическое следование и читается «следовательно». Название правила «введение конъюнкции» кратко обозначается, как «В˄». Далее, по аналогии:

  1. a˄b ⊧ а – удаление (исключение) конъюнкции ˄ (кратко У˄)
  2. ¬(a˄b) ⊧ ¬a∨¬b — отрицание ˄ (кратко О˄)
  3. а⊧ а˅b – введение ˅ (В˅)
  4. а˅b, ¬a ⊧ b — удаление ˅ (У˅)
  5. ¬(а˅b) ⊧¬a∧¬b — отрицание ˅ (О˅)
  6. а⊃b, a) ⊧ b – удаление ⊃ (У⊃)¹
  7. а⊃b, ¬b) ⊧ ¬a– удаление ⊃ (У⊃)²
  8. a, b ⊧ (а⊃b), (b⊃a) — введение ⊃ (В⊃)
  9. ¬(а⊃b) ⊧ a˄¬b — отрицание ⊃ (О⊃)
  10. а⊃b, b⊃a ⊧ a≡b — введение ≡ (В≡)
  11. a≡b ⊧ а⊃b, b⊃a — удаление ≡ (У≡)
  12. а⊧ ¬¬а — введение двойного отрицания (В¬¬)
  13. ¬¬а⊧ а — удаление двойного отрицания (У¬¬)

 

Правила вывода второго рода (которые нужны в любом случае):

((а⊃с)˄(b⊃с)) ⊧ (а˅b) →с – рассуждение разбором случаев (РРС)

(b˄¬b⊃а) ⊧ ¬а – сведение к абсурду (СА)

(¬а⊃ (b˄¬b)) ⊧ а – доказательство от противного (ДОП)

(Г, a⊧ b) ⊧ (Г⊧ a→b) — правило дедукции. Читается: если из множества гипотез Г и посылки а логически следует b, то из множества гипотез Г логически следует a⊃b.

 

Что касается правил кванторов  (с помощью которых мы осуществляли исчисления предикатов), то мы можем выбрать систему натурального вывода:

 

  1. ∀xP(x)⊃P(t) – схема удаления ∀(У∀)
  2. P(t)⊃ ƎхP(x) – схема введения Ǝ (ВƎ)
  3. P(t)⊃∀xP(x) — схема введения ∀ (В∀)
  4. ƎxP(x)⊃P(t) – схема удаления Ǝ (УƎ)

 

Или же, можем использовать аксиоматическую систему:

 

∀xP(x) ⊃P(t) – схема удаления ∀ (У∀)

P(t)⊃ƎхP(x) – схема введения Ǝ (ВƎ)

∀x(А⊃P(x))⊃(А⊃∀P(х)) – схема введения ∀ в консеквент.

∀x(P(x)⊃А)⊃(ƎхP(х)⊃А) – схема введения Ǝ в антецедент.

P(t)⊃∀xP(x) — правило обобщения.

 

Добавляем специальные правила натурального вывода модальной логики:

 

□A→A – правило удаления необходимости (У□)

A→ ◊A –- введение возможности (В◊)

¬□A→¬◊A – отрицание необходимости (О□)

¬◊A→□¬A – отрицание возможности (О◊)

□(A˄B)→□A˄□B – введение необходимости в конъюнкции (В□˄)

□A˄□B→□(A˄B) – удаление необходимости из конъюнкции (У□˄)

◊(A˅B)→ ◊A˅◊B – введение возможности в дизъюнкцию (В◊˅)

◊A˅◊B→◊(A˅B) – удаление возможности из дизъюнкции (У◊˅)

□A˅□B→□(A˅B) – удаление необходимости из дизъюнкции (У□˅)

◊(A˄B)→◊A˄◊B – введение возможности в конъюнкцию (В◊˄)

□(A⊃B)→□A⊃□B – введение необходимости в импликацию (В□⊃)

□A→□□A – введение дополнительной необходимости (В□□)

□∀xA(x)→∀x□A(x) – перестановка необходимости от всеобщности (∀□)

∀x□A(x)→□∀xA(x) – перестановка необходимости к всеобщности (□∀)

◊∃xA(x)→ ∃x◊A(x) — перестановка возможности от существования (∃◊)

∃x◊A(x)→◊ ∃xA(x) – перестановка возможности к существованию (◊∃)

◊A→□◊A – введение необходимости возможности (В□◊)

◊A, □B→◊(A˄B) — замена необходимости на возможность (З□◊)

(A↔B)→□(A↔B) – введение необходимой эквивалентности (В□↔)

□(A↔B)→(A↔B) – удаление необходимой эквивалентности (У□↔)

 

Правило второго рода:

A→□A – правило введения необходимости (В□) – правило Гёделя

 

Имеет смысл вспомнить эквивалентности:

□A⇔¬◊¬A

◊A⇔¬□¬A

∇A⇔◊A˄◊¬A

а также отрицания:

¬□А⇔◊¬ A;

¬◊A⇔□¬А;

¬∇А⇔□А∨□¬A

 

Предположим, дана выводимость

□∀x(A(x)⊃В(x))⊃□∀x(□A(x)⊃◊B(x)).

Попробуем доказать эту формулу от противного и предположим:

 

+¬(□∀x(A(x)⊃В(x))⊃□∀x(□A(x)⊃◊B(x)))

□∀x(A(x)⊃В(x)) – из 1 по О⊃

∀x□(A(x)⊃В(x)) – из 2 по ∀□

□(A(x)⊃В(x)) – из 3 по У∀

A(x)⊃В(x) – из 4 по У□

¬(□∀x(□A(x)⊃◊B(x))) — из 1 по О⊃

□∀x□A(x) – из 6 по О⊃

¬□∀x◊B(x) — из 6 по О⊃

¬◊∀x◊B(x) – из 8 по О□

□¬∀x◊B(x) – из 9 по О◊

¬∀x◊B(x) – из 10 по У□

∃х¬◊B(x) – из 11 по О∀

¬◊B(x) – из 12 по У∃ — х ограничена

□¬B(x) – из 13 по О◊

¬B(x) – из 14 по У□

∀x□A(x) – из 7 по У□

□A(x) – из 16 по У∀

A(x) – из 17 по У□

В(x) – из 5 и 18 по У⊃

В(x)˄¬B(x) – из 19 и 15 по В˄

(В(x)˄¬B(x))⊃¬(□∀x(A(x)⊃В(x))⊃□∀x(□A(x)⊃◊B(x))) —  из 20 и 1 по В⊃ (или по правилу дедукции)

□∀x(A(x)⊃В(x))⊃□∀x(□A(x)⊃◊B(x)) – из 21 по ДОП. ■

 

Решение задачи путём построения семантической таблицы:

В качестве еще одного примера, попробуем разобрать выводимость ⊧ □∀x□(P(x)˄S(x))˅◊∃x(◊¬P(x)˄◊S(x))˅¬◊∀x(P(x)˄¬S(x))˅

˅□∃x(□¬P(x)˄◊¬S(x)).

Начиная с 23 действия, мы могли бы эстетически построить таблицу по-другому:

Или, что то же самое, в классической системе натурального вывода:

  1. +¬(□∀x□(P(x)˄S(x))˅◊∃x(◊¬P(x)˄◊S(x))˅¬◊∀x(P(x)˄¬S(x))˅
    ˅□∃x(□¬P(x)˄◊¬S(x)))
  2. ¬□∀x□(P(x)˄S(x))˄¬◊ ∃x(◊¬P(x)˄◊S(x))˄◊∀xP(x)˄¬S(x)˄

˄¬□∃x(□¬P(x)˄◊¬S(x))) – из 1 по О˅

  1. ¬□∀x□(P(x)˄S(x)) – из 2 по У˄
  2. ¬◊∃x(◊¬P(x)˄◊S(x) – из 2 по У˄
  3. ◊∀xP(x)˄¬S(x) — из 2 по У˄
  4. ¬□∃x(□¬P(x)˄◊¬S(x) — из 2 по У˄
  5. ¬◊∀x□(P(x)˄S(x)) – из 3 по О□
  6. □¬∀x□(P(x)˄S(x)) – из 7 по О◊
  7. ¬∀x□(P(x)˄S(x)) – из 8 по У□
  8. ∃x□¬(P(x)˄S(x)) – из 9 по О∀
  9. □¬(P(x)˄S(x)) —  из 10 по У∃ (x ограничена)
  10. ¬(P(x)˄S(x)) – из 11 по У□
  11. □¬∃x(◊¬P(x)˄◊S(x)) – из 4 по О◊
  12. ¬∃x(◊¬P(x)˄◊S(x)) – из 13 по У□
  13. ∀x¬(◊¬P(x)˄◊S(x)) – из 14 по О∃
  14. ¬(◊¬P(x)˄◊S(x)) —  из 15 по У∀
  15. ◊(P(x)˄¬S(x)) — из 5 по У∀
  16. ◊P(x)˄◊¬S(x) – из 17 по В◊˄
  17. ¬◊∃x(□¬P(x)˄◊¬S(x) — из 6 по О□
  18. □¬∃x(□¬P(x)˄◊¬S(x) – из 19 О◊
  19. ¬∃x(□¬P(x)˄◊¬S(x) – из 20 по У□
  20. ∀x¬(□¬P(x)˄◊¬S(x) – из 21 по О∃
  21. ¬(□¬P(x)˄◊¬S(x) —  из 22 по У∀
  22. ◊P(x) – из 18 по У˄
  23. ◊¬S(x) – из 18 по У˄
  24. ¬P(x) ˅¬S(x)) – из 12 по О˄
  25. ¬◊¬P(x)˅¬◊S(x)) —  из 16 по О˄
  26. ¬□¬P(x)˅¬◊¬S(x) —  из 23 по О˄
  27. ¬□¬P(x) из 25 и 28 по У˅
  28. ¬◊¬P(x) из 29 по О□
  29. □¬¬P(x) из 30 по О◊
  30. P(x) из 31 по У¬¬ и У□
  31. S(x)) из 26 и 32 по У˅
  32. ¬P(x) – из 33 и 26 по У˅
  33. P(x)˄¬P(x) из 32 и 34 по В˄
  34. (P(x)˄¬P(x))⊃¬(□∀x□(P(x)˄S(x))˅◊∃x(◊¬P(x)˄◊S(x))˅ ˅¬◊∀x(P(x)˄¬S(x))˅□∃x(□¬P(x)˄◊¬S(x))) из 35 и 1 по В⊃
  35. □∀x□(P(x)˄S(x))˅◊∃x(◊¬P(x)˄◊S(x))˅¬◊∀x(P(x)˄¬S(x))˅

˅□∃x(□¬P(x)˄◊¬S(x)) – из 36 по ДОП.

Мы специально прописали вывод максимально подробно, чтобы читатель обратил внимание, что многие последовательности выводов часто повторяются. Например,

  • ¬□¬P(x) из 25 и 28 по У˅
  • ¬◊¬P(x) из 29 по О□
  • □¬¬P(x) из 30 по О◊
  • P(x) из 31 по У¬¬ и У□

или

  • ¬□∀x□(P(x)˄S(x))
  • ¬◊∀x□(P(x)˄S(x))
  • □¬∀x□(P(x)˄S(x))
  • ¬∀x□(P(x)˄S(x))

Такие последовательности позволяют нам самим создавать выводы второго рода.

В первом случае, это ¬□¬A→A и  ¬◊¬A→A; во втором — ¬□A→¬A и ¬◊A→¬A

Из практики исчислений можно добавить правила второго рода (схемы аксиом):

A→□A – правило введения необходимости (В□) – правило Гёделя
¬□A→□¬A
¬□A→¬A
¬□А→◊¬A
¬□¬A→◊A
□A→¬◊¬A
□¬А→¬◊A
¬◊A→¬A
¬◊¬A→□A
¬◊¬A→A
◊A→¬□¬A
◊¬A→¬□А

Попробуем решетить еще одну задачу. Правильным ли является рассуждение «Некоторые  испанцы в обед обязательно едят гаспачо. Любое гаспачо всегда готовится из томатов. Из этого следует, что некоторые испанцы, скорее всего, неравнодушны к помидорам»?

Попробуем перевести это умозаключение на формальный язык логики.

Некоторые испанцы в обед обязательно едят гаспачо.

Слово «некоторые» говорит нам, что необходим квантор существования. А слово «обязательно» намекает на знак необходимости:

▢∃x(I(x)˄G(x))

В принципе, сразу используя правило удаления необходимости, мы можем записать:

∃x(I(x)˄G(x))

Любое гаспачо всегда готовится из томатов:

▢∀x(G(x)⊃T(x))

Соответственно, снова используя правило удаления необходимости, получаем

∀x(G(x)⊃T(x))

Некоторые испанцы, скорее всего, неравнодушны к помидорам:

◊∃x(I(x)˄T(x))

В итоге получаем выводимость

⊨∃x(I(x)˄G(x))˄∀x(G(x)⊃T(x))⊃◊∃x(I(x)˄T(x))

Итак, дано:

 

⊨∃x(I(x)˄G(x))˄∀x(G(x)⊃T(x))⊃◊∃x(I(x)˄T(x))

  1. + ∃x(I(x)˄G(x))
  2. + ∀x(G(x)⊃T(x))

 

В качестве гипотез мы использовали посылки для построения заданного вывода «◊∃x(I(x)˄T(x))».

 

  1. I(x)˄G(x) – из 1 по У∃ — х ограничен
  2. G(x)⊃T(x) – из 2 по У∀
  3. I(x) – из 3 по У˄
  4. G(x) – из 3 по У˄
  5. T(x) – из 4 и 6 по У⊃
  6. I(x)˄T(x) – из 5 и 7 по В˄
  7. ∃x(I(x)˄T(x)) – из 8 по В∃
  8. ◊∃x(I(x)˄T(x)) — из 9 по В◊

 

Теперь мы получили искомый вывод. На этом исчисление можно закончить. Однако, для формального завершения можно дописать еще пару действий:

 

  1. ∃x(I(x)˄G(x))˄∀x(G(x)⊃T(x)) – из 1 и 2 по В˄
  2. ∃x(I(x)˄G(x))˄∀x(G(x)⊃T(x))⊃◊∃x(I(x)˄T(x)) из 10 и 11 по В⊃ (или правилу дедукции). ∎

Важно

 

В отличие от систем натурального вывода в классической логике (основанных на системах Куайна), в которых существует необходимое и достаточное количество правил для решения поставленных задач, в системах натурального вывода модальной логики (основанных в первую очередь на системах Льюиса) подобной однозначности нет. Этим объясняется большое количество вопросов к этим системам и продолжающийся поиск оптимальных решений.

 

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

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