Математическая логика и теория алгоритмов. Стенюшкина В.А. - 18 стр.

       4 Формальные теории

       4.1 Определение формальной теории

       Формальная теория (ФТ) - это четверка Т = (S, F, А, R) /2/,
       где S - алфавит - множество символов;
       F - множество формул - множество правильно построенных цепочек
символов из S;
       А - множество аксиом подмножество множества F;
       R - множество правил вывода - множество отношений ρ на множестве F.
       Множество S может быть конечным или бесконечным. Множество F
чаще всего бесконечно, задается синтаксическими правилами. S и F в совокуп-
ности определяют язык формальной теории. Множество А может быть конеч-
ным или бесконечным; если бесконечно, то задается схемами и правилами их
конкретизации. Множество R обычно конечно; будет предполагаться, что
ρ ⊂ F n+1 (при некотором n) , где Fn+1 - (n+1)-ая декартова степень множества F.

       4.2 Выводимость. Разрешимость

       Пусть F1, ..., Fn, G- формула формальной теории Т, то есть F1,..., Fn,G∈F и
пусть имеется правило ρ ∈ R такое, что (F1, …, Fn, G) ∈ ρ . Тогда формула G
называется непосредственно выводимой из формул F1, ..., Fn по правилу ρ.
                 F ,..., Fn
       Запись: 1            ρ , при этом формулы F1, ...., Fn называются посылками,
                    G
а формула G - заключением.
       Формула G называется выводимой из формул F1, ..., Fn, в формальной те-
ории Т, если существует последовательность формул Е1 , ...., Ek такая, что Еk=
G, а любая из Еi, i = 1 ...(k - 1), есть либо аксиома, либо одна из исходных фор-
мул F1,...,Fn, либо непосредственно выводима из подмножества ранее получен-
ных формул Ej1,…, Ej1, j1,...,jl < i. Последовательность Е1, ...., Еk называется при
этом выводом формулы G из формул F1, ... , Fn в теории Т.
       Запись: F1, ...,Fn |−…G; формулы F1, ..., Fn, называются гипотезами, фор-
мула G - тезисом. Знак теории Т можно опускать.
       Формула, выводимая только из аксиом, называется теоремой теории Т.
       Запись: |− G (множество гипотез пусто).
       При добавлении гипотез выводимость сохраняется, то есть если Г («га-
мма») и ∆ («дельта») - множества формул, причем Г|− TG, то есть Г, ∆ |− T G.
       Примечание - По отношению к теоремам формальной теории теоремы о
формальной теории называются метатеоремами.
       Формальная теория называется разрешимой, если существует алгоритм,
который для любой формулы определяет, является или нет эта формула теоре-
мой теории.
       Формальная теория называется полуразрешимой, если существует алго-
ритм, который для любой теоремы дает ответ «да», а для формулы, не являю-