REVIEW 3 major objections 5 minor 9 references
Properties of the connective implication in effect algebras
T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash
Pith's one-line read 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.
desk verdict 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. 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 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.
What would settle it
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).
Extended reading notes
Core claim
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.
Load-bearing premise
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.
Editorial extensions
If this is right
- 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.
Reading between the lines
- 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.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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.
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 (3)
- [Section 2, Definition 6, Theorem 4(viii), Theorem 7] 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.
- [Theorem 9] 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.
- [Theorem 8, Definition 6] 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.
minor comments (5)
- [Abstract] The phrase 'every productive logic is is equipped' contains a duplicated 'is'.
- [Section 1] 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.
- [Theorem 5(ii)] 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.
- [Theorem 13(ii)] The statement 'Ded(E) is atomic' should be stated as 'the poset (Ded(E), ⊆) is atomic' for precision.
- [References] 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.
Circularity Check
No significant circularity: Theorem 7 is a self-contained verification of a new structural definition, and the round-trip theorem provides independent content rather than a restatement of inputs.
full rationale
The paper defines a new implication x→y = x′ + L(x,y) on an arbitrary effect algebra and then introduces the class of strict unsharp residuated posets (Definition 6) as an abstraction of the properties this implication enjoys. Theorem 7 verifies, from the effect algebra axioms via Lemma 2, Lemma 3, and Theorem 4, that every effect algebra E gives such a structure C(E); it does not assume (C3) or (C5) for E but proves them. Theorem 9 gives a converse at the level of the reduct {≤,⊙,′,0,1}, and Theorem 10 shows E(C(E)) = E, so the construction is not a definitional identity: the round-trip is a proved equality, not the same equation on both sides. The self-citations [1]–[4] motivate the definition and cover lattice and monotone cases, but the proof of Theorem 7 is self-contained and does not rest on those results. The only soft spot is the under-specified set-valued extension of the partial operations (e.g., a·(a→b) in Theorem 4(viii) and A⊙B in Definition 6(C3)), where the paper treats expressions involving subsets using elementwise extension without an explicit definition; however, the identities are derived from the defined operations on subsets (A′, x+A, A+B) and are checkable, so this is a formalization gap, not a circular reduction. No claim in the paper reduces, by the paper's own equations, to its input definition.
Assumptions & free parameters
assumptions (4)
- standard math ZFC set theory and standard poset facts about lower and upper cones
- domain assumption Effect algebra axioms (E1)-(E4) and their consequences from Foulis-Bennett
- ad hoc to paper The new strict unsharp residuated poset axioms (C1)-(C4), in particular clause (C2) requiring x ≤ y implies x = y ⊙ (y ⊙ x')′
- ad hoc to paper Set-valued extensions of partial operations x + A and x · A are well-defined and order-compatible
invented entities (1)
-
Strict unsharp residuated poset (C, ≤, ⊙, →, ′, 0, 1)
independent evidence
Cite this review
Pith. "Pith review of Properties of the connective implication in effect algebras." pith.science (2026). https://pith.science/paper/D4JDTOZL
@misc{pith2026190805315,
author = {Pith},
title = {Pith review of: Properties of the connective implication in effect algebras},
year = {2026},
howpublished = {\url{https://pith.science/paper/D4JDTOZL}},
note = {Machine review of arXiv:1908.05315}
}
read the original abstract
Effect algebras form a formal algebraic description of the structure of the so-called effects in a Hilbert space which serves as an event-state space for effects in quantum mechanics. This is why effect algebras are considered as logics of quantum mechanics, more precisely as an algebraic semantics of these logics. Because every productive logic is is equipped with a connective implication, we introduce here such a concept and demonstrate its properties. In particular, we show that this implication is connected with conjunction via a certain "unsharp" residuation which is formulated on the basis of a strict unsharp residuated poset. Though this structure is rather complicated, it can be converted back into an effect algebra and hence it is sound. Further, we study the Modus Ponens rule for this implication by means of so-called deductive systems and finally we study the contraposition law.
Reference graph
Works this paper leans on
-
[1]
I. Chajda and R. Halaˇ s, Effect algebras are conditionally residua ted structures. Soft Comput. 15 (2011), 1383–1387. 13
work page 2011
-
[2]
I. Chajda and H. L¨ anger, Relatively residuated lattices and pos ets. Math. Slovaca (submitted). http://arxiv.org/abs/1901.06664
arXiv 1901
-
[3]
I. Chajda and H. L¨ anger, Residuation in lattice effect algebras. Fuzzy Sets Systems (submitted). http://arxiv.org/abs/1905.05496
arXiv 1905
-
[4]
I. Chajda and H. L¨ anger, Unsharp residuation in effect algebra s. J. Multiple-Valued Logic Soft Comput. (submitted). http://arxiv.org/abs/1907.027 38
work page 1907
-
[5]
Dvureˇ censkij and S
A. Dvureˇ censkij and S. Pulmannov´ a, New Trends in Quantum St ructures. Kluwer, Dordrecht 2000. ISBN 0-7923-6471-6
2000
-
[6]
A. Dvureˇ censkij and T. Vetterlein, Pseudoeffect algebras. I. Basic properties. Internat. J. Theoret. Phys. 40 (2001), 685–701
work page 2001
-
[7]
D. J. Foulis and M. K. Bennett, Effect algebras and unsharp quan tum logics. Found. Phys. 24 (1994), 1331–1352. Authors’ addresses: Ivan Chajda Palack´ y University Olomouc Faculty of Science Department of Algebra and Geometry
work page 1994
-
[9]
listopadu 12 771 46 Olomouc Czech Republic helmut.laenger@tuwien.ac.at 14
Show all 9 references
-
[17]
listopadu 12 771 46 Olomouc Czech Republic ivan.chajda@upol.cz Helmut L¨ anger TU Wien Faculty of Mathematics and Geoinformation Institute of Discrete Mathematics and Geometry Wiedner Hauptstraße 8-10 1040 Vienna Austria, and Palack´ y University Olomouc Faculty of Science Dep...
Reviewed August 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.