Логика предикатов. Деревья истинности

Логика предикатов Деревья истинности Математическая логика и теория алгоритмов Алексей Романов 25 мая 2020 г. МИЭТ Доказательства в логике предикатов • В логике предикатов естественно встаёт вопрос: • Дана формула, тождественно истинна ли она? • Что значит «Формула тождественно истинна»? 2/14 Доказательства в логике предикатов • В логике предикатов естественно встаёт вопрос: • Дана формула, тождественно истинна ли она? • Что значит «Формула тождественно истинна»? • Замкнутая: истинна на всех моделях её сигнатуры. 2/14 Доказательства в логике предикатов • В логике предикатов естественно встаёт вопрос: • Дана формула, тождественно истинна ли она? • Что значит «Формула тождественно истинна»? • Замкнутая: истинна на всех моделях её сигнатуры. • Со свободными переменными: можем навесить квантор всеобщности. 2/14 Доказательства в логике предикатов • В логике предикатов естественно встаёт вопрос: • Дана формула, тождественно истинна ли она? • Что значит «Формула тождественно истинна»? • Замкнутая: истинна на всех моделях её сигнатуры. • Со свободными переменными: можем навесить квантор всеобщности. • Варианты: эквивалентны ли две формулы? Является ли формула теоремой данной теории (это сложнее!)? • Как это можно проверить? • Нельзя просто перечислить все модели: 2/14 Доказательства в логике предикатов • В логике предикатов естественно встаёт вопрос: • Дана формула, тождественно истинна ли она? • Что значит «Формула тождественно истинна»? • Замкнутая: истинна на всех моделях её сигнатуры. • Со свободными переменными: можем навесить квантор всеобщности. • Варианты: эквивалентны ли две формулы? Является ли формула теоремой данной теории (это сложнее!)? • Как это можно проверить? • Нельзя просто перечислить все модели: их несчётно много! • Можно расширить деревья истинности и натуральную дедукцию. • Сегодня деревья истинности. 2/14 Правила деревьев истинности • • • • Правила для ∧/∨/→/¬ (типы α и β) сохраняются. Добавляются правила для формул с кванторами. Есть несколько способов, рассмотрим простейший. Добавляется бесконечное множество параметров a1 , a2 , . . ., не зависящих от сигнатуры. • Два новых типа формул: 3/14 Правила деревьев истинности • • • • Правила для ∧/∨/→/¬ (типы α и β) сохраняются. Добавляются правила для формул с кванторами. Есть несколько способов, рассмотрим простейший. Добавляется бесконечное множество параметров a1 , a2 , . . ., не зависящих от сигнатуры. • Два новых типа формул: γ ∀x A(x) = 1 ∃x A(x) = 0 γ(t) A(t) = 1 A(t) = 0 δ ∀x A(x) = 0 ∃x A(x) = 1 δ(t) A(t) = 0 A(t) = 1 • Правила для них: 3/14 Правила деревьев истинности • • • • Правила для ∧/∨/→/¬ (типы α и β) сохраняются. Добавляются правила для формул с кванторами. Есть несколько способов, рассмотрим простейший. Добавляется бесконечное множество параметров a1 , a2 , . . ., не зависящих от сигнатуры. • Два новых типа формул: γ ∀x A(x) = 1 ∃x A(x) = 0 γ(t) A(t) = 1 A(t) = 0 δ ∀x A(x) = 0 ∃x A(x) = 1 δ(t) A(t) = 0 A(t) = 1 • Правила для них: γ γ(t) t — замкнутый терм, можно раскрыть много раз 3/14 Правила деревьев истинности • • • • Правила для ∧/∨/→/¬ (типы α и β) сохраняются. Добавляются правила для формул с кванторами. Есть несколько способов, рассмотрим простейший. Добавляется бесконечное множество параметров a1 , a2 , . . ., не зависящих от сигнатуры. • Два новых типа формул: γ ∀x A(x) = 1 ∃x A(x) = 0 γ(t) A(t) = 1 A(t) = 0 δ ∀x A(x) = 0 ∃x A(x) = 1 δ(t) A(t) = 0 A(t) = 1 • Правила для них: γ δ γ(t) δ(a) t — замкнутый терм, можно раскрыть много раз a — новый (для ветви) параметр 3/14 Пояснения к правилам • Смысл правила γ: утверждение, верное для всех объектов, верно в том числе для значения t. • Смысл правила δ: мы даём название a тому объекту, существование которого утверждается. 4/14 Пояснения к правилам • Смысл правила γ: утверждение, верное для всех объектов, верно в том числе для значения t. • Смысл правила δ: мы даём название a тому объекту, существование которого утверждается. • Обратите внимание, что ∀x A(x) = 0 читается как 4/14 Пояснения к правилам • Смысл правила γ: утверждение, верное для всех объектов, верно в том числе для значения t. • Смысл правила δ: мы даём название a тому объекту, существование которого утверждается. • Обратите внимание, что ∀x A(x) = 0 читается как (∀x A(x)) = 0, а не ∀x (A(x) = 0). 4/14 Пояснения к правилам • Смысл правила γ: утверждение, верное для всех объектов, верно в том числе для значения t. • Смысл правила δ: мы даём название a тому объекту, существование которого утверждается. • Обратите внимание, что ∀x A(x) = 0 читается как (∀x A(x)) = 0, а не ∀x (A(x) = 0). • Замкнутый терм не содержит переменных. В случае без константных и функциональных символов это просто параметр. 4/14 Пояснения к правилам • Смысл правила γ: утверждение, верное для всех объектов, верно в том числе для значения t. • Смысл правила δ: мы даём название a тому объекту, существование которого утверждается. • Обратите внимание, что ∀x A(x) = 0 читается как (∀x A(x)) = 0, а не ∀x (A(x) = 0). • Замкнутый терм не содержит переменных. В случае без константных и функциональных символов это просто параметр. • γ-формулы не помечаются X при раскрытии, чтобы показать, что они могут быть повторно раскрыты. Только использованным термом. • Для δ-формул параметр можно указать рядом с X, чтобы легко увидеть использованные параметры. 4/14 Пример дерева истинности • Первый пример: одно из правил де Моргана для кванторов, ¬(∀x P(x)) → (∃x ¬P(x)). 1. ¬(∀x P(x)) → (∃x ¬P(x)) = 0 Дано 5/14 Пример дерева истинности • Первый пример: одно из правил де Моргана для кванторов, ¬(∀x P(x)) → (∃x ¬P(x)). 1. ¬(∀x P(x)) → (∃x ¬P(x)) = 0 X Дано 2. ¬(∀x P(x)) = 1 X 1 3. ∃x ¬P(x) = 0 1 4. ∀x P(x) = 0 2 5/14 Пример дерева истинности • Первый пример: одно из правил де Моргана для кванторов, ¬(∀x P(x)) → (∃x ¬P(x)). 1. 2. 3. 4. 5. ¬(∀x P(x)) → (∃x ¬P(x)) = 0 X ¬(∀x P(x)) = 1 X ∃x ¬P(x) = 0 ∀x P(x) = 0 Xa1 P(a1 ) = 0 X Дано 1 1 2 4 5/14 Пример дерева истинности • Первый пример: одно из правил де Моргана для кванторов, ¬(∀x P(x)) → (∃x ¬P(x)). 1. 2. 3. 4. 5. 6. 7. ¬(∀x P(x)) → (∃x ¬P(x)) = 0 X ¬(∀x P(x)) = 1 X ∃x ¬P(x) = 0 \a1 ∀x P(x) = 0 Xa1 P(a1 ) = 0 X ¬P(a1 ) = 0 X P(a1 ) = 1 X × 5,7 Дано 1 1 2 4 3 6 • Дерево закрылось, значит формула ¬(∀x P(x)) → (∃x ¬P(x)) 5/14 Пример дерева истинности • Первый пример: одно из правил де Моргана для кванторов, ¬(∀x P(x)) → (∃x ¬P(x)). 1. 2. 3. 4. 5. 6. 7. ¬(∀x P(x)) → (∃x ¬P(x)) = 0 X ¬(∀x P(x)) = 1 X ∃x ¬P(x) = 0 \a1 ∀x P(x) = 0 Xa1 P(a1 ) = 0 X ¬P(a1 ) = 0 X P(a1 ) = 1 X × 5,7 Дано 1 1 2 4 3 6 • Дерево закрылось, значит формула ¬(∀x P(x)) → (∃x ¬P(x)) тождественно истинна. 5/14 Порядок действий • Заметьте, что если сначала раскрыли бы строку 3 с параметром a1 , то в строке 4 пришлось бы использовать новый параметр a2 . • И противоречия не получится, пока не раскроем строку 3 с a2 . 6/14 Порядок действий • Заметьте, что если сначала раскрыли бы строку 3 с параметром a1 , то в строке 4 пришлось бы использовать новый параметр a2 . • И противоречия не получится, пока не раскроем строку 3 с a2 . • Также правила позволяют раскрыть строку 3 сколько угодно раз с разными параметрами и не дойти до строки 4. • Тогда опять не получим противоречия. 6/14 Порядок действий • Заметьте, что если сначала раскрыли бы строку 3 с параметром a1 , то в строке 4 пришлось бы использовать новый параметр a2 . • И противоречия не получится, пока не раскроем строку 3 с a2 . • Также правила позволяют раскрыть строку 3 сколько угодно раз с разными параметрами и не дойти до строки 4. • Тогда опять не получим противоречия. • Поэтому порядок раскрытия строк теперь важен для результата. 6/14 Порядок действий • Заметьте, что если сначала раскрыли бы строку 3 с параметром a1 , то в строке 4 пришлось бы использовать новый параметр a2 . • И противоречия не получится, пока не раскроем строку 3 с a2 . • Также правила позволяют раскрыть строку 3 сколько угодно раз с разными параметрами и не дойти до строки 4. • Тогда опять не получим противоречия. • Поэтому порядок раскрытия строк теперь важен для результата. • Сначала α и δ, потом β, потом γ. 6/14 Порядок действий • Заметьте, что если сначала раскрыли бы строку 3 с параметром a1 , то в строке 4 пришлось бы использовать новый параметр a2 . • И противоречия не получится, пока не раскроем строку 3 с a2 . • Также правила позволяют раскрыть строку 3 сколько угодно раз с разными параметрами и не дойти до строки 4. • Тогда опять не получим противоречия. • Поэтому порядок раскрытия строк теперь важен для результата. • Сначала α и δ, потом β, потом γ. • Это не единственно возможный, но достаточно простой. 6/14 Пример дерева истинности (2) • Ещё пример: ∀x P(x) ∧ Q(x) ` (∀x P(x)) ∧ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. ∀x P(x) ∧ Q(x) = 1 Дано 2. (∀x P(x)) ∧ (∀x Q(x)) = 0 Дано 7/14 Пример дерева истинности (2) • Ещё пример: ∀x P(x) ∧ Q(x) ` (∀x P(x)) ∧ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. ∀x P(x) ∧ Q(x) = 1 Дано 2. (∀x P(x)) ∧ (∀x Q(x)) = 0 X Дано 3. ∀x P(x) = 0 ∀x Q(x) = 0 2 7/14 Пример дерева истинности (2) • Ещё пример: ∀x P(x) ∧ Q(x) ` (∀x P(x)) ∧ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. ∀x P(x) ∧ Q(x) = 1 Дано 2. (∀x P(x)) ∧ (∀x Q(x)) = 0 X Дано 3. 4. ∀x P(x) = 0 Xa1 P(a1 ) = 0 X ∀x Q(x) = 0 Xa1 Q(a1 ) = 0 X 2 3 7/14 Пример дерева истинности (2) • Ещё пример: ∀x P(x) ∧ Q(x) ` (∀x P(x)) ∧ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. 2. 3. 4. 5. ∀x P(x) ∧ Q(x) = 1 \a1 (∀x P(x)) ∧ (∀x Q(x)) = 0 X ∀x P(x) = 0 Xa1 P(a1 ) = 0 X P(a1 ) ∧ Q(a1 ) = 1 ∀x Q(x) = 0 Xa1 Q(a1 ) = 0 X P(a1 ) ∧ Q(a1 ) = 1 Дано Дано 2 3 1 • В строке 3 можем использовать a1 в обеих ветвях. • Когда раскрываем строку 1, под ней две открытые ветви, результат пишем в обе. 7/14 Пример дерева истинности (2) • Ещё пример: ∀x P(x) ∧ Q(x) ` (∀x P(x)) ∧ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. 2. 3. 4. 5. 6. ∀x P(x) ∧ Q(x) = 1 \a1 (∀x P(x)) ∧ (∀x Q(x)) = 0 X ∀x P(x) = 0 Xa1 P(a1 ) = 0 X P(a1 ) ∧ Q(a1 ) = 1 X P(a1 ) = 1 X × 4,6 ∀x Q(x) = 0 Xa1 Q(a1 ) = 0 X P(a1 ) ∧ Q(a1 ) = 1 X Q(a1 ) = 1 X × 4,6 Дано Дано 2 3 1 5 • Дерево закрылось, значит секвенция • В строке 3 можем использовать a1 в обеих ветвях. • Когда раскрываем строку 1, под ней две открытые ветви, результат пишем в обе. 7/14 Пример дерева истинности (2) • Ещё пример: ∀x P(x) ∧ Q(x) ` (∀x P(x)) ∧ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. 2. 3. 4. 5. 6. ∀x P(x) ∧ Q(x) = 1 \a1 (∀x P(x)) ∧ (∀x Q(x)) = 0 X ∀x P(x) = 0 Xa1 P(a1 ) = 0 X P(a1 ) ∧ Q(a1 ) = 1 X P(a1 ) = 1 X × 4,6 ∀x Q(x) = 0 Xa1 Q(a1 ) = 0 X P(a1 ) ∧ Q(a1 ) = 1 X Q(a1 ) = 1 X × 4,6 Дано Дано 2 3 1 5 • Дерево закрылось, значит секвенция тождественно истинна. • В строке 3 можем использовать a1 в обеих ветвях. • Когда раскрываем строку 1, под ней две открытые ветви, результат пишем в обе. 7/14 Пример дерева истинности (3) • ∀x P(x) ∨ Q(x) ` (∀x P(x)) ∨ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. ∀x P(x) ∨ Q(x) = 1 Дано 2. (∀x P(x)) ∨ (∀x Q(x)) = 0 Дано 8/14 Пример дерева истинности (3) • ∀x P(x) ∨ Q(x) ` (∀x P(x)) ∨ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. ∀x P(x) ∨ Q(x) = 1 Дано 2. (∀x P(x)) ∨ (∀x Q(x)) = 0 X Дано 3. ∀x P(x) = 0 2 4. ∀x Q(x) = 0 2 8/14 Пример дерева истинности (3) • ∀x P(x) ∨ Q(x) ` (∀x P(x)) ∨ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. ∀x P(x) ∨ Q(x) = 1 Дано 2. (∀x P(x)) ∨ (∀x Q(x)) = 0 X Дано 3. ∀x P(x) = 0 Xa1 2 4. ∀x Q(x) = 0 Xa2 2 5. P(a1 ) = 0 X 3 6. Q(a2 ) = 0 X 4 8/14 Пример дерева истинности (3) • ∀x P(x) ∨ Q(x) ` (∀x P(x)) ∨ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. ∀x P(x) ∨ Q(x) = 1 \a1 Дано 2. (∀x P(x)) ∨ (∀x Q(x)) = 0 X Дано 3. ∀x P(x) = 0 Xa1 2 4. ∀x Q(x) = 0 Xa2 2 5. P(a1 ) = 0 X 3 6. Q(a2 ) = 0 X 4 7. P(a1 ) ∨ Q(a1 ) = 1 1 8/14 Пример дерева истинности (3) • ∀x P(x) ∨ Q(x) ` (∀x P(x)) ∨ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. ∀x P(x) ∨ Q(x) = 1 \a1 Дано 2. (∀x P(x)) ∨ (∀x Q(x)) = 0 X Дано 3. ∀x P(x) = 0 Xa1 2 4. ∀x Q(x) = 0 Xa2 2 5. P(a1 ) = 0 X 3 6. Q(a2 ) = 0 X 4 7. P(a1 ) ∨ Q(a1 ) = 1 X 1 8. P(a1 ) = 1 X × 5,8 Q(a1 ) = 1 X 7 (ветвь закончена?) 8/14 Пример дерева истинности (3) • ∀x P(x) ∨ Q(x) ` (∀x P(x)) ∨ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. ∀x P(x) ∨ Q(x) = 1 \a1 , a2 Дано 2. (∀x P(x)) ∨ (∀x Q(x)) = 0 X Дано 3. ∀x P(x) = 0 Xa1 2 4. ∀x Q(x) = 0 Xa2 2 5. P(a1 ) = 0 X 3 6. Q(a2 ) = 0 X 4 7. P(a1 ) ∨ Q(a1 ) = 1 X 1 8. 9. P(a1 ) = 1 X × 5,8 Q(a1 ) = 1 X P(a2 ) ∨ Q(a2 ) = 1 7 1 8/14 Пример дерева истинности (3) • ∀x P(x) ∨ Q(x) ` (∀x P(x)) ∨ (∀x Q(x)). Как думаете, тождественно истинна или нет? 1. ∀x P(x) ∨ Q(x) = 1 \a1 , a2 Дано 2. (∀x P(x)) ∨ (∀x Q(x)) = 0 X Дано 3. ∀x P(x) = 0 Xa1 2 4. ∀x Q(x) = 0 Xa2 2 5. P(a1 ) = 0 X 3 6. Q(a2 ) = 0 X 4 7. P(a1 ) ∨ Q(a1 ) = 1 X 1 8. 9. 10. P(a1 ) = 1 X × 5,8 Q(a1 ) = 1 X P(a2 ) ∨ Q(a2 ) = 1 X P(a2 ) = 1 X Q(a2 ) = 1 X × 6,10 • Дерево не закрылось! 7 1 9 8/14 Пример дерева истинности (3) • Получили открытую ветвь, в которой: • все α-, β-, δ- и ¬-формулы раскрыты; • все γ-формулы раскрыты со всеми параметрами (и хотя бы с одним). • Такая ветвь называется законченной. 9/14 Пример дерева истинности (3) • Получили открытую ветвь, в которой: • все α-, β-, δ- и ¬-формулы раскрыты; • все γ-формулы раскрыты со всеми параметрами (и хотя бы с одним). • Такая ветвь называется законченной. • В нашем случае атомы в ней P(a1 ) = 0, Q(a2 ) = 0, Q(a1 ) = 1, P(a2 ) = 1. • По ним строим модель. В ней два объекта, которые так и обозначим: a1 и a2 . 9/14 Пример дерева истинности (3) • Получили открытую ветвь, в которой: • все α-, β-, δ- и ¬-формулы раскрыты; • все γ-формулы раскрыты со всеми параметрами (и хотя бы с одним). • Такая ветвь называется законченной. • В нашем случае атомы в ней P(a1 ) = 0, Q(a2 ) = 0, Q(a1 ) = 1, P(a2 ) = 1. • По ним строим модель. В ней два объекта, которые так и обозначим: a1 и a2 . x a1 a2 P(x) 1 Q(x) 1 9/14 Пример дерева истинности (3) • Получили открытую ветвь, в которой: • все α-, β-, δ- и ¬-формулы раскрыты; • все γ-формулы раскрыты со всеми параметрами (и хотя бы с одним). • Такая ветвь называется законченной. • В нашем случае атомы в ней P(a1 ) = 0, Q(a2 ) = 0, Q(a1 ) = 1, P(a2 ) = 1. • По ним строим модель. В ней два объекта, которые так и обозначим: a1 и a2 . x a1 a2 P(x) 1 Q(x) 1 • Что делать, если бы в ветви не было атома c P(a1 ) (например)? 9/14 Пример дерева истинности (3) • Получили открытую ветвь, в которой: • все α-, β-, δ- и ¬-формулы раскрыты; • все γ-формулы раскрыты со всеми параметрами (и хотя бы с одним). • Такая ветвь называется законченной. • В нашем случае атомы в ней P(a1 ) = 0, Q(a2 ) = 0, Q(a1 ) = 1, P(a2 ) = 1. • По ним строим модель. В ней два объекта, которые так и обозначим: a1 и a2 . x a1 a2 P(x) 1 Q(x) 1 • Что делать, если бы в ветви не было атома c P(a1 ) (например)? • Можем поставить туда любое значение. 9/14 Пример дерева истинности (3) • Получили открытую ветвь, в которой: • все α-, β-, δ- и ¬-формулы раскрыты; • все γ-формулы раскрыты со всеми параметрами (и хотя бы с одним). • Такая ветвь называется законченной. • В нашем случае атомы в ней P(a1 ) = 0, Q(a2 ) = 0, Q(a1 ) = 1, P(a2 ) = 1. • По ним строим модель. В ней два объекта, которые так и обозначим: a1 и a2 . x a1 a2 P(x) 1 Q(x) 1 • Что делать, если бы в ветви не было атома c P(a1 ) (например)? • Можем поставить туда любое значение. • Снова видим, что x, связанные разными кванторами, по сути разные переменные (строки 5-6). 9/14 Пример дерева истинности (4) • ∀x∃y P(x, y) ` ∃y∀x P(x, y). Как думаете, тождественно истинна или нет? 1. ∀x∃y P(x, y) = 1 Дано 2. ∃y∀x P(x, y) = 0 Дано 10/14 Пример дерева истинности (4) • ∀x∃y P(x, y) ` ∃y∀x P(x, y). Как думаете, тождественно истинна или нет? 1. ∀x∃y P(x, y) = 1 \a1 Дано 2. ∃y∀x P(x, y) = 0 Дано 3. ∃y P(a1 , y) = 1 Xa2 1 4. P(a1 , a2 ) = 1 X 3 10/14 Пример дерева истинности (4) • ∀x∃y P(x, y) ` ∃y∀x P(x, y). Как думаете, тождественно истинна или нет? 1. ∀x∃y P(x, y) = 1 \a1 Дано 2. ∃y∀x P(x, y) = 0 \a2 Дано 3. ∃y P(a1 , y) = 1 Xa2 1 4. P(a1 , a2 ) = 1 X 3 5. ∀x P(x, a2 ) = 0 Xa3 2 6. P(a3 , a2 ) = 0 X 5 (ветвь закончена?) 10/14 Пример дерева истинности (4) • ∀x∃y P(x, y) ` ∃y∀x P(x, y). Как думаете, тождественно истинна или нет? 1. ∀x∃y P(x, y) = 1 \a1 , a3 , . . . Дано 2. ∃y∀x P(x, y) = 0 \a2 , . . . Дано 3. ∃y P(a1 , y) = 1 Xa2 1 4. P(a1 , a2 ) = 1 X 3 5. ∀x P(x, a2 ) = 0 Xa3 2 6. P(a3 , a2 ) = 0 X 5 7. ∃y P(a3 , y) = 1 Xa4 1 8. ... 10/14 Пример дерева истинности (4) • ∀x∃y P(x, y) ` ∃y∀x P(x, y). Как думаете, тождественно истинна или нет? 1. ∀x∃y P(x, y) = 1 \a1 , a3 , . . . Дано 2. ∃y∀x P(x, y) = 0 \a2 , . . . Дано 3. ∃y P(a1 , y) = 1 Xa2 1 4. P(a1 , a2 ) = 1 X 3 5. ∀x P(x, a2 ) = 0 Xa3 2 6. P(a3 , a2 ) = 0 X 5 7. ∃y P(a3 , y) = 1 Xa4 1 8. ... • На этот раз ситуация сложнее предыдущей. • Противоречия нет, но и законченной ветви (в смысле прошлого слайда) тоже. • По крайней мере после любого конечного числа шагов. 10/14 Пример дерева истинности (4) • ∀x∃y P(x, y) ` ∃y∀x P(x, y). Как думаете, тождественно истинна или нет? 1. ∀x∃y P(x, y) = 1 \a1 , a3 , . . . Дано 2. ∃y∀x P(x, y) = 0 \a2 , . . . Дано 3. ∃y P(a1 , y) = 1 Xa2 1 4. P(a1 , a2 ) = 1 X 3 5. ∀x P(x, a2 ) = 0 Xa3 2 6. P(a3 , a2 ) = 0 X 5 7. ∃y P(a3 , y) = 1 Xa4 1 8. ... • На этот раз ситуация сложнее предыдущей. • Противоречия нет, но и законченной ветви (в смысле прошлого слайда) тоже. • По крайней мере после любого конечного числа шагов. • Наверное, легко увидеть, что противоречия так и не 10/14 получим, но как это доказать? Бесконечные контрмодели • В нашей ветви видны некоторые значения предиката: y a1 a2 a3 a4 ... x a1 a2 a3 a4 ? ? ? ? 1 ? ? ? ? ? ? ? ? 1 ? ... • Как в терминах этой таблицы выглядят: • ∀x∃y P(x, y) = 1? 11/14 Бесконечные контрмодели • В нашей ветви видны некоторые значения предиката: y a1 a2 a3 a4 ... x a1 a2 a3 a4 ? ? ? ? 1 ? ? ? ? ? ? ? ? 1 ? ... • Как в терминах этой таблицы выглядят: • ∀x∃y P(x, y) = 1? В каждой строке есть 1. 11/14 Бесконечные контрмодели • В нашей ветви видны некоторые значения предиката: y a1 a2 a3 a4 ... x a1 a2 a3 a4 ? ? ? ? 1 ? ? ? ? ? ? ? ? 1 ? ... • Как в терминах этой таблицы выглядят: • ∀x∃y P(x, y) = 1? В каждой строке есть 1. • ∃y∀x P(x, y) = 0? 11/14 Бесконечные контрмодели • В нашей ветви видны некоторые значения предиката: y a1 a2 a3 a4 ... x a1 a2 a3 a4 ? ? ? ? 1 ? ? ? ? ? ? ? ? 1 ? ... • Как в терминах этой таблицы выглядят: • ∀x∃y P(x, y) = 1? В каждой строке есть 1. • ∃y∀x P(x, y) = 0? Нет столбца, где все 1. Помните, что это (∃y∀x P(x, y)) = 0, а не ∃y∀x (P(x, y) = 0)! 11/14 Бесконечные контрмодели • Видно, что расставить 0 и 1 на место ? произвольно нельзя, но вот вариант: x a1 a2 a3 a4 ... y a1 a2 a3 a4 1 1 1 ... 12/14 Бесконечные контрмодели • Видно, что расставить 0 и 1 на место ? произвольно нельзя, но вот вариант: x a1 a2 a3 a4 ... y a1 a2 a3 a4 1 1 1 ... • Мы нашли бесконечный контрпример для этой секвенции, а есть ли конечный? Напомню условия: • В каждой строке есть 1; нет столбца, где все 1. 12/14 Бесконечные контрмодели • Видно, что расставить 0 и 1 на место ? произвольно нельзя, но вот вариант: y x a1 a2 a3 a4 ... a1 a2 a3 a4 1 1 1 ... • Мы нашли бесконечный контрпример для этой секвенции, а есть ли конечный? Напомню условия: • В каждой строке есть 1; нет столбца, где все 1. • Конечно, есть. Например: y x a1 a2 a1 a2 1 1 12/14 Последние замечания • Есть варианты правил деревьев, которые позволят найти конечный контрпример в этом случае (и не только), но их сложнее объяснить и понять. • Краткое изложение в английской Википедии. 13/14 Последние замечания • Есть варианты правил деревьев, которые позволят найти конечный контрпример в этом случае (и не только), но их сложнее объяснить и понять. • Краткое изложение в английской Википедии. • Логика предикатов неразрешима: нет алгоритма, который для любой формулы скажет, тождественно истинна ли она. • Значит, в любой системе доказательств надо что-то придумывать (для некоторых формул), чисто механических действий недостаточно. 13/14 Домашнее задание С помощью деревьев докажите или опровергните: 1. (∀x P(x)) → (∃x P(x)) 2. ∀x P(x) → Q(x) ≡ (∀x P(x)) → (∀x Q(x)) 3. ∃x (P(x) → ∀y P(y)) 4. ∃x∀y P(x, y) ` ∀y∃x P(x, y) 5. (*) ∀x R(x, y) → R(y, x), ∀xyz R(x, y) ∧ R(y, z) → R(x, z) ` ∀x R(x, x) 6. (*) Найдите формулу или секвенцию, у которой есть только бесконечные контрпримеры. 14/14