Правило образования выводимых формул:
a-альфа, b-бета.
1)ПРАВИЛО ЗАКЛЮЧЕНИЯ: Если а и a->b - выводимые формулы ИВ, то b - также выводимая формула: ((a,a->b)/?);
2)ПРАВИЛО ПОДСТАНОВКИ в переменное высказывание и переменный предикат: а)замена переменного ВЫСКАЗЫВАНИЯ: пусть а (альфа) содержит переменное высказывание А, тогда мы можем заменить в формуле а букву А всюду, где где она входит любой формулой b (бета), удовлетв. след условиям: 1)свободные переменные в b обозначены буквами, отличными от связанных переменных в a; 2)если А в a нах-ся в области действия квантора, обозначенного к.-л. буквой, то эта буква не входит в b. Такая подстановка называется заменой перменной в b на A. б)замена переменного ПРЕДИКАТА: пусть ф-ла а содержит предикат F(n), перем. b(t1,t2,...tn), ti - свободн. перем., где i изменяется от 1 до n. t1,t2,...,tn -отличны от всех предметных переменных в а. Если для ф-лы b соблюд-ся условие 1) и 2) (см. выше) и если F в а нах-ся в обл-и действия квантора, связывающего к.-л. букву, то эта буква не входит в b, то возможна подстановка ф-лы b(бета) в а(альфа) вместо предиката F.
3)ПРАВИЛО ЗАМЕНЫ свободной предметной переменной: а(альфа)-выводимая ф-ла в ИП. а’ получается из а заменой любой свободн. предметной переменной другой свободн. предметной переменной, так что заменяемая переменная заменяется одинаковым образом всюду, где она входит в формулу а, тогда а' - тоже выводимая формула в ИП.
4)ПРАВИЛО ПЕРЕИМЕНОВАНИЯ связанных предметных переменных: если а выв-я в ИП то ф-ла а’ полученная из а заменой связанных предметных другими свазанными переменнымими, отличными от всех свободных предм. перменных в а, то a' также является выводимой формулой в ИП.
5)ПРАВИЛО СВЯЗЫВАНИЯ квантором: 1)если b->а(х) – выв ф-ла в ИП и b не содержит свободн. переменной х, то b->Vxf(х) - выводимая ф-ла в ИП; 2)если а(х)->b выв ф-ла в ИП и b не содержит своб переменной х, то Эxа(х)->b - выводимая ф-ла в ИП.
Примечание:1)среди выв-х ф-л в ИП нах-ся все выв-е ф-лы ИВ; 2)всякая ф-ла выведенная из аксиом по прав-м ИП явл-ся тожд истинной ф-лой.
