Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 29
Текст из файла (страница 29)
Соответствующее исчисление называется исчислением предикатов.Пусть фиксирована некоторая сигнатура σ. Формула ϕ этой сигнатуры (возможно, с параметрами) называется общезначимой, еслиона истинна в любой интерпретации сигнатуры σ на любой оценке.Общезначимые формулы в логике предикатов играют ту же роль,что тавтологии в логике высказываний. Между ними есть и формальная связь: если взять любую тавтологию и вместо входящих внеё пропозициональных переменных подставить произвольные формулы сигнатуры σ, получится общезначимая формула. В самом деле,пусть есть некоторая интерпретация сигнатуры σ и некоторая оценка (то есть фиксированы значения индивидных переменных).
Тогдакаждая из подставленных формул станет истинной или ложной, азначение всей формулы определяется с помощью таблиц истинностидля логических связок, то есть по тем же правилам, что в логикевысказываний.Конечно, бывают и другие общезначимые формулы, не являющиеся частными случаями пропозициональных тавтологий. Например,формула∀x A(x) → ∃yA(y)общезначима (здесь существенно, что носитель любой интерпретации непуст). Другие примеры общезначимых формул (во втором случае ϕ — произвольная формула):∃y ∀x B(x, y) → ∀x ∃y B(x, y),¬∀x ¬ϕ → ∃x ϕ.87.
Будет ли общезначима формула (а) ∀x ∃y B(x, y) → ∃y ∀x B(x, y);(б) ¬∀x ∃y B(x, y) → ∃x ∀y ¬B(x, y)?Многие вопросы можно сформулировать как вопросы об общезначимости некоторых формул. Например, можно записать свойства рефлексивности, транзитивности и антисимметричности в видеформул R, T и A сигнатуры (=, <) и затем написать формулуR ∧ T ∧ A → ∃x ∀y ((y < x) ∨ (y = x)).[п.
1]Общезначимые формулы129Общезначимость этой формулы означала бы, что любое линейно упорядоченное множество имеет наибольший элемент, так что она необщезначима.88. Напишите формулы R, T, A и проверьте, что приведённая намиформула не общезначима, хотя истинна во всех конечных интерпретациях.89. Известно, что формула истинна во всех конечных и счётных интерпретациях. Можно ли из этого заключить, что она общезначима? (Указание: воспользуйтесь теоремой Левенгейма – Сколема.)Две формулы ϕ и ψ (с параметрами или без) называются эквивалентными, если в любой интерпретации и на любой оценке, накоторой истинна одна из них, истинна и другая. Это определениеравносильно такому: формула ϕ ↔ ψ общезначима.
Здесь, напомним, ϕ ↔ ψ есть сокращение для ((ϕ → ψ) ∧ (ψ → ϕ)).Общезначимость любой формулы ϕ очевидно равносильна общезначимости её замыкания — формулы, которая получится, еслислева к ϕ приписать кванторы всеобщности по всем параметрам.Двойственное к общезначимости понятие — выполнимость. Формула называется выполнимой, если она истинна в некоторой интерпретации на некоторой оценке. Очевидно, формула ϕ общезначиматогда и только тогда, когда формула ¬ϕ не является выполнимой.90.
Закончите утверждение: выполнимость формулы с параметрамиравносильна выполнимости замкнутой формулы . . .Чтобы проверить, является ли формула тавтологией, достаточно подставить в неё все возможные наборы значений переменных.Хотя этот процесс может быть на практике невыполним (наборовслишком много), теоретически мы имеем простой алгоритм проверки, является ли формула тавтологией. Для общезначимых формул вобщем случае такого алгоритма не существует, как мы увидим в разделе 5.4 (теорема Чёрча, с.
191); разрешающий алгоритм есть толькодля очень ограниченных классов формул. Например, если сигнатура содержит только нульместные предикатные символы, то задачапо существу сводится к проверке тавтологичности (в этом случаекванторы фиктивны). Чуть более сложен случай с одноместнымипредикатами.91. Пусть сигнатура σ содержит только одноместные предикаты. Докажите, что всякая выполнимая формула этой сигнатуры, содержащаяn различных предикатов, выполнима в некоторой конечной интерпретации, содержащей не более 2n элементов.
Как использовать этот факт дляалгоритмической проверки выполнимости формул такой сигнатуры?Мы вернёмся к этому вопросу в разделе 5.4 (с. 188) и увидим, чторазрешимость сохраняется при добавлении аксиом равенства.130Исчисление предикатов[гл. 4]4.2. Аксиомы и правила выводаВозвратимся к нашей задаче: какие аксиомы и правила выводанам нужны, чтобы получить все общезначимые формулы некоторойсигнатуры σ? Естественно использовать все схемы аксиом (1) – (11)исчисления высказываний (раздел 2.1), но только вместо букв A, Bи C теперь можно подставлять произвольные формулы сигнатуры σ.Теорема о полноте исчисления высказываний гарантирует, что послеэтого мы сможем вывести любой частный случай любой пропозициональной тавтологии (то есть любую формулу, которая получаетсяиз пропозициональной тавтологии заменой пропозициональных переменных на формулы сигнатуры σ).
В самом деле, возьмём выводэтой тавтологии в исчислении высказываний (которое, как мы знаем, полно) и выполним соответствующую замену во всех формулахэтого вывода.Почти столь же просто понять, что ничего другого такие аксиомыне дадут: если пользоваться лишь схемами аксиом (1) – (11), разрешая брать в них в качестве A, B, C произвольные формулы сигнатуры σ, а в качестве правила вывода использовать modus ponens, то всевыводимые формулы будут частными случаями пропозициональныхтавтологий.
В самом деле, если какая-то подформула начинается сквантора, то в выводе она может встречаться только как единое целое, то есть такая подформула ведёт себя как пропозициональнаяпеременная.92. Проведите это рассуждение аккуратно.Это наблюдение скорее тривиально, чем удивительно — если среди наших аксиом и правил вывода нет ничего о смысле кванторов, тоформулы, начинающиеся с кванторов, будут вести себя как неделимые блоки.
Таким образом, нам нужны аксиомы и правила вывода,отражающие интуитивный смысл кванторов.Вспомним, как выглядели аксиомы исчисления высказываний.Было два типа аксиом для конъюнкции и дизъюнкции: одни говорили, что из них следует (например, из A ∧ B следовало B), а другие —как их можно доказать (например, аксиома (A → (B → (A ∧ B)))говорила, что для доказательства (A ∧ B) надо доказать A и B).Кванторы всеобщности и существования в некотором смысле аналогичны конъюнкции и дизъюнкции, и аксиомы для них тоже будутпохожими.
Например, среди аксиом будет формула∀x A(x) → A(t),[п. 2]Аксиомы и правила вывода131где A — одноместный предикатный символ нашей сигнатуры, а t —константа, переменная или вообще любой терм. (Если A верно длявсех x, то оно должно быть верно и для нашего конкретного t. Можносказать и так: из «бесконечной конъюнкции» всех A(x) вытекаетодин из её членов.)Конечно, такую аксиому надо иметь не только для одноместногопредикатного символа A, но для любой формулы ϕ, любой переменной ξ и любого терма t.
Естественно сказать, что если ϕ — любаяформула, а t — любой терм, то формула∀ξ ϕ → ϕ(t/ξ),где ϕ(t/ξ) обозначает результат подстановки t вместо всех вхождений переменной ξ в формулу ϕ, является аксиомой. (Запись ϕ(t/ξ)можно читать как «фи от тэ вместо кси».)К сожалению, всё не так просто. Например, если формула ϕ имеетвидA(x) ∧ ∃x B(x, x),то подстановка терма f (y) вместо x даст абсурдное выражениеA(f (y)) ∧ ∃f (y) B(f (y), f (y)),вообще не являющееся формулой.
А если подставить f (y) тольковнутри A и B, то получится выражениеA(f (y)) ∧ ∃x B(f (y), f (y)),которое хотя и будет формулой, но имеет совсем не тот смысл, который нам нужен.Конечно, в данном случае по смыслу ясно, что подставлять f (y)надо лишь вместо самого первого вхождения переменной x. Но еслимы хотим определить формальную систему аксиом и правил вывода,то надо дать формальные определения.Для каждого квантора в формуле рассмотрим его область действия — начинающуюся с него подформулу. Свободным вхождением индивидной переменной в формулу называется вхождение, не попадающее в область действия одноимённого квантора.
Легко понять,что это определение можно переформулировать индуктивно:• любое вхождение переменной в терм или атомарную формулусвободно;132Исчисление предикатов[гл. 4]• свободные вхождения переменной в формулу ϕ являются еёсвободными вхождениями в формулу ¬ϕ;• свободные вхождения любой переменной в одну из формул ϕи ψ являются свободными вхождениями в (ϕ ∧ ψ), (ϕ ∨ ψ) и(ϕ → ψ);• переменная ξ не имеет свободных вхождений в формулы ∀ξ ϕи ∃ξ ϕ; свободные вхождения остальных переменных в ϕ являются свободными вхождениями в эти две формулы.Сравнивая это определение с индуктивным определением параметров формулы в разделе 3.2, мы видим, что параметры — это переменные, имеющие свободные вхождения в формулу.Вхождения переменной, не являющиеся свободными (в том числе стоящие рядом с квантором) называют связанными.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
