ИП1: некоторые дополнительные метатеоремы
1.Подобные формулы
Определение. Пусть переменные 
, и формула 
получается из формулы 
подстановкой на место всех свободных вхождений переменной 
переменной 
.
Тогда формула 
называется подобной формуле 
, если терм 
свободен для переменной 
в формуле 
, а также 
.
Обозначение подобных формул: 
.
Пример. Формула 
подобна формуле 
(здесь p – унарный, а r – бинарный предикатные символы).
Заметим, что в формуле 
нельзя заменить 
на 
, так как тогда терм 
не будет свободен для переменной 
в формуле 
.
Утверждение 1. Если 
, то 
, т. е. эквивалентность формул определяет симметричное отношение.
Доказательство. Нужно показать, что если в формуле 
выполнить обратную замену, то условия подобия будут выполнены.
Действительно, свободных вхождений 
в 
нет, так как все они заменены переменной 
. Далее, ни одно свободное вхождение 
в 
не содержится в области действия квантора по 
, так как любое такое вхождение появилось в результате замены только свободных вхождений 
в 
, а свободных вхождений 
в 
нет, т. е. терм 
свободен для переменной 
в формуле 
, т. е. 
.
Утверждение 2. Если 
, то 
.
Доказательство. Вывод 
из 
:
- гипотеза; 
- схема (4) (терм 
свободен для 
!); 
- Gen, (2); 
- схема (5) (свободных вхождений 
в 
нет!); 
- MP, (3) и (4); 
- MP, (1) и (5). Аналогично доказывается обратная выводимость.
В силу доказанного можно (при соответствующих ограничениях) переименовывать формулах свободные переменные.
Утверждение 3. Если 
, то
; 
; 
; 
. Доказательство. (a) Используя правило Gen, получим 
+ 
, но поскольку формула A не содержит свободных вхождений x, применима теорема дедукции, и + 
.
Обратное следует из схемы (4). Тем самым 
+
.
(b) Докажем, что + 
.
Действительно, +
в силу п. (a). Но 
. Остается применить секвенцию (4).
С другой стороны, легко показать, что 
. Тогда 
+ 
. Итак, 
+
.
(c ) Выводимость «слева направо» имеет место в силу схемы (5).
Обратно:
- гипотеза; 
- правило (А4); 
- секвенция (1) к (1) и (2); 
- Gen, (3). Теорема дедукции применима, так как 
.
- гипотеза; 2. 
- (А4);
3. 
- MP, (1) и (2);
4. 
- пр. (7’);
5. 
- Gen, (4);
6. 
- схема (5);
7. 
- MP, (5) и (6);
8. 
- пр. (7’);
9. 
- секв. (3);
10. 
- секв. (1) к (8) и (9).
Итак, 
+ 
.
Обратно:
- гипотеза; 
- секв. (3); 
- секв. (1); (1) и (2); 
- пр. (6’), (3); 
- схема (4); 
- секв. (1); (4), (5); 
- пр. (6’), (6); 
- Gen, (7). Тем самым требуемая эквивалентность доказана.
Утверждение 4. Для любых формул A и B
+
.
Доказательство. [M, стр. 81-82].
Тогда, на основании доказанных результатов может быть доказана теорема, называемая теоремой эквивалентности.
Теорема 1. Если B есть подформула A и A’ есть результат замены некоторых (ни одного в том числе) вхождений B в A формулой C и если всякая свободная переменная формулы B или формулы C, которая одновременно является связанной переменной формулы A встречается в множестве переменных 
, то
+
.
Доказательство. [M, стр. 82-83].
Одно из следствий этой теоремы и утверждения 2 показывает возможность переименования связанных переменных.
Следствие. Если 
есть подформула формулы A, 
и A’ есть результат замены по крайней мере одного вхождения 
на 
, то 
.
