НОУ ІНТУІТ, Лекція, Повнота обчислення предикатів
Перейменування змінних
У цьому розділі ми спробуємо обережно розібратися з простим питанням про те, чому і як можна перейменовувати пов'язані змінні, не змінюючи значення формул. Ми вже бачили, що формули і доведено еквівалентні, тобто їхня еквівалентність доведена в обчисленні предикатів. Наразі ми хочемо довести загальне твердження про це.
Коректне формулювання твердження про перейменування змінних потребує обережності. Наприклад, не можна сказати, що формула завжди еквівалентна. Насамперед, підстановка може бути некоректною, як у разі формул
Найнаочніше, мабуть, зробити так. Давайте укладемо у рамку всі пов'язані входження всіх змінних (зокрема входження після кванторов). Після цього з'єднаємо змінними лініями після квантора і всі її входження, пов'язані саме цим входженням квантора. Вільні входження змінних залишаються у своїй без рамок. Вийде щось на кшталт
Теорема 52. (Перейменування пов'язаних змінних)Подібні формули доказово еквівалентні.
Доведемо дві прості леми.
Лемма 1. Якщо формула не містить змінної (ні пов'язано, ні вільно), то формули
Доведення . Насправді, підстановка коректна, так як немає кванторів по . Тому виведена формула
У зворотний бік: підстановка замість формулу коректна (оскільки була підставлена замість вільних входжень , при зворотній підстановці змінна не потрапить у дію кванторів у ній) і дає формулу . Тому формула
Аналогічне твердження для квантора існування доводиться так само.
Лемма 2. Заміна підформули на доказно еквівалентну дає доказно еквівалентну формулу.
Доведення . Як мибачили, що доведена еквівалентність зберігається після навішування квантора: якщо , то і (символ тут позначає еквівалентність, що доводиться ). Крім того, з і випливає, що , , і . (У цьому легко переконатися, написавши відповідні тавтології пропозиції .)
Тепер твердження леми легко довести індукцією (почавши із заміненої підформули та розглядаючи дедалі довші частини формули). Лемма 2 доведена.
Леми 1 і 2 дозволяють нам замінювати змінні всередині рамок схеми на нові (раніше не використані) змінні, отримуючи еквівалентну і подібну вихідну формулу. Такими замінами можна з двох подібних формул отримати третю, використовуючи для заміни одні й самі змінні. При цьому обидві вихідні формули доведено еквівалентні третій, а отже, і одна одній.
(Використання третьої формули істотно: ми можемо перетворити першу формулу відразу на другу, оскільки за заміні змінних у межах може виконуватися умова леми 1.)
Менш радикальний варіант полягає в тому, щоб розділити змінні на два типи – вільні та пов'язані. Так робиться, наприклад, у класичній книзі Гільберта та Бернайса Підстави математики [8]. Тоді можна сміливо підставляти терм замість вільної змінної, зате при навішуванні квантора треба замінювати вільну змінну на пов'язану.
Ще один варіант — домовитися, що при підстановці терму замість вільної змінної автоматично відбувається перейменування пов'язаних змінних, що створюють колізії.