Выводимость

Пусть F₁,..., F_n, G — формулы теории T, то есть F₁,..., F_n, G F. Если существует такое правило вывода R, R R, что (F₁,..., F_n, G) R, то говорят, что формула G непосредственно выводима из формул F₁,..., F_n по правилу вывода R. Обычно этот факт записывают следующим образом:

где формулы F₁,..., F_n называются посылками, а фор­мула G — заключением.

Обозначение правила вывода справа от черты, разделяющей посылки и заключение, часто опус­кают, если оно ясно из контекста.

Выводом формулы G из формул F₁,..., F_n в формальной теории T называется такая последователь­ность формул E₁,...,E_k, что Е_k = G, а любая формула Е_i (i < k) является либо аксиомой (E_i B), либо исходной формулой F_j (Е_i = F_j), либо непосредственно выводима из ранее полученных формул . Если в теории T существует вывод формулы G из формул F₁,..., F_n, то это записывают следующим образом:

_{├ T} G,

где формулы F₁,..., F_n называются гипотезами вывода. Если теория T подразумевается, то ее обо­значение обычно опускают. Приведем простейшие правила выводимости.

Если _{├ T} G, то формула G называется теоремой теории T (то есть теорема — это формула, выво­димая только из аксиом, без гипотез).

Если Г _{├ T} G, то Г, _{├ T} G, где Г и — любые множества формул (то есть пpи добавлении лишних гипотез выводимость сохраняется).

Г, А _{├ T} А. Действительно, вывод формулы А из системы гипотез Г, А состоит из одной формулы.

Если Г, А, В _{├ T} G, то Г, В,А _{├ T} G.

Если Г _{├ T} А, Г _{├ T} В и А, В _{├ T} С, то Г _{├ T} С. Действительно, пусть А ₁,…,А_n – вывод формулы А из Г; В ₁,…,В_m – вывод формулы В из Г, С ₁,…,С_k - вывод формулы С из А, В. Тогда очевидно, что А ₁,…,А_n, В ₁,…,В_m, С ₁,…,С_k есть вывод формулы С из Г.

Если Г, А _{├ T} В и Г _{├ T} А, то Г _{├ T} В (правило удаления выводимой гипотезы). Пусть В ₁,…,В_n – вывод формулы В из Г, А. Если в этом выводе не встречается формула А, то имеем вывод В из Г, если в этом выводе встречается формула А, то пусть В _i1,…,В_ik – все вхождения формулы А в вывод. Пусть также А ₁,…,А_m – вывод А из Г. Тогда B₁,…,В_i1-1,А ₁,…,А_m,B_i1+1,…,B_i2-1,А ₁,…,А_m, B_i2+1,…,B_ik-1,А ₁,…,А_m,B_ik+1,…,B_m - вывод формулы В из Г.

При изучении формальных теорий нужно различать теоремы формальной теории и теоремы о формальной теории или метатеоремы. Это различие не всегда явно формализуется, но всегда яв­ляется существенным. В этой главе теоремы конкретной формальной теории, как правило, записы­ваются в виде формул, составленных из специальных знаков, а мета теоремы формулируются на естественном языке, чтобы их легче было отличать от теорем самой формальной теории.