Формальные системы (ФС)

Формальная система суть исчисление, где выделено подмножество формул (слов), которое объявлено изначально выводимым. Эти формулы называются аксиомами. FS = (PPF,PPFA,PV), где

1. PPF – правильно построенные формулы в алфавите A,

2. PPF ∈ A_*, A_* – множество слов, построенное в алфавите A,

3. PPFA ⊂ {PPF} – аксиомы являются подмножеством PPF,

4. PV – правила вида (PPF₁,..., PPF_k) → PPF, что означает, из совокупности PPF выводима PPF. В любой ФС множество формул PPFA выводятся из PPFA с помощью правил PV. При этом {PPFV}⊆{PPF}– называются выводимыми формулами.

Например, исчисление высказываний является формальной системой, где PPF являются формулы, построенные из имён переменных, знаков операций (∧ –конъюнкция, ∨– дизъюнкция, ˥ – отрицание, →– импликация) и скобок. Выделяются PPF, которые объявляются аксиомами и единственное правило вывода «modus ponens» (термин средневековой логики, обозначающий правило вывода и соответствующий ему логический закон.). В исчислении высказываний порождаются только такие PPF, которые могут интерпретироваться как тождественно истинные формулы (тавтологии) и только они.

Формальные грамматики (ФГ)

Исчисление в виде ФС предложено американским математиком Хомским (1953г.) сначала для решения проблем структурной лингвистики, а далее описания формальных языков программирования. FG =〈A,V,S,P〉, где A = {a,b,c,...} – терминальный алфавит, V = {A, B,...,S} – вспомогательный алфавит, S – единственная аксиома, P – правила вида S → x и y → z, где x, y, z ∈ { A∪V }_*.

ФГ порождает характерный язык в виде подмножества слов L ⊂ {A}_*. Правила ФГ не содержат никаких ограничений на рекурсивность подстановок.