Если выводимая формулаF содержит некоторую переменную A (обозначим этот факт F(A)) и существует произвольная формула B, то формула F(B), получающаяся заменой всех вхождений A на формулу B, также выводима в исчислении высказываний. Этот факт формально описывают так:
Этот факт записывают так:
АòВF(А)
F(В).
Если F(A)=A, то АòВА
В.
Если F (ùA), то АòВF(ùА)
F(ùВ).
Следует еще раз обратить внимание, что формула F должна быть выводимой в исчислении высказываний.
Пример: Пусть даны формулы F=A&C®A и B=C®ùA.
Если выполнить подстановку формулы B в формулу F вместо формулы A, то получим новую формулу F`.
А ò C®ùA (A&C®A)
(C®ùA)&C®(C®ùA).
A |
B |
C |
1&3 |
4®1 |
3®ù1 |
6&3 |
7®6 |
||
|
1 |
2 |
3 |
4 |
5 |
6 |
7 |
8 |
||
|
л |
л |
л |
л |
и |
и |
л |
и |
||
|
л |
л |
и |
л |
и |
и |
и |
и |
||
|
л |
и |
л |
л |
и |
и |
л |
и |
||
|
л |
и |
и |
л |
и |
и |
и |
и |
||
|
и |
л |
л |
л |
и |
и |
л |
и |
||
|
и |
л |
и |
и |
и |
л |
л |
и |
||
|
и |
и |
л |
л |
и |
и |
л |
и |
||
|
и |
и |
и |
и |
и |
л |
л |
и |