{"id":"dee05b9b-5115-4991-819a-8c5e4ca77b6f","arxiv_id":"1908.05528","paper_version":4,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Vector spaces equipped with a bilinear product are shown to form Kripke-style frames whose subspace lattices are complete residuated lattices, yielding a complete vector space semantics for the modal non-associative Lambek calculus.","lead":"This paper interprets algebras over a field, vector spaces with a bilinear product, as Kripke frames for the modal Lambek calculus, and proves completeness and correspondence results for this vector space semantics. A generalist might read it because it connects the algebraic machinery of substructural logic to the vector-based models used in computational linguistics.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 6.2(3) can fail for admissible choices of ν_k: residual preservation is not guaranteed, so the embedding proof of Theorem 6.1 is incomplete.","rationale":"The reader's weakest_assumption pointed at the embedding lemma, which is indeed the load-bearing step, but the specific failure is not in the R relation: it is in the proof of Lemma 6.2(3), where membership of a linear combination in h(p_k) is taken to imply membership of every summand. That inference is false in general because the products e^m_j ⋆ e^i_j are basis vectors and can cancel. My counterexample uses only the paper's own construction with a permissible surjective ν_3 and a standard finite commutative residuated chain, so it is internal to the proof, not an external objection. I am not claiming Theorem 6.1 is false; a more careful choice of ν may salvage the completeness theorem. But the proof as written asserts existence of a D.NL♦-morphism h for every finite modal residuated poset, and a single admissible choice where h fails to preserve residuals means the argument does not go through. Therefore the reader's ACCEPT should be conditional on repairing Lemma 6.2.","tokens_in":16022,"tokens_out":30030,"duration_ms":279264,"concrete_test":"Reproduce the finite residual-algebra check: with P as above and ν_3 exactly as listed, compute in S(V) the subspace h(2)\\h(2) = {z : ∀w∈h(2), w⋆z∈h(2)}. Test z=e^2_1-e^2_2. For w=e^2_1,...,e^2_4 the row calculation gives 0, 0, e^2_1-e^2_2, e^2_4-e^2_1, and for w∈h(1) the product has upper index at most 2, so every product lies in h(2). Since z∉h(1), the claimed equality h(2\\2)=h(2)\\h(2) fails. If confirmed, Lemma 6.2 needs a substantive fix (e.g., constrained ν) before Theorem 6.1 can be accepted.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The weakest link is Lemma 6.2(3), not the R relation. In the proof of the converse inclusion, the authors infer from Σ α (e^m_j ⋆ e^i_j) ∈ h(p_k) that each summand e^m_j ⋆ e^i_j is in h(p_k). This inference is invalid because the summands are basis vectors and can cancel. The freedom in choosing the surjective maps ν_k is enough to make the residual fail. Concretely, let P be {1<2<3<4} with p_i⊗p_j=p_{min(i+j-1,4)} and identity modality, n=4. Choose ν_3 by: ν_3(1,1)=ν_3(1,2)=e^3_1, ν_3(2,1)=ν_3(2,2)=e^3_2, ν_3(3,1)=e^2_1, ν_3(3,2)=e^2_2, ν_3(3,3)=e^3_3, ν_3(3,4)=e^2_3, ν_3(4,1)=e^2_4, ν_3(4,2)=e^2_1, ν_3(4,3)=e^2_2, ν_3(4,4)=e^3_4, and complete with any ν_1,ν_2,ν_4 satisfying the stated diagonal condition. Then u=e^2_1-e^2_2 satisfies for every w∈h(2) that w⋆u∈h(2), so u∈h(2)\\h(2), while h(2\\2)=h(1) does not contain u. Hence the constructed h is not a D.NL♦-morphism. Since Lemma 6.2 is the only bridge from finite modal residuated posets to subspace lattices, Theorem 6.1 is not established by the proof given.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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).","tokens_in":16367,"tokens_out":12354,"duration_ms":115436,"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":[{"comment":"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":"Section 6, Lemma 6.2(3)"},{"comment":"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.","section":"Section 6, definition of R"}],"minor_comments":[{"comment":"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":"Section 4, Proposition 4.4(1)"},{"comment":"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":"Section 4, Proposition 4.4(3)"},{"comment":"The notation 'e(p_m)' appears where 'h(p_m)' is meant.","section":"Section 6, Lemma 6.2(2)"},{"comment":"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":"Section 4.1, Fact 4.5"},{"comment":"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.","section":"Section 6, Lemma 6.2(4)"}],"recommendation":"major_revision","confidential_remarks":"The paper is potentially valuable, but the completeness theorem is not yet established because of the gap in Lemma 6.2(3). The counterexample I give is internal to the construction; I do not see evidence that the theorem itself is false, and a more careful choice of the maps \\nu_k may repair the proof. I would be willing to look at a revised version."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Let me get to the point. The headline result—completeness of D.NL♦ over finite-dimensional modal K-algebras—is not proved. Lemma 6.2(3) has a cancellation problem. In the converse direction the authors take a specific w = Σ_j e^m_j and deduce from w⋆u ∈ h(p_k) that each e^m_j ⋆ e^i_j lies in h(p_k). That inference fails when several products collapse onto the same basis vector and their coefficients cancel. This is not a cosmetic issue. Here is a small admissible example: P = {1<2<3<4} with p_i⊗p_j = p_{min(i+j-1,4)}. Choose ν_3 so that ν_3(2,2)=e^3_2 while keeping surjectivity (this is easy to do; the stress-test's own ν_3 missed some e^1_j, but that can be fixed). Then u = e^2_1 - e^2_2 satisfies w⋆u = 0 for every w ∈ h(2), so u ∈ h(2)\\h(2), but h(2\\2)=h(1) does not contain u. So h is not a D.NL♦-morphism for that admissible choice of ν_k, and Lemma 6.2(3) is false as stated. Since the embedding lemma is the only bridge in Theorem 6.1, the completeness theorem is not established by this paper.\n\nThat is the main thing. The rest of the paper is on much firmer ground. The core idea—reading a K-algebra as a Routley-Meyer frame via the subspace closure nucleus—is genuinely new and it pays off in Section 4, where the quasi-variety correspondences (Prop 4.4) are clean and correct. The applications to quaternions and octonions are nice, and the modal extension in Section 5 is a sensible adaptation. Those parts deserve publication. The writing is dense in places (Section 6's R is hard to verify, some notation typos like '1=[1]' in the proof of Prop 4.4(3)), but the proofs there check out.\n\nThe reader's report gave soundness 8.0 and accepted; I don't agree. The flaw is in the central theorem. The authors need another constraint on ν_k or a different embedding argument. The theorem may still be true, but the paper as written doesn't show it. I would send it to a serious referee—the framework is worth engaging—but the verdict should be major revision, not acceptance. The correspondence results alone would be a solid paper, but the completeness claim needs to be fixed or qualified.","headline":"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.","tokens_in":16967,"tokens_out":11238,"would_cite":false,"duration_ms":91198,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B47","06F07","03G10"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["Lambek calculus","vector space semantics","K-algebras","modal residuated lattices","Kripke frames","substructural logics","finite model property","display calculus"],"falsifier":"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.","tokens_in":15772,"feed_emoji":"🧮","tokens_out":13085,"duration_ms":117196,"temperature":0.7,"pith_summary":"This paper tries to establish that the modal non-associative Lambek calculus — the type-logical grammar calculus D.NL✸ — can be given a genuine vector-space semantics, not just the commutative tensor-product semantics usually used in distributional linguistics. The key move is to regard a $K$-algebra (a vector space with a bilinear product) as a Kripke-style frame whose propositions are subspaces. Bilinearity of the product makes the subspace lattice into a complete residuated lattice, so all Lambek connectives — fusion and its two residuals — are interpretable on subspaces. The main theorem states that a sequent is provable in D.NL✸ exactly when it is valid in every finite-dimensional modal $K$-algebra. This matters because it is a step toward a semantics in which lexical and derivational meaning live in the same linear-algebraic structure.","feed_headline":"Vector spaces can serve as Kripke frames for modal Lambek logic","feed_subtitle":"A sequent is provable in the modal Lambek display calculus exactly when it holds in all finite-dimensional algebras over a field.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the completeness and finite model property of D.NL✸ with respect to finite modal residuated posets, which Theorem 6.1 lifts to modal $K$-algebras.","marker":"[16]"},{"why":"Provides the nucleus representation lemma for residuated lattices that justifies defining the subspace lattice of a $K$-algebra as a complete residuated lattice.","marker":"[15]"},{"why":"Extends the nucleus representation to the modal setting, supporting the diamond and box construction on subspaces of a modal $K$-algebra.","marker":"[2]"},{"why":"Gives the powerset-algebra completeness precedent for generalized Lambek calculi that the paper's embedding explicitly mirrors in Remark 6.4.","marker":"[3]"},{"why":"Introduces the proper display-calculus setting in which D.NL✸ is formulated, so its structural rules underlie the sequent-level completeness claim.","marker":"[32]"}],"fun_headline_variants":["Modal Lambek logic: vector spaces as Kripke frames","Finite-dimensional algebras give modal Lambek completeness","Vector spaces prove completeness for modal Lambek logic","From posets to vector spaces: a completeness proof","Vector space semantics for full Lambek calculus"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Modal Lambek logic: vector spaces as Kripke frames","Finite-dimensional algebras give modal Lambek completeness","Vector spaces prove completeness for modal Lambek logic","From posets to vector spaces: a completeness proof","Vector space semantics for full Lambek calculus"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000398,"raw_usage":{"total_tokens":2081,"prompt_tokens":945,"completion_tokens":1136,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":561,"completion_tokens_details":{"reasoning_tokens":1062}},"tokens_in":561,"tokens_out":1136,"duration_ms":10021,"temperature":1.0,"reasoning_tokens":1062,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:11:30.331184+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Algebraic proof theory for LE-logics","cited_arxiv_id":"1808.04642","evidence_quote":"Supplies the completeness and finite model property of D.NL✸ with respect to finite modal residuated posets, which Theorem 6.1 lifts to modal $K$-algebras."},{"cited_title":"Galatos, P","cited_arxiv_id":null,"evidence_quote":"Provides the nucleus representation lemma for residuated lattices that justifies defining the subspace lattice of a $K$-algebra as a complete residuated lattice."},{"cited_title":"Buszkowski","cited_arxiv_id":null,"evidence_quote":"Extends the nucleus representation to the modal setting, supporting the diamond and box construction on subspaces of a modal $K$-algebra."},{"cited_title":"Buszkowski","cited_arxiv_id":null,"evidence_quote":"Gives the powerset-algebra completeness precedent for generalized Lambek calculi that the paper's embedding explicitly mirrors in Remark 6.4."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces the proper display-calculus setting in which D.NL✸ is formulated, so its structural rules underlie the sequent-level completeness claim."}],"review_version":1}