Структурні знаки формальної мови

Теория первого порядка – это формальная теория, в которой нет классификатора, нет признаков и функций для предикатных функциональных символов, где кванторы не применяются к предикатным и функциональным символам. Теория множеств может быть построена как теория ZFC первого порядка. Ограничения рассмотрения теориями первого порядка призвано упростить анализ, т.е. не является принципиальным. Так формулировка BNG теории множеств использующая классификатор обладает очевидными достоинствами. В метаязыковых записях естественен выход за рамки символики теории первого порядка, в честности, - применение кванторов к функциональным предметным символам.

Обычно в языке-объекте обходятся в качестве вспомогательных символов скобками (,) и запятой,.В метаязыковых записях запас вспомогательных символов может быть существенно шире: разные виды скобок [, ] {, }, <, >, ¼, точка с запятой;, многоточие ¼ и т. д.

В содержательных записях, кроме знаков языка-объекта, используемых автономно, широко используются

Знаки начала 3и конца 8доказательства (первый можно читать как “доказательство”, а второй – что и требовалось доказать);

Знак тождества º, означающий что соединенных им выражения рассматриваются как обозначения одного и того же.

Знак равенства по определению: = или =:, означающий что из соединенных им выражений, стоящее со сторон двоеточия по определению равно другому;

Разные скобки, черточки дробей и линии диаграмм, стрелки и т.д. и т.п.

Переменные и константы (постоянные)