Определение

Система аксиом Т, ее аксиоматическая теория и аксиоматическая структура , определенные вне какой–либо реализации, называются абстрактными или формальными системой аксиом, теорий или структурой соответственно.

Если существует реализация R(T) этой системы, то система Т, теория и структурой называются содержательными.

Классическим примером формальной теории является геометрия Лобачевского. Эта мыслимая геометрия долгое время не воспринималась однозначно как аксиоматическая теория, пока не были найдены ее реализации, например, реализация Пуанкаре L₂, построенная в п.6. Таким образом, исторический опыт с геометрией Лобачевского имеет "хороший конец": были найдены реализации и сняты все вопросы в рамках этих реализаций.

Чтобы использовать реализации R(T) для исследования аксиоматических систем Т, введем понятие изоморфизма реализаций (структур).