Правило подстановки
Пусть U формула, содержащая переменную А. Тогда, если U - выводимая формула исчисления высказывания, то, заменив в ней
переменную А произвольной формулой b,получим так же выводимую формулу .
Правило заключения (modUs pones)
Если U и U->b выводимые формулы, то b так же выводима (правило отделения). (U, U->b b ).
Выводом формулы G из формул F1, …,Fn называется такая последовательность формул E1,…, En, где Ек=G и любая формула Ei(i<*>к)
является:
• либо аксиомой;
• либо формулой FJ(Ei=FJ);
• либо Ei получается из каких-либо предыдущих E1,…, Ei-1, одним из правил выведения ;
Сама формула G называется выводимой из формул F1,…,Fn .
F1,…,Fn ¬├ G.
Формула G выводимая только из аксиом называется теоремой, а вывод - доказательство этих теорем.
При построении вывода можно пользоваться уже полученными результатами, в частности, полученными теоремами и очень важной
теоремой: