Езици с формално равенство

Нека $\mathfrak{L}$ е предикатен език без формално равенство, да означим с $\mathfrak{L}^=$, езикът който се получава от $\mathfrak{L}$ при добавянето на формално равенство.
Тогава произволна структора $\mathcal{A}$ за езика $\mathfrak{L}$ е структура и за езика $\mathfrak{L}^=$

Свойства на формалното равенство

$\mathcal{A} \models \forall x \ (x \doteq x)$
$\mathcal{A} \models \forall x \forall y \ (x \doteq y \Rightarrow y \doteq x)$
$\mathcal{A} \models \forall x \forall y \forall z \ (x \doteq y\ \&\ y \doteq z \Rightarrow x \doteq z)$
$\mathcal{A} \models \forall x_1... \forall x_n \forall y_1... \forall y_n \ (x_1 \doteq y_1\ \&\ ...\ \&\ x_n \doteq y_n) \ \Rightarrow (p(x_1,..,x_n)=p(y_1,..,y_n))$
$p \in \underset{\#(p)=n}{Pred } \mathfrak{L}$

$\mathcal{A} \models \forall x_1... \forall x_n \forall y_1... \forall y_n \ (x_1 \doteq y_1\ \&\ ...\ \&\ x_n \doteq y_n) \ \Rightarrow (f(x_1,..,x_n)=f(y_1,..,y_n))$
$p \in \underset{\#(p)=n}{Func} \mathfrak{L}$

Проверка на две от равенствата:

Имаме $\mathcal{A}, \upsilon$ в $A$

$\mathcal{A} \underset{\upsilon}{\models} \forall x (x \doteq x)$ ще проверим това свойство за производен елемент $a \in A$ от универсума на структурта.

$\mathcal{A} \underset{\upsilon_a^x}{\models} (x \doteq x)$
$\iff ||a||^{\mathcal{A}}[\upsilon_a^x] = ||a||^{\mathcal{A}}[\upsilon_a^x]$
$\iff \upsilon_a^x(x) = \upsilon_a^x(x)$ -тук вече е очевидно
$a=a$

Сега проверяваме предпоследното свойство

$\mathcal{A} \underset{\upsilon}{\models} \varphi$ за произволни $a_1,a_2,...,a_n,b_1,b_2,...,b_n \in A$

(1)
\begin{align} \mathcal{A} \underset{\upsilon^{x_1,..,x_n,y_1,...,y_n}_{a_1,...,a_n,b_1,...,b_n}}{\models} \forall x_1... \forall x_n \forall y_1... \forall y_n \ (x_1 \doteq y_1& ... & x_n \doteq y_n) \Rightarrow (p(x_1,..,x_n)=p(y_1,..,y_n)) \end{align}

полагаме $\upsilon^{x_1,..,x_n,y_1,...,y_n}_{a_1,...,a_n,b_1,...,b_n} = \omega$

(2)
\begin{align} \mathcal{A} \underset{\omega}{\models} \forall x_1... \forall x_n \forall y_1... \forall y_n \ (x_1 \doteq y_1\ \&\ ...\ \&\ x_n \doteq y_n) \Rightarrow (p(x_1,..,x_n)=p(y_1,..,y_n)) \end{align}

$\iff$ за произволни $a_1,..,b_n \in A$ ако в $\mathcal{A} \underset{\omega}{\models} (x_1 \doteq y_1\ \&\ ...\ \&\ x_n \doteq y_n)$ тогава в
$\mathcal{A} \underset{\omega}{\models} p(x_1,..x_n) = p(y_1,..,y_n)$
Нека $\mathcal{A} \underset{\omega}{\models} (x_1 \doteq y_1\ \&\ ...\ \&\ x_n \doteq y_n)$
тогава имаме за всяка отделна оценка $\mathcal{A} \underset{\omega}{\models} (x_1 \doteq y_1),...,\mathcal{A} \underset{\omega}{\models} ( x_n \doteq y_n)$
от което следва $||x_1||^{\mathcal{A}}[\omega] = ||y_1||^{\mathcal{A}}[\omega],...,||x_n||^{\mathcal{A}}[\omega] = ||y_n||^{\mathcal{A}}[\omega]$
от което следва $a_1=b_1,..,a_n=b_n$
ние искаме да докажем $\mathcal{A} \underset{\omega}{\models} p(x_1,..,x_n) \iff p(y_1,..,y_n)$,
което е равносилно на $\mathcal{A} \underset{\omega}{\models} <||x_1||^{\mathcal{A}}[\omega],...,||x_n||^{\mathcal{A}}[\omega]> \in p^{\mathcal{A}}$ точно когатo $<||y_1||^{\mathcal{A}}[\omega],...,||y_n||^{\mathcal{A}}[\omega]> \in p^{\mathcal{A}}$,
което е равносилно на $<a_1,..,a_n> \in p^{\mathcal{A}}$ точно когато $<b_1,..,b_n> \in p^{\mathcal{A}}$

Аксиоми за равенство

Нека $Eq$ е двуместен предикатен символ и $\mathfrak{L}^{Eq}$. С $\Gamma_{\mathfrak{L}^{Eq}}$ да означим горните формули, като $\doteq$ е заместено с $Eq$, тоест $x \doteq x' \rightarrow Eq(x,x')$ и $f(x_1,..,x_n) \doteq f(y_1,...,y_n) \rightarrow Eq(f(x_1,..,x_n), f(y_1,...,y_n))$
Така дефинираното $\Gamma_{\mathfrak{L}^{Eq}}$ наричаме аксиоми за равенство за езика $\mathfrak{L}$

Твърдение, конгуренция

Нека $\mathcal{A}$ е структура за $\mathfrak{L}^{Eq}$. Ако $\mathcal{A} \models \Gamma_{\mathfrak{L}^{Eq}}$, то са в сила следните:

1. $Eq^{\mathcal{A}}$ - релация на еквивалентност в $A$;
2. За произволни $a_1,..,a_n,b_1,..,b_n$ ако $[a_1]=[b_1],..,[a_n]=[b_n]$, тo $<a_1,..,a_n> \in p^{\mathcal{A}} \iff <b_1,..,b_n> \in p^{\mathcal{A}}$
В този случай се казва, че $p^{\mathcal{A}}$ е съгласуван с $Eq^{\mathcal{A}}$ или
$Eq^{\mathcal{A}}$ е конгуренция при $p^{\mathcal{A}}$

3. За произволни $a_1,..,a_n,b_1,..,b_n$ ако $[a_1]=[b_1],..,[a_n]=[b_n]$, то $[f^{\mathcal{A}}(a_1,...,a_n)]=[f^{\mathcal{A}}(b_1,...,b_n)]$
В този случай се казва, че $f^{\mathcal{A}}$ е съгласуван с $Eq^{\mathcal{A}}$ или
$Eq^{\mathcal{A}}$ е конгуренция относно $f^{\mathcal{A}}$

Дефиниция

Нека $\mathcal{A}$ е структура за езика $\mathfrak{L}$. Нека $E$ е релация на еквивалентност в $A$ която е конгуренция относно $f^{\mathcal{A}}$ за приоизволнo $f$ от $\mathfrak{L}$.
Дефинираме структурата $A / E$ по следния начин: универсумът на тази структура е $А / Е = \{ [a]_{E} | a \in A\}$ (тоест фактормножеството)

  • $c^{A / E} \leftrightharpoons [c^{\mathcal{A}}]$ за всички индивидни константи $c \in \mathfrak{L}$
  • $[a_1],..,[a_n] \in A / E \leftrightharpoons \{ <[a_1],...,[a_n]> | <a_1,..,a_n> \in p^{A} \}$
  • $f^{A / E}([a_1]_{E},...,[a_n]_E) \leftrightharpoons [f^{\mathcal{A}}(a_1,..,a_n)]_E$.

За $A / E$ казваме че е факторгрупа на $A$ относно конгуренцията $E$.

Твърдение

Нека $\mathcal{A}$ е структура за $\mathcal{L}, Е$ е конгуренция в $A$. Нека $\upsilon$ е оценка в $A / E$.
Дефинираме оценката $\omega : \omega(x) \leftrightharpoons [\upsilon(x)]_{E}$.
Тогава

  1. За всеки терм $\tau$ от $\mathcal{L}$, стойността на $\tau$ $\big[ ||\tau||^{\mathcal{A}}[\upsilon]\big] = ||\tau||^{A / E}[\omega]$
  2. За всяка формула $\varphi$ $\mathcal{A} \underset{\upsilon}{\models} \varphi \iff A / E \underset{\omega}{\models} \varphi$ /$asd$/
  3. За всяка затворена формула $\mathcal{A} {\models} \varphi \iff A / E {\models} \varphi$

Нека $\mathcal{A} \models \Gamma \bigcup \Gamma_{\mathcal{L}^{Eq}}$ тогава $Eq^{\mathcal{A}}$ е контур в $A$.

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License