Логика предикатов

Логика предикатов Введение Математическая логика и теория алгоритмов Алексей Романов 27 апреля 2020 г. МИЭТ Сигнатуры, термы, формулы • Сигнатура Σ — 2/15 Сигнатуры, термы, формулы • Сигнатура Σ — конечные или счётные множества константных ConstΣ , функциональных FunΣ и предикатных PredΣ символов. Для каждого символа из FunΣ и PredΣ задано число аргументов (арность). • Переменные — 2/15 Сигнатуры, термы, формулы • Сигнатура Σ — конечные или счётные множества константных ConstΣ , функциональных FunΣ и предикатных PredΣ символов. Для каждого символа из FunΣ и PredΣ задано число аргументов (арность). • Переменные — x, y, z3 , . . .. Обозначают 2/15 Сигнатуры, термы, формулы • Сигнатура Σ — конечные или счётные множества константных ConstΣ , функциональных FunΣ и предикатных PredΣ символов. Для каждого символа из FunΣ и PredΣ задано число аргументов (арность). • Переменные — x, y, z3 , . . .. Обозначают какие-то объекты (не истину/ложь, как p, q, r). Множество Var не зависит от сигнатуры. 2/15 Сигнатуры, термы, формулы • Сигнатура Σ — конечные или счётные множества константных ConstΣ , функциональных FunΣ и предикатных PredΣ символов. Для каждого символа из FunΣ и PredΣ задано число аргументов (арность). • Переменные — x, y, z3 , . . .. Обозначают какие-то объекты (не истину/ложь, как p, q, r). Множество Var не зависит от сигнатуры. • Термы — 2/15 Сигнатуры, термы, формулы • Сигнатура Σ — конечные или счётные множества константных ConstΣ , функциональных FunΣ и предикатных PredΣ символов. Для каждого символа из FunΣ и PredΣ задано число аргументов (арность). • Переменные — x, y, z3 , . . .. Обозначают какие-то объекты (не истину/ложь, как p, q, r). Множество Var не зависит от сигнатуры. • Термы — x, (y + 2) · z, . . . Выражения, значения которых — объекты. Строятся из переменных и константных символов применением функциональных. Множество термов над Σ: TermΣ . 2/15 Сигнатуры, термы, формулы • Сигнатура Σ — конечные или счётные множества константных ConstΣ , функциональных FunΣ и предикатных PredΣ символов. Для каждого символа из FunΣ и PredΣ задано число аргументов (арность). • Переменные — x, y, z3 , . . .. Обозначают какие-то объекты (не истину/ложь, как p, q, r). Множество Var не зависит от сигнатуры. • Термы — x, (y + 2) · z, . . . Выражения, значения которых — объекты. Строятся из переменных и константных символов применением функциональных. Множество термов над Σ: TermΣ . • Формулы — 2/15 Сигнатуры, термы, формулы • Сигнатура Σ — конечные или счётные множества константных ConstΣ , функциональных FunΣ и предикатных PredΣ символов. Для каждого символа из FunΣ и PredΣ задано число аргументов (арность). • Переменные — x, y, z3 , . . .. Обозначают какие-то объекты (не истину/ложь, как p, q, r). Множество Var не зависит от сигнатуры. • Термы — x, (y + 2) · z, . . . Выражения, значения которых — объекты. Строятся из переменных и константных символов применением функциональных. Множество термов над Σ: TermΣ . • Формулы — x = y + 1; ∀x x 6= x2 . . . Вот их значения истина и ложь. Атомарные формулы строятся из термов применением предикатных символов, а остальные применением связок ∧/∨/. . . и кванторов ∀ и ∃ к формулам. Множество формул над Σ: FormΣ . 2/15 Модели • Модель M сигнатуры Σ состоит из: • Носитель (или универсум): 3/15 Модели • Модель M сигнатуры Σ состоит из: • Носитель (или универсум): множество M̄. • Для каждого символа c : ConstΣ 1 : 1Я пишу : вместо ∈ для объявления новой переменной. 3/15 Модели • Модель M сигнатуры Σ состоит из: • Носитель (или универсум): множество M̄. • Для каждого символа c : ConstΣ 1 : элемент cM : M̄. • Для f : FunΣ : 1Я пишу : вместо ∈ для объявления новой переменной. 3/15 Модели • Модель M сигнатуры Σ состоит из: • • • • 1Я Носитель (или универсум): множество M̄. Для каждого символа c : ConstΣ 1 : элемент cM : M̄. Для f : FunΣ : функция fM : Marity(f ) → M. Для P : PredΣ пишу : вместо ∈ для объявления новой переменной. 3/15 Модели • Модель M сигнатуры Σ состоит из: • • • • Носитель (или универсум): множество M̄. Для каждого символа c : ConstΣ 1 : элемент cM : M̄. Для f : FunΣ : функция fM : Marity(f ) → M. Для P : PredΣ предикат PM : Marity(P) → {0, 1}. • Оценка — значение переменных в модели, σ : Var → M̄. Или V → M̄ где V ⊂ Var. • Важно: символы сигнатуры сами по себе ничего не говорят об их интерпретации! +M может быть − или · Ry или x, y 7→ x tdt. 1Я пишу : вместо ∈ для объявления новой переменной. 3/15 Модели • Модель M сигнатуры Σ состоит из: • • • • Носитель (или универсум): множество M̄. Для каждого символа c : ConstΣ 1 : элемент cM : M̄. Для f : FunΣ : функция fM : Marity(f ) → M. Для P : PredΣ предикат PM : Marity(P) → {0, 1}. • Оценка — значение переменных в модели, σ : Var → M̄. Или V → M̄ где V ⊂ Var. • Важно: символы сигнатуры сами по себе ничего не говорят об их интерпретации! +M может быть − или · Ry или x, y 7→ x tdt. • Одно исключение: если есть =, то =M это равенство на M̄. 1Я пишу : вместо ∈ для объявления новой переменной. 3/15 Значения термов и формул • σ расширяется на TermΣ → ??? и на FormΣ → ??? по индукции: 4/15 Значения термов и формул • σ расширяется на TermΣ → M̄ и на FormΣ → {0, 1} по индукции: 4/15 Значения термов и формул • σ расширяется на TermΣ → M̄ и на FormΣ → {0, 1} по индукции: • σ(c) = cM . • σ(f (t1 , . . . , tn )) = fM (σ(t1 ), . . . , σ(tn )). • TODO 4/15 Свободные и связанные переменные • Связанное вхождение переменной — 5/15 Свободные и связанные переменные • Связанное вхождение переменной — v под квантором по этой же переменной ∀v/∃v. • Свободное вхождение переменной — 5/15 Свободные и связанные переменные • Связанное вхождение переменной — v под квантором по этой же переменной ∀v/∃v. • Свободное вхождение переменной — любое другое. • Переменная свободна в формуле, если имеет какие-то свободные вхождения. • Замкнутая формула (или предложение) — формула без свободных переменных. • Почему это важно? Какая между ними разница? 5/15 Свободные и связанные переменные • Связанное вхождение переменной — v под квантором по этой же переменной ∀v/∃v. • Свободное вхождение переменной — любое другое. • Переменная свободна в формуле, если имеет какие-то свободные вхождения. • Замкнутая формула (или предложение) — формула без свободных переменных. • Почему это важно? Какая между ними разница? • σ(∀/∃v . . .) не зависит от σ(v). 5/15 Свободные и связанные переменные • Связанное вхождение переменной — v под квантором по этой же переменной ∀v/∃v. • Свободное вхождение переменной — любое другое. • Переменная свободна в формуле, если имеет какие-то свободные вхождения. • Замкнутая формула (или предложение) — формула без свободных переменных. • Почему это важно? Какая между ними разница? • σ(∀/∃v . . .) не зависит от σ(v). • Отсюда можно доказать, что значение формулы ϕ зависит только от значений свободных переменных ϕ, но не от связанных. 5/15 Свободные и связанные переменные • Связанное вхождение переменной — v под квантором по этой же переменной ∀v/∃v. • Свободное вхождение переменной — любое другое. • Переменная свободна в формуле, если имеет какие-то свободные вхождения. • Замкнутая формула (или предложение) — формула без свободных переменных. • Почему это важно? Какая между ними разница? • σ(∀/∃v . . .) не зависит от σ(v). • Отсюда можно доказать, что значение формулы ϕ зависит только от значений свободных переменных ϕ, но не от связанных. • А значение замкнутой формулы? 5/15 Свободные и связанные переменные • Связанное вхождение переменной — v под квантором по этой же переменной ∀v/∃v. • Свободное вхождение переменной — любое другое. • Переменная свободна в формуле, если имеет какие-то свободные вхождения. • Замкнутая формула (или предложение) — формула без свободных переменных. • Почему это важно? Какая между ними разница? • σ(∀/∃v . . .) не зависит от σ(v). • Отсюда можно доказать, что значение формулы ϕ зависит только от значений свободных переменных ϕ, но не от связанных. • А значение замкнутой формулы? Вообще не зависит от оценки. 5/15 Примеры • Рассмотрим пример. • Формула (замкнутая): ∀x (P(x) → Q(x)). • Возьмём произвольную модель из 3 элементов: M̄ = {0, 1, 2}. • Как можно задать предикаты P и Q? 6/15 Примеры • Рассмотрим пример. • Формула (замкнутая): ∀x (P(x) → Q(x)). • Возьмём произвольную модель из 3 элементов: M̄ = {0, 1, 2}. • Как можно задать предикаты P и Q? x 0 1 2 P(x) 0 0 1 Q(x) 1 0 1 • Истинна ли формула? 6/15 Примеры • Рассмотрим пример. • Формула (замкнутая): ∀x (P(x) → Q(x)). • Возьмём произвольную модель из 3 элементов: M̄ = {0, 1, 2}. • Как можно задать предикаты P и Q? x 0 1 2 P(x) 0 0 1 Q(x) 1 0 1 • Истинна ли формула? Да. 6/15 Примеры • Рассмотрим пример. • Формула (замкнутая): ∀x (P(x) → Q(x)). • Возьмём произвольную модель из 3 элементов: M̄ = {0, 1, 2}. • Как можно задать предикаты P и Q? x 0 1 2 P(x) 0 0 1 Q(x) 1 0 1 • Истинна ли формула? Да. • Попробуем другую формулу на той же модели: ∃x (P(x) ∧ Q(x)) ∧ ∃x ¬P(x). Истинна ли она? 6/15 Примеры • Рассмотрим пример. • Формула (замкнутая): ∀x (P(x) → Q(x)). • Возьмём произвольную модель из 3 элементов: M̄ = {0, 1, 2}. • Как можно задать предикаты P и Q? x 0 1 2 P(x) 0 0 1 Q(x) 1 0 1 • Истинна ли формула? Да. • Попробуем другую формулу на той же модели: ∃x (P(x) ∧ Q(x)) ∧ ∃x ¬P(x). Истинна ли она? Да. 6/15 Примеры • Рассмотрим пример. • Формула (замкнутая): ∀x (P(x) → Q(x)). • Возьмём произвольную модель из 3 элементов: M̄ = {0, 1, 2}. • Как можно задать предикаты P и Q? x 0 1 2 P(x) 0 0 1 Q(x) 1 0 1 • Истинна ли формула? Да. • Попробуем другую формулу на той же модели: ∃x (P(x) ∧ Q(x)) ∧ ∃x ¬P(x). Истинна ли она? Да. • Как насчёт незамкнутой формулы P(x) → ∀x Q(x)? 6/15 Примеры • Рассмотрим пример. • Формула (замкнутая): ∀x (P(x) → Q(x)). • Возьмём произвольную модель из 3 элементов: M̄ = {0, 1, 2}. • Как можно задать предикаты P и Q? x 0 1 2 P(x) 0 0 1 Q(x) 1 0 1 • Истинна ли формула? Да. • Попробуем другую формулу на той же модели: ∃x (P(x) ∧ Q(x)) ∧ ∃x ¬P(x). Истинна ли она? Да. • Как насчёт незамкнутой формулы P(x) → ∀x Q(x)? Истинна при σ(x) = 0, σ(x) = 1, ложна при σ(x) = 2. 6/15 Примеры • Рассмотрим пример. • Формула (замкнутая): ∀x (P(x) → Q(x)). • Возьмём произвольную модель из 3 элементов: M̄ = {0, 1, 2}. • Как можно задать предикаты P и Q? x 0 1 2 P(x) 0 0 1 Q(x) 1 0 1 • Истинна ли формула? Да. • Попробуем другую формулу на той же модели: ∃x (P(x) ∧ Q(x)) ∧ ∃x ¬P(x). Истинна ли она? Да. • Как насчёт незамкнутой формулы P(x) → ∀x Q(x)? Истинна при σ(x) = 0, σ(x) = 1, ложна при σ(x) = 2. • Для простоты можно писать x = 0 вместо σ(x) = 0. 6/15 Примеры • Рассмотрим пример. • Формула (замкнутая): ∀x (P(x) → Q(x)). • Возьмём произвольную модель из 3 элементов: M̄ = {0, 1, 2}. • Как можно задать предикаты P и Q? x 0 1 2 P(x) 0 0 1 Q(x) 1 0 1 • Истинна ли формула? Да. • Попробуем другую формулу на той же модели: ∃x (P(x) ∧ Q(x)) ∧ ∃x ¬P(x). Истинна ли она? Да. • Как насчёт незамкнутой формулы P(x) → ∀x Q(x)? Истинна при σ(x) = 0, σ(x) = 1, ложна при σ(x) = 2. • Для простоты можно писать x = 0 вместо σ(x) = 0. • Ничего не изменится, если M̄ = {a, b, c}, какие-то абстрактные объекты. 6/15 Примеры • • • • Ещё пример с бинарным предикатом: Формула: ∀x∃y (P(x, y) → P(x, x)). Возьмём M̄ = {a, b, c}. Какой таблицей задаётся бинарный предикат? 7/15 Примеры • • • • Ещё пример с бинарным предикатом: Формула: ∀x∃y (P(x, y) → P(x, x)). Возьмём M̄ = {a, b, c}. Какой таблицей задаётся бинарный предикат? x a b c y a 0 1 1 b 0 1 0 c 1 1 0 • Истинна ли формула? 7/15 Примеры • • • • Ещё пример с бинарным предикатом: Формула: ∀x∃y (P(x, y) → P(x, x)). Возьмём M̄ = {a, b, c}. Какой таблицей задаётся бинарный предикат? x a b c y a 0 1 1 b 0 1 0 c 1 1 0 • Истинна ли формула? Да. 7/15 Примеры • • • • Ещё пример с бинарным предикатом: Формула: ∀x∃y (P(x, y) → P(x, x)). Возьмём M̄ = {a, b, c}. Какой таблицей задаётся бинарный предикат? x a b c y a 0 1 1 b 0 1 0 c 1 1 0 • Истинна ли формула? Да. • Слегка поменяем: ∀x ((∃y P(x, y)) → P(x, x)). 7/15 Примеры • • • • Ещё пример с бинарным предикатом: Формула: ∀x∃y (P(x, y) → P(x, x)). Возьмём M̄ = {a, b, c}. Какой таблицей задаётся бинарный предикат? x a b c y a 0 1 1 b 0 1 0 c 1 1 0 • Истинна ли формула? Да. • Слегка поменяем: ∀x ((∃y P(x, y)) → P(x, x)). Эта формула ложна. 7/15 Примеры • • • • Ещё пример с бинарным предикатом: Формула: ∀x∃y (P(x, y) → P(x, x)). Возьмём M̄ = {a, b, c}. Какой таблицей задаётся бинарный предикат? x a b c y a 0 1 1 b 0 1 0 c 1 1 0 • Истинна ли формула? Да. • Слегка поменяем: ∀x ((∃y P(x, y)) → P(x, x)). Эта формула ложна. • На бесконечных моделях работает так же, но мы не можем просто перечислить все значения переменных, чтобы найти значение формулы! 7/15 Примеры • • • • • • • • Ещё пример с бинарным предикатом: Формула: ∀x∃y (P(x, y) → P(x, x)). Возьмём M̄ = {a, b, c}. Какой таблицей задаётся бинарный предикат? x a b c y a 0 1 1 b 0 1 0 c 1 1 0 Истинна ли формула? Да. Слегка поменяем: ∀x ((∃y P(x, y)) → P(x, x)). Эта формула ложна. На бесконечных моделях работает так же, но мы не можем просто перечислить все значения переменных, чтобы найти значение формулы! Вместо механического процесса приходится думать. 7/15 Примеры • • • • • • • • • Ещё пример с бинарным предикатом: Формула: ∀x∃y (P(x, y) → P(x, x)). Возьмём M̄ = {a, b, c}. Какой таблицей задаётся бинарный предикат? x a b c y a 0 1 1 b 0 1 0 c 1 1 0 Истинна ли формула? Да. Слегка поменяем: ∀x ((∃y P(x, y)) → P(x, x)). Эта формула ложна. На бесконечных моделях работает так же, но мы не можем просто перечислить все значения переменных, чтобы найти значение формулы! Вместо механического процесса приходится думать. На практике для больших конечных тоже. 7/15 Подстановки • TODO 8/15 Ограниченные кванторы • В математических текстах мы часто видим что-то вроде ∀x > 1 x2 > x. Но по нашему определению это не формула! В чём дело? 9/15 Ограниченные кванторы • В математических текстах мы часто видим что-то вроде ∀x > 1 x2 > x. Но по нашему определению это не формула! В чём дело? • Это сокращённая запись формулы, но какой? • ∀x (x > 1 ? x2 > x). Какую связку нужно поставить? 9/15 Ограниченные кванторы • В математических текстах мы часто видим что-то вроде ∀x > 1 x2 > x. Но по нашему определению это не формула! В чём дело? • Это сокращённая запись формулы, но какой? • ∀x (x > 1 ? x2 > x). Какую связку нужно поставить? • ∀x (x > 1 → x2 > x). 9/15 Ограниченные кванторы • В математических текстах мы часто видим что-то вроде ∀x > 1 x2 > x. Но по нашему определению это не формула! В чём дело? • Это сокращённая запись формулы, но какой? • ∀x (x > 1 ? x2 > x). Какую связку нужно поставить? • ∀x (x > 1 → x2 > x). • А для случая ∃x > 1 x2 > x? 9/15 Ограниченные кванторы • В математических текстах мы часто видим что-то вроде ∀x > 1 x2 > x. Но по нашему определению это не формула! В чём дело? • Это сокращённая запись формулы, но какой? • ∀x (x > 1 ? x2 > x). Какую связку нужно поставить? • ∀x (x > 1 → x2 > x). • А для случая ∃x > 1 x2 > x? • ∃x (x > 1 ∧ x2 > x). 9/15 Ограниченные кванторы • В математических текстах мы часто видим что-то вроде ∀x > 1 x2 > x. Но по нашему определению это не формула! В чём дело? • Это сокращённая запись формулы, но какой? • ∀x (x > 1 ? x2 > x). Какую связку нужно поставить? • ∀x (x > 1 → x2 > x). • А для случая ∃x > 1 x2 > x? • ∃x (x > 1 ∧ x2 > x). • Убедитесь, что это работает, если заменить x > 1 и x2 > 1 на любые другие 9/15 Ограниченные кванторы • В математических текстах мы часто видим что-то вроде ∀x > 1 x2 > x. Но по нашему определению это не формула! В чём дело? • Это сокращённая запись формулы, но какой? • ∀x (x > 1 ? x2 > x). Какую связку нужно поставить? • ∀x (x > 1 → x2 > x). • А для случая ∃x > 1 x2 > x? • ∃x (x > 1 ∧ x2 > x). • Убедитесь, что это работает, если заменить x > 1 и x2 > 1 на любые другие формулы. 9/15 ∃! • ∃!x P(x) читается как 10/15 Существование и единственность • ∃!x P(x) читается как «Существует единственное x такое, что. . . » • P здесь — формула со свободной переменной x. 10/15 Существование и единственность • ∃!x P(x) читается как «Существует единственное x такое, что. . . » • P здесь — формула со свободной переменной x. • Но в нашем языке такого символа нет. • Может быть, ! — предикатный символ (или функциональный, или константный)? 10/15 Существование и единственность • ∃!x P(x) читается как «Существует единственное x такое, что. . . » • P здесь — формула со свободной переменной x. • Но в нашем языке такого символа нет. • Может быть, ! — предикатный символ (или функциональный, или константный)? Тогда бы не получилась формула. После квантора может стоять только переменная. 10/15 Существование и единственность • ∃!x P(x) читается как «Существует единственное x такое, что. . . » • P здесь — формула со свободной переменной x. • Но в нашем языке такого символа нет. • Может быть, ! — предикатный символ (или функциональный, или константный)? Тогда бы не получилась формула. После квантора может стоять только переменная. • Это сокращение, как и ограниченные кванторы. Осталось его расшифровать. 10/15 Существование и единственность • ∃!x P(x) читается как «Существует единственное x такое, что. . . » • P здесь — формула со свободной переменной x. • Но в нашем языке такого символа нет. • Может быть, ! — предикатный символ (или функциональный, или константный)? Тогда бы не получилась формула. После квантора может стоять только переменная. • Это сокращение, как и ограниченные кванторы. Осталось его расшифровать. • ∃x (P(x) ∧ ???) 10/15 Существование и единственность • ∃!x P(x) читается как «Существует единственное x такое, что. . . » • P здесь — формула со свободной переменной x. • Но в нашем языке такого символа нет. • Может быть, ! — предикатный символ (или функциональный, или константный)? Тогда бы не получилась формула. После квантора может стоять только переменная. • Это сокращение, как и ограниченные кванторы. Осталось его расшифровать. • ∃x (P(x) ∧ ???) • ∃x (P(x) ∧ ∀y (P(y) → x = y)) или • (∃x P(x)) ∧ ∀y, z (P(y) ∧ P(z) → y = z) 10/15 Формализация • Часто возникает задача: дано утверждение (математическое или в терминах «реального мира»), нужно записать его в виде формулы данной сигнатуры. • Пример: «Кто-то любит всех на свете». Универсум: люди, предикат Loves(x, y) для «x любит y». • Кто-то любит всех на свете ≡ ∃x x любит всех на свете 11/15 Формализация • Часто возникает задача: дано утверждение (математическое или в терминах «реального мира»), нужно записать его в виде формулы данной сигнатуры. • Пример: «Кто-то любит всех на свете». Универсум: люди, предикат Loves(x, y) для «x любит y». • Кто-то любит всех на свете ≡ ∃x x любит всех на свете ≡ ∃x ∀y x любит y 11/15 Формализация • Часто возникает задача: дано утверждение (математическое или в терминах «реального мира»), нужно записать его в виде формулы данной сигнатуры. • Пример: «Кто-то любит всех на свете». Универсум: люди, предикат Loves(x, y) для «x любит y». • Кто-то любит всех на свете ≡ ∃x x любит всех на свете ≡ ∃x ∀y x любит y ≡ ∃x ∀y Loves(x, y). 11/15 Формализация • Часто возникает задача: дано утверждение (математическое или в терминах «реального мира»), нужно записать его в виде формулы данной сигнатуры. • Пример: «Кто-то любит всех на свете». Универсум: люди, предикат Loves(x, y) для «x любит y». • Кто-то любит всех на свете ≡ ∃x x любит всех на свете ≡ ∃x ∀y x любит y ≡ ∃x ∀y Loves(x, y). • Ещё пример в той же сигнатуре: «Всякая любовь взаимна». • Ответ: 11/15 Формализация • Часто возникает задача: дано утверждение (математическое или в терминах «реального мира»), нужно записать его в виде формулы данной сигнатуры. • Пример: «Кто-то любит всех на свете». Универсум: люди, предикат Loves(x, y) для «x любит y». • Кто-то любит всех на свете ≡ ∃x x любит всех на свете ≡ ∃x ∀y x любит y ≡ ∃x ∀y Loves(x, y). • Ещё пример в той же сигнатуре: «Всякая любовь взаимна». • Ответ: ∀x ∀y (Loves(x, y) → Loves(y, x)). 11/15 Формализация • Часто возникает задача: дано утверждение (математическое или в терминах «реального мира»), нужно записать его в виде формулы данной сигнатуры. • Пример: «Кто-то любит всех на свете». Универсум: люди, предикат Loves(x, y) для «x любит y». • Кто-то любит всех на свете ≡ ∃x x любит всех на свете ≡ ∃x ∀y x любит y ≡ ∃x ∀y Loves(x, y). • Ещё пример в той же сигнатуре: «Всякая любовь взаимна». • Ответ: ∀x ∀y (Loves(x, y) → Loves(y, x)). • И ещё: «Кто-то не любит никого, кто любит его». • Ответ: 11/15 Формализация • Часто возникает задача: дано утверждение (математическое или в терминах «реального мира»), нужно записать его в виде формулы данной сигнатуры. • Пример: «Кто-то любит всех на свете». Универсум: люди, предикат Loves(x, y) для «x любит y». • Кто-то любит всех на свете ≡ ∃x x любит всех на свете ≡ ∃x ∀y x любит y ≡ ∃x ∀y Loves(x, y). • Ещё пример в той же сигнатуре: «Всякая любовь взаимна». • Ответ: ∀x ∀y (Loves(x, y) → Loves(y, x)). • И ещё: «Кто-то не любит никого, кто любит его». • Ответ: ∃x ∀y (Loves(y, x) → ¬Loves(x, y)). 11/15 Формализация со свободными переменными • У нас на предыдущем слайде появлялись утверждения с переменными (например, «x любит всех на свете») в промежуточных результатах. • Может и сразу быть дано такое утверждение. 12/15 Формализация со свободными переменными • У нас на предыдущем слайде появлялись утверждения с переменными (например, «x любит всех на свете») в промежуточных результатах. • Может и сразу быть дано такое утверждение. • В результате должна получиться формула с теми же свободными переменными (и какими угодно связанными). 12/15 Формализация со свободными переменными • У нас на предыдущем слайде появлялись утверждения с переменными (например, «x любит всех на свете») в промежуточных результатах. • Может и сразу быть дано такое утверждение. • В результате должна получиться формула с теми же свободными переменными (и какими угодно связанными). • Если в формуле есть «лишние» свободные переменные или связана одна из тех, что есть в формализуемом утверждении, это заведомо неверный ответ. 12/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! • Более того, если / — функциональный символ, то он должен иметь значение в нашем универсуме для любых аргументов. Есть варианты логики, которые снимают это ограничение, но мы их не изучаем. 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! • Более того, если / — функциональный символ, то он должен иметь значение в нашем универсуме для любых аргументов. Есть варианты логики, которые снимают это ограничение, но мы их не изучаем. • Ответ (возможный): 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! • Более того, если / — функциональный символ, то он должен иметь значение в нашем универсуме для любых аргументов. Есть варианты логики, которые снимают это ограничение, но мы их не изучаем. • Ответ (возможный): ∃y x = 2 · y. 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! • Более того, если / — функциональный символ, то он должен иметь значение в нашем универсуме для любых аргументов. Есть варианты логики, которые снимают это ограничение, но мы их не изучаем. • Ответ (возможный): ∃y x = 2 · y. • Можно ли то же самое записать без ·? 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! • Более того, если / — функциональный символ, то он должен иметь значение в нашем универсуме для любых аргументов. Есть варианты логики, которые снимают это ограничение, но мы их не изучаем. • Ответ (возможный): ∃y x = 2 · y. • Можно ли то же самое записать без ·? Да! ∃y x = y + y. 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! • Более того, если / — функциональный символ, то он должен иметь значение в нашем универсуме для любых аргументов. Есть варианты логики, которые снимают это ограничение, но мы их не изучаем. • Ответ (возможный): ∃y x = 2 · y. • Можно ли то же самое записать без ·? Да! ∃y x = y + y. • Вот «x делится на y» без · записать уже не получится. 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! • Более того, если / — функциональный символ, то он должен иметь значение в нашем универсуме для любых аргументов. Есть варианты логики, которые снимают это ограничение, но мы их не изучаем. • Ответ (возможный): ∃y x = 2 · y. • Можно ли то же самое записать без ·? Да! ∃y x = y + y. • Вот «x делится на y» без · записать уже не получится. • Задание сложнее: «x — простое число». • Ответ (возможный): 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! • Более того, если / — функциональный символ, то он должен иметь значение в нашем универсуме для любых аргументов. Есть варианты логики, которые снимают это ограничение, но мы их не изучаем. • Ответ (возможный): ∃y x = 2 · y. • Можно ли то же самое записать без ·? Да! ∃y x = y + y. • Вот «x делится на y» без · записать уже не получится. • Задание сложнее: «x — простое число». • Ответ (возможный): ∀y ∀z x = y · z → y = 1 ∨ z = 1. 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! • Более того, если / — функциональный символ, то он должен иметь значение в нашем универсуме для любых аргументов. Есть варианты логики, которые снимают это ограничение, но мы их не изучаем. • Ответ (возможный): ∃y x = 2 · y. • Можно ли то же самое записать без ·? Да! ∃y x = y + y. • Вот «x делится на y» без · записать уже не получится. • Задание сложнее: «x — простое число». • Ответ (возможный): ∀y ∀z x = y · z → y = 1 ∨ z = 1. • Неправда! В чём ошибка? 13/15 Ещё примеры формализации • «x делится на 2». Универсум: натуральные числа. • Если предположили что-то вроде x/2 ∈ N: это не подойдёт. Почему? • Например, N это не объект нашего универсума. А если ∈ N рассматривать как единый предикатный символ, он верен для всех объектов! • Более того, если / — функциональный символ, то он должен иметь значение в нашем универсуме для любых аргументов. Есть варианты логики, которые снимают это ограничение, но мы их не изучаем. • Ответ (возможный): ∃y x = 2 · y. • Можно ли то же самое записать без ·? Да! ∃y x = y + y. • Вот «x делится на y» без · записать уже не получится. • Задание сложнее: «x — простое число». • Ответ (возможный): ∀y ∀z x = y · z → y = 1 ∨ z = 1. • Неправда! В чём ошибка? 13/15 x 6= 1 ∧ ∀y ∀z x = y · z → y = 1 ∨ z = 1. Многосортная логика предикатов • Часто удобно одновременно говорить о нескольких разных типах объектов. Пример: числа, множества чисел и функции в мат. анализе. Тогда • К сигнатуре добавляется набор сортов. Каждый сорт обозначает какое-то множество объектов. 14/15 Многосортная логика предикатов • Часто удобно одновременно говорить о нескольких разных типах объектов. Пример: числа, множества чисел и функции в мат. анализе. Тогда • К сигнатуре добавляется набор сортов. Каждый сорт обозначает какое-то множество объектов. • У функциональных и предикатных символов кроме числа аргументов задан сорт каждого, у функциональных ещё и сорт результата. 14/15 Многосортная логика предикатов • Часто удобно одновременно говорить о нескольких разных типах объектов. Пример: числа, множества чисел и функции в мат. анализе. Тогда • К сигнатуре добавляется набор сортов. Каждый сорт обозначает какое-то множество объектов. • У функциональных и предикатных символов кроме числа аргументов задан сорт каждого, у функциональных ещё и сорт результата. • Каждая переменная имеет сорт: x : S. 14/15 Многосортная логика предикатов • Часто удобно одновременно говорить о нескольких разных типах объектов. Пример: числа, множества чисел и функции в мат. анализе. Тогда • К сигнатуре добавляется набор сортов. Каждый сорт обозначает какое-то множество объектов. • У функциональных и предикатных символов кроме числа аргументов задан сорт каждого, у функциональных ещё и сорт результата. • Каждая переменная имеет сорт: x : S. • Можно индуктивно определить сорт любого терма. Применение символов к аргументам не тех сортов считается бессмысленным (т.е. его результат не является термом/формулой). • TODO Что делаем с этими ситуациями в односортном случае. • TODO модели 14/15 Домашнее задание • TODO 15/15