Линейно упорядоченное поле

Линейно упорядоченное поле по отношению и операциям

• $a,b,c,d,e,f,g,h,i,j$ - множества,
• $d = \langle e,f,g \rangle$ - упорядоченная тройка,
• $d = \mathrm{\Sigma}(e,f,g)$ - сигнатура,
• $h\in e \ \land \ e(h) = 2_\mathrm{N}$ - символ бинарного отношения,
• $(i\in f \ \land \ e(i) = 2_\mathrm{N}) \ \land \ (j\in f \ \land \ e(j) = 2_\mathrm{N})$ - символы бинарных операций,
• $a = \langle b,c,d \rangle$ - упорядоченная тройка,
• $a = \mathrm{AlgStruct}(b,c,d)$ - алгебраическая структура.

Алгебраическая структура $a$ сигнатуры $d$, образованная множествами $b, c$ — линейно упорядоченное поле (англ. linearly ordered field, нем. linear geordnete Körper) по отношению $h$ и операциям $i,j$ или кратко линейно упорядоченное поле, если алгебраическая структура $a$ является линейно упорядоченной структурой по отношению $h$ и алгебраическая структура $a$ является полем по операциям $i,j$:

$\Upsilon(a,b,c,d,e,f,g,h,i,j) \ \stackrel{\mathrm{def}}{=} \ a\in \mathrm{LinOrdStruct}(b;h) \ \land \ a\in \mathrm{Field}(b;i,j)$

Обозначим $\Upsilon(a,b,c,d,e,f,g,h,i,j) \ \stackrel{\mathrm{def}}{=} \ a\in \mathrm{LinOrdField}(b;h;i,j)$.

Замечание

Линейно упорядоченное поле по отношению $\leqslant$ и операциям $+, \cdot$ будем называть стандартным линейно упорядоченным полем (англ. standard linearly ordered field, нем. standard linear geordnete Körper).

Согласованное по сложению стандартное линейно упорядоченное поле

• $a,b,c,d,e,f,g$ - множества,
• $d = \langle e,f,g \rangle$ - упорядоченная тройка,
• $d = \mathrm{\Sigma}(e,f,g)$ - сигнатура,
• $\leqslant\in e \ \land \ e(\leqslant) = 2_\mathrm{N}$ - символ бинарного отношения,
• $(+\in f \ \land \ e(+) = 2_\mathrm{N}) \ \land \ (\cdot\in f \ \land \ e(\cdot) = 2_\mathrm{N})$ - символы бинарных операций,
• $a = \langle b,c,d \rangle$ - упорядоченная тройка,
• $a = \mathrm{AlgStruct}(b,c,d)$ - алгебраическая структура,
• $a\in \mathrm{LinOrdField}(b; \leqslant; +,\cdot)$ - стандартное линейно упорядоченное поле.

Стандартное линейно упорядоченное стандартное поле $a$ — согласованное по сложению стандартное линейно упорядоченное поле (англ. associated by addition standard linearly ordered field, нем. angeschlossen beim Addition standard linear geordnete Körper), если для любых четырёх элементов носителя $b$ стандартного линейно упорядоченного поля $a$ если {упорядоченная пара множеств $i,j$ принадлежит интерпретации символа отношения $\leqslant$ на множестве $b$} и {упорядоченная пара множеств $k, l$ принадлежит интерпретации символа отношения $\leqslant$ на множестве $b$}, то упорядоченная пара {суммы множеств $i,k$} и {суммы множеств $j,l$} принадлежит интерпретации символа операции $\leqslant$ на множестве $b$:

$\Upsilon(a,b,c,d,e,f,g) \ \stackrel{\mathrm{def}}{=} \ \forall i \ \forall j \ \forall k \ \forall l \quad \bigl( (i\in b \ \land \ j\in b) \ \land \ (k\in b \ \land \ l\in b) \bigr) \Rightarrow \Bigl( \bigl( \langle i,j \rangle\in \leqslant_a \ \land \ \langle k,l \rangle\in \leqslant_a \bigr) \Rightarrow \bigr\langle +(i,k), +(j,l) \bigr\rangle\in \leqslant_a \Bigr)$

