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