Спирина, М.С. Дискретная математика

ствами. Это отношение назовем правилом вывода. Если пара (/, g), ГДе / = ( / i , / 2, е Fn, a g e F, принадлежит R (т.е. (/", g) е R или f R g), то формула g называется непосредственным следствием фор­ мул f , f i , ■■■,/„ или непосредственно выводимым выражением из формул / ь / 2, полученным по правилу вывода R. Основным требованием считается конечность правил вывода: совокупность от­ ношений {/?ь R2, ..., Rk}, которую далее будем обозначать R, долж­ на быть конечной. Если существует R, е R, такое, что ({/j,/2, ..., f„), g) е Rh то g называется непосредственным следствием формул / ь / 2, ..., /„ безотносительно к одному определенному правилу f f f вывода. Обозначение как J , f 2, ■■■,f„\=g или % g 4. Во множестве формул F выделим подмножество Р с F, эле­ менты которого назовем аксиомами теории. Выбор этого подмно­ жества опять же произволен: это те формулы, которые условно можно считать априорно истинными, т.е. истинными изначально и безоговорочно. Условность заключается прежде всего в том, что мы пока не определили понятие «истинный». В алгебре логики ему соответствовало значение «1» булевой функции или переменной, здесь же речь идет о произвольных алфавитах, не обязательно со ­ держащих букву «1». Обычно стремятся к тому, чтобы число акси­ ом было по возможности наименьшим. Но может получиться так, что каждая аксиома из меньшего числа будет менее априорно понятной. Например, в подразд. 4.8 было показано, что все буле­ вы функции можно описать с помощью одной функции, напри­ мер штриха Шеффера. Но нам интуитивно ближе операции отри­ цание, конъюнкция и дизъюнкция в качестве базовых, так как они опираются на повседневный человеческий опыт и имеют аналогию в теории множеств. 5. Формула h называется выводимой из формул {/ь / 2, ...,/„} = Ф или следствием формул Ф, если существует кортеж формул (gb g2, ..., gp) е Fp, такой, что gp = h и V/ < р g, е РиФ 11 Gh где G, = = {g IФ, gx, g2, g,_ i |= g}. Каждая формула в этой цепочке являет­ ся или аксиомой, или исходной формулой, или непосредственно выводимой из предыдущих. Тогда кортеж (gu g2, ..., gp) называется выводом, или доказательством, формулы И, а набор { f \ , f2, ...,/„} — гипотезами, или посылками, что обозначается как Ф \— И или / , , / 2, ...,/„ \—И. Обращаем внимание, что аксиомы всегда подразуме­ ваются в качестве посылок, поэтому как гипотезы в явном виде они не пишутся. Очевидно, что если Ф (= И, то Ф |— И. 6. Если Ф = 0 и Ф |— И, т. е. формула является следствием только аксиом, то И называется теоремой. Вместо записи 0 |— /г обычно используют (— А. Очевидно, что каждый элемент g,, g2, ..., gp вы­ вода теоремы И также является теоремой. 7. Заданные алфавит, множество формул, аксиомы и правила вывода, т.е. совокупность Т ={A, F, Р, R), называются формальной 8* 211