REVIEW 2 major objections 5 minor 32 references
Vector spaces as Kripke frames
T0 review · 2 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash
Pith's one-line read The paper proves that the modal non-associative Lambek calculus is complete with respect to finite-dimensional algebras over a field, read as Kripke frames.
desk verdict The framework is fresh and the correspondence results are solid, but the completeness theorem rests on an invalid cancellation step in Lemma 6.2(3) and is not established. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing mechanism is the subspace lattice of a $K$-algebra together with the closure operator that sends a set of vectors to the subspace it spans. Bilinearity of the product makes this closure operator a nucleus for the set-level product of two sets of vectors, and a nucleus on a powerset gives a complete residuated lattice of closed sets. For the modal expansion, a compatible relation on the underlying vector space, satisfying the three linearity conditions (L1R)-(L3R), defines the diamond and box operators on subspaces. Lemma 6.2 then shows how to choose the basis, the bilinear product, and the relation so that a map $h$ from a given finite modal residuated poset into this subspace lattice preserves all the connectives and is an order embedding.
What would settle it
Take a small finite modal residuated poset, such as the four-element Boolean lattice with a non-trivial diamond, and run the construction of Section 6 to check whether the embedding clause for the diamond holds: the image of the modal operation in the subspace lattice must equal the closure of the relation-applied image. If these two subspaces ever differ, the embedding lemma fails and the completeness theorem does not follow.
Extended reading notes
Core claim
The central claim is a completeness theorem: any sequent of the display calculus D.NL✸ that is valid in every finite-dimensional modal $K$-algebra over a field $K$ is provable in D.NL✸. The proof is a representation result: every finite modal residuated poset can be embedded, preserving order, fusion, residuals, diamond, and box, into the lattice of subspaces of a finite-dimensional modal $K$-algebra. Because D.NL✸ is already complete and has the finite model property with respect to finite modal residuated posets, this embedding transfers validity in those posets to validity in finite-dimensional modal $K$-algebras. The construction is explicit: it builds a vector space of dimension $n^2$ from an $n$-element poset, with basis vectors indexed by pairs of poset elements.
Load-bearing premise
The argument depends on the relation $R$ defined just before Lemma 6.2 realizing the modal order of every finite modal residuated poset; the paper states that $R$ satisfies the required frame conditions immediately, but if some modal poset escapes this construction, the completeness theorem does not follow.
Editorial extensions
If this is right
- Every sequent valid in all finite-dimensional modal $K$-algebras is provable in D.NL✸, so the display calculus and the vector-space semantics agree on the full modal non-associative Lambek fragment.
- The fusion connective can be interpreted as a genuine bilinear product on a vector space, so non-commutative and non-associative syntactic behaviour need not be collapsed to the commutative tensor product used in earlier vector-space models.
- The subspace lattice of every modal $K$-algebra is a complete modal residuated lattice, placing vector-space semantics inside the standard ternary-relational semantics for substructural logics.
- The first-order conditions of Section 4 characterize exactly when the subspace semantics validates commutativity, associativity, unitality, and related identities; the quaternion and octonion algebras provide concrete failures of commutativity and associativity respectively.
Reading between the lines
- If the theorem is right, the explicit construction makes non-derivability decidable in principle: every non-provable sequent is refuted in a finite-dimensional modal $K$-algebra whose dimension is bounded by the square of the size of a finite modal residuated poset, so an exhaustive search can in principle settle derivability.
- The correspondence results suggest that analytic structural rules such as controlled associativity and commutativity can be read as inequalities on the bilinear product; this gives a route to search for vector-space models that validate one structural rule but not another.
- Because the authors note that finiteness of the poset is used only for the dimension of the vector space, the embedding should lift to arbitrary modal residuated posets, yielding a canonical possibly infinite-dimensional modal $K$-algebra into which the Lindenbaum-Tarski algebra of D.NL✸ embeds; checking this would give a single vector-space model that characterizes the whole logic.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes a vector-space (K-algebra) semantics for the modal non-associative Lambek calculus D.NL◘. It views a K-algebra (V,⋆) as a Routley-Meyer-style frame, using the closure operator on the powerset of V to obtain the lattice of subspaces S(V) as a complete residuated lattice, and extends this to modal K-algebras with a relation R. The main results are Sahlqvist-style correspondence statements (Proposition 4.4 and Proposition 5.7) and a claimed completeness theorem (Theorem 6.1) for D.NL◘ with respect to finite-dimensional modal K-algebras. The proof of Theorem 6.1 proceeds by embedding every finite modal residuated poset into the subspace lattice of a finite-dimensional modal K-algebra via an explicit construction (Lemma 6.2).
Significance. The conceptual move of treating K-algebras as Kripke frames is attractive and connects compositional distributional semantics with display logic and substructural logics. The paper contains some clean and well-presented arguments, especially Lemma 3.1 and Proposition 4.4, and the concrete examples with quaternions and octonions are instructive. If the embedding lemma can be repaired, the completeness theorem would be a valuable contribution. However, the completeness theorem currently rests on Lemma 6.2, and the proof of that lemma has a load-bearing gap; the paper does not provide machine-checked proofs, but the explicit construction is otherwise reproducible.
major comments (2)
- [Section 6, Lemma 6.2(3)] The proof of the converse inclusion is invalid. From (\Sigma_j e^m_j) \star (\Sigma_{i,j} \alpha^i_j e^i_j) \in h(p_k) the authors infer that each e^m_j \star e^i_j \in h(p_k) because 'every element has a unique representation given a base.' That inference is not legitimate: the left-hand side is a linear combination of basis vectors, and cancellations among the coefficients can occur. The lemma is in fact false for admissible choices of the maps \nu_k. For P = {1<2<3<4}, p_i \otimes p_j = p_{\min(i+j-1,4)}, identity modality, n=4, choose \nu_3 so that \nu_3(1,1)=\nu_3(1,2)=e^3_1, \nu_3(2,1)=\nu_3(2,2)=e^3_2, \nu_3(3,1)=e^2_1, \nu_3(3,2)=e^2_2, \nu_3(3,3)=e^3_3, \nu_3(3,4)=e^2_3, \nu_3(4,1)=e^2_4, \nu_3(4,2)=e^2_1, \nu_3(4,3)=e^2_2, \nu_3(4,4)=e^3_4, and choose any \nu_1,\nu_2,\nu_4 satisfying the stated diagonal condition. Then u=e^2_1-e^2_2 satisfies w \star u \in h(2) for every w \in h(2), so u \in h(2)\setminus h(2), while h(2\setminus 2)=h(1) does not contain u. Thus h is not a D.NL\u25d8-morphism for this admissible choice of \nu. Since Lemma 6.2 is the only bridge between finite modal residuated posets and subspace lattices, the proof of Theorem 6.1 does not go through as written. The same problem affects clause (4), whose proof is the same.
- [Section 6, definition of R] The sentence 'It is immediate that R satisfies the properties of Definition 5.1' is not backed by a proof. The relation R is defined by sums of basis vectors with arity conditions and inequalities p_{k_i} \leq \diamondsuit p_{m_i} and j_i \neq j_k, and the verification of (L1R)-(L3R), in particular the existential quantifiers in (L2R), is not shown. Because Lemma 6.2(5)-(6) and hence the modal part of the completeness theorem depend on this relation, a detailed verification should be supplied.
minor comments (5)
- [Section 4, Proposition 4.4(1)] The displayed equality in the left-to-right direction should be [u] \otimes [v] = [v] \otimes [u], not [u] \otimes [v] = [v] \otimes [v].
- [Section 4, Proposition 4.4(3)] The phrase 'let 1 \in V such that 1 = [1]' is a typo; the intended statement is that the unit is a one-dimensional subspace identified with the vector 1.
- [Section 6, Lemma 6.2(2)] The notation 'e(p_m)' appears where 'h(p_m)' is meant.
- [Section 4.1, Fact 4.5] In the proof of Fact 4.5, 'it follows that \alpha = 1 and a = -1' should read 'it follows that \alpha = 1 and \alpha = -1'.
- [Section 6, Lemma 6.2(4)] The proof of item (4) is omitted with the words 'the same as item 3'; since item (3) itself needs repair, item (4) should be proved explicitly in the revision.
Circularity Check
No significant circularity: the completeness proof constructs finite-dimensional modal K-algebras explicitly from arbitrary finite modal residuated posets, without feeding the target sequents into the construction.
full rationale
The paper's central completeness theorem (Theorem 6.1) is established by an explicit embedding of any finite modal residuated poset P into the subspace lattice S(V) of a finite-dimensional modal K-algebra. The vector space V, the bilinear product ⋆, and the relation R are all defined directly from P and its order/fusion structure, with the choice functions ν_k and the compatibility relation R stated independently of any particular sequent X ⇒ Y. The proof of Lemma 6.2 verifies that h preserves the order, fusion, residuals, and modal operators; although parts of that verification (especially Lemma 6.2(3)) may be open to correctness objections, the construction is not circular because the target equations are never used as inputs. The only externally cited ingredient is the finite model property of D.NL✸ with respect to modal residuated posets, cited to [16]; that result is parameter-free, does not assume completeness with respect to modal K-algebras, and is itself a theorem about the display calculus rather than a re-statement of the paper's conclusion. Hence no step reduces by construction to its own inputs, and there is no fitted parameter renamed as a prediction. Possible gaps in Lemma 6.2 are correctness risks, not circularity.
Assumptions & free parameters
assumptions (4)
- domain assumption D.NL◸ has the finite model property with respect to modal residuated posets (cited as [16, Theorem 49]).
- standard math A nucleus on a partially ordered monoid induces a complete residuated lattice (cited as [15, Lemma 3.33]).
- standard math The display calculus D.NL◸ is sound and complete with respect to modal residuated posets, and its Lindenbaum-Tarski algebra is a modal residuated poset (cited as [16, Prop. 9]).
- domain assumption The relation R in a modal K-algebra is assumed to satisfy compatibility conditions (L1R)-(L3R) from Definition 5.1.
Cite this review
Pith. "Pith review of Vector spaces as Kripke frames." pith.science (2026). https://pith.science/paper/J67D7DXP
@misc{pith2026190805528,
author = {Pith},
title = {Pith review of: Vector spaces as Kripke frames},
year = {2026},
howpublished = {\url{https://pith.science/paper/J67D7DXP}},
note = {Machine review of arXiv:1908.05528}
}
abstract
In recent years, the compositional distributional approach in computational linguistics has opened the way for an integration of the \emph{lexical} aspects of meaning into Lambek's type-logical grammar program. This approach is based on the observation that a sound semantics for the associative, commutative and unital Lambek calculus can be based on vector spaces by interpreting fusion as the tensor product of vector spaces. In this paper, we build on this observation and extend it to a `vector space semantics' for the \emph{general} Lambek calculus, based on \emph{algebras over a field} $\mathbb{K}$ (or $\mathbb{K}$-algebras), i.e. vector spaces endowed with a bilinear binary product. Such structures are well known in algebraic geometry and algebraic topology, since they are important instances of Lie algebras and Hopf algebras. Applying results and insights from duality and representation theory for the algebraic semantics of nonclassical logics, we regard $\mathbb{K}$-algebras as `Kripke frames' the complex algebras of which are complete residuated lattices. This perspective makes it possible to establish a systematic connection between vector space semantics and the standard Routley-Meyer semantics of (modal) substructural logics.
Reference graph
Works this paper leans on
- [1]
-
[2]
W. Buszkowski. Interpolation and FEP for logics of residuated algebras. Logic Journal of IGPL, 19:437–454, 2011
work page 2011
-
[3]
W. Buszkowski. On involutive nonassociative Lambek cal culus. Journal of Logic, Language and Information , 28(2):157–181, 2019
work page 2019
-
[4]
J. Chen, G. Greco, A. Palmigiano, and A. Tzimoulis. Non normal logics: Semantic analysisand prooftheory. In d. Q. R. Iemhoff R., MoortgatM.,editor, Logic, Language, Information, and Computation, WoLLIC 2019 , volume 11541 ofLNCS, pages 99–118. Springer, Berlin, Heidelberg, 2019. ArXiv:1903.04868
work page Pith review arXiv 2019
- [5]
- [6]
-
[7]
W. Conradie,S. Ghilardi, andA. Palmigiano. Unified Correspondence. InA. Baltagand S. Smets, editors,Johan van Benthem on Logic and Information Dynamics , volume 5 of Outstanding Contributions to Logic , pages 933–975. Springer International Publishing, 2014
work page 2014
-
[8]
W. Conradie and A. Palmigiano. Algorithmic correspondence and canonicity for non- distributive logics. Annals of Pure and Applied Logic , 170(9):923–974, 2019
work page 2019
Show all 32 references
-
[9]
Conradie, A
W. Conradie, A. Palmigiano, and A. Tzimoulis. Goldblatt-Thomason for LE-logics. Submitted, 2018. ArXiv:1809.08225
2018 arXiv
-
[10]
J. H. Conway and D. Smith.On Quaternions and Octonions: Their Geometry, Arith- metic, and Symmetry . AK Peters/CRC Press, 2003
2003
-
[11]
B. A. Davey and H. A. Priestley.Introduction to lattices and order . Cambridge univer- sity press, 2002
2002
-
[12]
O. Frink. Complemented modular lattices and projective spaces of infinite dimension. Transactions of the American Mathematical Society , 60(3):452–467, 1946. Greco, Liang, Moortgat, Palmigiano, and Tzimoulis
1946
-
[13]
Frittella, G
S. Frittella, G. Greco, A. Kurz, A. Palmigiano, and V. Sikimić. A multi-type display calculus for dynamic epistemic logic.Journal of Logic and Computation , 26(6):2017– 2065, 2016
2017
-
[14]
Frittella, G
S. Frittella, G. Greco, A. Palmigiano, and F. Yang. A multi-type calculus for inquisitive logic. In J. Väänänen, Å. Hirvonen, and R. de Queiroz, editor s, Logic, Language, Information, and Computation, WoLLIC 2016 , volume 9803 ofLNCS, pages 215–233. Springer Berlin Heidelberg, 2016
2016
-
[15]
Galatos, P
N. Galatos, P. Jipsen, T. Kowalski, and H. Ono. Residuated lattices: an algebraic glimpse at substructural logics , volume 151. Elsevier, 2007
2007
-
[16]
Greco, P
G. Greco, P. Jipsen, F. Liang, A. Palmigiano, and A. Tzimoulis. Algebraic proof theory for LE-logics. ArXiv:1808.04642, submitted, 2019
2019 arXiv
-
[17]
Greco, F
G. Greco, F. Liang, M. A. Moshier, and A. Palmigiano. Multi-type display calculus for semi De Morgan logic. In Logic, Language, Information, and Computation, WoLLIC 2017, volume 10388 ofLNCS, pages 199–215. Springer Berlin Heidelberg, 2017
2017
-
[18]
Greco, F
G. Greco, F. Liang, A. Palmigiano, and U. Rivieccio. Bilattice logic properly displayed. Fuzzy Sets and Systems , 363:138–155, 2019
2019
-
[19]
Greco, M
G. Greco, M. Ma, A. Palmigiano, A. Tzimoulis, and Z. Zhao. Unified correspondence as a proof-theoretic tool.Journal of Logic and Computation , 28(7):1367–1442, 2016
2016
-
[20]
Greco and A
G. Greco and A. Palmigiano. Lattice logic properly displayed. In Logic, Language, Information, and Computation, WoLLIC 2017 , volume 10388 ofLNCS, pages 153–169. Springer Berlin Heidelberg, 2017
2017
-
[21]
Greco and A
G. Greco and A. Palmigiano. Linear logic properly displ ayed. Submitted, ArXiv:1611.04181
-
[22]
B. Jónsson. On the representation of lattices. Mathematica Scandinavica, 1:193–206, 1953
1953
-
[23]
B. Jónsson. Modular lattices and Desargues’ theorem. Marhematica Scandinavica, 2:295–314, 1955
1955
-
[24]
Kubota and R
Y. Kubota and R. Levine. Gapping as like-category coordination. In D. Béchet and A. J. Dikovsky, editors,Logical Aspects of Computational Linguistics - 7th Interna tional Conference, LACL 2012, Nantes, France, July 2-4, 2012. Proc eedings, volume 7351 of Lecture Notes in Compu...
2012
-
[25]
J. Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154–170, 1958
1958
-
[26]
J. Lambek. On the calculus of syntactic types. In R. Jako bson, editor, Structure of Language and its Mathematical Aspects , volume XII ofProceedings of Symposia in Applied Mathematics, pages 166–178. American Mathematical Society, 1961
1961
-
[27]
S. Lang. Linear Algebra. Springer Undergraduate Texts in Mathematics and Technol- ogy. Springer, 1987
1987
-
[28]
Moortgat
M. Moortgat. Multimodal linguistic inference. Journal of Logic, Language and Infor- mation, 5(3-4):349–385, 1996
1996
-
[29]
Moortgat and G
M. Moortgat and G. Wijnholds. Lexical and derivationalmeaning in vector-based mod- Vector spaces as Kripke frames els ofrelativisation. InA. Cremers, T.van Gessel, andF. Roelofsen, editors,Proceedings of the 21st Amsterdam Colloquium , pages 55–64.ILLC, University of Amsterdam, 2017
2017
-
[30]
Morrill, O
G. Morrill, O. Valentín, and M. Fadda. The displacementcalculus. Journal of Logic, Language and Information, 20(1):1–48, 2011
2011
-
[31]
Sadrzadeh, S
M. Sadrzadeh, S. Clark, and B. Coecke. The Frobenius anatomy of word meanings I: Subject and object relative pronouns. Journal of Logic and Computation , pages 1293–1317, 2013
2013
-
[32]
H. Wansing. Displaying Modal Logic. Kluwer, 1998
1998
Reviewed August 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.