Язык первого порядка; Строго ли мое простое доказательство?

[creative]

Утверждение:

$\models \neg \forall x A \equiv \exists x \neg A$

Мое доказательство:

Пусть $M$ - произвольная модель языка, а $\theta$ - произвольная оценка для нашей формулы.
Нужно доказать $M \models (\neg \forall x A \equiv \exists x \neg A) \theta$.
Пусть $M \models (\neg \forall x A \equiv \exists x \neg A) \theta$.
Так как $x$ не входит свободно в $M \models (\neg \forall x A \equiv \exists x \neg A) \theta$, то пусть $dom \theta ' = dom \theta \backslash \{x\}$ и $\theta ' (x) = \theta (x)$ для всех $x \in dom \theta '$.
Согласно п. 2 § 2 гл. 2 $M \models (\neg \forall x A) \theta \equiv (\exists x \neg A) \theta$.
Согласно п. 2 § 2 гл. 2 $M \models \neg ((\forall x A) \theta) \equiv \exists x ((\neg A)\theta ')$.
Согласно п. 2 § 2 гл. 2 $M \models \neg \forall x (A \theta ') \equiv \exists x \neg (A \theta ')$.

Согласно п. 5 и п. 6 § 3 гл. 2 пусть $M \models \neg \forall x (A \theta ') \rightarrow \exists x \neg (A \theta ')$.
Согласно п. 5 § 3 гл. 2 положим $M \models \neg \forall x (A \theta ')$.
Тогда согласно п. 5 § 3 гл. 2 нужно доказать $M \models \exists x \neg (A \theta ')$.
Поскольку $M \models \neg \forall x (A \theta ')$, то неверно, что $M \models \forall x (A \theta ')$.
Значит неверно, что для любого объекта $a$ из области соответствующего сорта $M \models {(A \theta ')_\underline{a}}^x$.
Следовательно, существует $a$, такое, что неверно $M \models {(A \theta ')_\underline{a}}^x$, что означает $M \models \neg {(A \theta ')_\underline{a}}^x$.
Тогда согласно п. 5 § 3 гл. 2 $M \models \exists x \neg (A \theta ')$.
Следовательно $M \models \neg \forall x (A \theta ') \rightarrow \exists x \neg (A \theta ')$.

Согласно п. 5 и п. 6 § 3 гл. 2 пусть $M \models \exists x \neg (A \theta ') \rightarrow \neg \forall x (A \theta ')$.
Согласно п. 5 § 3 гл. 2 положим $M \models \exists x \neg (A \theta ')$.
Тогда согласно п. 5 § 3 гл. 2 нужно доказать $M \models \neg \forall x (A \theta ')$.
Поскольку $M \models \exists x \neg (A \theta ')$, то существует $a$ из области соответствующего сорта $M \models {\neg (A \theta ')_\underline{a}}^x$, а значит для этого $a$ неверно, что $M \models {(A \theta ')_\underline{a}}^x$.
Поэтому неверно, что для любого $a$ верно $M \models {(A \theta ')_\underline{a}}^x$.
Тогда согласно п. 5 § 3 гл. 2 $M \models \neg \forall x (A \theta ')$.
Следовательно $M \models \exists x \neg (A \theta ') \rightarrow \neg \forall x (A \theta ')$.

Так как $M \models \neg \forall x (A \theta ') \rightarrow \exists x \neg (A \theta ')$ и $M \models \exists x \neg (A \theta ') \rightarrow \neg \forall x (A \theta ')$, то согласно п. 5 и п. 6 § 3 гл. 2 $M \models \neg \forall x (A \theta ') \equiv \exists x \neg (A \theta ')$ и соответственно $M \models (\neg \forall x A \equiv \exists x \neg A) \theta$.

Так как $M \models (\neg \forall x A \equiv \exists x \neg A) \theta$ для любой произвольно выбранной модели $M$ и оценки $\theta$, то $\models \neg \forall x A \equiv \exists x \neg A$ $\Box$

Основные определения из книги Колмогоров А.Н. Драгалин А.Г. Введение в математическую логику 1982:

Модель $M$ п. 3 § 3 гл. 2.
Оценка $\theta$ для выражения $T$ п. 2 § 3 гл. 2.
$Fv(T)$ п. 10 § 1 гл. 2.

Вопросы:

В1: Верно ли доказательство?
В2: Если ответ на В1 положительный, то можно ли считать его достаточно строгим? (это главный вопрос топика)

P.S. Если по каким-то определениям есть вопросы, а в книге сходу не нашли, то спрашивайте, так как я не все определения дал расчитывая на их общеизвестность и экономию своего времени (переписывать целые абзацы очень долго).

[Профессор Снэйп]

Как у Вас страшно всё выглядит!

Колмогорова и Драгалина не читал, так что проверить доказательство не могу. У нас в НГУ мат. логику изучают по книге Ершова и Палютина, там всё гораздо короче и проще для понимания (и уж точно никак не менее строго).

[creative]

В книжке Колмогорова, Драгалина все просто. И доказательство простое. Я специально развернул все шаги, чтобы проверить себя на строгость мышления, а так же то насколько хорошо усвоил определения.

[Xaositect]

Ссылки не проверял, последовательность шагов правильная, но слова, поясняющие эту последовательность, ужасны. Вы постоянно пишете "Пусть $M \models $какую-то формулу" когда вам на самом деле это надо доказать.

Ну то есть, допустим, первый абзац надо переписать так:
Нужно доказать $M\models (\neg \forall x A\equiv \exists x \neg A)\theta$. По определению оцененной формулы и подстановки $(\neg \forall x A\equiv \exists x \neg A)\theta$ преобразуется в $\neg\forall x (A\theta') \equiv \exists x \neg (A\theta')$. По определению истинности $\equiv$ для того, чтобы доказать $M\models\neg\forall x (A\theta') \equiv \exists x \neg (A\theta')$, необходимо и достаточно доказать $M\models \neg\forall x (A\theta') \to \exists x \neg (A\theta')$ и $M\models \exists x \neg (A\theta') \to \neg\forall x (A\theta')$

[creative]

Xaositect

Осмыслил свою ошибку. Большое спасибо!