Здравствуйте, Lazin, Вы писали:

L>Формальная система может иметь бесконечное количество аксиом, а также множество интерпретаций, или вообще не иметь. В общем, формальные системы никак не могут нам помочь в данном случае.

Непонятно как из первого утверждения следует второе. Формальные системы помогают определить термины "понятие" и "определение". Например, под "понятиями" можно понимать унарные предикаты, а под определениями формулы вида "A(x) <-> ...", где слева произвольная формула с одной свободной переменной. Так работает, например, description logic — формальная система для многих современных систем управления терминологией (например, в медицинской информатике).

Большинство теорий в DL имеют множество интерпретаций, более того, в силу Löwenheim–Skolem theorem теория не может, как правило, контролировать размер этих интерпретаций. Но это нестрашно, главное что теория — это всегда система ограничений на допустимые интерпретации. Поэтому она и полезна.