В Вашем же комментарии нужны ещё и собственные аксиомы.
Нет, я как раз говорил о формальной системе без прикладных аксиом.
Если нет формул, то все формулы истинны на всех интерпретациях и, соответственно, общезначимы. Вырожденный случай.
Почему-то мне кажется, что тот, кто давал определение, вовсе не этот случай имел в виду.
В разных интерпретациях функциональным и предикатным символам может придаваться разное значение. Т.е. в исчислении предикатов выводимы те и только те формулы, истинность которых не зависит от смысла входящих в них предикатных и функциональных символов.
Это всё понятно, но вопрос был с дальним прицелом, чуть позже я поясню... Я прекрасно вижу, что формула:
не является общезначимой, поскольку может быть такая интерпретация операции сложения, согласно которой оно не является коммутативным. Нашли интерпретацию, в которой формула ложна, - значит она не общезначима, всё понятно.
Вопрос в том,
как мы можем понять, что формула общезначима, если она такова. Например, формула
судя по всему является общезначимой, поскольку это утверждение не опирается ни на какие свойства операции сложения и ни на какие свойства отношения равенства. Т.е. именно "её истинность не зависит от смысла входящих в неё предикатных и функциональных символов". Но это что, чисто
интуитивный вывод? Как это
доказать? Если буквально следовать определению, то мы должны проверить
все возможные интерпретации. Не могу себе представить, чтобы это было возможно.
Теперь про "дальный прицел". Известно, что для логики второго порядка нет аналога теоремы полноты. Т.е. среди формул второго порядка имеются логически общезначимые, но невыводимые. Поэтому очень любопытно было бы:
1) Найти пример такой формулы.
2) Доказать, что она - логически общезначима (хотя бы понять, как это делается).
3) Доказать, что она невыводима в исчислении предикатов второго порядка (без прикладных аксиом).