2. Формальные системы

2.1. Понятие формальной системы

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

В формальной системе (ФС), оперирующей теми или иными символами, эти символы воспринимаются просто как элементы, с которыми обращаются согласно определенным правилам, завися­щим лишь от формы выражений, образованных из символов. Здесь нет понятия истинности, оно появляется лишь в связи с возможны­ми приложениями (интерпретациями) этой системы.

Формальные системы, с которыми мы будем иметь дело, – это аксиоматические системы, т. е. системы с наличием определенного числа исходных заранее выбранных и фиксированных высказыва­ний, называемых аксиомами.

Говорят, что аксиоматическая ФС «проста» и «эффективна». Под «простотой» будем понимать то, что для любой реальной систе­мы, являющейся интерпретацией данной аксиоматической системы, можно обойтись одним и тем же числом исходных допущений, необходимых для получения тех или иных выводов любой системы. Говоря об «эффективности» ФС, следует иметь в виду то, что каж­дый вывод аксиоматической системы может быть автоматически перенесен на любую из ее интерпретаций. Поскольку любая рас­сматриваемая в книге формальная система имеет аксиомы, слово «аксиоматическая» в дальнейшем будет опускаться.

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

Формальная система считается заданной, если выполнены сле­дующие условия.

Задано некоторое множество, состоящее из конечного или бесконечного числа элементов, которые носят название термов. Имеется другое конечное множество, элементы которого есть связки или операции.

Любую линейно упорядоченную совокупность термов и операций¹ будем называть формулой. Из множества формул выделим подмножество правильно построенных формул (ППФ). Для ППФ задаются правила их конструирования, т. е. определяется эффективная процедура, позволяющая по данному выражению выяснить, является ли оно ППФ или нет в данной ФС.

Выделено некоторое множество ППФ, называемых аксиомами ФС. Понятие аксиомы должно быть эффективным, т. е., так же как и для ППФ, должна иметься эффективная процедура, позволяю­щая для произвольной ППФ решить, является ли она аксиомой.

Имеется конечное множество R₁, R₂,…,R_k отношений между ППФ, называемых правилами вывода. Понятие «вывода» также долж­но быть эффективным. Иными словами, должна иметься эффективная процедура, позволяющая для произвольной конечной последователь­ности ППФ решить, может ли каждый член этой последовательности быть выведен из одной или нескольких предшествующих ППФ этой последовательности посредством некоторых фиксированных правил вывода.

Выводом в ФС называется любая последовательность ППФ A₁, A₂, …, А_n такая, что для любого i (1 ≤ i ≤ n) ППФ A_i есть либо аксиома ФС, либо непосредственное следствие каких-либо предыдущих ППФ по одному из правил вывода. ППФ В называется теоремой (или выводимой ППФ) ФС, если существует вывод в ФС, в котором последней ППФ является В. Понятие теоремы не обязательно эффективно, так как, вообще говоря, может и не существовать эффективной процедуры, позволяющей узнавать по дан­ной ППФ существует ли ее вывод в ФС. Формальная система, для которой такая эффективная процедура существует, называется раз­решимой, в противном случае – неразрешимой.

ППФ В выводима из ППФ A₁, A₂, …, А_n (или является следствием множества A₁, A₂, …, А_n) тогда и только тогда, когда существует такая конечная последовательность ППФ B₁, B₂,_, …, B_r, что В_r есть В и для любого i (1 ≤ i ≤ r) В_i есть:

• либо аксиома,

• либо А_i (1 ≤ i ≤ n),

• либо непосредственное следствие некоторых предыдущих ППФ по одному из правил вывода.

Элементы последовательности ППФ A₁, A₂, …, А_n называются посылками вывода (или гипотезами). Сокращенно вывод В из A₁, A₂, …, А_n будем записывать A₁, A₂, …, А_n ├ B , или если Г = {A₁, A₂, …, А_n}, то Г ├ В. Вывод ППФ В без использования посылок есть доказательство ППФ В, а сама В – теорема, что записывается ├ В.

