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

VI. Система натурального вывода

Урок VI.

Система натурального вывода.

Считается, что в логике высказывание существует так называемая «разрешающая процедура», т.е. автоматизированная процедура (алгоритм), которая позволяет определить, является ли формула тождественно-ложной, тождественно-истинной или выполнимой. Такой процедурой является построение таблиц истинности (хотя этот способ и не является единственным для логики высказываний).

В логике предикатов (в логике, где мы анализируем отношения внутри высказывания) такой процедуры не существует. Поэтому решение о том, является ли та или иная формула в логике предикатов тождественно-истинной или тождественно-ложной зависит от творческих способностей исследователя.

Тем не менее, существует несколько механизмов, позволяющих исследователю облегчить этот процесс. Одним из самых распространённых является натуральное исчисление предикатов. Здесь мы будем опираться на систему, построенную Уиллардом Куайном — знаменитым американским философом, логиком и математиком.

Смысл этого метода заключается в том, что исследователю предлагается несколько правил вывода первого порядка (прямых правил) и несколько правил вывода второго порядка (непрямых правил). Правила первого порядка – это правила, в которых из одной формулы следует другая. Правила второго порядка (непрямые правила), это правила, которые возникают в результате некой «цепочки» выводов.

Поясним на примере математики. Из формула «2х2» непосредственно следует «4». В логике бы это правило «2х2→4» называлось бы правилом первого порядка или прямым правилом. А вот формула «2+2х2» требует нескольких действий. Сначала мы должны 2 умножить на 2 и получать 4, а затем прибавить к четырем два. В результате мы получим 6. В логике такое правило «2+2х2→6» называлось бы правилом второго рода или непрямым правилом.

Иными словами. Если мы вынуждены, чтобы доказать некую формулу «а» пройти ряд процедур (a→b→c→d→e) чтобы получить в результате «e», вывод «a→e» назывался бы непрямым (выводом второго порядка).

Понятно, что правил второго рода (непрямых правил) может быть сколько угодно, в зависимости от предпочтений исследователя. А вот правила первого рода (прямые правила) весьма ограничены.

Сначала перечислим их, а затем разъясним:

 

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

  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), где a — любое допущение в системе вывода.

Проще говоря, имея в выводе формулу «а», мы имеем право записать «а⊃b» или «b⊃a», только если «b» где-то встречается в нашей системе выводов.

 

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

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

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

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

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

 

Дополнительная информация

 

Очевидно, что правило введения импликации «a, b ⊧ (а⊃b), (b⊃a)» и правило дедукции «(Г, a⊧ b)╞ (Г⊧ a⊃b)» взаимозаменяемы. Однако, для упрощения мы приводим здесь оба правила.

Правило введения импликации можно прочитать так: Если в системе вывода мы имеем «a» и «b», то мы вправе сделать вывод «а⊃b» или «b⊃a».

Правило дедукции мы можем прочитать так: Если из множества посылок следует «b», то мы можем сделать вывод «а⊃b», где «а» — любая посылка из этого множества.

 

В другом написании эти правила выглядят так:

 

В˄ а, b У˄ a˄b О˄ ¬(a˄b) В˅ а У˅ а˅b, ¬a О˅ ¬(а˅b)
a˄b а ¬a∨¬b а˅b b ¬a∧¬b

 

У⊃ а⊃b, a У⊃ а⊃b, ¬b В⊃ a, b О⊃ ¬(а⊃b)
b ¬a (а⊃b), (b⊃a) a˄¬b

 

В≡ а⊃b, b⊃a У≡ a≡b В¬¬ а У¬¬ ¬¬а
a≡b а⊃b, b⊃a ¬¬а a

 

РРС (а⊃с)˄(b⊃с) СА (b˄¬b)⊃а ДОП ¬а⊃(b˄¬b)
(а˅b)→с ¬а а

 

ПД Г, a ⊧b
Г⊧ a⊃b

 

