О теореме Эрбрана

[Tcirkubakin]

Не понял ход доказательства теоремы Эрбрана на шаге $\left( \mathrm{iii} \right)\Rightarrow \left( \mathrm{i} \right)$ (https://archive.org/details/a-concise-i ... 9/mode/1up) Не знаю, как довести дело до конца в случае с заменой простейших формул первого порядка в формулах из множества $ \overset{\sim}{\mathrm{U}}\ \cup \left\{ \neg \alpha\frac{\vec t}{\vec x} | \ \vec t \in \mathcal{T}^{n}\right\} $ на пропозициональные переменные($\overset{\sim}{\mathrm{U}}$ - set of all instances, "instance" определяют на конце 137-ой - начале 138-ой страниц (https://archive.org/details/a-concise-i ... 7/mode/1up)).
1. Первый вопрос: корректно ли доказательство у автора(например на предмет опечаток)? Если я неправильно понимаю доказательство, то где я ошибаюсь?
2.Рассуждаю следующим образом:
По книге известно, что простейшие формулы первого порядка имеют вид $s=t$ или $rt_{1}t_{2}...t_{n}$ , где $r$ - отношение (или предикат), а $s,t,t_{k}$-термы. Чтобы создать пропозициональную формулу, эквивалентно удовлетворимую(satisfiably equivalent) $\neg \alpha\frac{\vec{t}}{\vec{x}}$, пытаюсь провести замену переменных следующим способом: (разным простейшим формулам первого порядка - разные проп. переменные, как писал автор) равенства(формулы вида $s=t$) заменяю проп. переменными $p_{s=t}$, т.к. существует модель, интерпретирующая все равенства в формулах $\neg \alpha\frac{\vec{t}}{\vec{x}}$, как верные. С отношениями (предикатами) дело обстоит сложнее. Если формула не удовлетворима при любой интерпретации(например, $x>x$), то, думаю, её стоит заменить пропозициональным противоречием($p_{x>x}\wedge \neg p_{x>x}$). Но в одной формуле могут встретиться отношения(+равенства), не являющиеся(при интерпретациях) одновременно истинными(например: $x > y \vee x < y \vee y=x$). Вторым вопросом является то, как в данном (+общем) случае произвести требуемую замену(учитывая все ньюансы)(примеры такого рода замен даны в 1.5).
3. Так как полученные после замены(замены в формулах из $ \overset{\sim}{\mathrm{U}}\ \cup \left\{ \neg \alpha\frac{\vec t}{\vec x} | \ \vec t \in \mathcal{T}^{n}\right\} $) формулы (обозначу для удобства пропозициональные формулы, полученные путём замены через $\beta$ с индексами первоначальных формул: $\beta_{\overset{\sim}{\mathrm{U}}}\cup \beta_{\neg \alpha\frac{\vec t}{\vec x}} \left\{ \neg \alpha\frac{\vec t}{\vec x} | \ \vec t \in \mathcal{T}^{n}\right\}$ )эквивалентно удовлетворимы исходному множеству формул(по теореме о полноте первого порядка заменяем в исходном множестве формул $ \overset{\sim}{\mathrm{U}}\ \cup \left\{ \neg \alpha\frac{\vec t}{\vec x} | \ \vec t \in \mathcal{T}^{n}\right\} $ противоречивость(inconsistent) неудовлетворимостью), то, исходя из теоремы(плюс по теореме о полноте первого порядка), они также не будут удовлетворимы. Из $\beta_{\overset{\sim}{\mathrm{U}}}\cup \beta_{\neg \alpha\frac{\vec t}{\vec x}} \left\{ \neg \alpha\frac{\vec t}{\vec x} | \ \vec t \in \mathcal{T}^{n}\right\}\models \perp $ следует $\beta_{\overset{\sim}{\mathrm{U}}}\cup \beta_{\neg \alpha\frac{\vec t}{\vec x}} \left\{ \neg \alpha\frac{\vec t}{\vec x} | \ \vec t \in \mathcal{T}^{n}\right\}\vdash \perp $ (по теореме о пропозиц. полноте), следовательно по упражнению 1 из 1.4 (https://archive.org/details/a-concise-i ... 0/mode/1up) следует (знак негации в формулах $\beta_{\neg \alpha\frac{\vec t}{\vec x}} \left\{ \neg \alpha\frac{\vec t}{\vec x} | \ \vec t \in \mathcal{T}^{n}\right\}$ при переносе в правую часть уходит):$\beta_{\overset{\sim}{\mathrm{U}}} \vdash \bigvee_{k=0}^{m}{\beta_{k}}_{ \alpha\frac{\vec t}{\vec x}} \left\{ \alpha\frac{\vec t}{\vec x} | \ \vec t \in \mathcal{T}^{n}\right\} $. Как (для завершения доказательства) получить эквивалентное этому выражение с формулами первого порядка (и стоит ли это делать, если нет, почему)?.
4. Множество $Y=\left\{ \alpha\frac{t}{x} | t\in \mathcal{T}\right\}$ (откуда оно появляется, пропозиционально ли оно и почему $\frac{\vec t}{\vec x}$ заменили на $\frac{t}{x}$). Благодарю.