Формальные системы (общая теория систем)
Формальная система состоит из:
1) алфавита (перечисление некоторых символов);
2) синтаксиса (перечисление некоторых правил построения слов (формул) с использованием символов алфавита);
3) аксиоматика (некоторое количество слов (формул, аксимом – это синонимы));
4) некоторое продукционных правил.
Под формальной системой будем понимать неинтерпретированное исчисление, подразумевающее разделение символьных последовательностей на классы нетеорем и теорем.
Под исчислением будем понимать формальный аппарат использования знаков, посредством однозначных правил, дающий возможность точно описать классы задач.
Также под формальной системой можно понимать некоторое количество абстрактных символов (объектов) и правила оперирования этими символами (объектами) абстрагируясь от их смысла.
Под формальным языком будем понимать язык состоящий из алфавита и синтаксиса.
Под языком будем понимать алфавит, синтаксис и класс интерпретации слов (формул).
Если какой язык используется для описания другого языка, то этот используемый язык называют метаязыком для языка в описании которого он участвует.
Если язык имеет общий алфавит и синтаксис с формальной системой, то метаязык этого языка будет метаязыком формальной системы.
Теоремой может являться аксиома либо результат использования продукционного правила к некоторым теоремам.
Под доказательством будем понимать граф-дерево имеющее корневую вершину соответствующую формуле, терминальные вершины соответствуют аксиомам, дуги граф-дерева соответствуют продукционным правилам.
Формулу считают теоремой, только если для нее есть доказательство.
Под формальной теорией будем понимать множество теорем формальной системы.
Теорем может быть бесконечное количество.
При существовании доказательство верно то, что существует алгоритм, построения доказательство, с использованием конечного количества шагов. Верно и обратное отверждение, т.е. если формула не теорема, то не существует и алгоритма доказательства, что формула не является теоремой.
Однако, например при конечности количества слов, возможно существование алгоритмов рекурсивного перечисления нетеорем.

Автор к.п.н., магистр психологии Румянцев Сергей Александрович