Что значит доказать формулу? Это означает, что мы её сначала разбиваем на части (согласно правилам вывода) а затем собираем по частям (согласно тем же правилам). Простой пример: Надо доказать элементарную формулу вида a˄b. Записываем ее первым действием:

  1. a˄b
  2. а – получаем из действия 1 путем применения правила исключения конъюнкции.
  3. b — получаем из действия 1 путем применения правила исключения конъюнкции.
  4. a˄b — получаем из действий 2 и 3 путем применения правила введения конъюнкции. ■

Формула считается доказанной. Это значит, что она выполнима и не является тождественно-ложной.

Важно

 

Чтобы доказать, что формула является тождественно-истинной, мы должны строить доказательство «от противного», т.е. должны предположить, что формула ложна. Если мы найдем в формуле противоречие (предположив, что она ложная), значит изначальная формула – тождественно-истинная.

 

Предположим, дается формула a⊃(b⊃a) — закон ввода истинного антецедента.

Пытаемся понять смысл формулы.

Дано некое «a». Из этого мы делаем вывод, что «а» истинно при условии «b» (по-научному – может ли произвольное «b» имплицировать «а»?)

Постараемся все это перевести на естественный язык.

а — Москва – столица России.

b – Париж столица Франции.

Если верно, что «Москва столица России», следует ли из этого, что «Москва столица России при условии, что Париж столица Франции»?

Пытаемся разобраться. Дана формула a⊃(b⊃a). Доказательство от противного:

Предположим, что формула не верна. Записываем допущение, где эту формулу отрицаем.

Действие первое.

  1. + ¬(a⊃(b⊃a)).

Чтобы отрицать формулу, берём её всю в скобки и ставим перед ней знак отрицания «¬». Получаем + ¬(a⊃(b⊃a)).

Действие второе. Вспоминаем, как отрицается импликация. Схема такая: ¬(a⊃b)→a˄¬b. Следовательно, записываем:

  1. a˄¬(b⊃a) из 1 по О⊃.

Читаем второе действие так: a˄¬(b⊃a) из первого действия по закону отрицания импликации.

  1. a из 2 по У˄.
  2. ¬(b→a) из 2 по У˄.

В 3 и 4 действии мы разделили формулу a˄¬(b⊃a) пополам по закону удаления конъюнкции.

  1. b˄¬a – из 4 по О⊃.
  2. ¬a – из 5 по У˄.

Теперь обратите внимание: у нас есть «¬a» в шестом действии и «а» в третьем действии. Мы создаем противоречие по закону введения конъюнкции:

  1. a˄¬a – из 6 и 3 по В˄.

Теперь мы по закону введения импликации соединяем формулы из седьмого и первого действий. Из противоречия выводим отрицание основной формулы:

  1. (a˄¬a)⊃¬(a⊃ (b⊃a)) из 7 и 1 по В⊃.

Поскольку из противоречия мы получили отрицание основной формулы, следовательно, мы делаем вывод о том, что верна основная формула. Это – закон доказательства от противного. Записываем последнее действие:

  1. a⊃(b⊃a) из 8 по ДОП.■

Значит, рассуждение «Если верно, что «Москва столица России», следовательно «Москва столица России при условии, что Париж столица Фран-ции» — рассуждение верное.

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

Дано:

a⊃(b⊃a)

Доказательство:

  1. + a
  2. + b.

Т.е., мы берем в качестве посылок антецедент всей формулы (a) и антецедент из консеквента (b⊃a) – «b». Пытаемся составить формулу по правилам натурального вывода.

  1. b⊃a – из 1 и 2 по В⊃.

Понятно, что мы можем из двух посылок получить и «a⊃b», и «a⊃а», и «b⊃b», и «a˄b», и «a˅b»… Но для доказательства исходной формулы нам нужно именно «b⊃a». Важно, что это действие мы выполняем строго по законам натурального вывода.

  1. a⊃(b⊃a) из 3 и 1 по В⊃. ■

Теперь давайте попробуем решить более сложную теорему. Предположим, что дано (a˄b)⊃c))⊃(a⊃(b⊃c)) – закон экспортации. В качестве допущения принимаем антецеденты формулы:

 

  1. + (a˄b)⊃c
  2. + a
  3. + b

 

Для удобства, допущения мы обозначаем знаком «+».

 

  1. a˄b – из 2 и 3 по В˄
  2. с – из 1 и 4 по У⊃

 

Последний пункт надо пояснить. Имея в первом действии (a˄b)⊃c и в четвертом a˄b, легко получаем «с» по правилу (а⊃b), a╞ b. Правило называется «Удаление импликации» (У⊃).

 

  1. b⊃c из 5 и 3 по В⊃
  2. a⊃(b⊃c) из 6 и 2 по В⊃
  3. (a˄b)⊃c))⊃(a⊃(b⊃c)) – из 7 и 1 по В⊃■

 

Попробуем эту же формулу решить методом «от противного». В качестве допущения предположим, что она ложна:

 

  1. + ¬((a˄b)⊃c))⊃(a⊃(b⊃c)))
  2. (a˄b)⊃c))˄¬(a⊃(b⊃c)) из 1 по О⊃
  3. (a˄b)⊃c) из 2 по У˄
  4. ¬(a⊃(b⊃c)) из 2 по У˄
  5. a˄¬(b⊃c) из 4 по О⊃
  6. a из 5 по У˄
  7. ¬(b⊃c) из 5 по У˄
  8. b˄¬c из 7 по О⊃
  9. b из 8 по У˄
  10. ¬c из 8 по У˄
  11. ¬(a˄b) из 10 и 3 по У⊃
  12. ¬a˅¬b из 11 по О˄
  13. ¬a из 12 и 9 по У˅
  14. ¬a˄a из 13 и 6 по В˄
  15. ¬((a˄b)⊃c))⊃(a⊃(b⊃c)))⊃(¬a˄a) из 1 и 14 по В⊃
  16. (a˄b)⊃c))⊃(a⊃(b⊃c)) из 15 по ДОП■

 

Некоторые действия требуют пояснений.

Действие 11. В выводе мы имеем две формулы «¬c» и «(a˄b)⊃c)». По правилу удаления импликации «а⊃b, ¬b) ╞ ¬a» получаем формулу «¬(a˄b)».

Действие 13. В выводе мы имеем две формулы «¬a˅¬b» и «b». По правилу удаления дизъюнкции «а˅b, ¬a ╞ b» получаем формулу «¬(a˄b)».

Действие 14. В этом действии мы достигли главного результата — противоречия.

Действие 15. По правилу введения импликации, мы привели формулу к противоречию. Мы могли бы свести формулу к абсурду, если бы поменяли местами условие и следствие: «(¬a˄a)⊃¬((a˄b)⊃c))⊃(a⊃(b⊃c)))». Правило сведения к абсурду и правило доказательства от противного – идентичны.

Действие 16. Поскольку мы доказали ложность нашего предположения (что формула ложна), значит изначальная формула истинна.

Важно

 

Если мы доказываем формулу «от противного» и нам это удается, значит, формула тождественно-истинная. Если нам это не удается – формула опровержима.

Если мы доказываем формулу «прямым» способом и нам это удается, значит, формула выполнима. Если не удается – формула тождественно-ложная.

Совет

 

Рекомендуем всякую формулу попытаться решить «от противного».

Если это невозможно, то воспользуйтесь другими советами.

Если формула представляет собой тождество «A≡B», то решая её «от противного», предположите, что либо антецедент, либо консеквент — ложные. То есть, либо «¬(¬A⊃B)», либо «¬(A⊃¬B)».

Если формула представляет собой сложную импликацию вида «A⊃B⊃C⊃D⊃E», то в качестве допущений можно взять все формулы, кроме последнего члена импликации.

Если формула представляет собой сложную импликацию вида «A⊃B⊃C⊃D⊃E», то её можно решить методом «от противного», взяв в качестве допущений все формулы, кроме последнего члена импликации, и допустить, что последний член импликации ложен.

 

Для закрепления навыков, попробуем решить еще одну аксиому:

(a⊃b)≡¬(a˄¬b)

Сложность в том, что специального правила для отрицания тождества нет.

Мы можем предположить, что эта формула не верна, если отрицаем одну из частей тождества:

¬(a⊃b)≡¬(a˄¬b) или

(a⊃b)≡(a˄¬b)