Приведем несколько свойств понятия выводимости из посылок.

1. Если Г  П и Г ├ В, то П ├ В. Это значит, что если ППФ В выводима из множества посылок Г, то она также будет выводима, если к Г добавятся новые посылки.

2. Г ├ В тогда и только тогда, когда в Г существует конечное подмножество П, для которого П ├ В. Это очевидно, исходя из (1).

3. Если П ├ A и Г ├ В для любой ППФ В из множества П, то Г ├ A . Это значит, что если ППФ А выводима из П и каждая содержащаяся в П ППФ выводима из Г, то ППФ А выводима из Г.

Таким образом, любая ФС задается четверкой:

<Т, Н, А, R,

где Т – множество термов и операций; Н – множество правил кон­струирования ППФ; А – система аксиом; R – множество правил вывода.

Пример 2.1. Рассмотрим «неандертальскую» систему счисления. Множество Т состоит из палочек и операций: сложения, приписы­вания одной палочки к другой и равенства.

Правила конструирования ППФ:

1. | есть ППФ;

2. если α – ППФ. то α| также ППФ;

3. если α и β – ППФ, то α + β также ППФ;

4. если α и β – ППФ, то α = β также ППФ;

5. других ППФ нет.

Отсюда

|| … || – ППФ (правило 2);

|| … || + || … || – ППФ (правила 2, 3);

– ППФ (правила 2, 4) (как в случае n ≠ m, так и в случае n = m);

|| … || + || … || = || … || + || … || + … + || … || = || … || … – ППФ (прави­ла 2, 3, 4) и т.д., но + || не есть ППФ, так как нет такого правила образования ППФ.

Система аксиом состоит из одной аксиомы: | = |.

Правила вывода:

1. все аксиомы выводимы, т. е. являются теоремами;

2. если ├ α = β, то ├ α + | = β|;

3. других правил вывода нет.

Найдем множество теорем: | = | – теорема (правило 1);

| + | = || – теорема (правило 2);

– теорема (правило 2),

т. е. теоремой будет любая ППФ, в которой слева и справа от зна­ка равенства стоит одно и то же число палочек.

Теперь рассмотрим расширение формальной системы путем вво­да дополнительных правил на множества H, А и R. Пусть на мно­жество H, задающее синтаксис ФС, действуют некоторые правила η, фиксирующие изменения в правилах H, т. е. правила η изменя­ют синтаксис формальной системы. В системах принятия решений такая задача может рассматриваться, например, как задача пере­вода фактов из одной системы представления знаний в другую.

Далее, пусть в ФС допускается как добавление новых аксиом, так и исключение старых. Это может делаться с помощью некото­рых правил γ, изменяющих систему аксиом А. Эти правила целе­направленно изменяют А, причем нахождение тех из них, которые задают целевые факты, может трактоваться, например, как задача поиска закономерностей мира, в котором функционирует та или иная система принятия решений.

И, наконец, пусть в ФС разрешается изменять набор правил вывода R, что и делается с помощью некоторых правил ρ. Для систем принятия решений проблема изменения правил R может пониматься, например, как задача адаптации данной системы к внешней среде.

Таким образом, полученная семерка

<Т, H, А, R, η, γ, ρ>

будет характеризовать расширение формальной системы, называе­мое семиотической системой. Ее особенность проявляется прежде всего в том, что семиотическая система является открытой, так как множество аксиом А может изменяться с помощью правил γ. Кро­ме того, такая система пригодна как для реализации дедуктивных, так и недедуктивных процессов, а также вследствие ее открытости процессов обучения и адаптации.

Для функционирования семиотической системы необходимо за­дать проблемно ориентированную формальную систему и правила ее изменения. Отметим, что сама формальная система не является ни языком, ни системой знания, она не содержит никаких утверж­дений об объектах, а является просто исчислением – некоторого рода действиями по определенным правилам над последовательно­стями термов.

Мы рассмотрим два класса формальных систем, являющихся ма­тематической базой для построения систем принятия решений: исчис­ление высказываний и исчисление предикатов первого порядка.