{"id":"3b9db2db-9b78-478f-8251-99215807d5ea","arxiv_id":"1908.05315","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Every effect algebra admits a subset-valued implication that forms a divisible strict unsharp residuated poset, and this structure is equivalent to the original effect algebra.","lead":"This paper defines a subset-valued implication operation on effect algebras, which are algebraic models of quantum logic, and proves it satisfies a generalized residuation property without requiring a lattice structure. It establishes an equivalence between effect algebras and a new class of ordered structures, making the construction sound.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the only soft spot is an under-specified set-valued extension of ⊙, which is a formalization gap rather than a mathematical flaw.","rationale":"The reader's weakest assumption correctly identifies the missing set-valued product as the main formal gap. However, the intended extension is transparent and the central identities check out under it; the gap does not indicate a false theorem. I therefore do not see a load-bearing mathematical objection that would change the acceptance. The concrete test would close the formalization gap by making the set-valued operations explicit and re-verifying the critical equalities.","tokens_in":10202,"tokens_out":36273,"duration_ms":376899,"concrete_test":"Add an explicit definition of the set-valued product, e.g. x⊙A := {x⊙a | a∈A, x′≤a} and A⊙B := (A′+B′)′ when A′≤B, then re-derive Theorem 4(viii) and the (C5) step of Theorem 7 line by line. If the equality a·(a→b)=L(a,b) still holds in an arbitrary effect algebra (for instance, check the 81 rows of the 9-element Example 15), the formalization gap is closed and the central claim is sound.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I read the central claim as: for every effect algebra E, C(E) with x⊙y=(x′+y′)′ (defined iff x′≤y) and x→y=x′+L(x,y) is a divisible strict unsharp residuated poset, with a converse construction and round-trip E(C(E))=E. I checked the proof of Theorem 7 against Theorem 4 and found the algebraic steps valid: Theorem 4(viii) follows from Lemma 2(v), and the C3 chain in Theorem 7 is a valid sequence of equivalences. The genuinely load-bearing weakness is formal: the paper defines set versions of + and →, but never defines the set-valued product x⊙A or A⊙B, even though Theorem 4(viii) writes a·(a→b), Definition 6(C3) writes U(x,y′)⊙y, and Definition 6(C5) writes x⊙(x→y). As written, the statement of Theorem 7 is therefore not fully checkable. The natural elementwise or de Morgan extension makes the identities true, and I found no counterexample, so this is a presentation gap, not a correctness failure. Theorem 9 also omits the proof that the induced order of E(C) equals the given order, but this follows from C2 monotonicity, so it is not a separate obstacle.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper introduces an implication connective on arbitrary effect algebras, defined by x→y := x′ + L(x, y), whose value is a subset rather than an element, together with a conjunction x⊙y := (x′ + y′)′ defined when x′ ≤ y. The authors define a class of 'strict unsharp residuated posets' via axioms (C1)–(C5), show in Theorem 7 that every effect algebra E can be organized into such a structure C(E), prove in Theorem 9 that every strict unsharp residuated poset gives an effect algebra E(C), and prove in Theorem 10 that E(C(E)) = E. The remainder of the paper develops deductive systems for Modus Ponens and a contraposition law for the new implication, with examples showing failure of the contraposition law in a non-lattice effect algebra and in a lattice effect algebra.","tokens_in":10539,"tokens_out":18291,"duration_ms":160628,"significance":"If correct, the paper's construction provides a uniform implication connective for arbitrary, possibly non-lattice, effect algebras, with a soundness guarantee that the passage to the residuated structure loses no information. The central algebraic verification is original and mostly self-contained, and the paper includes concrete examples, a full operation table for a nine-element effect algebra, and a negative result for contraposition. However, the formulation currently has a load-bearing formal gap: the set-valued extension of the product operation is never defined, and the proof of the converse construction (Theorem 9) is too compressed to verify as written.","major_comments":[{"comment":"The paper defines set-valued addition x + A and A + B, but never defines the set-valued product A⊙B or x⊙A, despite using U(x, y′)⊙y in (C3), x⊙(x→y) in (C5), and a·(a→b) in Theorem 4(viii). The proof of Theorem 7 also uses U(a, b′)⊙b and identifies it with (b→a′)′. Please define A⊙B elementwise (for example, {x⊙y | x∈A, y∈B, x′≤y}), verify that every set occurring in (C3) and (C5) satisfies the required definedness condition, and state the elementary set identities used in the C3 chain. Without these definitions, the statement of Definition 6 and the central equivalence in Theorem 7 are not fully checkable.","section":"Section 2, Definition 6, Theorem 4(viii), Theorem 7"},{"comment":"The proof says 'Obviously, (E1), (E2) and (E4) hold' and then asserts that the induced order of E(C) coincides with the order of C, but none of these statements is demonstrated. In particular, (E2) requires proving both the definedness equivalence ((x+y)+z is defined iff x+(y+z) is defined) and the equality of the two sums, using the partial-monoid associativity of ⊙. The claim about the induced order needs a proof from the second clause of (C2). The step (a⊙(a⊙0′)′)′ = 0′ in the proof of (E3) should be justified explicitly by applying (C2) with x = 0 and y = a. Please expand this proof.","section":"Theorem 9"},{"comment":"The equivalence between (C3) and Theorem 4(xi) is presented as a chain of equivalences that silently uses set-valued products, set complementation, and monotonicity of set addition. After the set product is defined, the chain should be rewritten with explicit references to the relevant set identities and to the conditions under which each step is defined, so that the reader can verify both directions without reconstructing the notation.","section":"Theorem 8, Definition 6"}],"minor_comments":[{"comment":"The phrase 'every productive logic is is equipped' contains a duplicated 'is'.","section":"Abstract"},{"comment":"The sentence 'effect algebras are considered as a logic of quantum mechanics' should be rephrased as 'as a logic' or 'as logics' for grammatical consistency.","section":"Section 1"},{"comment":"The equality L(a, b′+L(b, c)) = L(a, b′) should be justified with a one-line argument using 0 ∈ L(b, c); as written, it is not immediate from the notation.","section":"Theorem 5(ii)"},{"comment":"The statement 'Ded(E) is atomic' should be stated as 'the poset (Ded(E), ⊆) is atomic' for precision.","section":"Theorem 13(ii)"},{"comment":"References [2], [3], and [4] are listed as 'submitted'; if possible, the final version should update them to published versions or provide arXiv identifiers in the reference list.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is technically plausible, and the flaws identified above are fixable within the scope of a revision. The central Theorem 7 appears to be correct once the set-valued product is properly defined; the primary risk is the under-specification of set-valued operations, which occurs already in the statement of Definition 6, so the revision should address it in the definitions section rather than as a remark. The paper fits the scope of the journal as a contribution to algebraic logic and quantum structures."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear [colleague],\n\nThe headline result is real: Chajda and Länger define a subset-valued implication x→y := x′ + L(x,y) for every effect algebra, non-lattice included, and prove that the resulting structure C(E) is a divisible strict unsharp residuated poset. Theorems 7, 9, and 10 give a converse construction and the round trip E(C(E)) = E, so the concept is sound. That is a genuine extension of their earlier lattice and monotone results, and it answers their question (2) for arbitrary effect algebras.\n\nWhat the paper does well: the main construction is natural, the proof of Theorem 7 is a clean chain of equivalences using Theorem 4, and the examples (the 9-element non-lattice and the 6-element lattice) actually show where the anticipated laws fail. The deductive systems and contraposition material is secondary but competently done.\n\nThe soft spots are mostly formal. The paper uses set-valued extensions of the partial operations without defining them. Theorem 4(viii) writes a·(a→b), and Definition 6(C3) writes U(x,y′)⊙y; what x⊙A or A⊙B means is never stated. The natural elementwise extension makes the identities true, and I could not find a counterexample, so this is a presentation gap rather than a mathematical flaw, but it does make the statements not fully checkable as written. Relatedly, the proof of Theorem 9 omits the verification that the order induced by E(C) equals the given order, though that follows from C2. There are typos and compressed steps throughout, but none that obscure the central argument.\n\nThe self-citations to the authors' earlier work are appropriate; the new result is precisely the removal of the lattice/monotonicity assumptions.\n\nWho is this for? Colleagues in algebraic logic and quantum-logic semantics. It deserves a serious referee: the referee should ask for explicit set-valued operation definitions and a cleaned-up proof of Theorem 9, but the mathematical core should survive. I'd send it out.","headline":"New subset-valued implication for every effect algebra, with a sound two-way equivalence to strict unsharp residuated posets; the main remaining issue is under-specified set-valued notation.","tokens_in":11020,"tokens_out":2412,"would_cite":true,"duration_ms":22574,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03G25","03G12","03B47","06A11"],"pacs":[],"model":"deepseek-v4-flash","headline":"Every effect algebra—not just lattice-ordered ones—can be equipped with a sound, set-valued implication connective, and the construction recovers the original algebra when converted back.","keywords":["effect algebra","connective implication","unsharp adjointness","strict unsharp residuated poset","Modus Ponens","deductive system","unsharp contraposition law","quantum logic"],"falsifier":"A reader could settle the central claim by taking the 6-element lattice effect algebra of Example 17, forming $C(E)$ with the paper's definitions, and converting back: the recovered addition must have exactly the table of Example 17. Any mismatch would refute Theorem 10; likewise, direct computation of $x\\odot(x\\to y)$ versus $L(x,y)$ for incomparable elements would test the divisibility condition (C5).","tokens_in":9990,"feed_emoji":"🧮","tokens_out":7201,"duration_ms":71661,"temperature":0.7,"pith_summary":"Effect algebras are partial algebraic structures that model the effects of quantum-mechanical events and serve as algebraic semantics for quantum logic. A logic is productive only if it has an implication connective, but the natural candidate $x\\to y=x'+y$ works only in lattice-ordered cases and with definedness restrictions. This paper introduces a set-valued implication $x\\to y=x'+L(x,y)$ using the lower cone $L(x,y)$, together with a partial conjunction $x\\odot y=(x'+y')'$, and proves that every effect algebra becomes a 'divisible strict unsharp residuated poset' under these operations. The central result is the equivalence: starting from any effect algebra, building this structure, and converting back recovers the original partial addition, so the implication is sound rather than ad hoc. A sympathetic reader should care because it supplies a uniform implication for all effect algebras, not just lattice ones, and connects it to unsharp adjointness, Modus Ponens, and contraposition.","feed_headline":"Every effect algebra gets a sound implication connective","feed_subtitle":"A set-valued arrow built from lower cones works even without lattice structure and recovers the original algebra.","key_machinery":"The load-bearing mechanism is the lower-cone construction $L(x,y)$ and its extension to subsets. Since effect algebras need not be lattices, the meet $x\\wedge y$ may not exist; the lower cone replaces it by the set of all lower bounds. The implication $x\\to y=x'+L(x,y)$ is then always defined as a subset, and the conjunction $x\\odot y=(x'+y')'$ is defined exactly when the effect-algebra addition $x'+y'$ is defined. The 'strict unsharp residuated poset' packages these into a partial commutative monoid with an antitone involution, unsharp adjointness (C3), and divisibility (C5); the equivalence of (C3) with the exchange property (xi) is what makes the proof of Theorem 7 work via Theorem 4.","core_discovery":"The paper's central discovery is that the subset-valued implication $x\\to y:=x'+L(x,y)$, where $L(x,y)$ is the lower cone $\\{z:z\\le x\\text{ and }z\\le y\\}$, is the right connective for arbitrary effect algebras. Together with the partial conjunction $x\\odot y:=(x'+y')'$ defined exactly when $x'\\le y$, it satisfies an 'unsharp adjointness': $U(x,y')\\odot y\\subseteq UL(y,z)$ if and only if $U(x,y')\\subseteq U(y\\to z)$, and the divisibility condition $x\\odot(x\\to y)=L(x,y)$. Theorem 7 proves every effect algebra $E$ gives a divisible strict unsharp residuated poset $C(E)$; Theorem 9 proves the converse construction from any such poset yields an effect algebra; and Theorem 10 proves $E(C(E))=E$. Thus the implication, despite returning a set of values rather than a single element, is logically sound and carries the full information of the original partial addition.","pith_inferences":["Not stated in the paper, but the set-valued reading of implication suggests a possible-worlds semantics: each element of $x\\to y$ is a truth value at least $x'$ and compatible with the lower cone of $x$ and $y$, so one could try to prove a completeness theorem for the resulting logic against effect-algebra models.","A natural extension would be to internalize the implication by choosing a canonical representative of each set, for instance the least element $x'$; the paper's results imply that such a selection cannot preserve full unsharp adjointness, since the adjointness is stated for the sets themselves.","Because Theorem 8 shows unsharp adjointness and the exchange property (xi) are equivalent, one could test whether either condition alone, together with divisibility, characterizes effect algebras among ordered structures; the paper does not pursue that characterization."],"forward_implications":["Because Theorem 7 applies to every effect algebra, the set-valued implication gives a uniform logical connective for both lattice and non-lattice effect algebras, without requiring meets or joins.","Theorem 10's round-trip identity means the subset-valued implication is not an ad hoc extension: the original partial addition can be recovered from the induced strict unsharp residuated poset, so the implication encodes the algebra's structure.","In any proper deductive system, the unsharp Modus Ponens rule is equivalent to the system being disjoint from its own complement (Theorem 12), giving a clean syntactic characterization.","The unsharp contraposition law holds for comparable elements in every effect algebra (Proposition 14), and for lattice effect algebras it is equivalent to $x'+(x\\wedge y)=y+(x'\\wedge y')$ (Proposition 16).","Boolean algebras, viewed as effect algebras, satisfy the unsharp contraposition law, whereas the 6-element lattice example fails it."],"supporting_citations":[{"why":"Introduces effect algebras and the partial-addition axiomatization (E1)–(E4) on which the whole construction is built.","marker":"[7]"},{"why":"Prior work by the authors defining unsharp residuation in effect algebras; the present implication is the non-lattice generalization of that approach.","marker":"[4]"},{"why":"Shows lattice effect algebras are conditionally residuated, the restricted case this paper's set-valued implication generalizes.","marker":"[1]"},{"why":"Supplies the standard facts about induced order and the event-state semantics of effect algebras used in Lemma 2.","marker":"[6]"},{"why":"Monograph on quantum structures that motivates treating non-lattice effect algebras as the appropriate setting for quantum logic.","marker":"[5]"}],"fun_headline_variants":["Set-valued arrow: sound implication for all effect algebras","Lower cones alone define a sound implication","Unsharp residuation makes logic sound for effects","No lattice needed: effect algebras get a sound arrow","Implication from lower cones: sound and reversible"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The argument treats set-valued expressions like $a\\cdot(a\\to b)$ as if the usual laws for element-level operations still apply, and on that subset-extension the main equivalence rests; if the extension is not legitimate, the central theorem does not follow.","fun_headline_variants_meta":{"raw":{"variants":["Set-valued arrow: sound implication for all effect algebras","Lower cones alone define a sound implication","Unsharp residuation makes logic sound for effects","No lattice needed: effect algebras get a sound arrow","Implication from lower cones: sound and reversible"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000965,"raw_usage":{"total_tokens":4083,"prompt_tokens":898,"completion_tokens":3185,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":514,"completion_tokens_details":{"reasoning_tokens":3114}},"tokens_in":514,"tokens_out":3185,"duration_ms":24114,"temperature":1.0,"reasoning_tokens":3114,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:17:58.494925+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A reader could settle the central claim by taking the 6-element lattice effect algebra of Example 17, forming $C(E)$ with the paper's definitions, and converting back: the recovered addition must have exactly the table of Example 17. Any mismatch would refute Theorem 10; likewise, direct computation of $x\\odot(x\\to y)$ versus $L(x,y)$ for incomparable elements would test the divisibility condition (C5).","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces effect algebras and the partial-addition axiomatization (E1)–(E4) on which the whole construction is built."},{"cited_title":"Chajda and H","cited_arxiv_id":null,"evidence_quote":"Prior work by the authors defining unsharp residuation in effect algebras; the present implication is the non-lattice generalization of that approach."},{"cited_title":"Chajda and R","cited_arxiv_id":null,"evidence_quote":"Shows lattice effect algebras are conditionally residuated, the restricted case this paper's set-valued implication generalizes."},{"cited_title":"Dvureˇ censkij and T","cited_arxiv_id":null,"evidence_quote":"Supplies the standard facts about induced order and the event-state semantics of effect algebras used in Lemma 2."}],"review_version":1}