Предположим, мы выбираем второй вариант. Записываем наши предположения в посылках:

  1. + a⊃b
  2. + a˄¬b
  3. a – из 2 по У˄
  4. ¬b– из 2 по У˄
  5. b– из 1 и 3 по У⊃
  6. b˄¬b– из 5 и 4 по В˄
  7. (b˄¬b)⊃(a˄¬b) – из 2 и 6 по В⊃
  8. ¬(a˄¬b) – из 7 по СА.

Итак, получили промежуточный вывод — ¬(a˄¬b). Вводим новое допущение:

  1. + a
  2. ¬a˅¬¬b – из 8 по О˄
  3. ¬¬b– из 9 и 10 по У⊃
  4. b – из 11 по У¬¬
  5. a⊃b – из 9 и 12 по В⊃
  6. (a⊃b)⊃¬(a˄¬b) – из 13 и 8 по В⊃

15.¬(a˄¬b)⊃(a⊃b) – из 13 и 8 по В⊃

  1. (a⊃b)≡¬(a˄¬b) – из 14 и 15 по В≡ ■

 

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

Для дальнейшей работы нам необходимо ввести несколько определений.

Терм (t) — предметная (индивидная) переменная или предметная (индивидная) константа в формуле. От простой переменной терм отличается тем, что фиксирует не абстрактную переменную в формуле, а конкретную константу (конкретный объект), либо предметную переменную (множество объектов определённого класса).

Свободное и связанное вхождение переменной в формулу. Свободной называется переменная, не находящаяся под действием кванторов (P(x) — «х» свободна, «х» имеет свободное вхождение в формулу). Связанной называется переменная под действием любого квантора (ƎxP(x) или ∀xP(x) — «х» связана, «х» имеет связанное вхождение в формулу).

Правила кванторов можно сформулировать на основе системы Уилларда Куайна KQ2 (системы Куайна — KQ1, KQ2 и KQ3 отличаются лишь формулировкой правил кванторов, главным образом В∀ и УƎ):

 

  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) УƎ ƎxP(x)
P(t) ƎхP(x) ∀xP(x) P(t)

 

Для двух последних правил — В∀ и УƎ необходима оговорка. Переменные (термы), возникающие в результате применения этих правил, должны быть «ограниченными» (или «отмеченными») . Это означает, что для данных переменных повторное применение этих правил недопустимо. Иными словами, переменная не может быть отмечена (ограничена) более одного раза.

Поясним сказанное на примере. Предположим, надо решить теорему ƎxP(x)⊃∀xP(x).

  1. + ƎxP(x)
  2. P(x) из 1 по УƎ, х — ограничена

Иными словами, используя правила В∀ и УƎ мы ограничиваем переменную (в данном случае «х») и фиксируем это, написав «х — ограничена»

  1. ∀xP(x) из 2 по В∀, х — ограничен

Как видим, «х» ограничена два раза, что недопустимо. Следовательно, вывод неправильный.

К четырем правилам натурального вывода предикатов можно добавить еще два. Они не являются необходимыми, но в некоторых случаях могут оказаться весьма полезными:

 

  1. ¬∀xP(x)→Ǝx¬P(x) — правило отрицания ∀ (О∀)
  2. ¬ƎxP(x)→∀x¬P(x) — правило отрицания Ǝ (ОƎ)

 

О∀ ¬∀xP(x) ОƎ ¬ƎxP(x)
Ǝx¬P(x) ∀x¬P(x)

 

Попробуем использовать эти правила для решения всё той же задачи — ƎxP(x)⊃∀xP(x). Попробуем теперь решить эту задачу «от противного», чтобы создать противоречие. Предположим, что формула ƎxP(x)⊃∀xP(x) неверна.

  1. + ¬(ƎxP(x)⊃∀xP(x))
  2. ƎxP(x)∧¬∀xP(x) — из 1 по О⊃
  3. ƎxP(x) — из 2 по У∧
  4. ¬∀xP(x) — из 2 по У∧
  5. Ǝx¬P(x) — из 4 по О∀
  6. P(x) — из 3 по УƎ, х — ограничена
  7. ¬P(x) — из 5 по УƎ, х — ограничена

Мы опять пришли к повторному ограничению «х». Формула не доказана. Впрочем, она и не может быть доказана, поскольку неверна.

