Логика предикатов. Натуральная дедукция

Логика предикатов Натуральная дедукция Математическая логика и теория алгоритмов Алексей Романов 15 июня 2020 г. МИЭТ Правила натуральной дедукции • Снова сохраняются правила из логики высказываний. • Добавляются правила введения и исключения для кванторов. 2/9 Правила натуральной дедукции • Снова сохраняются правила из логики высказываний. • Добавляются правила введения и исключения для кванторов. ∀x A(x) A(t) ∀E ∃I • Начнём с простых: A(t) и ∃x A(x) . t — любой терм (обычно просто параметр). • Это аналоги типа γ в деревьях. 2/9 Правила натуральной дедукции • Снова сохраняются правила из логики высказываний. • Добавляются правила введения и исключения для кванторов. ∀x A(x) A(t) ∀E ∃I • Начнём с простых: A(t) и ∃x A(x) . t — любой терм (обычно просто параметр). • Это аналоги типа γ в деревьях. ·· ·· · A(a) ∃x A(x) ∀I A(a) ·· ·· · B ∃E • ∀x A(x) и B Здесь a — новый параметр, как в δ. 2/9 Пояснения к правилам • Смысл правила ∀I: чтобы доказать ∀x A(x), нужно доказать A(a) для произвольного a. Произвольность как раз обеспечивается тем, что это новый параметр и о нём ничего неизвестно. 3/9 Пояснения к правилам • Смысл правила ∀I: чтобы доказать ∀x A(x), нужно доказать A(a) для произвольного a. Произвольность как раз обеспечивается тем, что это новый параметр и о нём ничего неизвестно. • Смысл правила ∃E: мы временно даём название a тому объекту, существование которого утверждается. Правило немного аналогично ∨E. • Удобно помечать подвывод, вводящий параметр, этим параметром. • Есть упрощённый вариант ∃E, не вводящий подвывод, но он усложняет определение контрмоделей для недоказумых секвенций и мы его не используем. 3/9 Пример 1 • Докажем ∀x P(x) ∧ Q(x) ` (∀x P(x)) ∧ (∀x Q(x)): ∀x P(x) ∧ Q(x) ` ∀x P(x) ∧ Q(x) ∀x P(x) ∧ Q(x) ` P(a1 ) ∧ Q(a1 ) ∀x P(x) ∧ Q(x) ` P(a1 ) ∀x P(x) ∧ Q(x) ` ∀x P(x) ∀I ax ∀E ∧E ·· ·· · ∀x P(x) ∧ Q(x) ` ∀x Q(x) ∀x P(x) ∧ Q(x) ` (∀x P(x)) ∧ (∀x Q(x)) ∧I • В стиле с вынесенными предположениями: дано ∀x P(x) ∧ Q(x) P(a1 ) ∧ Q(a1 ) P(a1 ) ∀x P(x) ∀E ∧E ∀I a1 дано ∀x P(x) ∧ Q(x) P(a2 ) ∧ Q(a2 ) Q(a2 ) ∀x Q(x) (∀x P(x)) ∧ (∀x Q(x)) • Можно ли оба раза использовать a1 ? ∀E ∧E ∀I a2 ∧I 4/9 Пример 1 • Докажем ∀x P(x) ∧ Q(x) ` (∀x P(x)) ∧ (∀x Q(x)): ∀x P(x) ∧ Q(x) ` ∀x P(x) ∧ Q(x) ∀x P(x) ∧ Q(x) ` P(a1 ) ∧ Q(a1 ) ∀x P(x) ∧ Q(x) ` P(a1 ) ∀x P(x) ∧ Q(x) ` ∀x P(x) ∀I ax ∀E ∧E ·· ·· · ∀x P(x) ∧ Q(x) ` ∀x Q(x) ∀x P(x) ∧ Q(x) ` (∀x P(x)) ∧ (∀x Q(x)) ∧I • В стиле с вынесенными предположениями: дано ∀x P(x) ∧ Q(x) P(a1 ) ∧ Q(a1 ) P(a1 ) ∀x P(x) ∀E ∧E ∀I a1 дано ∀x P(x) ∧ Q(x) P(a2 ) ∧ Q(a2 ) Q(a2 ) ∀x Q(x) (∀x P(x)) ∧ (∀x Q(x)) ∀E ∧E ∀I a2 ∧I • Можно ли оба раза использовать a1 ? Да! Но незачем. 4/9 Пример 1 с флагами 1 7 5 8 6 1 ∀x P(x) ∧ Q(x) 7 P(a1 ) ∧ Q(a1 ) ∀x P(x) ∧ Q(x) a1 P(a1 ) ∧ Q(a1 ) P(a1 ) a2 P(a2 ) ∧ Q(a2 ) Q(a2 ) ∀E, 1 ∧E, 7 ∀E, 1 ∧E, 8 5 a1 P(a1 ) ∧E, 7 6 a1 Q(a1 ) ∧E, 8 3 ∀x P(x) ∀I, 5–5 4 ∀x Q(x) ∀I, 6–6 2 (∀x P(x)) ∧ (∀x Q(x)) ∧I, 3, 4 3 ∀x P(x) ∀I, 7–5 4 ∀x Q(x) ∀I, 8–6 2 (∀x P(x)) ∧ (∀x Q(x)) ∧I, 3, 4 появилась после 5 и 6, или ∀E, 1 (здесь важно, что строка 7 иначе в них нельзя использовать a1 ) 5/9 Пример 2 • Доказываем ∃x∀y P(x, y) ` ∀y∃x P(x, y): ∀y P(a2 , y) ∃x∀y P(x, y) дано P(a2 , a1 ) ∃x P(x, a1 ) ∀E ∃I ∃E a2 ; ∀y P(a2 , y) ` ∃x P(x, a1 ) ∀y∃x P(x, y) для ∃E ∀I a1 • Полное дерево (сначала попробуйте написать сами): 6/9 Пример 2 • Доказываем ∃x∀y P(x, y) ` ∀y∃x P(x, y): ∀y P(a2 , y) ∃x∀y P(x, y) дано P(a2 , a1 ) ∃x P(x, a1 ) для ∃E ∀E ∃I ∃E a2 ; ∀y P(a2 , y) ` ∃x P(x, a1 ) ∀y∃x P(x, y) ∀I a1 • Полное дерево (сначала попробуйте написать сами): ∃x∀y P(x, y), ∀y P(a2 , y) ` ∀y P(a2 , y) ∃x∀y P(x, y) ` ∃x∀y P(x, y) ax ∃x∀y P(x, y), ∀y P(a2 , y) ` P(a2 , a1 ) ∃x∀y P(x, y), ∀y P(a2 , y) ` ∃x P(x, a1 ) ∃x∀y P(x, y) ` ∃x P(x, a1 ) ∃x∀y P(x, y) ` ∀y∃x P(x, y) ax ∀E ∃I ∃E ∀I 6/9 Пример 2 • Доказываем ∃x∀y P(x, y) ` ∀y∃x P(x, y) с флагами: 1 ∃x∀y P(x, y) 4 a1 a2 ∀y P(a2 , y) 6 P(a2 , a1 ) ∀E, 4 5 ∃x P(x, a1 ) ∃I, 6 3 2 ∃x P(x, a1 ) ∀y∃x P(x, y) ∃E, 1, 4–5 ∀I, 4–3 7/9 Построение контрмодели • Если формулу или секвенцию доказать не получается, можно предположить, что она неверна и попробовать построить контрмодель. • В случае полного дерева выбираем вершину (секвенцию), на которой застряли. В контрмодели все её посылки должны быть истинны, а заключение ложно. • Значения предикатов должны быть заданы на всех параметрах этих формул (если они все без параметров, то на одном параметре a1 ). • Может понадобиться добавить ещё параметры. • Для дерева с вынесенными посылками выбираем вершину, а для флагов — строку. Все видимые посылки истинны, а сама выбранная формула ложна. 8/9 Домашнее задание С помощью натуральной дедукции докажите: 1. (∀x P(x)) → (∃x P(x)) 2. ∀x P(x) → Q(x) ` (∀x P(x)) → (∀x Q(x)) 3. (∃x P(x)) ∨ (∃x Q(x)) ` ∃x P(x) ∨ Q(x) 4. Убедитесь, что ∃x P(x) ` ∀x P(x) нельзя доказать и постройте контрмодель. 5. (*) ∃x (P(x) → ∀y P(y)) 6. (*) ∀x R(x, y) → R(y, x), ∀xyz R(x, y) ∧ R(y, z) → R(x, z), ∀x∃y R(x, y) ` ∀x R(x, x) Подсказка: так как ∀x∃y R(x, y), то для этого y также верно R(y, x), а из R(x, y) и R(y, x) заключаем R(x, x). 9/9