Correspondence Theory on Vector Spaces

This paper extends correspondence theory to the framework of \(\mathbb {K}\)-algebras, i.e. vector spaces endowed with a bilinear operation, seen as ‘Kripke frames’. For every \(\mathbb {K}\)-algebra, the lattice of its subspaces can be endowed with the structure of a complete (non necessarily monoidal) residuated lattice. Hence, a sequent of the logic of residuated lattices can be interpreted as a property of its lattice of subspaces. Thus, correspondence theory can be developed between the propositional language of this logic and the first order language of \(\mathbb {K}\)-algebras, analogously to the well known correspondence theory between classical normal modal logic and the first-order language of Kripke frames. In this paper, we develop such a theory for the class of analytic inductive inequalities.

1. 1.

   An element \(x\ne \bot \) of a lattice L is completely join irreducible whenever for any set \(A \subseteq L\), \(x = \bigvee A\) implies \(x \in A\).

2. 2.

   A \(+\) (resp. −) sign in a node u of \(+s\) (resp. \(-t\)) indicates that s (resp. t) is monotone w.r.t. the subterm rooted in u, while a − (resp. \(+\)) sign indicates that is antitone.

3. 3.

   Although we use the symbol \(\backslash \) to denote both a connective in the language and the substitution symbol, in the remainder of the paper no ambiguity ever arises, since the terms in substitutions will not contain any explicit occurrence of \(\backslash \).

4. 4.

   An order type over the variables of a term specifies which polarity serves to compute the minimal valuation for each variable [6]. Hence, \(\varepsilon \)-critical nodes are the occurrences of the variables in such polarities.

5. 5.

   The acronym PIA means positive implies atomic. It was first introduced in [1] and used as in this context in [6]. The acronym SRR stands for syntactical right residual.

6. 6.

   The canonical extension \(\mathbb {L}^\delta \) of a preresiduated lattice \(\mathbb {L}\) is a completion of \(\mathbb {L}\), with a lattice embedding \(e: \mathbb {L} \rightarrow \mathbb {L}^\delta \). The canonical extension of a lattice \(\mathbb {L}\) is a quantale which is join-generated (resp. meet generated) by the set \(K(\mathbb {L}^\delta )\) (resp. \(O(\mathbb {L}^\delta )\)) of elements which are in the meet closure (resp. join closure) in \(\mathbb {L}^\delta \) of \(e[\mathbb {L}]\), which are called closed (resp. open) elements. Furthermore, the operations \(\cdot \), \(/\), and \(\backslash \) are extended to \(\mathbb {L}^\delta \) in such a way that they still satisfy residuation rules; hence,

   $$\begin{aligned} \begin{array} {ccccr} \bigvee \nolimits _{s \in S} s \cdot a = \bigvee \nolimits _{s \in S} (s \cdot a) &{}\quad \quad &{} a \cdot \bigvee \nolimits _{s \in S} s = \bigvee \nolimits _{s \in S} (a \cdot s) &{}\quad \quad &{} \text {for every a}\in \mathbb {L}^\delta , S \subseteq \mathbb {L}^\delta , \\ \bigwedge \nolimits _{s \in S} s /a = \bigwedge \nolimits _{s \in S} (s /a) &{}\quad \quad &{} a /\bigvee \nolimits _{s \in S} s = \bigwedge \nolimits _{s \in S} (a /s) &{}\quad \quad &{} \text {for every a}\in \mathbb {L}^\delta , S \subseteq \mathbb {L}^\delta , \\ \bigvee \nolimits _{s \in S} s \backslash a = \bigwedge \nolimits _{s \in S} (s \backslash a) &{}\quad \quad &{} a \backslash \bigwedge \nolimits _{s \in S} s = \bigwedge \nolimits _{s \in S} (a \backslash s) &{}\quad \quad &{} \text {for every a}\in \mathbb {L}^\delta , S \subseteq \mathbb {L}^\delta . \\ \end{array} \end{aligned}$$

   It can be shown that \(\mathbb {L}^\delta \) is join generated (resp. meet generated) by a subset of \(K(\mathbb {L}^\delta )\) (resp. \(O(\mathbb {L}^\delta )\)), i.e., the set \(J^\infty (\mathbb {L}^\delta )\) (resp. \(M^\infty (\mathbb {L}^\delta )\)) of completely join irreducible (resp. completely meet irreducible) elements of \(\mathbb {L}^\delta \) (see [7, Corollary 2.10]).

7. 7.

   For all \(A, B \subseteq \mathbb {L^\delta }\), \(\bigvee A \le \bigwedge B\) iff \((\forall a \in A)(\forall b \in B) a \le b\).

