Superabelian logics

Take an evaluation e such that, for each \xi \in \Gamma, we have e(\xi) \geq 0. Then clearly e(\xi \lor \ensuremath{\varphi}) \geq 0 ({\ensuremath{\boldsymbol {\mathit{A}}}} has a lattice reduct). Thus by our assumption for \ensuremath{\psi}=\ensuremath{\varphi}, we know that e(\ensuremath{\varphi}) = e(\ensuremath{\varphi} \lor \ensuremath{\varphi}) \geq 0.

For the converse implication, take an evaluation e such that e(\xi \lor \ensuremath{\psi}) \geq 0 for each \xi \in \Gamma. Since we assume that {\ensuremath{\boldsymbol {\mathit{A}}}} is linearly ordered, we can derive that either e(\ensuremath{\psi}) \geq 0 or, for all \xi \in \Gamma, we have e(\xi) \geq 0. In the latter case, the assumption \Gamma \vDash_{\ensuremath{\boldsymbol {\mathit{A}}}} \ensuremath{\varphi} gives us e(\ensuremath{\varphi}) \geq 0 and so in both cases we have e(\ensuremath{\varphi} \lor \ensuremath{\psi}) \geq 0.

As {\ensuremath{\ensuremath{\mathrm {Ab}}}} has a countable presentation, it suffices to prove that \vee is a strong disjunction which, thanks to Theorem 2.11, follows if we prove that {\ensuremath{\mathrm{(Adj)}}}^\lor and {\ensuremath{\mathrm{(MP)}}}^\lor are valid in {\ensuremath{\ensuremath{\mathrm {Ab}}}}.

For the first one, let A be an Abelian \ell-group and e an {\ensuremath{\boldsymbol {\mathit{A}}}}-evaluation such that e(\ensuremath{\varphi} \lor \xi) \geq 0 and e(\ensuremath{\psi} \lor \xi) \geq 0. Then, by the assumptions and distributivity of the lattice operations, we have:

To prove the validity of {\ensuremath{\mathrm{(MP)}}}^\lor, consider an evaluation e such that 0 \leq e(\ensuremath{\varphi} \lor \xi) and 0 \leq e((\ensuremath{\varphi} \rightarrow \ensuremath{\psi}) \lor \xi). This gives us 0=e(\ensuremath{\varphi} \lor \xi) \land 0=e((\ensuremath{\varphi} \rightarrow \ensuremath{\psi}) \lor \xi) \land 0. Using the distributivity of the lattice operations, we obtain

For simplicity, let us set e(\ensuremath{\varphi} \land \ensuremath{\mathtt{t}}) = a, e(\ensuremath{\psi}) = b, e(\xi \land \ensuremath{\mathtt{t}}) = c and e((\ensuremath{\varphi}\rightarrow \ensuremath{\psi}) \land \ensuremath{\mathtt{t}})=d. As in \ell-groups it holds (a \lor b) + c= (a+c) \lor (b+c), we obtain

Note that, due to monotonicity of addition, we have

Therefore, we obtain 0 \leq b \lor c=e(\ensuremath{\psi}) \lor e(\xi \wedge \ensuremath{\mathtt{t}}) \leq e(\ensuremath{\psi} \lor \xi) as required.

We first show the implication from 1 to 2. Let e be an evaluation such that we have e(\ensuremath{\varphi}) \ngeq 0. We set a=-e(\ensuremath{\varphi}) and b=-e(\ensuremath{\psi}). Since {\ensuremath{\boldsymbol {\mathit{A}}}} is Archimedean and a\nleq 0, there is an n \in \ensuremath{\mathbb{N}} such that n \cdot a \nleq b. Consequently, there is an n \in \ensuremath{\mathbb{N}} such that n \cdot e(\ensuremath{\varphi}) \ngeq e(\ensuremath{\psi}); thus e(\ensuremath{\psi} \rightarrow n \cdot \ensuremath{\varphi}) \ngeq 0. This shows that (Arch) holds.

