ОК, хорошо, я понял в чём проблема, кажись.
Будем отталкиваться от того, что у вас написано. То что написано в (1) и (2) объединим и назовём теорией (первого порядка). Заметим, что аксиомы теории состоят как из логических аксиом, так и из собственных аксиом теории. При этом важно отметить, что в самом начале фиксируется сигнатура, только потом можно говорить про какие либо формулы и теории. Теперь если собственные аксиомы теории отсутствуют и получается то, что называется исчислением предикатов первого порядка. Тогда становится удобно говорить что теория это исчисление предикатов + собственные аксиомы теории. И тогда понятно почему собственное множество аксиом тоже называют теорией.
(3) Общезначимость. Вы не правы,
![$\forall x \, x = x $ $\forall x \, x = x $](https://dxdy-01.korotkov.co.uk/f/c/1/8/c1840ff32b005688c1291dd9fc3cbed382.png)
-- не общезначима. Так как она должна быть истинна на любой модели (про нормальные модели молчим пока), а
![$=$ $=$](https://dxdy-02.korotkov.co.uk/f/5/9/1/591ff9c1652b7e605ef0190a9713c14082.png)
-- это просто бинарный предикатный символ, его можете интерпретировать как
![$=$ $=$](https://dxdy-02.korotkov.co.uk/f/5/9/1/591ff9c1652b7e605ef0190a9713c14082.png)
, как
![$<$ $<$](https://dxdy-02.korotkov.co.uk/f/d/e/7/de76ecbd9818ca51b348b16e75347a4a82.png)
, как
![$>$ $>$](https://dxdy-03.korotkov.co.uk/f/6/d/e/6de15a59c5cd495a7f9f6484e738623b82.png)
, как
![$\not{=}$ $\not{=}$](https://dxdy-02.korotkov.co.uk/f/1/a/c/1ac738f1675fa233257eb517e173b30282.png)
, ... вообще любым бинарным отношением заданным на носителе.
А общезначимой формулой будет, например,
![$\forall x \, ((x = x) \vee \neg (x = x)) $ $\forall x \, ((x = x) \vee \neg (x = x)) $](https://dxdy-01.korotkov.co.uk/f/0/b/1/0b11031b6508df927872426aba3b464082.png)
,
![$(\forall x \, x = x) \to (\exists x \, x = x)$ $(\forall x \, x = x) \to (\exists x \, x = x)$](https://dxdy-04.korotkov.co.uk/f/3/7/3/373649407e89efd21d5500eeff39270d82.png)
, и так далее. Это понятие нужно для установления свойств кванторов и логических связок, а не для символов сигнатуры.
Что такое выводимость вам понятно. Так вот важный факт -- корректность исчисления предикатов -- любая выводимая в исчислении предикатов формула является общезначимой.
Что и записывается в виде
![$\vdash \varphi \; \Rightarrow \; \models \varphi$ $\vdash \varphi \; \Rightarrow \; \models \varphi$](https://dxdy-02.korotkov.co.uk/f/1/0/b/10b702c7c1edbbdecf89425e780100c882.png)
.
Заметьте, здесь пока что нет собственных аксиом теории.
Теперь пусть есть собственные аксиомы теории
![$T$ $T$](https://dxdy-03.korotkov.co.uk/f/2/f/1/2f118ee06d05f3c2d98361d9c30e38ce82.png)
(можно мыслить
![$T$ $T$](https://dxdy-03.korotkov.co.uk/f/2/f/1/2f118ee06d05f3c2d98361d9c30e38ce82.png)
и как обозначение теории и как обозначение множества аксиом теории). В этом случае также имеется теорема о корректности, которая утверждает, что всякая выводимая в теории
![$T$ $T$](https://dxdy-03.korotkov.co.uk/f/2/f/1/2f118ee06d05f3c2d98361d9c30e38ce82.png)
формула, истинна на любой модели теории
![$T$ $T$](https://dxdy-03.korotkov.co.uk/f/2/f/1/2f118ee06d05f3c2d98361d9c30e38ce82.png)
, что и записывается в виде
![$T \vdash \varphi \; \Rightarrow \; T\models \varphi$ $T \vdash \varphi \; \Rightarrow \; T\models \varphi$](https://dxdy-03.korotkov.co.uk/f/e/2/1/e21bd80107cf61e018d79b37171c98f882.png)
.
Заметьте отличие от предыдущей теоремы, там общезначимость, то есть истинность на _любой_ модели, а здесь истинность на моделях теории. Вернёмся к вашему примеру
![$\forall x \, x = x$ $\forall x \, x = x$](https://dxdy-02.korotkov.co.uk/f/9/2/5/9258c59fc8ecfefb7065f5893887654682.png)
, рассмотрим теперь теорию равенства, то есть аксиомы (то есть предложения) которые говорят, что значок
![$=$ $=$](https://dxdy-02.korotkov.co.uk/f/5/9/1/591ff9c1652b7e605ef0190a9713c14082.png)
обладает привычными на свойствами (в любой книге их найдёте). Тогда
это формула будет истинной на любых моделях в которых равенство проинтерпретировано естественным образом.
Можно повториться, сказав что общезначимые формулы это те формулы которые остаются истинными в любых моделях любых теорий, какие бы вы их ненапридумывали.
Теперь перейдём к полноте теории.
Как вы правильно сказали, что теория полна, если для любой формулы, выводится либо она сама, либо её отрицание.
Простой содержательный пример неполной теории -- теория групп. Так как существуют коммутативные и некоммутативные группы.
Другими словами теория полна, если про любое предложение можно сказать, истинно оно или ложно.
А что такое полнота исчисления предикатов? Это утверждение о том, что любая общезначимая формула выводима в исчислении предикатов, то есть
![$\models \varphi \; \Rightarrow \; \vdash \varphi$ $\models \varphi \; \Rightarrow \; \vdash \varphi$](https://dxdy-03.korotkov.co.uk/f/2/c/4/2c4d1e576e00b3c2ec08a24dfedee13382.png)
То есть вывести мы можем всё, что истинно всегда и везде.
Или сильная форма утверждения о полноте исчисления предикатов (когда добавляются аксиомы теории)
![$T \models \varphi \; \Rightarrow \; T\vdash \varphi$ $T \models \varphi \; \Rightarrow \; T\vdash \varphi$](https://dxdy-04.korotkov.co.uk/f/b/8/b/b8b4d8cf6bd1d66c70dd9d4baab4f41482.png)
.
Таким образом собрав всё вместе и немножко допустив вольность речи понимаем что это разные понятия:
(1) Полнота теории -- это значит что для любой формулы мы можем установить истинна она или ложна на любых моделях этой теории. (то есть про все формулы можно что-то сказать.)
(2) Полнота исчисления предикатов -- всё что истинно на моделях можно вывести. (то есть меньше не получилось).
Спасибо. Вопросы?
(а с нумерацией я прокосячил, сначала хотел о четырёх вещах спросить.)