План лекций (очень подробный), страница 3

Кванторы:

aai+ |- a.vf => |- (svw)f w - новая константа

ase- a.vf => (svt)f t - терм, свободный для v

eai- |- e.vf => їe.vf |- (svt)f в формуле f

esi- f => e.v (stv)f

ПОИСК НАТУРАЛЬНОГО ВЫВОДА формулы a.

Основная идея: начиная с |- a, по обе стороны от знака |- добав-

ляем формулы (в соответствии с правилами поиска вывода) до тех пор,

пока не получится фрагмент a1,...,an |- an,an+1,...,am, который можно

заменить на вывод a1,...,an,an+1,...,am.

Правила поиска вывода делятся на аналитические (в названии кото-

рых встречается буква a) и синтетические (с буквой s). Синтетическое

правило имеет вид b1,...,bn => b ( n>=1, в записи нет знака |-). Пра-

вило применимо в том случае, когда в строящемся выводе слева от |-

есть формулы b1,...,bn (возможно, не подряд и в другом порядке). Ре-

зультатом его применения является добавление формулы b слева от |- (в

вертикальной записи - выше |-). Все остальное остается без изменений.

Аналитическое правило имеет вид b1,...,bn |-c => d1 |-e1 /... /

dm |-em (n>=0, m>=1). В результате его применения на месте "старого"

знака |- возникают подвыводы d1|-e1,...,dm|-em. В дальнейшем каждый из

------ ------

них достраивается отдельно (причем все формулы из объемлющих подвыво-

дов, стоящие выше |-, считаются доступными в текущем подвыводе). Вывод

считается построеным, если построены все его подвыводы.

$3. Исчисление секвенций (g-исчисление).

Формула, выводимая в натуральном исчислении, по определению, не

зависит ни от каких гипотез, что означает возможность ее доказательст-

ва безо всяких дополнительных предположений (например, аксиом ка-

кой-либо математической теории, а это значит, что: такая формула дока-

зуема во всех таких теориях). Содержательно это напоминает понятие об-

щезначимости, но формально связь n-выводимости и общезначимости пока

не установлена. Для ее установления введем еще одно исчисление - сек-

венциальное, связанное, с одной стороны, с понятием истинности, а с

другой - с исчислением натурального вывода. Секвенция - это конструк-

ция a1,...,an -> b1,...,bm (n,m>=0, ai, bj - формулы), содержательно

понимаемая как "из a1,...,an следует хотя бы одно из утверждений

b1,...,bm". Списки формул a1,...,an и b1,...,bm считаются неупорядо-

ченными (т.е. a,b->c,d означает то же самое, что и b,a->d,c). Формула

a выводима в секвенциальном исчислении (|-g a), если можно по правилам

g-вывода построить вывод из g-аксиом секвенции ->a. Правила g-вывода

таковы, что поиск вывода в этом исчислении можно осуществлять конт-

рприменениями (применениями снизу вверх) правил вывода. Такой поиск

вывода можно, в частности, рассматривать как попытку построения конт-

рпримера для формулы a (анализируем структуру формулы a, и либо нахо-

дим контрпример, либо убеждаемся, что его невозможно построить; пос-

леднее наблюдается, когда все ветви вывода заканчиваются аксиомами,

т.е. формула a является g-выводимой).

Пусть f1 и f2 - формулы, а l и r - списки формул.

Аксиома СЕКВЕНЦИАЛЬНОГО ВЫВОДА: f1,l -> r,f1.

Правила СЕКВЕНЦИАЛЬНОГО ВЫВОДА.

Конъюнкция:

f1,f2,l->r l->r,f1 l->r,f2

(&<-) ---------- (->&) -----------------

f1&f2,l->r l->r,f1&f2

Дизъюнкция:

f1,l->r f2,l->r l->r,f1,f2

(v<-) ----------------- (->v) ----------

f1vf2,l->r l->r,f1vf2

Импликация:

l->r,f1 f2,l->r f1,l->r,f2

(><-) ----------------- (->>) ----------

f1>f2,l->r l->r,f1>f2

Отрицание:

l->r,f1 f1,l->r

(ї<-) -------- (->ї) --------

їf1,l->r l->r,їf1

Кванторы:

a.vf1,(svt)f1,l->r l->r,(svw)f1

(a<-) ------------------ (->a) ------------

a.vf1,l->r l->r,a.vf1

(svw)f1,l->r l->r,(svt)f1,e.vf1

(e<-) ------------ (->e) ------------------

e.vf1,l->r l->r,e.vf1

Обозначения:

w - константа, не встречающаяся в заключениях правил ->a и e<-;

t - терм, свободный для v в f1;

(Правила ->a и e<- называются положительными, a a<- и ->e - отрица-

тельными кванторными правилами.)

---------------------------------------- ------------------------------------

Если рассматривать поиск вывода формулы как метод установления ее

общезначимости, то возникает вопрос о корректности (правильности) это-

го метода: верно ли, что если вывод построен (т.е. на вопрос "общезна-

чима ли формула?" метод дает ответ "да"), то формула действительно об-

щезначима? Поэтому логическое исчисление называется корректным, если в

нем выводимы только общезначимые формулы (выводимость влечет общезна-

чимость).

Т3. Исчисление g корректно (|-g a => |=a). Д.: по определению,

секвенция a1,...,an->b1,...,bm общезначима, если общезначима соответс-

твующая ей формула a1&...&an>b1v...vbm; аксиома общезначима; примене-

ния (сверху вниз) правил вывода сохраняют общезначимость (для каждого

правила можно показать, что если его заключение имеет контрпример, то

хотя бы одна из посылок имеет конрпример).

Метод установления общезначимости можно считать полным, если он

дает ответ "формула общезначима" про каждую общезначимую формулу. Поэ-

тому исчисление называется полным, если в нем выводимы все общезначи-

мые формулы (общезначимость влечет выводимость).

В исчислении g следующим образом описывается систематический ме-

тод поиска вывода, позволяющий построить (может быть, бесконечное) де-

рево, нагруженное секвенциями, которое либо является выводом, либо

позволяет описать контрпример: 0) исходный фрагмент вывода есть дере-

во, состоящее из единственной вершины, которой приписана выводимая

секвенция (эта вершина - одновременно и корневая, и висячая); 1) если

в построенном фрагменте вывода нет никаких пометок на формулах, то от-

метим все неатомарные формулы, расположенные в висячих вершинах дерева

(если таких формул нет - построение закончено); 2) если в дереве есть

хотя бы одна помеченная формула, то применим (снизу вверх) подходящее

правило вывода к самой левой из таких формул; если рассматриваемая по-

меченная формула есть формула с квантором qx a, к которой применимо

отрицательное кванторное правило (требующее замены в формуле a пере-

менной x на некоторый терм), то сопоставим формуле a множество w всех

таких термов без переменных, какие присутствуют (в качестве аргументов

предикатов или подтермов других термов) в ветви дерева от корня до

рассматриваемой висячей вершины, но нигде ниже не подставлялись в фор-