Следует еще раз обратить внимание, что формула F должна быть выводимой в исчислении высказываний.
Если выводимая формула F содержит некоторую переменную A (обозначим этот факт F(A)) и сущест-вует произвольная формула B, то формула F(B), получающаяся заменой всех вхождений A на формулу B, также выводима в исчислении высказываний. Этот факт формально описывают так
Правила подстановки
B,
Есть определенная связь между отношением логичес-кого вывода в схеме дедукивного вывода и импликацией в схеме закона алгебры высказываний .
Правила вывода
Выводом формулы В из множества формул F1; F2; . . . Fn называется такая последовательность формул, что любая Fi есть либо аксиома, либо непосредственно выводима из подмножества предшествующих ей формул F1; F2; . . . Fn.
В этом случае формулу B называют заключением, а последовательность формул F1; F2; . . . Fn, сформирован -ная отношением логического вывода, представляет схему дедуктивного вывода.
Схему дедуктивного вывода записывают так:
F1; F2; . . . Fn |¾ B,
где символ |¾ означает “верно, что B выводима из F1; F2;... Fn“.
Этот факт записывают так:
|¾ F1&F2&. . . &Fn®B.
Известна другая форма записи дедуктивного вывода формулы В:
F1; F2; . . . Fn
где над чертой записывают множество посылок и аксиом F1; F2;...Fn, а под чертой заключение В, принимающее значение “истины” при истинности всех посылок.
Если F(A)=A, то
Если F (ùA), то
При выводе заключения удобно правила введения и удаления логических связок представить также как и правила вывода:
1) если посылки F1 и F2 имеют значение “и”, то истинной является их конъюнкция, т.е.
F1 ; F2
(F1&F2) .
Эта запись при истинности посылок F1 и F2 предусматривает возможность введения в заключение логической связки конъюнкции; это правило тождественно аксиоме А5;
2) если (F1&F2) имеет значение “и”, то истинными являются подформулы F1 и F2, т.е.
(F1&F2) (F1&F2)
F1 и F2.
Эта запись при истинности (F1&F2) предусматри -вает возможность удаления в заключении логической связки конъюнкции и рассматривать истинные значения подформул F1 и F2; это правило тождественно аксиомам А3 и А4;
3) если F1 имеет значение “и”, а (F1&F2) – “л”, то ложной является подформулы F2, т.е.
F1;ù (F1&F2)
ù F2.
Эта запись при ложности (F1&F2) и истинности одной из подформул предусматривает возможность удаления в заключении логической связки конъюнкции и рассматривать ложным значение второй подформулы;
4) если истинна хотя бы одна посылка F1 или F2, то истинной является их дизъюнкция, т.е.
F1 F2
(F1ÚF2) или (F1ÚF2).
Эта запись при истинности хотя бы одной подформулы F1 или F2 предусматривает возможность введения в заключение логической связки дизъюнкции; это правило тождественно аксиомам А6 и А7;
5) если (F1ÚF2) имеет значение “и” и одна из подформул F1 или F2 имеет значение “л”, то истинной является вторая подформула F2 или F1, т.е.
(F1ÚF2); ùF1 (F1ÚF2);ùF2
F2 или F1.
Эта запись при истинности (F1ÚF2) предусматривает возможность удаления в заключении логической связки дизъюнкции и рассматривать истинные значения подформул F1 или F2;
6) если подформула F2 имеет значение “и”, то истинной является формула (F1®F2) при любом значении подформулы F1, т.е
F2
(F1®F2).
Эта запись при истинном значении F2 предусматривает возможность введения в заключение логической связки импликации при любом значении подформулы F1 (“истина из чего угодно”); это правило тождественно аксиоме 1;
7) если подформула F1 имеет значение “л”, то истинной является формула (F1®F2) при любом значении подформулы F2, т.е
ù F1
(F1®F2).
Эта запись при ложном значении F1 предусматривает возможность введения в заключение логической связки импликации при любом значении подформулы F2 (“ из ложного что угодно”);
8) если формула (F1®F2) имеет значение “и”, то истинной является формула (ù F2®ù F1), т.е
(F1®F2)
(ù F2®ù F1).
Эта запись при истинном значении (F1®F2) определяет возможность замены местами полюсов импликации при одновременном изменении их значений; это- закон контрапозиции;
9) если формула (F1®F2) имеет значение “и”, то истинной является формула (F1ÚF3)®(F2ÚF3) при любом значении F3, т.е
(F1®F2)
(F1ÚF3)®(F2ÚF3).
Эта запись при истинном значении (F1®F2) определяет возможность выполнить операцию дизъюнкции при любом значении формулы F3 над каждым полюсом импликации; это правило тождественно аксиоме А11.
10) если формула (F1®F2) имеет значение “и”, то истинной является формула (F1&F3)®(F2&F3) при любом значении F3, т.е
(F1®F2)
(F1&F3)®(F2&F3).
Эта запись при истинном значении (F1®F2) определяет возможность выполнить операцию конъюнкции при любом значении формулы F3 над каждым полюсом импликации; это правило тождественно аксиоме А10.
11) если формулы (F1®F2) и (F2®F3) имеют значение “и”, то истинной является формула (F1®F3), т.е
(F1®F2); (F2®F3)
(F1®F3).
Эта запись при истинном значении (F1®F2) и (F2®F3) предусматривает возможность формирования импликации (F1®F3) (закон силлогизма);