To show the implication from 2 to 1, we assume that {\ensuremath{\boldsymbol {\mathit{A}}}} is not Archimedean. Therefore, there exist a,b \in A such that a \nleq 0 and n \cdot a \leq b for each n \in \ensuremath{\mathbb{N}}. Consider an evaluation e such that e(\ensuremath{\varphi})=-a and e(\ensuremath{\psi})=-b. Then, for each n \in \ensuremath{\mathbb{N}}, we have n \cdot e(\ensuremath{\varphi}) \geq e(\ensuremath{\psi}) and thus e(\ensuremath{\psi} \rightarrow n \cdot \ensuremath{\varphi}) \geq 0 for each n \in \ensuremath{\mathbb{N}}. However, by assumption, e(\ensuremath{\varphi})=-a \ngeq 0 and thus (Arch) fails in {\ensuremath{\boldsymbol {\mathit{A}}}}.

The rest of the statement follows from Lemma 2.10.

Let us denote the logic {\ensuremath{\ensuremath{\mathrm {Ab}}}}+\ensuremath{\mathrm{(Arch)}}^\lor\! by \ensuremath{\mathrm L}. First note that, by Corollary 2.13, we know that \ensuremath{\mathrm L} is a semilinear logic and so it is strongly complete with respect to the class \mathbf{Alg}^{\ell}(\ensuremath{\mathrm L}), which, due to the previous lemma, consists of linearly ordered Archimedean \ell-groups. By Hölder’s Theorem [Holder:Axiome], each such \ell-group is embeddable into \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}} and so the proof follows.

Since the logic {\ensuremath{\ensuremath{\mathrm {rAb}}}}+\ensuremath{\mathrm{(str_\gamma)}}^\lor satisfies the conditions from Corollary 2.13, it is semilinear. Since {\ensuremath{\ensuremath{\mathrm {rAb}}}}+\ensuremath{\mathrm{(str_\gamma)}}^\lor is an extension of {\ensuremath{\ensuremath{\mathrm {rAb}}}}, we obtain that {\ensuremath{\ensuremath{\mathrm {rAb}}}}+\ensuremath{\mathrm{(str_\gamma)}}^\lor is strongly complete w.r.t. some subclass of \ensuremath{\mathbf{S}}(\ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}).

We need the following technical observation:

First, let us take an arbitrary {\ensuremath{\boldsymbol {\mathit{A}}}} \in \mathbb K. We show that {\ensuremath{\boldsymbol {\mathit{A}}}} satisfies \ensuremath{\mathrm{(str_\gamma)}}^\lor. By the observation and the definition of {{\mathbb K}}, if, for a,b \in A, we have q_j \cdot a \leq b and b \leq r_j \cdot a for each j \in \ensuremath{\mathbb{N}}, then it must be that a=0. Thus, any evaluation in {\ensuremath{\boldsymbol {\mathit{A}}}} that satisfies the premise of \ensuremath{\mathrm{(str_\gamma)}} must map \ensuremath{\varphi} to 0, thereby satisfying the conclusion \ensuremath{\varphi} \rightarrow \ensuremath{\mathtt{t}}. Therefore, \ensuremath{\mathrm{(str_\gamma)}} is valid in {\ensuremath{\boldsymbol {\mathit{A}}}}. Since {\ensuremath{\boldsymbol {\mathit{A}}}} is a chain, by Lemma 2.10 \ensuremath{\mathrm{(str_\gamma)}}^{\lor} is also valid in {\ensuremath{\boldsymbol {\mathit{A}}}}, and thus {\ensuremath{\boldsymbol {\mathit{A}}}} is a model of {\ensuremath{\ensuremath{\mathrm {rAb}}}}+\ensuremath{\mathrm{(str_\gamma)}}^\lor.

