Появление формальных систем было обусловлено осознанием того факта, что совершенно различные системы, будь то технические, социальные, экономические или биологические, обладают глубоким сходством.
В формальной системе (ФС), оперирующей теми или иными символами, эти символы воспринимаются просто как элементы, с которыми обращаются согласно определенным правилам, зависящим только от формы выражений, образованных из символов. Понятие истинности появляется только в связи с возможными приложениями (интерпретациями) этой системы.
Формальные системы – это аксиоматические системы, т.е. системы с наличием определенного числа исходных, заранее выбранных и фиксированных высказываний, называемых аксиомами.
Формальную систему называют также аксиоматикой, или формальной теорией, еще проще – множеством формул. Формальная система – это совокупность следующих компонентов:
Ф = < Т, L, Q, R>,
где Т – множество базовых элементов (конечный алфавит), единственное требование к элементам множества Т – для всякого элемента за конечное число шагов можно узнать, принадлежит ли он Т или нет, и отличать одни элементы от других, отождествляя одинаковые элементы;
L – множество синтаксических правил построения слов и формул;
Q – множество выделенных синтаксически правильных образований (аксиом), т. е. Q – априорно выведенные формулы;
R – совокупность процедур – правил вывода одних формул из других.
Формальная система обладает свойством автономности, т.е. если задать ФС, то она самостоятельно начнет генерировать множество выводимых синтаксически правильных совокупностей. Они будут порождаться в результате применения правил вывода к совокупностям из множества Q.
Пример. Формальная система (JP)
Алфавит º {a, b, •}.
Формулы: символ или последовательность символов, или •.
Одна аксиома: a•a.
Одно правило вывода: с1•с2 ® bc1•bc2.
Принято, что в этом правиле вывода символы c1 и с2 означают какие-то последовательности символов а или b и могут быть замещены любыми последовательностями а или b.
Символы c1 и с2 не являются символами данной формальной системы. Они служат посредниками для формализации правил вывода. Здесь а и b называют константами, а •– оператором.
Из определения данной формальной системы непосредственно вытекает следующий способ получения допустимых формул:
a•a;
ba•ab;
bba•abb;
bbba•abbb и т.д.