Абстрактные формальные системы

Абстрактная формальная система – это

Алфавит А (множество слов в этом алфавите – А*).

Разрешимое множество А₁ Í А*, элементы множества А₁ называют аксиомами.

Конечное множество вычислимых отношений R_i (a₁, …, a_n, b) на множестве A*, называемых правилами вывода. Говорят, что слово b выводимо из слов a₁, …, a_n по правилу R_i.

Аксиомы тоже могут быть заданы как унарные отношения, но это не всегда удобно.

Выводимость. Вывод формулы В из формул A₁, A₂, …, A_n - последовательность формул F₁, F₂, …, F_m = B, такая, что F_i (i=1,…m) либо аксиома, либо одна из формул A₁, A₂, …, A_n, либо непосредственно выводима из F₁, F₂, …, F_i-1 по одному из правил вывода. Если существует вывод формулы В из формул A₁, A₂, …, A_n, то В выводима из A₁, A₂, …, A_n. Множество формул, выводимых из аксиом, называется теоремами теории.

Теорема. Для любой формальной теории множество выводимых в ней слов перечислимо.

Док- во:

А** - множество всех конечных последовательностей a₁, …, a_n, где a_i - слова в алфавите А. А** - перечислимо. Из-за разрешимости множества аксиом и вычислимости правил вывода по любой последовательности можно эффективно узнать, является ли она выводом в данной формальной системе (FS).

Если в процессе перечисления А** отбрасывать все последовательности, не являющиеся выводами, то получаем перечисление множества выводов Þ последних слов выводов.

Þ множество слов (формул), выводимых в произвольной формальной системе, перечислимо.

Примеры формальных систем: системы продукций Поста (канонические системы), системы подстановок, формальные грамматики, исчисления и т.д.

Каноническая система <A, X, M, R>

A= {a₁,a₂,…, a_n} – алфавит констант,

X= {x₁, x₂,…,x_m} – алфавит переменных,

M= {M₁, M₂, …, M_k} – множество аксиом, M_iÎ(AÈX)*,

R = {R₁, R₂, …, R_l} – множество продукций, имеющих вид

g₁, g₂,…, g_jÞd, g_i, dÎ(AÈX)*, g₁, g₂,…,g_j называются посылками, d - следствием.

Слова в (AÈX)* называются термами, слова в А* - просто словами.

Слово a называется применением аксиомы w, если a получается из w подстановкой слов вместо переменных.

Слово a непосредственно выводимо из a₁, …, a_n применением продукции R, если существует подстановка слов вместо переменных в продукцию R, которая посылки превратит в a₁, …, a_n, а заключение – в a.

Например, из acb, cabb применением продукции a x₁ b, x₁ b x₂ Þ b x₂ (подстановка x₁=ca, x₂=b) непосредственно выводимо bb.

Выводимость – транзитивное и рефлексивное замыкание непосредственной выводимости.

Доказуемо (теорема формальной системы) - выводимо из множества аксиом.

Например, <{I}, {x}, {I}, {xÞx I I}> позволяет построить множество нечетных чисел в унарном представлении.

Теорема. Для любого перечислимого множества М слов в алфавите А существует каконическая система над А, множество теорем которой совпадает с М.

(доказательство, с использованием МТ, приводится в [3])