To prove the other direction, assume for an algebra {\ensuremath{\boldsymbol {\mathit{1}}}} \neq {\ensuremath{\boldsymbol {\mathit{A}}}} \subseteq \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}} that there exist a,b \in A such that b=\gamma \cdot a and a \neq 0. Clearly, \gamma \cdot (-a)=-b holds as well. Since {\ensuremath{\boldsymbol {\mathit{A}}}} is totally ordered, we can assume without loss of generality that a > 0. By the observation, this implies that for each j \in \ensuremath{\mathbb{N}}, q_j \cdot a \leq b and b \leq r_j \cdot a. But since a,b \in A and a > 0, this is a counterexample to the validity of rule \ensuremath{\mathrm{(str_\gamma)}} in {\ensuremath{\boldsymbol {\mathit{A}}}}. By Lemma 2.10, \ensuremath{\mathrm{(str_\gamma)}}^\lor fails in {\ensuremath{\boldsymbol {\mathit{A}}}} as well. This shows {\ensuremath{\boldsymbol {\mathit{A}}}} is not a model of {\ensuremath{\ensuremath{\mathrm {rAb}}}}+\ensuremath{\mathrm{(str_\gamma)}}^\lor.

It is a well-known result that the transcendence degree of \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}} over \ensuremath{{\ensuremath{\boldsymbol {\mathit{Q}}}}} is 2^\omega. From this, it follows that there are 2^{2^\omega} distinct subfields of \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}} that are field extensions of \ensuremath{{\ensuremath{\boldsymbol {\mathit{Q}}}}}. We argue that the \ell-group reduct of each such field is a model of a different infinitary extension of {\ensuremath{\ensuremath{\mathrm {Ab}}}}. Let {\ensuremath{\boldsymbol {\mathit{A}}}} and {\ensuremath{\boldsymbol {\mathit{B}}}} be the \ell-group reducts of two distinct subfields of \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}} that are field extensions of \ensuremath{{\ensuremath{\boldsymbol {\mathit{Q}}}}}. Without loss of generality, assume that there is a \gamma \in A \setminus B such that 0 < \gamma. By Proposition 3.5, an \ell-subgroup of \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}} validates the rule \ensuremath{\mathrm{(str_\gamma)}}^\lor if and only if b=\gamma \cdot a \implies a=0 for all a,b in the corresponding \ell-subgroup. Since {\ensuremath{\boldsymbol {\mathit{A}}}} and {\ensuremath{\boldsymbol {\mathit{B}}}} are the \ell-group reducts of subfields of \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}, this condition holds if and only if \gamma is not an element of their respective universes. Hence we obtain that the rule \ensuremath{\mathrm{(str_\gamma)}}^\lor is valid in {\ensuremath{\boldsymbol {\mathit{B}}}} but is not valid in {\ensuremath{\boldsymbol {\mathit{A}}}}. This shows that \vDash_{\ensuremath{\boldsymbol {\mathit{A}}}} and \vDash_{\ensuremath{\boldsymbol {\mathit{B}}}} are different logics.

Let {\ensuremath{\boldsymbol {\mathit{A}}}} be a non-trivial linearly ordered Archimedean Abelian \ell-group. We want to show that (IDC) is valid in {\ensuremath{\boldsymbol {\mathit{A}}}} if and only if {\ensuremath{\boldsymbol {\mathit{A}}}} is isomorphic to \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}. By the previous proposition, (IDC) is valid in {\ensuremath{\boldsymbol {\mathit{A}}}} if and only if {\ensuremath{\boldsymbol {\mathit{A}}}} has only the trivial strongly decreasing sequence.

Since {\ensuremath{\boldsymbol {\mathit{A}}}} is an Archimedean chain, by Lemma ?, ?, having only the trivial strongly decreasing sequence is equivalent to having no strictly decreasing sequence of positive elements.

Thus, it suffices to show that a non-trivial linearly ordered Archimedean \ell-group {\ensuremath{\boldsymbol {\mathit{A}}}} has no strictly decreasing sequence of positive elements if and only if {\ensuremath{\boldsymbol {\mathit{A}}}} \cong \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}.

Clearly, \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}} has no decreasing sequences of positive elements. To show the other implication, one has to argue that \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}} is the only non-trivial linearly ordered Archimedean \ell-group with no strictly decreasing sequences of positive elements. We can assume, by Hölder’s Theorem, that without loss of generality, \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}} \subseteq {\ensuremath{\boldsymbol {\mathit{A}}}} \subseteq \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}} and {\ensuremath{\boldsymbol {\mathit{A}}}} is not isomorphic to \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}. We have to distinguish two cases.