8. 8.

   The Ackermann Lemma in this setting implies that for any residuated lattice \(\mathbb {L}\), any variable p, and any formulas \(\alpha ,\beta _1,\ldots , \beta _n\), \(\gamma _1,\ldots ,\gamma _n\), \(\xi \), and \(\zeta \) such that p does not occur in \(\alpha \), is positive in each \(\beta _i\) and \(\zeta \), and negative in each \(\gamma _i\) and \(\xi \), the following quasi-inequalities are equivalent in \(\mathbb {L}\)

   $$\begin{aligned} \alpha \le p, \beta _1\le \gamma _1,\ldots ,\beta _n\le \gamma _n\Rightarrow \xi \le \zeta \quad \text { iff }\quad (\beta _1\le \gamma _1,\ldots ,\beta _n\le \gamma _n\Rightarrow \xi \le \zeta )[\alpha /p]. \end{aligned}$$

   The conditions on the polarity of each variable in the other inequalities are trivially satisfied here. The condition that states that the eliminated variable does not occur in \(\alpha \) (in this case it is equivalent to saying that \(p_i\) does not occur in \(\bigvee M_i[\bigvee M_1/p_1]\cdots [\bigvee M_{i-1} / p_{i-1}]\)) is implied by item 2 of Definition 2 (see [6]).

Authors and Affiliations

1. Vrije Universiteit Amsterdam, Amsterdam, The Netherlands

   Alessandra Palmigiano, Mattia Panettiere & Ni Wayan Switrayni

2. Department of Mathematics and Applied Mathematics, University of Johannesburg, Johannesburg, South Africa

   Alessandra Palmigiano

Corresponding author

Correspondence to Mattia Panettiere .

Editors and Affiliations

1. University of Bern, Bern, Switzerland

   George Metcalfe

2. University of Bern, Bern, Switzerland

   Thomas Studer

3. Federal University of Pernambuco, Recife, Brazil

   Ruy de Queiroz

A Examples

The present section collects some examples that showcase the results in the paper.

Example 2

The inequality \((p\vee q)\otimes (r/(p\otimes q))\le (q\otimes (p\vee r))/((p\backslash q)\vee r)\) is analytic \((\varOmega ,\varepsilon )\)-inductive for \(\varepsilon (p,q,r)=(1,1,1)\) and \(p<q<r\). By distributing \(\otimes \) over \(\vee \) and following the fact that / is join reversing on its right coordinate, we get the inequality:

which is equivalent to the system

By residuation, the system can be rewritten as follows (thus reaching the shape in Lemma 5)

Using notation in Lemma 5, the first inequality has shape \(\varphi (\overline{x})[ \overline{\xi }/ \overline{x}] \le \bigvee _i \beta _i(\overline{r_i})\), where \(\varphi (x_1, x_2, x_3) := (x_1 \otimes x_2) \otimes x_3\), \(\xi _1 := \alpha _1(p) := p\), \(\xi _2 := \alpha _2(r, p, q) = r /(p \otimes q)\), \(\xi _3 := \alpha _3(p, q) := p \backslash q\), \(\beta _1(q, p) := q \otimes p\), and \(\beta _2(q, r) := q \otimes r\).

Example 3

The inequality \((((q\otimes r)\backslash p)\vee s)\otimes ((s\backslash q)\otimes (p/s))\le ((p/(s\otimes r))\backslash (p\otimes s))\wedge ((s\otimes (p\otimes q))/((p/s)\wedge r))\) is analytic \((\varOmega ,\varepsilon )\)-inductive with \(\varepsilon (p,q,r,s)=(\partial ,1,\partial ,1)\) and \(s<q<p<r\). By distributing \(\otimes \) over \(\vee \) we get

which is equivalent (by also applying residuation) to the system:

Example 4

Let us find the correspondent of the first inequality in the system in Example 2. First we show that it is equivalent to a quasi-left primitive.

Hence, by Theorem 3, the inequality correspond to the \(\mathcal {L}_\textrm{FO}\)-formula

Example 5

The inequality \((p\otimes (q/r))\otimes ((s\backslash q)\wedge (s/t))\le (t\wedge (r/s))\backslash (t \otimes (p\vee q))\) is analytic \((\varOmega ,\varepsilon )\)-inductive for \(\varepsilon (p,q,r,s,t)=(\partial ,\partial ,\partial ,\partial ,1)\) and \(t<q<r<s\), \(t<p\). By distributing \(\otimes \) over \(\vee \) and applying the residuation rule, we get

We show by the procedure in Sect. 3.2 that the inequality is inductive also for \(\varepsilon '(p,q,r,s,t) = (1,1,1,1,1)\). The definite positive PIAs in the formula are

hence, the sets \(Q_v\) are

Of course, \(\varepsilon ^{(0)}(p, q, r, s, t) = (\partial , \partial , \partial , \partial , 1)\) and \(\varOmega ^{(0)}\) is the smallest relation for which it is inductive, i.e. \(\{ (t, p), (t, q), (r, s), (q, r), (q, s), (t, r), (t, s) \}\).

The following table represents the steps of the procedure. At the i-th step, a variable \(v_i\) such that \(\varepsilon ^{(i-1)}(v_i) = \partial \) maximal w.r.t. \(\varOmega ^{(i - 1)}\) is picked, all the edges where it is an endpoint are removed from \(\varOmega ^{(i - 1)}\) (this is denoted by \(\varOmega ^{(i - 1)-}\)), and the edges in \(Q_{v_i} \times \{v_i\}\) are added in \(\varOmega ^{(i)}\).

By Lemma 6, the inequality is \((\varepsilon ^{(i)}, \varOmega ^{(i)})\)-inductive for every \(i \in \{0, 1, 2, 3, 4 \}\).

Reprints and permissions

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics