ID | Название | Описание |
X# | Базисное множество | Базовое (невыводимое) понятие, интерпретация которого задается разработчиком |
C# | Константное множество | Вспомогательное понятие, имеющие общеизвестную интерпретацию в рассматриваемой предметной области |
S# | Родовая структура | Базисное (невыводимое) структурированное понятие, интерпретация которого задается разработчиком и ограничивается аксиомами |
H# | Ступень | Сокращение множества-ступени. Не является понятием. Использовалось для анализа типизаций термов до появления анализаторов, вычисляющих типизацию автоматически. |
A# | Аксиома | Логическое выражение, задающее некоторое усмотренное в предметной области ограничение на базовые и выводимые понятия. В корректной КМ аксиомы истинны для всех значений локальных переменных. |
D# | Терм | Выводимое понятие, задаваемое теоретико-множественным выражением |
F# | Терм-функция | Статически типизированное параметризованное теоретико-множественное выражением. Используется для сокращения выражений выводимых понятий, имеющих схожий способ вывода и используемые понятия. |
T# | Теорема | Логическое выражение, выводимое в проектируемой системе понятий |
Под объявлением терм-функции понимается выражение вида
F# = [α1∈ТМВ1, α2∈ТМВ2, ... ,αk∈ТМВk] ТМВ(α1, ... , αk), где
F# - имя терм функции
α1, ... , αk - параметры терм-функции. Имена переменных-параметров терм-функции не должны совпадать с внутренними переменными выражения ТМВ(α1, ... , αk) и именами конституент РС-формы.
ТМВ1, ... , ТМВk - области определения параметров терм-функции, заданные ступенями, принадлежащими шкале ступеней над базисными и константными множествами РС-формы.
 
ТМВ(α1, ... , αk) - "тело" терм-функции - теоретико-множественное типизированное выражение, зависящее от параметров терм-функции и конституент типов базисное множество, константное множество, родовая структура, ступень, терм.
Под использованием терм-функции понимается выражение вида
F#[A1, A2, ... , Ak], где
F# - имя объявленной ранее терм-функции
A1, A2, ... , Ak - имена конституент или локальных переменных, для которых биективно переносимо (корректно типизировано) выражение А1>∈ТМВ1 & А2∈ТМВ2 & ... & Аk∈ТМВk.