формула b ВЫВОДИМА из формул a1, a2, ..., an (a1, a2, ..., an|-b): 1) ai (i изменяется от 1 до n) выводима из формул a1, a2, ..., an. 2) каждая выводимая в ИВ формула выводима из a1, a2, ..., an. 3) a и a->b выводимы из a1, a2, ..., an, то и формула b также выводима из a1, a2, ..., an. Утверждение что формула b ВЫВОДИМА из a1, a2, ..., an обозначается так: a1, a2, ..., an|-b.
если n=0, т.е. если ai нет, будем считать что b является просто выводимой формулой ИВ. т.е. |-b.
теорема ДЕДУКЦИИ: если формула a1, ..., an|-b, то a1->(a2->(...(an->b)...)) - выводимая формула.
PS: теоремы о выводимости формул ИВ: Т1: |-B->R Т2: A->A Т3: (A->B)->((B->C)->(A-C)) Т4:|-(A->(B->C))->(B->(A->C)) Т5: |-A->(B->A&B) Т6: a) |-(A->(B->C))->(A&B->C), b)|-(A&B->C)->(A->(B->C)) Т7: |-T->A, где Т - тау Т8: |-a&(not a)->T, где Т - тау.
