{"id":"fe6c5e4f-9f2c-4433-b0b4-7a837dcd592e","arxiv_id":"2501.00495","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper presents a first-order star semantics for BD+, defines an explosive intuitionistic variant QBDi3, and proves its completeness, disjunction/existence properties, and a four-valued characterization of a two-state fragment.","lead":"This paper studies formal logics that allow some contradictions to be true without everything following, and it maps several known systems onto each other. It also introduces a new system in this family and proves that it satisfies useful constructive properties.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"MH strong completeness is not merely unproved: with the maximal-successor semantics it is false, so the model-existence step in Theorem 2 needs a different argument.","rationale":"The reader's weakest assumption already identifies the external MH strong completeness as the load-bearing point of Theorem 2. My stress-test agrees with that diagnosis and sharpens it: the external result is not merely unproved in the paper but is false for the natural reading of the MH semantics, namely the maximal-successor Kripke semantics obtained by restricting Definition 8. The concrete non-compactness example shows that a finitary MH proof system cannot be strongly complete for arbitrary infinite theories. This undermines the model-existence step in the completeness proof for QBDi3. The central claim of the paper, Theorem 2, may still be true and provable by other means, so I do not move the reader's CONDITIONAL verdict to REJECT; but the required revision is more serious than 'fill in the details': the proof must either restrict the use of MH strong completeness, prove a special compactness/completeness lemma for the theories that actually arise from the reduction, or construct the QBDi3 model directly. The assessment of novelty and the absence of other internal inconsistencies are unchanged.","tokens_in":17643,"tokens_out":39606,"duration_ms":424618,"concrete_test":"Re-derive the MH model-existence step for Σ = {¬¬R(c_n) : n ∈ N} ∪ {¬∀xR(x)} in the language of Remark 9. Verify (1) every finite subset has a two-world MH model with a maximal successor, and (2) any MH model with maximal successors forces ∀xR(x) at a maximal successor of any world satisfying all of Σ, so no model of Σ exists. If both hold, MH strong completeness for the semantics used in the paper is refuted. Then check whether [3] and [12] actually state strong completeness for arbitrary infinite theories or only weak completeness; if the latter, locate exactly where the proof of Theorem 2 overstates the cited result.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 2's completeness proof needs a model of the infinite MH theory f(Γ)' ∪ E_{f(Γ∪{A})} refuting f(A)' at a world. The proof cites strong completeness of MH from [3,12]. This is the load-bearing step, and it is not merely an unverified citation: for the Kripke semantics with maximal successors described by Definition 8 (and apparently retained in Remark 9), strong completeness of MH is false. Consider the MH theory Σ = {¬¬R(c_n) : n ∈ N} ∪ {¬∀xR(x)}. No MH model satisfies Σ: if w makes all formulas true, let z be a maximal successor of w. At a maximal node, double negation collapses, so w ⊨ ¬¬R(c_n) forces z ⊨ R(c_n) for every n, hence z ⊨ ∀xR(x). But w ⊨ ¬∀xR(x) requires that no successor forces ∀xR(x), contradicting w ≤ z. Every finite subset of Σ is satisfiable: take a two-world frame w < z with z maximal, make R(c_n) true at z for exactly the finitely many indices occurring in the finite subset, and false for some other constant so that ¬∀xR(x) holds. Thus MH has a non-compact consequence relation, so a finitary proof system cannot be strongly complete. If, on the other hand, the cited MH semantics omits the maximal-successor condition, then the QBDi3 model constructed from the MH countermodel may fail Definition 8's frame requirement. Either way, the proof of Theorem 2 as written is unsupported; a different model-existence lemma is needed.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies the relation between two intuitionistic counterparts of the logic BD+ (Belnap-Dunn logic with Boolean negation): Kamide's BDi (the \"American\" plan) and HYPE (the \"Australian\" plan). It provides a new star semantics for first-order BD+, introduces an explosive predicate logic QBDi3 obtained from BDi by adding the ex contradictione and potential omniscience, and proves a soundness and completeness theorem for QBDi3 by reducing it to the intermediate logic MH (intuitionistic logic with the double negation shift). The authors also establish constructive properties (disjunction, existence, and constructible falsity), study a propositional extension for which they give four-valued truth tables, and compare related systems QBDi, QDN3, QDN4, and a connexive variant.","tokens_in":17926,"tokens_out":29129,"duration_ms":285897,"significance":"If the central completeness theorem is correct, the paper offers a useful bridge between the American and Australian semantic traditions for BD+, and the reduction of QBDi3 to MH is an interesting technical result. The paper is clearly written and contains several valuable observations, such as the star semantics for QBD+ and the four-valued characterization of BDi3+(AxG). The constructive properties for QBDi3 are also a nice addition. However, the paper's main theorem relies on an external strong-completeness result for MH whose match to the semantics defined in Remark 9 is not verified, so the significance is conditional on closing that gap.","major_comments":[{"comment":"The completeness proof of Theorem 2 depends on the 'strong completeness for MH' cited as [3,12] for the class of MH models introduced in Remark 9. Remark 9 defines MH models by restricting QBDi3-models, so they inherit the maximal-successor frame condition and the monotone increasing domains of Definition 8. It is not stated whether [3,12] proves strong completeness for exactly this class; if the cited result concerns a different semantics (e.g., without the maximal-successor condition, or with constant domains), the model produced by the completeness step need not satisfy Definition 8's frame requirements, and the constructed QBDi3 model in Theorem 2 may be ill-defined. The authors should either supply a precise statement of the MH completeness theorem that matches Remark 9, or replace the appeal by a direct model-existence construction for the infinite theory f(Γ)' ∪ E_{f(Γ∪{A})}.","section":"Theorem 2, Section 3.3"},{"comment":"Proposition 20, which is essential for the reduction used in Theorem 2, is only partially proved: the cases for implication and universal quantification are sketched, and the existential case is omitted. Since the derivation in the universal case uses the double negation shift (i1) inside a reduced proof and involves a non-trivial chain of intuitionistic equivalences, the sketch is not enough to verify without reworking the entire argument. Please expand the proof or provide a fully formal derivation for all cases.","section":"Proposition 20, Section 3.3"}],"minor_comments":[{"comment":"In the atomic clauses of Definition 8, the occurrences of V+(x,P) and V−(x,P) should read V+(w,P) and V−(w,P).","section":"Definition 8"},{"comment":"In the proof of Theorem 2, after '1 ∉ I(w, f(A)′)' the text says 'for some x∈W'; the variable is inconsistent and should be 'for that w'.","section":"Theorem 2 proof"},{"comment":"The completeness direction of Proposition 6 is left to the reader; although the induction is straightforward, the two-state model construction deserves a brief verification of the star condition and the stated equivalences.","section":"Proposition 6"},{"comment":"Remark 9's phrase 'additional predicates P′, Q′, etc.' should clarify that for each n-ary predicate P there is a corresponding predicate P′ of the same arity.","section":"Remark 9"},{"comment":"In the proof of Theorem 5, the notation I(x,A) = {1} suggests a set of truth values; the intended reading is a single value, and this should be adjusted to avoid confusion.","section":"Theorem 5 proof"}],"recommendation":"major_revision","confidential_remarks":"The central issue is the match between the cited strong completeness of MH and the semantics defined in Remark 9. A stress-test concern about non-compactness of MH with maximal successors was raised, but this particular counterexample appears inconclusive because domains may contain elements not named by constants. Nevertheless, the onus is on the authors to verify the citation and, if necessary, supply a direct model-existence proof. The paper has solid ideas and is likely fixable, but the current proof is not self-contained at the load-bearing point."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nThe short version: this is a solid piece of non-classical logic, and the central claim—completeness of QBDi3—looks right. The stress-test note tries to shoot down the use of MH strong completeness, but the counterexample doesn't work. The theory {¬¬R(c_n)} ∪ {¬∀xR(x)} is satisfiable in a two-world model with a maximal top node if the domain at the top node contains an element not named by any constant and that element fails R. Definition 8 only requires D(w) ⊇ Con; it does not require the domain to be exactly the constants. So \"double negation collapses at the maximal node\" gives you R(c_n) for every constant at the top node, but it does not give you ∀xR(x) when the domain is larger. The compactness objection dissolves. I would need a different example to worry about MH strong completeness.\n\nWhat is actually new: the star semantics for first-order BD+ (Proposition 6), the QBDi3 system with its completeness theorem (Theorem 2), and the four-valued characterization of BDi3+(AxG) (Corollary 27). These are natural extensions of known machinery—Routley stars, Gurevich reductions, G3 semantics—but they are put together cleanly and fill a real gap. The paper also does useful housekeeping: showing (i1) and (i3) are redundant, relating QBDi3 to DN3, and proving constructible falsity via an Aczel slash. The reduction f and the translation to MH with auxiliary predicates is the right technical core, and the proof sketches are believable.\n\nThe soft spots are about compression, not correctness. Proposition 6's completeness direction is \"safely left to the readers\"—fine for a conference paper, but annoying to verify. Proposition 20 covers selected cases and says \"the case for ∨ is similar\"; Theorem 4 is asserted by analogy with Theorem 2, and the four-valued tables are only shown adequate via two theorems that should be checked. The proof of Theorem 2 depends on strong completeness of MH for an infinite theory; that is an external result, not proved here, but the citation is standard. A referee should push for a more self-contained completeness proof or at least more detail in an appendix.\n\nWho it is for: people working on Belnap-Dunn logic, strong negation, and intermediate predicate logics. It will not change the world, but it is honest progress. I would recommend sending it to peer review; it deserves a serious referee, though the referee should ask for the gaps to be filled.\n\nBest,\n[You]","headline":"Genuinely useful first-order extension of BD+ work, with a completeness proof that survives the stress-test objection.","tokens_in":18529,"tokens_out":7621,"would_cite":true,"duration_ms":76913,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B20","03B53","03B55","03B60"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that QBDi3, the explosive first-order extension of the intuitionistic paraconsistent logic BDi, is sound and complete for a Kripke semantics whose implication-falsity condition enforces potential omniscience.","keywords":["Belnap-Dunn logic","Boolean negation","intuitionistic logic","paraconsistent logic","strong negation","Kripke semantics","double negation shift","potential omniscience"],"falsifier":"Find a QBDi3-model with maximal successors, monotone extensions and anti-extensions, and potential omniscience that fails one of the axioms (i1), (i2), or (i3) at some state; that would refute soundness. Alternatively, exhibit a reduced set $\\Gamma\\cup\\{A\\}$ such that the translated theory $f(\\Gamma)'\\cup E_{f(\\Gamma\\cup\\{A\\})}$ is MH-derivable for $f(A)'$ while $\\Gamma\\not\\vdash_{\\mathrm{i3}} A$, which would refute Proposition 21 and with it the completeness argument.","tokens_in":17446,"feed_emoji":"","tokens_out":11607,"duration_ms":108269,"temperature":0.7,"pith_summary":"The paper explains why a single four-valued logic, Belnap-Dunn logic expanded with Boolean negation (BD+), splits into two different intuitionistic logics, the system BDi and the system HYPE, once the base setting moves from classical to intuitionistic logic. To make the split perspicuous, it formulates a two-state 'star' semantics for first-order BD+ and shows that BD+ is obtained from HYPE by collapsing the constructive order. Its main technical result is that the first-order explosive extension QBDi3 is sound and complete for a Kripke-style semantics with monotone extensions and anti-extensions, maximal successors, and potential omniscience. The completeness theorem matters because it shows that the falsity condition for implication in this semantics forces the double negation shift and potential omniscience, and because QBDi3 nevertheless retains the disjunction property, the existence property, and constructible falsity.","feed_headline":"QBDi3 proved sound and complete for its Kripke semantics","feed_subtitle":"The completeness proof shows the falsity clause for implication forces double negation shift and potential omniscience.","key_machinery":"The load-bearing machinery is a reduction $f$ (Definition 17) that rewrites every formula by pushing the strong negation $\\sim$ inward through quantifiers and connectives until it applies only to prime formulas. A reduced formula is then translated into the intermediate logic MH by replacing each $\\sim P$ with a fresh predicate $P'$ and adding the axioms $\\forall\\vec{x}(P'\\to\\neg P)$ and $\\forall\\vec{x}\\neg\\neg(P'\\vee P)$; Proposition 21 says QBDi3 derivability of a reduced formula is equivalent to MH derivability of the translated formula from the translated theory plus those axioms. The completeness proof builds a QBDi3-model out of an MH-model supplied by strong completeness of MH. On the semantic side, the QBDi3-model itself is the central object, with its monotone extension and anti-extension sets, maximal successors, and potential omniscience.","core_discovery":"The central claim, stated as Theorem 2, is that for all sets of sentences $\\Gamma\\cup\\{A\\}$, $\\Gamma \\vdash_{\\mathrm{i3}} A$ if and only if $\\Gamma \\models_{\\mathrm{i3}} A$, where the semantic consequence is taken over the class of QBDi3-models. In those models, each world has a maximal successor, extensions and anti-extensions of predicates are monotone, and every atomic sentence is eventually settled along every branch, an assumption called potential omniscience. The paper also proves that the star semantics for first-order BD+ is sound and complete, making explicit that BDi and HYPE are the American-plan and Australian-plan intuitionistic counterparts of BD+, and that the propositional extension of BDi3 by the linearity axiom (AxG) is characterized by a four-valued truth table.","pith_inferences":["One testable extension is to vary the falsity clause for implication in the BDi semantics while leaving the rest untouched, and check which axioms become valid; the paper's results suggest that potential omniscience and the double negation shift are sensitive to exactly that clause.","The completeness proof routes through MH, so proof-theoretic properties of MH such as cut elimination or interpolation may transfer to QBDi3 through the reduction, a connection the paper does not explore.","The finite-valued description of BDi3+(AxG) suggests a systematic search for other finite-frame extensions of QBDi3 whose semantics collapse to finite matrices.","If the external completeness of MH were ever questioned, a canonical-model proof for QBDi3 built directly from its own semantics would make the result self-contained; the reduction does not provide that by itself."],"forward_implications":["Every QBDi3-valid sequent is provable, so the axiomatic system captures exactly the intended Kripke semantics.","Making BDi explosive forces potential omniscience and the double negation shift; equivalently, the falsity condition for implication in the semantics commits the logic to these principles.","The star semantics for first-order BD+ gives a common vantage point from which BDi and HYPE are visible as two distinct constructivisations of the same classical four-valued logic.","QBDi3 has the disjunction property, the existence property, and constructible falsity despite containing the double negation shift.","The four-valued truth tables for the propositional extension BDi3+(AxG) provide a finite-valued description of that extension."],"supporting_citations":[{"why":"Supplies the strong completeness of the intermediate logic MH used in the model-existence step.","marker":"[3]"},{"why":"Provides the intermediate logic MH with the double negation shift, whose completeness the reduction invokes.","marker":"[12]"},{"why":"Supplies the reduction technique that pushes strong negation down to prime formulas.","marker":"[14]"},{"why":"Introduces potential omniscience and its Kripke-semantic treatment in first-order strong-negation logic.","marker":"[15]"},{"why":"Introduced BDi, the intuitionistic counterpart of BD+ that the paper extends.","marker":"[16]"},{"why":"Gives the first-order BD+ Dunn semantics and completeness theorem on which the new star semantics and BDi rest.","marker":"[18]"},{"why":"Introduced HYPE, the Australian-plan counterpart logic that BDi is compared with.","marker":"[22]"},{"why":"Supplies a semantics for HYPE via a star construction, which the paper connects to its star semantics for BD+.","marker":"[25]"}],"fun_headline_variants":["QBDi3 sound and complete for its Kripke models","Potential omniscience ensures QBDi3 completeness","American vs Australian plans: QBDi3 completeness","First-order BD+ Australian view: QBDi3 proven complete","QBDi3 semantics: sound and complete with potential omniscience"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The completeness proof leans on the strong completeness of the intermediate logic MH for an extended language with fresh predicates and possibly infinite theories, an external theorem that is cited, not proved here, and whose failure would collapse the model-existence step.","fun_headline_variants_meta":{"raw":{"variants":["QBDi3 sound and complete for its Kripke models","Potential omniscience ensures QBDi3 completeness","American vs Australian plans: QBDi3 completeness","First-order BD+ Australian view: QBDi3 proven complete","QBDi3 semantics: sound and complete with potential omniscience"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001419,"raw_usage":{"total_tokens":5708,"prompt_tokens":903,"completion_tokens":4805,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":519,"completion_tokens_details":{"reasoning_tokens":4719}},"tokens_in":519,"tokens_out":4805,"duration_ms":36674,"temperature":1.0,"reasoning_tokens":4719,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T22:49:33.436387+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find a QBDi3-model with maximal successors, monotone extensions and anti-extensions, and potential omniscience that fails one of the axioms (i1), (i2), or (i3) at some state; that would refute soundness. Alternatively, exhibit a reduced set $\\Gamma\\cup\\{A\\}$ such that the translated theory $f(\\Gamma)'\\cup E_{f(\\Gamma\\cup\\{A\\})}$ is MH-derivable for $f(A)'$ while $\\Gamma\\not\\vdash_{\\mathrm{i3}} A$, which would refute Proposition 21 and with it the completeness argument.","supporting_citations":[{"cited_title":"Mojtaba Mojtahedi (2014): Completeness of intermediate logics with doubly negated axioms","cited_arxiv_id":null,"evidence_quote":"Supplies the strong completeness of the intermediate logic MH used in the model-existence step."},{"cited_title":"The Journal of Symbolic Logic 37(1), pp","cited_arxiv_id":null,"evidence_quote":"Provides the intermediate logic MH with the double negation shift, whose completeness the reduction invokes."},{"cited_title":"Logic Journal of IGPL 11(6), pp","cited_arxiv_id":null,"evidence_quote":"Introduces potential omniscience and its Kripke-semantic treatment in first-order strong-negation logic."},{"cited_title":"Journal of Logic, Language and Information 30, p","cited_arxiv_id":null,"evidence_quote":"Introduced BDi, the intuitionistic counterpart of BD+ that the paper extends."},{"cited_title":"In: International Workshop on Logic, Rationality and Interact ion, Springer, pp","cited_arxiv_id":null,"evidence_quote":"Gives the first-order BD+ Dunn semantics and completeness theorem on which the new star semantics and BDi rest."},{"cited_title":"Journal of Philosophical Logic 48(2), pp","cited_arxiv_id":null,"evidence_quote":"Introduced HYPE, the Australian-plan counterpart logic that BDi is compared with."},{"cited_title":"Journal of Philosophical Logic 50(1), pp","cited_arxiv_id":null,"evidence_quote":"Supplies a semantics for HYPE via a star construction, which the paper connects to its star semantics for BD+."}],"review_version":1}