Строго ли мое доказательство? Кванторы в формуле.

[creative]

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

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

Если $x \notin Fv(A)$, то $\models A \vee \forall x B(x) \supset \forall x (A \vee B(x))$;

Доказательство:

$\rhd$
По определению свободных и связанных переменных в п. 9 § 1 гл. 2: переменная $x$ входит связанно и не входит свободно в формулу $A \vee \forall x B(x) \supset \forall x (A \vee B(x))$;
По определению оценки в п. 2 § 3 гл. 2 и формальной подстановки в п. 2 § 2 гл. 2: подстановка $\theta$ замещает только свободные вхождения переменных, поэтому достаточно рассматривать только такие подстановки $\theta$, для которых $x \notin dom \theta$;
По определению $\models$ в п. 2 § 5 гл. 2: $\models A \vee \forall x B(x) \supset \forall x (A \vee B(x))$ означает, что $M \models (A \vee \forall x B(x) \supset \forall x (A \vee B(x)))\theta$, для любой модели $M$ и любой оценки $\theta$, для которой верно что $x \notin dom\theta$;
Достаточно доказать $M \models (A \vee \forall x B(x) \supset \forall x (A \vee B(x)))\theta$, где $M$ обозначает произвольную модель и $\theta$ обозначает произвольную (среди тех, для которых выполняется условие $x \notin dom\theta$) оценку в модели;
Согласно правилам вычисления подстановки в п. 2 § 2 гл. 2: $M \models (A \vee \forall x B(x) \supset \forall x (A \vee B(x)))\theta$ эквивалентно $M \models A\theta \vee \forall x (B(x)\theta ) \supset \forall x (A\theta \vee B(x) \theta)$;
Достаточно доказать $M \models A\theta \vee \forall x (B(x)\theta) \supset \forall x (A\theta \vee B(x) \theta)$;
По определению импликации $\supset$ в п. 6 § 3 гл. 2 и п. 5 § 3 гл. 2: достаточно доказать $M \models \forall x (A\theta \vee B(x) \theta)$, когда $M \models A\theta \vee \forall x (B(x)\theta)$ верно;
Пусть $M \models A\theta \vee \forall x (B(x)\theta)$, докажу $M \models \forall x (A\theta \vee B(x) \theta)$;
Обозначу $A\theta \vee B(x) \theta$ через букву $F$.
По определению в п. 5 § 3: $M \models \forall x F$ означает, что для всякого $a \in D_\pi$ верно $M \models {F_\underline{a}}^x$;
По определению ${\Phi_\underline{a}}^x$ (где $\Phi$ есть формула) в п. 12 § 1 гл. 2 и определению свободных и связанных переменных в п. 9 § 1 гл. 2 (Б): переменная $x$ свободна в $B(x)\theta$ и по условию не свободна в $A\theta$;
Следовательно $M \models \forall x (A\theta \vee B(x) \theta)$ означает, что $M \models A\theta \vee {(B(x)\theta)_\underline{a}}^x$ для всех $a \in D_\pi$;
По определению в п. 5 § 3 гл. 2: $M \models A\theta \vee {(B(x)\theta)_\underline{a}}^x$ (при всех $a \in D_\pi$) обозначает $M \models A\theta \vee \forall x (B(x)\theta)$;
Поскольку $M \models \forall x (A\theta \vee B(x) \theta)$ имеет вид $M \models A\theta \vee \forall x (B(x)\theta)$, следовательно верно;
Поскольку $M \models \forall x (A\theta \vee B(x) \theta)$ доказано, то доказано и $M \models A\theta \vee \forall x (B(x)\theta) \supset \forall x (A\theta \vee B(x) \theta)$;
$\lhd$

Вопрос:

Моё доказательство строго и правильно?

P.S. По всем возникающим вопросам пишите, так как не имею возможности дословно написать все определения из книги используемые в доказательстве.

[Xaositect]

Доказательство правильно.
В предпоследней строчке оборот "имеет вид" некорректен на мой взгяд. Здесь лучше написать "эквивалентно" или "Мы получили, что $M\models F$ тогда и только тогда, когда $M\models F'$"
В последней надо бы упомянуть, что $M\models F$ доказано в предположении $M\models F'$.

[creative]

Xaositect

Большое спасибо!

Думаю, что ещё пропустил такой момент:

Я описал оценку $\theta$ такую, что $x \notin dom\theta$. Далее в конце доказательства утверждал, что согласно п. 9 § 1 гл. 2 (Б) переменная $x$ свободна в $B(x) \theta$ и по условию не свободна в $A \theta$. Но хоть это и очевидно, но я явно не доказал, что в $B(x) \theta$ переменная $x$ останется свободной (в $B(x)$ переменная $x$ свободна). И что в $A\theta$ переменная $x$ также не входит свободно (для $A$ выполняется $x \notin Fv(A)$).