1. Let \zeta \in\mathbb R\setminus \mathbb Q be an element of A. Without loss of generality we can assume \zeta>1. Since 1 \in A, we can generate recursively the following sequence. We start with r_0=\zeta and r_1=1. For n> 0, we define k_n=\lfloor \frac{r_{n-1}}{r_n} \rfloor and let r_{n+1}=r_{n-1}-k_n \cdot r_n. By the properties of division, 0 \leq r_{n+1}<r_n for all n \geq 1. This means that the sequence \ensuremath{\langle{r_n}\rangle}_{n \in \ensuremath{\mathbb{N}}} is strictly decreasing. Furthermore, because \zeta is irrational, the ratio \frac{r_n}{r_{n+1}} is irrational for each n \in \ensuremath{\mathbb{N}}. This shows that this algorithm never terminates with a zero remainder; thus, r_n>0 for all n.

2. {\ensuremath{\boldsymbol {\mathit{A}}}} \subseteq \mathbb \ensuremath{{\ensuremath{\boldsymbol {\mathit{Q}}}}}. Since {\ensuremath{\boldsymbol {\mathit{A}}}} is not isomorphic to \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}, {\ensuremath{\boldsymbol {\mathit{A}}}} is not generated by any single element. Thus, for each 0<a_n \in A, there is a 0<b_n \in A such that a_n does not generate b_n. If b_n<a_n we set a_{n+1}=b_n; otherwise, we set k_n=\lfloor \frac{b_{n}}{a_n} \rfloor and a_{n+1}=b_n- k_n \cdot a_n. Thus, we have constructed 0<a_{n+1}<a_n. This allows us to build the desired sequence, and therefore we finish the proof.

To prove the first claim, it suffices to show the strictness. Assume that a_i=a_{i+1} for some i \in \ensuremath{\mathbb{N}}. Then the inequality a_i \geq 2 \cdot a_{i+1} becomes a_i \geq 2 \cdot a_i and thus 0 \geq a_i. Since also a_i \geq 0, we obtain a_i=0. For each j > i we have a_i \geq a_j \geq 0, thus we get a_j=0 as well. Similarly, for j < i, there is an n \in \ensuremath{\mathbb{N}} such that n \cdot a_i \geq a_j \geq 0 and thus again a_j=0. Therefore, the sequence {\ensuremath{\langle{a_i}\rangle}}_{i \in \ensuremath{\mathbb{N}}} has to be trivial, a contradiction.

We will prove the second claim. Let us assume that {\ensuremath{\boldsymbol {\mathit{A}}}} is an Archimedean chain and {\ensuremath{\langle{a_i}\rangle}}_{i \in \ensuremath{\mathbb{N}}} is a strictly decreasing sequence of positive elements. Without loss of generality, as {\ensuremath{\boldsymbol {\mathit{A}}}} is Archimedean, we can assume that {\ensuremath{\boldsymbol {\mathit{A}}}} \subseteq \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}, by Hölder’s Theorem. We construct a non-trivial strongly decreasing sequence {\ensuremath{\langle{b_i}\rangle}}_{i \in \ensuremath{\mathbb{N}}}. Set b_0 > 0 arbitrarily. We will define the rest of the sequence recursively. Assume that we have already constructed \ensuremath{\langle{b_i}\rangle}_{i \leq n} satisfying the conditions from the definition of a strongly decreasing sequence. Now we want a b_{n+1} such that 0< 2 \cdot b_{n+1}\leq b_n.

Since {\ensuremath{\langle{a_i}\rangle}}_{i \in \ensuremath{\mathbb{N}}} is a strictly decreasing sequence, it follows that there exists a j \in \ensuremath{\mathbb{N}} such that \frac{a_j}{b_n} \notin \mathbb Z (otherwise \ensuremath{\langle{\frac{a_j}{b_n}}\rangle}_{j \in \ensuremath{\mathbb{N}}} would be a strictly decreasing sequence of positive elements in \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}, which is not possible).

