Выводимость ф-лы ? из ф-лы ?:1)каждая выв-я ф-ла ? в ИПвыводима из ф-лы ? если ?->? не содержит коллизии.2)?+?.3)если ф-лы ?1 и ?1??2 выводимы из ? то ?+ ?2.4)если ?1??2(х) выводимы из ? причём ? и ? не содержит пер-ю х то ф-ла ?1?Vx?2(х) также выв-ма из ?.5)если ?+?2(х)??1 причём ?1 и ? не содержат х то ?+Эх?2(х)??1.6)если ?+?, то ?+?’ где ?’-ф-ла полученная из ? любым пер-ем связанных переменных не приводящим к коллизии переменных.7)если ?+?, то ?+?’ где ?’-ф-ла полученная из ? подстановкой своб предмет пер-х не входящих в ? не привлдящих к коллизии пер-х с ?.8)если ?+?, то ?+?’ где ?’-ф-ла полученная из ? подстановкой пер-х В или П не входящих в ? и если подстановка не приводит к коллизии пер-х с ?. Теорема дедукции. Если формула a выводима из формулы b, то формула выводима в исчислении предикатов.
