Понятие формализации

При использовании разговорного языка при передачи знаний от одного человека к другому возможно появление неоднозначностей. В то же время знание требует однозначного восприятия, поэтому ФОРМАЛИЗАЦИЯ – процесс перехода от словесного описания к более точному символьному.

При формализации надо некоторое множество символов, из которых по некоторым правилам составляются слова формального языка, некоторые слова принимаются за исходные (их смысл не может оспариваться), кроме того задается набор правил по которым из одного слова можно получать другое. Многократно применяя эти правила, из одних истин мы получаем другие.

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

Так, в цепочке преобразований (a + b)(a - b) = a(a - b) + b(a - b) = a² - ab + ba - b² = a² - b² использовано:

Во-первых, целый набор равенств, выражающих свойства чисел и операций над ними:

Во-вторых, применен общий принцип подстановки: если выражение содержит в себе другое выражение, а выражение получается заменой на равное ему выражение D, то выражения и равны.

В-третьих, цепочка равенств A=B=C=D представляет сокращенную запись равенств: A = B, B = C, C = D.

В-четвертых, неявно использован еще один принцип: если A = B и B = C, то A = C. Его двукратное применение позволяет придти к равенству: (a + b)(a - b) = a² - b²

Алфавиты, слова, языки

Формальные теории, не пользуясь естественным (разговорным) языком, нуждаются в собственном формальном языке, на котором записываются встречающиеся в нем выражения. Опишем используемые для этого средства:

Алфавит - конечное множество A = {a1, a2, ..., an}, элементы которого называются буквами или символами.

Слово в алфавите - любая конечная последовательность символов α=b₁b₂b₃...b_k, где b_i €A, для i = 1...k. Слово может состоять только из одной буквы, а может вообще не содержать букв, тогда оно называется пустым и обозначается λ(Е). Число букв в слове ' называется его длиной и обозначается | λ |. В частности, | λ |= 0.

Множество всех слов в алфавите A, включая пустое слово, обозначается A*. Любое подмножество множества A*. называется языком в алфавите A, а совокупность правил, позволяющих установить принадлежность слова языку, - грамматикой этого языка. Иногда такую грамматику называют распознающей, в отличие от порождающей грамматики, позволяющей выписывать произвольные слова данного языка и только их. Порождение и распознавание должно осуществляться эффективно, то есть за конечное и небольшое число шагов.

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

Т:

1. А={a,b}

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

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

4. 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)

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