Чтобы закрепить навыки, попробуем решить задачу посложнее:

∀x(S(x)⊃P(x))∧∀x(P(x)⊃Q(x))⊃∀x(S(x)⊃Q(x))

 

  1. + ¬(∀x(S(x)⊃P(x))∧∀x(P(x)⊃Q(x))⊃∀x(S(x)⊃Q(x)))
  2. (∀x(S(x)⊃P(x))∧∀x(P(x)⊃Q(x)))∧¬∀x(S(x)⊃Q(x)) — из 1 по О⊃
  3. ∀x(S(x)⊃P(x))∧∀x(P(x)⊃Q(x)) — из 2 по О∧
  4. ¬∀x(S(x)⊃Q(x)) — из 2 по О∧
  5. ∀x(S(x)⊃P(x)) — из 3 по О∧
  6. ∀x(P(x)⊃Q(x)) — из 3 по О∧
  7. S(x)⊃P(x) — из 5 по У∀
  8. P(x)⊃Q(x) — из 6 по У∀
  9. Ǝx¬(S(x)⊃Q(x)) — из 4 по О∀

 

Здесь необходимы пояснения, поскольку у студентов зачастую возникает непонимание: как в системе натурального вывода отрицаются простые суждения.

Дело в том, что до сих пор мы с вами отрицали простые суждения по очень простой формуле:

 

суждение его отрицание
∀xS(x) ∃x¬S(x)
∃xS(x) ∀x¬S(x)
∃x¬S(x) ∀xS(x)
∀x¬S(x) ∃xS(x)

 

Однако теперь, в логике предикатов, мы стали использовать более подробную запись простых суждений. Если выражение «∀xS(x)» до сих пор означало для нас «Все x суть S», то теперь оно означает «Для всех x, если он S, то он и P».

Поясним. Выражение «Все люди млекопитающие» ранее мы записывали как «∀xS(x)». Теперь же мы то же выражение записываем как «∀x(S(x)⊃P(x))». Читаем: «Для всех x правомерно, что, если он человек, то он млекопитающее». Соответственно, выражение «Некоторые люди млекопитающие», которое мы обозначали как «∃xS(x)», теперь обозначается «∃x(S(x)∧P(x))» и читается соответственно – «Для некоторых x верно, что он человек и млекопитающее».

Последний абзац рекомендуем студентам перечитать несколько раз.

Мы с вами прекрасно знаем, как отрицаются простые суждения. Необходимо изменить квантор на противоположный и изменить качество суждения также на противоположное. С кванторами всё понятно: было Ǝ, стало — ∀; было ∀ — стало Ǝ. Но как поменять качество суждения? Как грамотно превратить утвердительное суждение в отрицательное и наоборот?

Предположим, мы отрицаем суждение «∀x(S(x)⊃P(x))». Первое, что приходит в голову, записать его отрицание так: «∃x¬(S(x)⊃P(x))». Но, с другой стороны, в частном суждении должна быть не импликация, а конъюнкция: «∃x(S(x)˄¬P(x))». Эквивалентны ли эти записи? Т.е. верно ли, что «∃x¬(S(x)⊃P(x))≡∃x(S(x)˄¬P(x))»?

На самом деле данные записи являются эквивалентными (основные эквивалентности вы можете посмотреть в приложении к данному учебному пособию). Поэтому,

 

¬∀x(S(x)⊃P(x))↔∃x¬(S(x)⊃P(x))↔∃x(S(x)˄¬P(x))

¬∃x(S(x)˄P(x))↔∀x¬(S(x)˄P(x))↔∀x(S(x)⊃¬P(x))↔∀x(¬S(x)˅¬P(x))

 

Продолжим.

 

  1. ¬(S(x)⊃Q(x)) — из 9 по УƎ — х ограничен
  2. S(x)∧¬Q(x) — из 10 по О⊃
  3. S(x) — из 11 по У∧
  4. ¬Q(x) — из 11 по У∧
  5. P(x) — из 7 и 12 по У⊃
  6. Q(x) — из 8 и 14 по У⊃
  7. Q(x)∧¬Q(x) из 15 и 13 по В∧
  8. ¬(∀x(S(x)⊃P(x))∧∀x(P(x)⊃Q(x))⊃∀x(S(x)⊃Q(x)))⊃(Q(x)∧

∧¬Q(x)) — из 1 и 16 по В⊃

  1. ∀x(S(x)⊃P(x))∧∀x(P(x)⊃Q(x))→∀x(S(x)⊃Q(x)) — из 17 по СА (сведение к абсурду). ■

