5. Формальные теории: определение, построение.

Формальная теория T - это:

1.множество A символов, образующих алфавит A и множество слов A*;

2.множество F слов в алфавите A, F A*, которые называются формулами;

3.подмножество B формул, B F, которые называются аксиомами;

4.множество R отношений на множестве формул, которые называются правилами вывода.

Множество символов A, как правило, конечно. Обычно, для образования символов используют буквы, к которым приписывают в качестве индексов натуральные числа. Множество формул F обычно задается индуктивным определением, например, с помощью формальной грамматики. Как правило, это множество бесконечно. Множества A и F в совокупности определяют язык или сигнатуру формальной теории. Множество аксиом B может быть конечным или бесконечным. Если множество аксиом бесконечно, то оно задается с помощью конечного множества схем аксиом и правил порождения. Множество правил вывода R, как правило, конечно.

6. Вывод в формальной теории. Интерпретация, полнота и непротиворечивость формальной теории.

Пусть F1, F2, . . . , Fm,G - формулы теории T , то есть F1, F2, . . . , Fm,G F. Если существует такое правило вывода R,R R, что (F1, F2, . . . Fm,G) R, то говорят, что формула G непосредственно выводима из формул F1, F2, . . . , Fm по правилу вывода R. Символически это записывается следующим

образом:

((F1, F2, . . . , Fm)/G)*R.Если мы можем указать в каком отношении формула G относится к F1, F2, . . . , Fm, то она находится по правилу R. F1=a; F2=b;

G=a+b ; R=F1F2/F1+F2.

Вывод (выводимость)-Выводом формулы G набора формул F1, F2, . . . , Fm в формальной теории (ФТ) называется такая последовательность формул E1,E2, . . . ,Ek, что Ek = G, а любая формула Ei, (i < k) является либо аксиомой (Ei B), либо исходной формулой Fj(Ei = Fj), либо непосредственно выводима из ранее полученных формул. Если в теории T существует вывод формулы G из F1, F2, . . . , Fm, то это записывается, как F1, F2, . . . , Fm `T G где формулы F1, F2, . . . , Fm называются гипотезами вывода. Формула G формальной теории T называется выводимой, если существует ее вывод в теории T . Утверждение, что формула G выводима в теории T , то есть является ее теоремой, кратко записывается в виде: `T G.

Пример1: Построить (ФТ) Т с алфавитом из 2 букв А и Б каждая из которых является палиндромом. Построить вывод формулы G=ababaababa

Т:

А={a,b}

F- палиндромом.

B1=a, B2=b, B3=aa, B4=bb

R1=F/(aFa), R2=F/(bFb).

Вывод: F1= aa(B3)

F2=baab(F1,R2)

F3=abaaba(F2,R1)

F4=babaabab(F3,R2)

F5=ababaababa(F4,R1)

Другими словами аксиома представляет собой формулу выводимую из пустого множества.

Пример2:Построить (ФТ) Т с алфавитом x,y,+,-,(,),каждая формула которая представляет собой правильно построенное алгебраическое выражение. Построить вывод формулы G=((x+y)-(y-x)) в (ФТ) Т.

1)Ā={x,y,+,-,(,)}

2)F-…

3)B1=x, B2=y

4)R1=F1F2/F1+F2, R2=F1F2/F1-F2

Вывод:

F1=x(B1)

F2=y(B2)

F3=(x+y)(F1,F2,R1)

F4=(y-x)(F2,F1,R2)

F5=((x+y)-(y-x))(F3,F4,R2)

Любая формула полученная в рамках нашей теории будет являться правильной согласно алгебре. Неправильно построенная формула не будет принадлежать теории, потому-что не существует еѐ вывода в рамках теории.

Интерпретация формальной теории

Интерпретацией формальной теории T в область интерпретации называется функция I, которая каждой формуле формальной теории однозначно сопоставляет некоторое содержательное высказывание относительно объектов множества. Это высказывание может быть истинным или ложным. Если высказывание является истинным, то говорят, что формула выполняется в данной интерпретации. Интерпретация I называется моделью множества формул, если все формулы этого множества выполняются в интерпретации I. Интерпретация I называется моделью формальной теории T , если все формулы этой теории выполняются в интерпретации I (то есть все выводимые формулы оказываются истинными в данной интерпретации).

Общезначимость и непротиворечивость

Формула называется общезначимой(или тавтологией), если она истинна в любой интерпретации. Формула называется противоречивой, если она ложна в любой интерпретации. Формула G называется логическим следствием множества формул,

если G выполняется в любой модели. Формальная теория T называется семантически непротиворечивой, если ни одна ее теорема не является противоречием.

Таким образом, формальная теория пригодна для описания тех множеств, которые являются ее моделями.

Модель для формальной теории T существует тогда и только тогда, когда T

семантически непротиворечива. Формальная теория T называется формально непротиворечивой, если в ней не являются выводимыми одновременно формулы FךF. Теория T формально непротиворечива тогда и только тогда, когда она семантически непротиворечива