Since {\ensuremath{\boldsymbol {\mathit{A}}}} is Archimedean, there is a k \in \ensuremath{\mathbb{N}} such that 0 \leq a_j -k \cdot b_n < b_n. Since \frac{a_j}{b_n} \notin \mathbb Z, we have 0 \neq a_j -k \cdot b_n and thus 0 < a_j -k \cdot b_n < b_n. Hence,

Therefore, we set

Clearly, b_{n+1}>0 and 2 \cdot b_{n+1}\leq b_n. The second condition for strong decreasing sequences easily follows from the fact that {\ensuremath{\boldsymbol {\mathit{A}}}} is Archimedean. Thus, {\ensuremath{\langle{b_i}\rangle}}_{i \in \ensuremath{\mathbb{N}}} is a non-trivial strongly decreasing sequence.

First, assume that {\ensuremath{\boldsymbol {\mathit{A}}}} has a non-trivial strongly decreasing sequence {\ensuremath{\langle{a_i}\rangle}}_{i \in \ensuremath{\mathbb{N}}} and note that w.l.o.g. we can assume that n_i = 4 for each i (if for some i we have a_i > 4\cdot a_{i+1}, expand the sequence by putting 2\cdot a_{i+1} in a proper place, and repeat …). Let us consider the {\ensuremath{\boldsymbol {\mathit{A}}}}-evaluation e induced by setting e(x_i) = a_i. Clearly, all the premises of (IDC) are valid but we have e(x_0 \rightarrow \ensuremath{\mathtt{t}}) = - a_0 < 0 and thus the rule (IDC) is not valid in {\ensuremath{\boldsymbol {\mathit{A}}}}.

Conversely, assume that the rule (IDC) is not valid in {\ensuremath{\boldsymbol {\mathit{A}}}}, i.e., we have an evaluation e such that if we set e(\ensuremath{\varphi}_i) = a_i the validity of premises of (IDC) tells us that 4 \cdot a_{i+1} \geq a_{i} \geq 2 \cdot a_{i+1}, i.e., {\ensuremath{\langle{a_i}\rangle}}_{i \in \ensuremath{\mathbb{N}}} is a strongly decreasing sequence and, by the failure of the conclusion of the rule, we have a_0 > 0, i.e., the sequence is non-trivial.

Assume that \Gamma\not\vdash_{\ensuremath{\ensuremath{\mathrm {pAb}}}}\ensuremath{\varphi}. Given an \ensuremath{\mathcal L}_{\ensuremath{\ensuremath{\mathrm {pAb}}}}-formula \ensuremath{\psi}, we define a \ensuremath{\mathcal L}_{\ensuremath{\ensuremath{\mathrm {Ab}}}}-formula \ensuremath{\psi}' by replacing all occurrences of \ensuremath{\mathtt{f}} by an arbitrary fixed variable p not occurring in \Gamma\cup\{\ensuremath{\varphi}\}. Let us denote \Gamma'=\{\ensuremath{\psi}' \mid \ensuremath{\psi} \in \Gamma\}. Then, clearly, \Gamma'\not\vdash_{\ensuremath{\ensuremath{\mathrm {Ab}}}}\ensuremath{\varphi}' and so \Gamma'\not\vDash_{\ensuremath{\boldsymbol {\mathit{A}}}}\ensuremath{\varphi}' as witnessed by an evaluation e which entails \Gamma\not\vDash_{{\ensuremath{\boldsymbol {\mathit{A}}}}_{e(p)}}\ensuremath{\varphi}.

If \mathbf{A}_a and \mathbf{A}_b are isomorphic, the isomorphism must preserve the underlying natural order, which trivially forces the designated units a and b to have the same sign; hence a \cdot b > 0. For the other direction, assume a \cdot b > 0. Then \frac{b}{a} > 0, and the mapping h\colon x \mapsto \frac{b}{a} \cdot x is an order-preserving group automorphism mapping a to b, providing the needed isomorphism.

One direction is obvious. To prove the converse one, let us assume a \neq b. To show that \ensuremath{\mathbf{HSP}}(\ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}_a) \neq \ensuremath{\mathbf{HSP}}(\ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}_b), it is sufficient to find an equation which is valid in one of the generating algebras, \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}_a or \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}_b, but not in the other. If a<0 and b \geq 0 take the equation \ensuremath{\mathtt{f}} \geq 0. This equation clearly holds in \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}_b but it does not hold in \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}_a. The case a \leq 0 and b>0 is similar. Therefore, it remains to check the cases where a,b>0 or a,b<0. We will check only the first case (the second one is analogous). Moreover, let us assume without loss of generality that 0 <a<b.