Пункты 17 и 18 мы могли бы записать по-другому:

  1. (Q(x)∧¬Q(x))⊃¬(∀x(S(x)⊃P(x))∧∀x(P(x)⊃Q(x))→∀x(S(x)⊃Q(x))) — из 16 и 1 по В⊃
  2. ∀x(S(x)⊃P(x))∧∀x(P(x)⊃Q(x))⊃∀x(S(x)⊃Q(x)) — из 17 по ДОП (доказательство от противного). ■

 

Важно

 

Напоминаем: Для общих суждений (с квантором ∀) свойства объекта выражаются через импликацию «⊃», например, ∀x(S(x)⊃P(x)).

Для частных суждений (с квантором ∃) свойства объекта выражаются через конъюнкцию «∧», например, ∃x(S(x)∧P(x)).

Соответственно, мы имеем запись суждений:

Обще-утвердительные — ∀x(S(x)⊃P(x));

Частно-утвердительные — ∃x(S(x)∧P(x));

Обще-отрицательные — ∀x(S(x)⊃¬P(x));

Частно-отрицательные — ∃x(S(x)∧¬P(x)).

Логическое следование «⊨ » (на основе правила дедукции) всегда можно преобразовать в импликацию «⊃», но не наоборот. Логическое следование более сильный термин, нежели импликация.

 

Проверим на истинность силлогизма:

 

Никто из студентов+ не получает пенсию+
Некоторые пенсионеры — ворчливые старики
Некоторые ворчливые старики не учатся в вузах+

 

Переведем его на формальный язык логики:

 

∀x(S(x)⊃¬P(x))
∃x(P(x)∧Q(x))
∃x(Q(x)∧¬S(x))

 

Объединим посылки знаком конъюнкции, а заключение знаком импликации:

 

∀x(S(x)⊃¬P(x))∧∃x(P(x)∧Q(x))⊃∃x(Q(x)∧¬S(x))

 

  1. + ¬(∀x(S(x)⊃¬P(x))∧∃x(P(x)∧Q(x))⊃∃x(Q(x)∧¬S(x)))
  2. ∀x(S(x)⊃¬P(x))∧∃x(P(x)∧Q(x))∧¬∃x(Q(x)∧¬S(x)) – из 1 по О⊃
  3. ∀x(S(x)⊃¬P(x)) – из 2 по У∧
  4. ∃x(P(x)∧Q(x)) – из 2 по У∧
  5. ¬∃x(Q(x)∧¬S(x)) – из 2 по У∧
  6. S(x)⊃¬P(x) – из 3 по У∀
  7. P(x)∧Q(x) – из 4 по У∃ х — ограничен
  8. ∀x(Q(x)⊃S(x)) – из 5 по О∃
  9. Q(x)⊃S(x) – из 8 по У∀
  10. P(x) – из 7 по У∧
  11. Q(x) — – из 7 по У∧
  12. S(x) – из 11 и 9 по У⊃
  13. ¬P(x) – из 6 и 12 по У⊃
  14. P(x)∧¬P(x) – из 13 и 10 по В∧
  15. (P(x)∧¬P(x))⊃¬(∀x(S(x)⊃¬P(x))∧∃x(P(x)∧Q(x))⊃∃x(Q(x)∧¬S(x))) – из 14 и 1 по В⊃
  16. ∀x(S(x)⊃¬P(x))∧∃x(P(x)∧Q(x))⊃∃x(Q(x)∧¬S(x)) – из 15 по ДОП. ■

 