Обозначим $\Upsilon(a,b,c,d,e,f,g,\leqslant) \ \stackrel{\mathrm{def}}{=} \ a\in \mathrm{AddAssocLinOrdField}(b;\leqslant;+,\cdot)$.

Согласованное по умножению стандартное линейно упорядоченное поле

• $a,b,c,d,e,f,g$ - множества,
• $d = \langle e,f,g \rangle$ - упорядоченная тройка,
• $d = \mathrm{\Sigma}(e,f,g)$ - сигнатура,
• $\leqslant\in e \ \land \ e(\leqslant) = 2_\mathrm{N}$ - символ бинарного отношения,
• $(+\in f \ \land \ e(+) = 2_\mathrm{N}) \ \land \ (\cdot\in f \ \land \ e(\cdot) = 2_\mathrm{N})$ - символы бинарных операций,
• $a = \langle b,c,d \rangle$ - упорядоченная тройка,
• $a = \mathrm{AlgStruct}(b,c,d)$ - алгебраическая структура,
• $a\in \mathrm{LinOrdField}(b; \leqslant; +,\cdot)$ - стандартное линейно упорядоченное поле.

Стандартное линейно упорядоченное поле $a$ — согласованное по умножению стандартное линейно упорядоченное поле (англ. associated by multiplication standard linearly ordered field, нем. angeschlossen beim Multiplikation standard linear geordnete Körper), если выполняются следующие условия:

1. для любого элемента носителя $b$ стандартного линейно упорядоченного поля $a$, который не равен нолю стандартного линейно упорядоченного поля, {если упорядоченная пара множества $i$ и ноля стандартного линейно упорядоченного поля $a$ принадлежит интерпретации символа отношения $\leqslant$ на множестве $b$, то упорядоченная пара инверсии множества $i$ и ноля стандартного линейно упорядоченного поля $a$ принадлежит интерпретации символа отношения $\leqslant$ на множестве $b$}, и {если упорядоченная пара ноля стандартного линейно упорядоченного поля $a$ и множества $i$ принадлежит интерпретации символа отношения $\leqslant$ на множестве $b$, то упорядоченная пара ноля стандартного линейно упорядоченного поля $a$ и инверсии множества $i$ принадлежит интерпретации символа отношения $\leqslant$ на множестве $b$},
2. для любых двух элементов носителя $b$ стандартного линейно упорядоченного поля $a$ если упорядоченная пара множеств $i,j$ принадлежит интерпретации символа отношения $\leqslant$ на множестве $b$, то для любого элемента носителя $b$ стандартного линейно упорядоченного поля $a$ справедливы следующие утверждения:
   1. если {упорядоченная пара множества $k$ и ноля стандартного линейно упорядоченного поля $a$ принадлежит интерпретации символа отношения $\leqslant$ на множестве $b$}, то упорядоченная пара {произведения множеств $j, k$} и {произведения множеств $i,k$} принадлежит интерпретации символа операции $\leqslant$ на множестве $b$,
   2. если {упорядоченная пара ноля стандартного линейно упорядоченного поля $a$ и множества $k$ принадлежит интерпретации символа отношения $\leqslant$ на множестве $b$}, то упорядоченная пара {произведения множеств $j, k$} и {произведения множеств $i,k$} принадлежит интерпретации символа операции $\leqslant$ на множестве $b$:

$\begin{cases} \Upsilon(a,b,c,d,e,f,g) \ \stackrel{\mathrm{def}}{=} \ \begin{cases} \forall h \quad h\in b \Rightarrow \Bigl( h \neq \mathrm{Neutral}(+_a) \Rightarrow \bigl( \forall i \quad i = \mathrm{Neutral}(+_a) \Rightarrow \Phi(a,b,c,d,e,f,g,h,i) \bigr) \Bigr)\\ \forall h \ \forall i \quad (h\in b \ \land \ i\in b) \Rightarrow \Bigl( \langle h,i \rangle\in \leqslant_a \Rightarrow \bigl( \forall j \quad j\in b \Rightarrow (\Chi(a,b,c,d,e,f,g,h,i,j) \ \land \ \Psi(a,b,c,d,e,f,g,h,i,j)) \bigr) \Bigr) \end{cases}\\ \Phi(a,b,c,d,e,f,g,h,i) \ \stackrel{\mathrm{def}}{=} \ \begin{cases} \langle h,i \rangle\in \leqslant_a \Rightarrow \bigl( \forall j \quad j = \mathrm{Inverse}_{\,\cdot_{\, a}}(h) \Rightarrow \langle j,i \rangle\in \leqslant_a \bigr)\\ \langle i,h \rangle\in \leqslant_a \Rightarrow \bigl( \forall j \quad j = \mathrm{Inverse}_{\,\cdot_{\, a}}(h) \Rightarrow \langle i,j \rangle\in \leqslant_a \bigr)\\ \end{cases}\\ \Chi(a,b,c,d,e,f,g,h,i,j) \ \stackrel{\mathrm{def}}{=} \ \forall k \quad k = \mathrm{Neutral}(+_a) \Rightarrow \Bigl( \langle j,k \rangle\in \leqslant_a \Rightarrow \bigl\langle \cdot_{\, a}(i,j),\cdot_{\, a}(h,j) \bigr\rangle\in \leqslant_a \Bigr)\\ \Psi(a,b,c,d,e,f,g,h,i,j) \ \stackrel{\mathrm{def}}{=} \ \forall k \quad k = \mathrm{Neutral}(+_a) \Rightarrow \Bigl( \langle k,j \rangle\in \leqslant_a \Rightarrow \bigl\langle \cdot_{\, a}(h,j),\cdot_{\, a}(i,j) \bigr\rangle\in \leqslant_a \Bigr)\\ \end{cases}$

Обозначим $\Upsilon(a,b,c,d,e,f,g) \ \stackrel{\mathrm{def}}{=} \ a\in \mathrm{MultAssocLinOrdField}(b;\leqslant;+,\cdot)$.

Согласованное стандартное линейно упорядоченное поле

• $a,b,c,d,e,f,g$ - множества,
• $d = \langle e,f,g \rangle$ - упорядоченная тройка,
• $d = \mathrm{\Sigma}(e,f,g)$ - сигнатура,
• $\leqslant\in e \ \land \ e(\leqslant) = 2_\mathrm{N}$ - символ бинарного отношения,
• $(+\in f \ \land \ e(+) = 2_\mathrm{N}) \ \land \ (\cdot\in f \ \land \ e(\cdot) = 2_\mathrm{N})$ - символы бинарных операций,
• $a = \langle b,c,d \rangle$ - упорядоченная тройка,
• $a = \mathrm{AlgStruct}(b,c,d)$ - алгебраическая структура,
• $a\in \mathrm{LinOrdField}(b; \leqslant; +,\cdot)$ - стандартное линейно упорядоченное поле.

Линейно упорядоченное стандартное поле $a$ — согласованное стандартное линейно упорядоченное поле (англ. associated standard linearly ordered field, нем. angeschlossen standard linear geordnete Körper), если стандартное линейно упорядоченное поле $a$ является согласованным по сложению стандартным линейно упорядоченным полем и стандартное линейно упорядоченное поле $a$ является согласованным по умножению стандартным линейно упорядоченным полем:

$\Upsilon(a,b,c,d,e,f,g) \ \stackrel{\mathrm{def}}{=} \ a\in \mathrm{AddAssocLinOrdField}(b; \leqslant; +,\cdot) \ \land \ a\in \mathrm{MultAssocLinOrdField}(b; \leqslant; +,\cdot)$

Обозначим $\Upsilon(a,b,c,d,e,f,g) \ \stackrel{\mathrm{def}}{=} \ a\in \mathrm{AssocLinOrdField}(b;\leqslant;+,\cdot)$.