Consider the following equation:

This equation is not valid in \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}_b, since if we take an evaluation e such that e(x)=1 we get (a \cdot e(x) -b) \lor (-e(x))=(a-b) \lor -1 < 0. Thus the equation (*) does not hold in \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}_b.

We show the same equation holds in \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}_a. First let us consider an evaluation e such that e(x) \leq 0. Clearly, we get -e(x) \geq 0 and thus (a \cdot e(x) - a) \lor e(-x) \geq 0. It remains to consider an evaluation e such that e(x)>0 (and thus e(x) \geq 1). Then a \cdot e(x) -a \geq a \cdot 1-a=0. Thus the equation (*) is valid in \ensuremath{{\ensuremath{\boldsymbol {\mathit{Z}}}}}_a.

By Corollary 2.13, it is enough to check that (\ensuremath{\mathtt{f}} \lor \ensuremath{\varphi}) \lor \ensuremath{\psi} \mathrel{\blacktriangleright} \ensuremath{\varphi} \lor \ensuremath{\psi} is valid in \ensuremath{\ensuremath{\mathrm {Lu}}}. This clearly follows from the use of rules \ensuremath{\mathrm{(A_\lor)}} and \ensuremath{\mathtt{f}} \lor \ensuremath{\varphi} \mathrel{\blacktriangleright} \ensuremath{\varphi}.

The implications from 1 to 2 and from 1 to 3 are clear (note that in the second case we need to use linearity of {\ensuremath{\boldsymbol {\mathit{A}}}} to obtain that if \ensuremath{\mathtt{f}}^{\ensuremath{\boldsymbol {\mathit{A}}}} \not\geq 0 and \ensuremath{\mathtt{f}} \vee \ensuremath{\varphi} \geq 0, then \ensuremath{\varphi} \geq 0). We prove the converse ones at once by contradiction: assume that \ensuremath{\mathtt{f}} \vDash_{\ensuremath{\boldsymbol {\mathit{A}}}} \varphi (resp. that \ensuremath{\mathtt{f}}\vee \varphi \vDash_{\ensuremath{\boldsymbol {\mathit{A}}}} \varphi) and \ensuremath{\mathtt{f}}^{\ensuremath{\boldsymbol {\mathit{A}}}} \geq 0. For an arbitrary element a and any evaluation e(\varphi) = a, the premises of both rules are trivially valid and so we obtain a \geq 0, a contradiction with the assumption that {\ensuremath{\boldsymbol {\mathit{A}}}} \neq {\ensuremath{\boldsymbol {\mathit{1}}}}.

We prove the final part of the claim, the rest then follows from Lemma 4.4. Using Theorem 4.3 and Corollary 2.17, we know that

Clearly, for any non-trivial element of \ensuremath{\mathbf{ISP}}_\mathrm{U}(\{{\ensuremath{\boldsymbol {\mathit{A}}}}_{a} \mid a \geq 0\}), we have \ensuremath{\mathtt{f}}^{{\ensuremath{\boldsymbol {\mathit{A}}}}_{a}}\geq 0 (an equation preserved by ultrapowers) and thus it is not a member of \mathbf{Alg}^{\ell}(\ensuremath{\mathrm \ensuremath{\ensuremath{\mathrm {Lu}}}}) due to the previous lemma. Thus

and so the proof is done by Corollary 2.17.