Пробуем решить эту же формулу с помощью гипотез.

 

  1. + ∀x(S(x)⊃¬P(x))
  2. + ∃x(P(x)∧Q(x))
  3. S(x)⊃¬P(x) – из 1 по У∀
  4. P(x)∧Q(x) – из 2 по У∃ х — ограничен
  5. P(x) – из 4 по У∧
  6. Q(x) – из 4 по У∧
  7. ¬S(x) – из 3 и 5 по У⊃
  8. Q(x)∧¬S(x) – из 6 и 7 по В∧
  9. ∃x(Q(x)∧¬S(x)) — из 8 по В∃
  10. ∀x(S(x)⊃¬P(x))∧∃x(P(x)∧Q(x)) — из 1 и 2 по В∧
  11. ∀x(S(x)⊃¬P(x))∧∃x(P(x)∧Q(x))⊃∃x(Q(x)∧¬S(x)) — из 9 и 10 по В⊃. ■

 

Совет

 

В ряде случаев, когда в общей формуле мы встречаем выражение вида «a⊃b», мы можем предположить (ввести допущение), что существует «a». Из этого допущения по правилу удаления импликации, мы получаем «b» (a⊃b, a ⊧ b). Для подобных частных случаев мы вправе сформулировать своё собственное правило второго порядка: «a⊃b ⊧ a, b).

 

Дополнительная информация

 

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

Вообще, схемой аксиом, может служить любая доказанная тождественно-истинная формула. При этом, аксиома служит «прототипом» бесконечного множества истинных формул, построенных по форме (схеме) этой аксиомы.

Возьмем, к примеру, закон утверждения консеквента – «B⊃(A⊃B)». Это тождественно-истинная формула (при желании, студент может её доказать). А это значит, что любая формула такого вида (такой схемы) также является тождественно-истинной. Поэтому, встретив в выводе формулу подобной схемы, доказывать её уже не имеет смысла. Можно просто сослаться на данную схему и принять истинность формулы данный схемы по аналогии.

Когда мы говорим, что аксиома служит «прототипом» бесконечного количества истинных формул, мы имеем ввиду, что схема «B⊃(A⊃B)» может быть выражена как «с⊃(a⊃с)», «d⊃(c⊃d)», «с˅b⊃(a⊃(с˅b))», «(d⊃(c⊃d))⊃(¬z⊃(d⊃(c⊃d))) и т.д.

Студент может самостоятельно добавлять схемы аксиом в свою систему исчислений. Для этого достаточно убедиться, что добавленная аксиома действительно является аксиомой (тождественно-истинной формулой). Кроме того, поскольку правила натурального вывода и правила аксиоматической системы исчислений не противоречат друг другу, читатель может смело использовать все известные ему правила одновременно.

Основными правилами аксиоматической системы исчисления предикатов остаются те же, что мы использовали в системе натурального вывода. Однако, меняются правила кванторов:

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

Пояснение: если каждый «х» имеет признак P, то признак P имеет и константа «t» (из множества «х»).

«Если все в группе ЮРДб хорошо знают логику, то и г-н Агафонов (из группы ЮРДб) тоже хорошо знает логику»

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

Пояснение: Если мы имеем константу «t», обладающую признаком P, то верно, что некоторые «x» (из множества, в которое входит «t») тоже обладают признаком P.

«Если г-н Агафонов из группы ЮРДб хорошо знает логику, следовательно, некоторые студенты ЮРДб хорошо знают логику» (если быть более точным, то «Если г-н Агафонов из группы ЮРДб хорошо знает логику, следовательно, существует хотя бы один студент из группы ЮРДб хорошо знающий логику»

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

Пояснение: Если для всех «х» верно, что он имеет признак P при условии А, то при условии A признак P будет свойственен всем «х».

«Если все студенты хорошо успевают, то они получают стипендию → Если студенты хорошо успевают, то все они получают стипендию».

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

Пояснение: если для всех «х» верно, что некий признак P ведет к результату A, то это верно и для некоторых «x».

«Если все студенты, хорошо учась, получают стипендию, следовательно, это верно и для некоторых студентов».

5. P(t)⊧∀xP(x) — правило обобщения (В∀), при условии, что терм «t» не был ранее связан квантором Ǝ и не является константой.

«Если студенты ЮРДб хорошо знают логику, следовательно, все студенты ЮРДб хорошо знают логику».