ЗНАЙ ИНТУИТ, Лекция, Пълнота на предикатното смятане
Преименуване на променливи
В този раздел ще се опитаме да се справим спретнато с простия въпрос защо и как можете да преименувате обвързани променливи, без да променяте значението на формулите. Вече видяхме, че формулите и са доказуемо еквивалентни, тоест тяхната еквивалентност е доказуема в предикатното смятане. Сега искаме да докажем общо твърдение за това.
Правилното формулиране на оператор за преименуване на променлива изисква внимание. Например, не може да се каже, че формулата винаги е еквивалентна. На първо място, заместването може да е неправилно, както в случая с формулите
Очевидно най-очевидният начин е да се направи това. Нека рамкираме всички асоциирани събития на всички променливи (включително появите след кванторите). След това свързваме с редове променливата след квантора и всички нейни появявания, свързани от тази конкретна поява на квантора. Свободното появяване на променливи остава без граници. Ще се получи нещо като
Теорема 52. (преименуване на обвързани променливи) Такива формули са доказано еквивалентни.
Нека докажем две прости леми.
Лема 1. Ако формулата не съдържа променлива (нито обвързана, нито свободна), тогава формулите
Доказателство. Всъщност заместването е правилно, тъй като няма квантори за. Следователно извличаме формулата
В обратната посока: заместването вместо във формулата е правилно (тъй като е заместено вместо свободни записи, в случай на обратно заместване променливата няма да попадне в обхвата на кванторите от нея) и дава формулата. Следователно формулата