Абстрактные формальные системы
Абстрактная формальная система – это
Алфавит А( множество слов в этом алфавите – А*).
Разрешимое множество А1 Í А*, элементы множества А1 называют аксиомами.
Конечное множество вычислимых отношений Ri (a1, …, an, b)на множестве A*,называемых правилами вывода. Говорят, что слово bвыводимо из слов a1, …, an по правилу Ri.
Аксиомы тоже могут быть заданы как унарные отношения, но это не всегда удобно.
Выводимость. Вывод формулы В из формул A1, A2, … , An - последовательность формул F1, F2, … , Fm = B, такая, что Fi (i=1,…m) либо аксиома, либо одна из формул A1, A2, … , An, либо непосредственно выводима из F1, F2, … , Fi-1 по одному из правил вывода. Если существует вывод формулы В из формул A1, A2, … , An, то В выводима из A1, A2, … , An . Множество формул, выводимых из аксиом, называется теоремами теории.
Теорема. Для любой формальной теории множество выводимых в ней слов перечислимо.
Док-во:
А** - множество всех конечных последовательностей a1, …, an,где ai- слова в алфавите А. А** - перечислимо. Из-за разрешимости множества аксиом и вычислимости правил вывода по любой последовательности можно эффективно узнать, является ли она выводом в данной формальной системе (FS).
Если в процессе перечисления А** отбрасывать все последовательности, не являющиеся выводами, то получаем перечисление множества выводов Þ последних слов выводов.
Þ множество слов (формул), выводимых в произвольной формальной системе, перечислимо.
Примеры формальных систем: системы продукций Поста (канонические системы), системы подстановок, формальные грамматики, исчисления и т.д.
Каноническая система <A, X, M, R>
A= {a1,a2,…, an} – алфавит констант,
X= {x1, x2,…,xm} – алфавит переменных,
M= {M1, M2, …, Mk} – множество аксиом, MiÎ(AÈX)*,
R = {R1, R2, …, Rl} – множество продукций, имеющих вид
g1, g2,…, gjÞd, gi, dÎ(AÈX)*, g1, g2,…,gj называются посылками, d - следствием.
Слова в (AÈX)* называются термами, слова в А* - просто словами.
Слово a называется применением аксиомы w, если a получается из w подстановкой слов вместо переменных.
Слово a непосредственно выводимо из a1, …, an применением продукции R , если существует подстановка слов вместо переменных в продукцию R, которая посылки превратит в a1, …, an, а заключение – в a.
Например, из acb , cabb применением продукции a x1 b, x1 b x2 Þ b x2 (подстановка x1=ca, x2=b) непосредственно выводимо bb.
Выводимость – транзитивное и рефлексивное замыкание непосредственной выводимости.
Доказуемо (теорема формальной системы ) - выводимо из множества аксиом.
Например, <{I}, {x}, {I}, {xÞx I I}> позволяет построить множество нечетных чисел в унарном представлении.
Теорема. Для любого перечислимого множества М слов в алфавите А существует каконическая система над А, множество теорем которой совпадает с М.
(доказательство, с использованием МТ, приводится в [3])