{"id":"9e95c9ab-f4bf-4c34-ab47-0cb16dc16a57","arxiv_id":"2411.15940","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"The modal logic of minimal upper bounds (MIN) has exactly the same valid formulas as the modal information logic of least upper bounds (MIL).","lead":"This paper defines a modal logic of minimal upper bounds, where combining two information states may yield several incomparable results, and proves it has exactly the same valid formulas as the older logic of least upper bounds. The result gives a complete axiom system and a decision procedure for the new logic, and shows that modal validity cannot tell the two fusion notions apart.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The model-level valuation gap in Lemma 1 is real but immediately fillable; once V'(x,i)=V(x) is defined, the p-morphic preservation proof goes through, so the central claim survives.","rationale":"I reviewed the central proof in detail. Lemma 1's construction is correct: the G(t,u) downset argument proves the needed strict inequalities, the order on P' is a partial order, condition 4 holds because G(t,u) is closed under binary suprema, and the forth/back clauses for the supremum p-morphism are verified. The iterative repair in Proposition 1 is also sound: once a triple is repaired it stays repaired, and the enumeration argument eliminates all bad triples at the limit. The only substantive weakness is the missing valuation on the duplicate copy, which the reader correctly identified. This is a presentation gap rather than a flaw, because the pullback valuation V'(x,i)=V(x) is the obvious choice and makes the p-morphic image theorem work for the binary modality. I also checked Theorem 2: the MIL axioms (Re.), (4), (Co.), and (Dk.) are valid under the minimal-upper-bound semantics, with ⟨P⟩ϕ defined as ⟨mub⟩ϕ⊤; the equivalence with the backwards modality uses u=s as a witness, and (Dk.) uses the pair (s,t). Theorem 5's residual-implication back condition is not superfluous: it is exactly the back condition needed for the residual implication, and the case analysis (j=0, j=1 with x∈↓s, j=1 with x∉↓s) is correct. The transfinite recursion for uncountable posets is only sketched, but the standard limit-stage argument works and preserves cardinality. Overall, the central claim MIN = MIL appears correct; the conditional verdict is appropriate pending the author filling the stated gaps.","tokens_in":1037,"tokens_out":2843,"duration_ms":332942,"concrete_test":"Re-prove Lemma 1 and Proposition 1 at the level of pointed models by setting V'(x,i):=V(x) for every (x,i)∈P' (equivalently, the pullback of V along the p-morphism f). Then verify by induction on the structure of ϕ∈L that for every (x,i)∈P', M',(x,i)⊩_S ϕ iff M,x⊩_S ϕ, using the forth clause to handle the upper-bound direction of ⟨sup⟩ and the back clause to lift witnesses. If the induction closes, the MIN⊆MIL direction is complete. As a second check, confirm that the same pullback valuation is consistent through the transfinite iteration in Proposition 1, so that the limit model satisfies the same preservation property.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The most load-bearing concern is the one the reader identified: Lemma 1 is stated for frames, but the proof of MIN ⊆ MIL (Theorem 3) needs p-morphic preservation at the level of pointed models. The proof strategy in §3 announces a model M'=(P',≤',V') extending M, but neither Lemma 1 nor Proposition 1 defines V' on the duplicated copy ↓s. Without a valuation, the induction for formulas containing proposition letters cannot be run, and the asserted preservation of ⊩_S by p-morphic images is not actually verified. This matters because the refutation of a MIL-invalid formula must be transferred from a model on P to a model on P'. The concern is genuine as a rigor gap, but it is not a mathematical counterexample: the natural choice V'(x,i)=V(x) for all (x,i)∈P' is the pullback of V along f, and with this valuation f satisfies the standard bounded-morphism conditions for the ternary supremum relation. The forth clause (if x'=sup'{y',z'} then f(x')=sup{f(y'),f(z')}) and back clause (if f(x')=sup{y,z} then witnesses lift) proved in Lemma 1 are exactly what the induction for the binary modality needs, so the model-level preservation theorem closes. The other flagged gaps—transfinite recursion for uncountable posets and the residual-implication back condition in Theorem 5—are also sketched rather than fully detailed, but the arguments are standard and the case analysis in Theorem 5 is correct. No fatal flaw in the central equality MIN = MIL is apparent.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper defines MIN, the modal logic of minimal upper bounds on posets, and proves that MIN coincides with van Benthem's MIL, the modal logic of least upper bounds. The proof uses a step-by-step p-morphic representation that eliminates failures of the implication mub ⇒ sup by duplicating downsets and adding infinite descending chains of upper bounds. From this equality and the author's earlier axiomatization and decidability result for MIL, the paper derives an axiomatization and decidability for MIN; it then extends the result to preorder frames and to the residual-implication extensions MIN(\\) and MIL(\\).","tokens_in":118,"tokens_out":6084,"duration_ms":184558,"significance":"The result is genuinely interesting: although the two semantic clauses differ at the model level, the paper claims that no modal formula separates them, so the modal language cannot distinguish least from minimal upper bounds at the level of validities. The central construction is explicit, the iterative representation is natural, and the corollaries concerning axiomatization and decidability are a real payoff. If the proof gaps noted below are closed, the paper makes a solid contribution to modal information logic; the finite-frame remark also gives a useful boundary for the main result.","major_comments":[{"comment":"The construction is carried out for frames only: Lemma 1 defines P', ≤', and f, but never defines the valuation V' on the duplicated copy ↓s. The Proof Strategy paragraph announces a model M'=(P',≤',V'), and Theorem 3 requires transferring refutations of formulas containing proposition letters. The natural pullback V'(x,i)=V(x) for all (x,i)∈P' should be stated explicitly, and the standard p-morphic preservation induction showing M',(x,i) ⊩_S φ iff M,f(x,i) ⊩_S φ for all φ should be written out. As the text stands, the model-level preservation claim is asserted rather than proved, so the converse inclusion in Theorem 3 is not fully justified.","section":"§3, Lemma 1 and Proposition 1"},{"comment":"In the third case of the \\-back verification, the proof asserts 'Thus, v /∈ ↓s, hence we must have i = 0' without giving the needed argument. The reader must infer that x∉↓s and x≤v imply v∉↓s, since if v∈↓s then x≤v≤s contradicts x∉↓s; then i=1 would force v∈↓s by the definition of ≤'. This is a small but real omission in the proof of the residual implication case, and it should be supplied explicitly.","section":"§4, Theorem 5"}],"minor_comments":[{"comment":"The notation P' := P ⊔ ↓s = {(x,0),(y,1) | x∈P, y∈↓s} is a slight abuse of notation for a disjoint union; condition 1, which says P⊆P', should be read under the identification x ↦ (x,0). This identification deserves to be stated once explicitly.","section":"§3, Lemma 1"},{"comment":"Footnote 7 suppresses the transfinite recursion needed for uncountable posets. Since Theorem 3 is claimed for all posets, a brief indication of the limit step would make Proposition 1 completely rigorous.","section":"§3, Proposition 1"},{"comment":"The soundness of the axioms (Re.), (4), (Co.), and (Dk.) with respect to MIN is dismissed as a routine check. In particular, a sentence showing how (Dk.) is verified under the mub semantics would help the reader confirm the inclusion MIL ⊆ MIN.","section":"§2, Theorem 2"},{"comment":"The strict inequality 'x ⁄< s' should be written as the explicit condition 'it is not the case that x < s' to avoid ambiguity, especially since the paper uses '≤' and '<' informally in the surrounding discussion.","section":"§2, Definition 3"}],"recommendation":"major_revision","confidential_remarks":"The main proof has a genuine but easily repairable gap: the valuation on the constructed model is never defined, and the p-morphic preservation theorem is not stated at the model level. I see no sign of a mathematical counterexample, and the natural choice V'(x,i)=V(x) should close the gap. The reliance on the author's own [11] for the axiomatization and decidability of MIL is appropriate. The paper fits the postproceedings venue, provided the proof details are tightened."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this paper proves something I didn't expect: the minimal-upper-bound semantics and the least-upper-bound semantics are modally indistinguishable. The proof that MIN = MIL is the real result. The technique — duplicating downsets to replace incomparable minimal upper bounds by infinite descending chains — is a genuine contribution, and the way it forces suprema to be preserved is clever.\n\nWhat's new: MIN is a new logic, the equality with MIL is not in the literature, and the finite-frame distinguishing formula (valid on finite frames for MIN, not MIL) is a nice observation. The paper does a good job of showing MIL ⊆ MIN by verifying the known MIL axioms under the mub clause, and the principal lemma (Lemma 1) is worked out in detail.\n\nWhere the soft spots are, in proportion: the biggest one is the one the reader flagged. Lemma 1 is stated for frames, but the proof of Theorem 3 needs preservation of satisfaction at the level of models with valuations. The paper never defines the valuation on the duplicated copy ↓s. This is a real rigor gap. But it is not a mathematical problem: defining V'(x,i) = V(x) on the disjoint copy gives you the pullback, and with that valuation the p-morphism conditions proved in Lemma 1 are exactly the forth/back conditions needed for the induction on formulas. So the central claim survives; the paper just needs to state the valuation and the model-level preservation lemma explicitly.\n\nTwo smaller gaps: the transfinite recursion for uncountable posets is dismissed as 'straightforward' — it is, but a line or two would help — and the proof of Theorem 5 (the residual implication) says the back condition suffices and then does the case analysis, but the preservation argument for formulas with '\\' is only sketched. Again, standard, but worth tightening.\n\nThe citation pattern is fine: the axiomatization and decidability come from the author's published prior work on MIL, which is independent support. Self-citation here is legitimate.\n\nOverall: this is a solid, interesting paper. The main theorem appears correct, the proof method is novel, and the gaps are fillable without changing the argument. I'd send it to a serious referee. It will be of value to anyone working on modal logics over order-based information semantics, and the equality result will be cited.","headline":"A clever p-morphic construction shows minimal and least upper bounds are modally indistinguishable; the proof is essentially correct with fillable valuation gaps.","tokens_in":11705,"tokens_out":2131,"would_cite":true,"duration_ms":20019,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B45","03B25"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that the modal logic of minimal upper bounds (MIN) coincides exactly with the modal logic of least upper bounds (MIL): no formula distinguishes the two interpretations, and MIN inherits the complete axiomatization and…","keywords":["modal logic","modal information logic","minimal upper bound","least upper bound","axiomatization","decidability","partial orders","p-morphism"],"falsifier":"Test the formula $(\\langle P\\rangle p \\land \\langle P\\rangle q) \\to \\langle P\\rangle(\\langle mub\\rangle pq)$ on infinite posets formed by adding an infinite descending chain to a configuration with two incomparable upper bounds; the paper's argument predicts the formula stays valid under both semantics on these infinite posets, so finding an infinite model where it holds under MIN but fails under MIL would refute Theorem 3.","tokens_in":10618,"feed_emoji":"🔀","tokens_out":12148,"duration_ms":103815,"temperature":0.7,"pith_summary":"This paper sets out to show that two competing semantics for the same modal language—least upper bounds (informational sums as unique suprema) and minimal upper bounds (informational sums as possibly multiple incomparable fusions)—cannot be told apart by the logic. The main theorem states MIN = MIL: every formula valid under the minimal-upper-bound semantics is valid under the least-upper-bound semantics, and conversely. The paper also proves the same equality for the logics enriched with the residual implication and for preorder frames. If the result is right, the minimal-upper-bound logic inherits a complete axiomatization and decidability from the already-studied least-upper-bound logic.","feed_headline":"Modal logic can't tell minimal from least upper bounds","feed_subtitle":"The two semantics yield the same validities, so MIN inherits a complete axiomatization and decidability.","key_machinery":"The load-bearing mechanism is the distinction between the relations $s \\in \\operatorname{mub}\\{t,u\\}$ and $s = \\sup\\{t,u\\}$ in a partial order, together with a representation lemma that forces the two to coincide. Lemma 1 takes a poset containing a minimal upper bound $s$ that is not a supremum, forms the disjoint union $P \\sqcup \\downarrow s$, and positions a duplicate of the whole downset $\\downarrow s$ directly below $s$, so that $(s,1) \\leq' (s,0)$ and $s$ ceases to be a minimal upper bound of $\\{t,u\\}$. A set $G(t,u)$, defined as the least downset containing $t,u$ and closed under binary suprema, ensures that all existing suprema are preserved; iterating the construction over an enumeration of triples yields a poset satisfying $s' \\in \\operatorname{mub}\\{t',u'\\}$ iff $s' = \\sup\\{t',u'\\}$. A supremum p-morphism—a function preserving and reflecting suprema—then transfers validity from the constructed poset back to the original one.","core_discovery":"The central claim is that the modal language cannot distinguish minimal from least upper bounds. Writing MIN for the logic whose modality says 's is a minimal upper bound of two states' and MIL for the logic whose modality says 's is their least upper bound,' the paper proves MIN = MIL at the level of validities and consequences, and extends the equality to the residual-implication extensions and to preorder frames. The difficult inclusion is obtained by a representation construction: every poset is shown to be the p-morphic image of a poset in which every minimal upper bound is a least upper bound, and p-morphic images preserve the least-upper-bound semantics. Because MIL is known to be completely axiomatized and decidable, the equality transfers those properties to MIN.","pith_inferences":["If the equality holds, the philosophical contrast between unique and multiple information fusions is not expressible in ordinary modal validities; it would show up only in finite-frame behavior or in model-level definitions.","The construction depends essentially on infinite descending chains, so restricting to well-founded or finite posets is the natural place to look for a logic genuinely different from MIL; the paper's finite-frame witness is a starting point.","A testable extension is to add a device that can express uniqueness of a minimal upper bound; such an enrichment would likely produce formulas that separate MIN from MIL.","The same duplicating-downset technique may apply to other binary order-theoretic connectives, such as maximal lower bounds, possibly yielding analogous collapse theorems for their modal logics."],"forward_implications":["MIN and MIL have the same valid formulas and the same consequence relation, so no modal principle separates the minimal-upper-bound reading from the least-upper-bound reading.","MIN is completely axiomatized by the axioms (Re.), (4), (Co.), and (Dk.) and is decidable, because these properties hold for MIL.","The residual-implication extensions of MIN and MIL also coincide and are decidable.","The poset and preorder variants of the four logics form one uniform family: MINPos = MINPre = MILPre = MILPos.","On finite frames the two semantics genuinely differ, and the paper exhibits a formula that separates them there."],"supporting_citations":[{"why":"Introduces the least-upper-bound modal information logic MIL, the system MIN is compared with.","marker":"[3]"},{"why":"Provides the complete axiomatization and decidability proof for MIL that the paper transfers to MIN.","marker":"[11]"},{"why":"Introduces the residual-implication extension of MIL that Theorem 5 extends to MIN.","marker":"[5]"},{"why":"Supplies the semantic clause for the residual implication used in the extended logics.","marker":"[13]"}],"fun_headline_variants":["Minimal and least upper bounds are modally identical","Modal logic can't separate minimal from least upper bounds","MIN and MIL: same logic, same theorems","Upper bounds: minimal equals least for modal logic","Modal logic finds no gap between upper bound semantics"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The central proof assumes that the representation construction can be lifted from posets to models: the duplicated downset must be given a valuation so that every formula satisfied at an original point is also satisfied at its duplicate, and the paper states this preservation without explicitly constructing the valuation.","fun_headline_variants_meta":{"raw":{"variants":["Minimal and least upper bounds are modally identical","Modal logic can't separate minimal from least upper bounds","MIN and MIL: same logic, same theorems","Upper bounds: minimal equals least for modal logic","Modal logic finds no gap between upper bound semantics"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000229,"raw_usage":{"total_tokens":1413,"prompt_tokens":815,"completion_tokens":598,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":431,"completion_tokens_details":{"reasoning_tokens":525}},"tokens_in":431,"tokens_out":598,"duration_ms":5643,"temperature":1.0,"reasoning_tokens":525,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T13:46:57.933666+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Test the formula $(\\langle P\\rangle p \\land \\langle P\\rangle q) \\to \\langle P\\rangle(\\langle mub\\rangle pq)$ on infinite posets formed by adding an infinite descending chain to a configuration with two incomparable upper bounds; the paper's argument predicts the formula stays valid under both semantics on these infinite posets, so finding an infinite model where it holds under MIN but fails under MIL would refute Theorem 3.","supporting_citations":[{"cited_title":"In : Copeland, J","cited_arxiv_id":null,"evidence_quote":"Introduces the least-upper-bound modal information logic MIL, the system MIN is compared with."},{"cited_title":"Journal of Philosophical Logic pp","cited_arxiv_id":null,"evidence_quote":"Provides the complete axiomatization and decidability proof for MIL that the paper transfers to MIN."},{"cited_title":"In: Weiss, Y., Birman, R","cited_arxiv_id":null,"evidence_quote":"Introduces the residual-implication extension of MIL that Theorem 5 extends to MIN."},{"cited_title":"Journal of Symbolic Logic 37, 159–169 (1972)","cited_arxiv_id":null,"evidence_quote":"Supplies the semantic clause for the residual implication used in the extended logics."}],"review_version":1}