Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

4. Задано конечное число правил вывода Ri, R2,..., Rn, согласно каждом которых некоторая формула, именуемая непосредственным следствием (заключением), непосредственно выводима из некоторого конечного множества формул, называемых посылками. При этом для каждого Ri существует целое положительное к такое, что для каждого множества, состоящего из к формул, и каждой формулы А эффективно решается вопрос о том, является ли А непосредственным следствием данных к формул по правилу Ri. Выводом в В называется всякая последовательность Ai, А2,...^п формул, такая, что для каждого i (l<i <п) формула^/ есть либо аксиома теории В, либо непосредственное следствие каких-либо предыдущих формул этой последовательности по одному из правил вывода. Формула А теории В называется теоремой теории в, если существует вывод в Б, в котором последней формулой является А, такой вывод называется выводом формулы^. Формула А называется следствием множества формул G тогда и только тогда, когда существует такая последовательность формул Ai, А2,..., An, что Ап=А и для любого i Ai есть либо аксиома, либо элемент G, либо непосредственное следствие некоторых предыдущих формул этой последовательности по одному из правил вывода. Такая последовательность называется выводом А из G. Элементы G называются гипотезами или посылками вывода. Для сокращения утверждения <А есть следствие G » будем употреблять запись: G\-A . Например, если G={Bi,B2,...Bn], то будем писать Bi,B2,...,B „ \- А. Нетрудно видеть, что если G есть пустое множество, т. е. G =0, то 0 - А имеет место тогда и только тогда, когда А является теоремой. Вместо 0 - А принято писать просто М' что читается: «формула^ является теоремой». Приведённая формальная аксиоматическая теория называют исчислением гилъбертовского типа по имени Гильберта, который использовал подобные исчисления в своей программе формального построения математики. Существуют и другие варианты построения формальных теорий (исчилений), одну из которых мы рассмотрим в § 17-18 данной главы. § 6. Свойства выводимости Пусть G - некоторое множество формул данной теории, ^4, 5 и С - произвольные формулы той же теории. Рассмотрим некоторые свойства выводимости в формальных аксиоматических теориях. 1. Если G содержится в некотором множестве формул F и если G |-^, то F \-А. Доказательство. Пусть А имеет вывод 107