Математическая логика и теория алгоритмов

каждого множестйа, состоящего из к формул, и каждой формулы Л эффективно решается вопрос о том, является пи А непосредственным следствием данных к формул по правилу R,. Выводом в В называется всякая последовательность Л ь формул, такая что для каждого i (1< i < п) формула^, есть либо ак­ сиома теории В , либо непосредственное следствие каких-либо преды­ дущих формул этой последовательности по одному из правил вывода. Формула А теории В называется теоремой теории В , если существует вывод в 8 , в котором последней формулой является А , такой вывод называется выводом формулы^. Формула А называется,следсотемелг в В множества формул G тогда и только тогда, когда существует такая последовательность формул Ai, А2,..., A f „ что А„=А и для любого i Ai есть либо аксиома, либо элемент G , либо непосредственное следствие некоторых преды­ дущих формул этой последовательности по одному из правил вывода. Такая последовательность называется выводом А из G. Элементы G называются гипотезами или посылкамивывода. Для сокращения утверждения «А есть следствие G » будем употреблять запись: G \-А. Например, если то будем писать В\,Въ...,Вт \-А. Нетрудно видеть, что если G есть пустое множество, т. е. G =0 , то 0 \- А имеет место тогда и только тогда, когда А является теоре­ мой. Вместо 0 \-А принято писать просто \- А, что читается; «фор­ мула А является теоремой». Чтобы избежать путаницы там, где будут рассматриваться не одна, а несколько теорий, употребляют запись; G \-А и \-А, В В указывая индексом В на то, о какой теории идет речь. § 6. Свойства выводимости Пусть G - некоторое множество формул данной теории. А, В и С - произвольные формулы той же теории. Рассмотрим некоторые свойства выводимости в формальных аксиоматических теориях. 147