By Corollary 2.13, the logic \ensuremath{\ensuremath{\mathrm {Lu}}}_{\infty} is semilinear. Since \ensuremath{\ensuremath{\mathrm {Lu}}}_{\infty} is an expansion of {\ensuremath{\ensuremath{\mathrm {rAb}}}}, every linearly ordered \ensuremath{\ensuremath{\mathrm {Lu}}}_{\infty}-algebra is a pointed Archimedean \ell-group. Since \ensuremath{\ensuremath{\mathrm {Lu}}}_{\infty} is an extension of \ensuremath{\ensuremath{\mathrm {Lu}}}, by Lemma 5.3, we know that in any non-trivial {\ensuremath{\boldsymbol {\mathit{A}}}} linearly ordered \ensuremath{\ensuremath{\mathrm {Lu}}}_{\infty}-algebra we have \ensuremath{\mathtt{f}}^{\ensuremath{\boldsymbol {\mathit{A}}}} < 0. Thus, {\ensuremath{\boldsymbol {\mathit{A}}}} has to be a pointed Archimedean \ell-group with a negative point a. Thus, by Hölder’s Theorem [Holder:Axiome], there is an embedding h of the \ensuremath{\mathtt{f}}-free reduct of {\ensuremath{\boldsymbol {\mathit{A}}}} into \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}. Clearly h can be seen as an embedding of {\ensuremath{\boldsymbol {\mathit{A}}}} into \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}_{h(a)}. As h(a) < 0, we know that \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}_{h(a)} is isomorphic to \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}_{-1} (Lemma 4.4). Therefore, \mathbf{Alg}^{\ell}(\ensuremath{\mathrm \ensuremath{\ensuremath{\mathrm {Lu}}}_{\infty}}) \subseteq \ensuremath{\mathbf{IS}}(\ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}_{-1}). Since \ensuremath{\ensuremath{\mathrm {Lu}}}_{\infty} is semilinear and \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}_{-1} is an \ensuremath{\ensuremath{\mathrm {Lu}}}_{\infty}-algebra it follows that \ensuremath{\ensuremath{\mathrm {Lu}}}_{\infty} is strongly complete with respect to \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}_{-1}.

Recall that, thanks to the known completeness properties, we can replace the syntactical consequence relations by semantical ones w.r.t. algebras {\mathchoice{\mbox{\bf\L}}{\mbox{\bf\L}}{\mbox{\bf\scriptsize\L}}{\mbox{\bf\tiny\L}}} and {\ensuremath{\boldsymbol {\mathit{\ensuremath{\ensuremath{\mathrm {Lu}}}}}}} (because it is an isomorphic copy of \ensuremath{{\ensuremath{\boldsymbol {\mathit{R}}}}}_{-1}).

Let us consider any mapping e of propositional variables into reals and define the mapping \bar e as its restriction to [0,1], i.e.,

We denote by (\bar e)^{\mathchoice{\mbox{\bf\L}}{\mbox{\bf\L}}{\mbox{\bf\scriptsize\L}}{\mbox{\bf\tiny\L}}} and e^{\ensuremath{\boldsymbol {\mathit{Lu}}}} the corresponding evaluations. By a simple proof by induction over the complexity of formula \ensuremath{\chi}, we obtain:

Clearly, it holds for variables and constants by definition of \bar e and \tau. Now assume (\bar e)^{\mathchoice{\mbox{\bf\L}}{\mbox{\bf\L}}{\mbox{\bf\scriptsize\L}}{\mbox{\bf\tiny\L}}}(\alpha) = e^{\ensuremath{\boldsymbol {\mathit{Lu}}}}(\tau(\alpha)) and (\bar e)^{\mathchoice{\mbox{\bf\L}}{\mbox{\bf\L}}{\mbox{\bf\scriptsize\L}}{\mbox{\bf\tiny\L}}}(\beta) = e^{\ensuremath{\boldsymbol {\mathit{Lu}}}}(\tau(\beta)) for formulas \alpha,\beta. We want to show that (\bar e)^{\mathchoice{\mbox{\bf\L}}{\mbox{\bf\L}}{\mbox{\bf\scriptsize\L}}{\mbox{\bf\tiny\L}}}(\alpha \circ \beta) = e^{\ensuremath{\boldsymbol {\mathit{Lu}}}}(\tau(\alpha \circ \beta)) for \circ \in \{\land,\lor,\ensuremath{\mathbin{\&}},\rightarrow\}. We show this step only for \circ=\ensuremath{\mathbin{\&}}. We write:

Now we can prove the left-to-right direction of the first equivalence. Assume that \Gamma\vDash_{{\mathchoice{\mbox{\bf\L}}{\mbox{\bf\L}}{\mbox{\bf\scriptsize\L}}{\mbox{\bf\tiny\L}}}} \ensuremath{\varphi} and that e is a mapping such that for each \gamma\in \Gamma we have (recall that \ensuremath{\mathtt{t}}^{\ensuremath{\boldsymbol {\mathit{LU}}}} = 1)

As e^{\ensuremath{\boldsymbol {\mathit{Lu}}}}(\tau(\gamma)) = (\bar e)^{\mathchoice{\mbox{\bf\L}}{\mbox{\bf\L}}{\mbox{\bf\scriptsize\L}}{\mbox{\bf\tiny\L}}}(\gamma) we have (\bar e)^{\mathchoice{\mbox{\bf\L}}{\mbox{\bf\L}}{\mbox{\bf\scriptsize\L}}{\mbox{\bf\tiny\L}}}(\gamma) = 1 for \gamma\in\Gamma and so, by the assumption, also (\bar e)^{\mathchoice{\mbox{\bf\L}}{\mbox{\bf\L}}{\mbox{\bf\scriptsize\L}}{\mbox{\bf\tiny\L}}}(\ensuremath{\varphi}) = 1, which entails e^{\ensuremath{\boldsymbol {\mathit{\ensuremath{\ensuremath{\mathrm {Lu}}}}}}}(\tau(\ensuremath{\varphi})) = 1.

To prove the converse direction, it suffices to note that if the co-domain of e is a subset of [0,1], then e = \bar e.

The second equivalence can either be proved in exactly the same way or actually follows from the first one and the fact that on finite sets of premises the Ł ukasiewicz (unbound) logic coincides with its infinitary variant.

Consider an arbitrary {\ensuremath{\boldsymbol {\mathit{A}}}}_a-evaluation e_1\colon\ensuremath{\mathit{Fm}_{\!\ensuremath{\mathcal L_{{\ensuremath{\ensuremath{\mathrm {pAb}}}}}}}} \longrightarrow {\ensuremath{\boldsymbol {\mathit{A}}}}_a. Clearly, e_1 extends the evaluation e_0\colon\ensuremath{\mathit{Fm}_{\!\ensuremath{\mathcal L_{{\ensuremath{\ensuremath{\mathrm {Ab}}}}}}}} \longrightarrow {\ensuremath{\boldsymbol {\mathit{A}}}}. Clearly there is a unique evaluation e_2\colon\ensuremath{\mathit{Fm}_{\!\ensuremath{\mathcal L_{{\ensuremath{\ensuremath{\mathrm {pAb}}}}}}}} \longrightarrow {\ensuremath{\boldsymbol {\mathit{A}}}}_{-a} extending e_0 such that e_1(\ensuremath{\mathtt{f}})=-e_2(\ensuremath{\mathtt{f}})=e_2(-\ensuremath{\mathtt{f}}) and e_1(x)=e_2(x) for all variables x. By induction one can show that e_1(\ensuremath{\psi}) =e_2(\tau(\ensuremath{\psi}) ) for each formula \ensuremath{\psi} \in \ensuremath{\mathit{Fm}_{\!\ensuremath{\mathcal L_{{\ensuremath{\ensuremath{\mathrm {pAb}}}}}}}}. Therefore, e_1(\ensuremath{\psi}) \geq 0 iff e_2(\tau(\ensuremath{\psi}) ) \geq 0. From this, one can easily derive the statement of this theorem.