Понятие формальной системы.
ФС- способ описания предметной области.
Для описания предметной области вводится понятие формальной системы.
Определение:
Формальная система — синтаксический объект, который состоит из нескольких частей:
на примере ФС «Секвенциальный вариант конструктивного исчисления предикатов» (СКИП).
Конечный алфавит.
А = {P, Q, R, x, y, z, (,), f, g, h, &, Ú, 
, É, 
, ", $, ®, c, d, e}
P, Q, R – для записи элементарных предикатов
x, y, z – для записи объектных переменных
f, g, h – для записи символов функций
c, d, e – для записи объектных констант
В общем виде А = {a1, …, an} – конечное множество символов.
*(В каждой системе алфавит задается свой).
Синтаксическое определение правильно построенных выражений.
В формальных системах требуется, чтобы правильные выражения были четко определены (синтаксически).
В СКИП определяются выражения трёх типов: термы, формулы и секвенции.
Определение:
Терм.
а) Любая объектная переменная и любая объектная константа есть терм,
б) Пусть f(n) – некоторый n–местный, функциональный символ,
t1 ,…, tn – произвольные термы,
тогда f(t1 ,…, tn) – терм.
в) Никаких других термов (кроме термов, построенных по пунктам а) и б) не существует).
Определение носит синтаксический характер.
Пример:
x, y, c - термы
f () – не терм
f(h(x), f(x, y)) – терм.
Определение:
Формула.
а) Пусть P(n) – произвольный n–местный предикатный символ,
t1 ,…, tn – произвольные термы,
тогда P(t1 ,…, tn) является (элементарной) формулой.
б) Пусть F1 и F2 –формулы,
тогда (F1 & F2), (F1 Ú F2), (F1 É F2), (F1 
F2), (F1 
F2), ( F1), (ØF2) тоже являются формулами.
в) Пусть F формула,
x – произвольная объектная переменная,
тогда выражения ("x F(x)), ($x F(x)) тоже являются формулами.
г) Никаких других формул (кроме формул, построенных по пунктам а), б), в)) не существует.
Определение имеет синтаксический характер.
Вводится приоритет операций, который позволяет исключить скобки.
", $, Ø, &, Ú, É, 
Пример:
P É (Q É P & ØR) – правильно построенное выражение - формула.
Определение:
Секвенция:
Пусть F1,…, Fn, G произвольные формулы, тогда F1,…, Fn ® G называется секвенцией.
При этом n может быть равным 0 и G может быть пустой формулой.
В СКИП в правой части секвенции не может быть больше одной формулы.
…®… – пустая секвенция.
Антецедент –левая часть секвенции (допущения).
Сукцедент – правая часть секвенции (заключение).
Смысл секвенции: G является логическим следствием формул F1,…,Fn.
То же, что выражает формула F1 &… & Fn É G.
Определение секвенции носит синтаксический характер.
Синтаксически определенные аксиомы.
а) все секвенции вида: F®F – где F – произвольная формула являются аксиомами СКИП
б) секвенция f®, где f - константа ложь, является аксиомой СКИП.
4). Синтаксическое определение правил вывода. 
В СКИП существуют 2 правила для каждой связки: введение (связка справа от ®) и удаление (связка слева от ®).
Везде ниже Г–произвольный список формул конструктивного исчисления предикатов.
Логические правила вывода.
1) Введение &: Удаление &:
2) Введение Ú: Удаление Ú:
3) Введение É: Удаление É:
4) Отрицание Ø
В СКИП это определяемая связка:
= 
f (ложь)
5 )
Определение понятия «х свободно входит в F »:
Свободные переменные являются параметрами формулы.
а) все переменные х, входящие в элементарные формулы, входят в них свободно.
б) пусть х входит свободно хотя бы в одну F1, F2, тогда она входит свободно в (F1&F2), (F1 Ú F2), (F1 É F2), (ØF1), (ØF2).
в) пусть y входит свободно в F, тогда если y¹x, то y входит свободно в формулы
("x F(x)), ($x F(x)), а x входит в них связано.
Критерием связанности является невозможность подставить вместо переменной конкретное значение – при этом формула потеряет смысл.
Связанные переменные можно переименовывать (без изменения смысла выражения).
Введение 
: Удаление :
y не входит свободно ни в одну
формулу из Г t - произвольный терм без ограничений
6) Введение 
: Удаление :
y не входит свободно ни в одну из Г.