{"id":"e6843a83-5070-4598-8404-07aab0c272fc","arxiv_id":"2601.02821","paper_version":2,"verdict":"REJECT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"If EF has uniform effective interpolation, then all 'normal' proof systems have it and disjoint NE-pairs are separated by a set in E, giving NE∩coNE=E.","lead":"The paper proves conditional transfer theorems: if Extended Frege has uniform effective disjunction or interpolation, then 'sufficiently strong' proof systems inherit the property, and disjoint NE-pairs become separable in E. It is a proof-complexity paper whose headline consequence (NE∩coNE=E, conditional on EF's interpolation) rests on several unproved assertions.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Unproved soundness of the modal provability logic (Theorem 15) is the load-bearing weakness: axiom T demands V1^1-provable reflection for G*1, which is not established and is likely unprovable, so the transfer theorem collapses.","rationale":"The reader's weakest_assumption identifies the unproved soundness of Theorem 15 as the first load-bearing step. This is indeed the most fundamental issue: the paper's modal logic is a black box whose soundness is asserted, and a specific axiom (T) makes soundness equivalent to a reflection principle that V1^1 cannot prove. Without Theorem 15, the chain from G*1's uniform effective disjunction/interpolation to .2/.3-properties and then to all normal systems is unsupported. The other concerns raised by the reader (Proposition 35 unproved normality of G*1+, and applying UEIP to Π formulas) are real and would independently block Theorem 34, but they are downstream of the modal-logic failure; even a correct Proposition 35 would not rescue Theorem 29 if the modal logic is unsound. I therefore agree with the reader's rejection, and no change to the verdict is needed.","tokens_in":21461,"tokens_out":9963,"duration_ms":105323,"concrete_test":"Formalize the single modal sequent △^1 p ⇒ p in the logic of Definition 14 and attempt to prove its V1^1-validity under the arithmetic interpretation * with p* := (x = x+1). This is equivalent to V1^1 proving ∃n0∀x≥n0(Prf_G*1(x^1, ⟨x=x+1⟩_x) → (x=x+1)), a uniform consistency statement for G*1. Because V1^1 is consistent and can formalize G*1's syntax, Gödel's second incompleteness forbids such a proof; hence axiom T cannot be a valid initial sequent, and Theorem 15 fails. If the author instead intends to drop or restrict axiom T, every subsequent derivation using it—especially Lemma 28's finite-consistency step—must be re-derived without that axiom.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central transfer theorem (Theorem 29) rests on the soundness of the 'logic of polynomial provability' (Theorem 15). Yet Theorem 15 is explicitly not proved: 'we leave the proof to the reader.' The obstruction is axiom T (Definition 14): △iA ⇒ A. Under Definition 10, (△iA)* is ∃π Prf_G*1(x^i, ⟨A*⟩_x), so V1^1-validity of this axiom would require V1^1 to prove a uniform reflection principle for G*1. Taking A = p with p* := (x = x+1), this reduces to V1^1 proving ∃n0∀x≥n0(Prf_G*1(x^i, ⟨x=x+1⟩_x) → (x=x+1)), i.e., the consistency of G*1. By Gödel's second incompleteness, no consistent, sufficiently strong theory can prove such a consistency statement; V1^1 is such a theory. Consequently Theorem 15 is not merely unproved but false as stated. Since Lemmas 16, 17, 21, 23, Proposition 37, and Theorems 20, 24, 29 all use this modal logic to justify G*1-validity, the entire transfer argument loses its foundation. The final collapse theorem (Theorem 34) also depends on this via Proposition 35, but even if Proposition 35 were true, the modal-logic soundness failure would still invalidate the transfer to G*1+.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies uniform effective disjunction and uniform effective interpolation for proof systems tied to the bounded arithmetic theory V_1^1. Its main theorem is conditional on the corresponding property for the system G*_1 (equivalently EF): if G*_1 has uniform effective disjunction, then every 'normal' sufficiently strong proof system S has it, and if G*_1 has uniform effective interpolation, then every normal S also has it. From this the paper derives two consequences: under uniform effective interpolation for EF, every disjoint NE-pair is separated by a set in E (so NE∩coNE=E), and for any NE-pair covering N there is an exponential-time algorithm that, on input n of length O(log n), selects an index i with n∈A_i. The proof strategy is a modal logic of polynomial provability, with operators △_i and ▲_i, plus a normality condition on proof systems. The main argument is purely theoretical and explicitly conditional; there are no empirical or fitted components.","tokens_in":22005,"tokens_out":7933,"duration_ms":403796,"significance":"If the main results were established, they would be a striking contribution to proof complexity and to the connection between propositional proof systems and complexity classes: uniform effective interpolation for EF would yield a collapse-style separation of NE∩coNE by E. The paper is also commendably explicit about the conditional structure: the conclusions are not asserted unconditionally, and no parameters are hidden after the hypotheses are fixed. However, the entire transfer theorem rests on two pillars that are not supplied: the soundness of the modal logic of polynomial provability (Theorem 15) and the normality of the enlarged system G*+_1 (Proposition 35). The soundness claim is not merely unproved; its axiom T appears to be false when interpreted in V_1^1, since it demands a weak reflection principle for G*_1. The stress-test concern lands. The paper therefore cannot currently serve as a proof of its advertised theorems.","major_comments":[{"comment":"The soundness of the modal logic is load-bearing and is explicitly not proved: 'The fact that all initial sequents are V_1^1-valid ... can be easily proved and we leave the proof to the reader.' This is not a routine omission. Under Definition 10, (△_i A)* is ∃π Prf_{G*_1}(x^i, ⟨A*(y)⟩_x)[π]. The axiom △_i A ⇒ A would therefore require V_1^1 to prove, for every A*, a bounded reflection principle for G*_1. Taking A = ⊥ with ⊥* := (x = x+1), the sequent △_i⊥ ⇒ ⊥ translates into a statement that, for all sufficiently large x, there is no G*_1 proof of a contradictory formula, i.e. a consistency statement for G*_1. By Gödel's second incompleteness, no consistent sufficiently strong theory such as V_1^1 proves such a statement. Thus Theorem 15 is not just unproved but appears to be false as stated. Since Lemmas 16, 17, 21, 23 and Theorems 20, 24, 29 all rely on this modal logic for their vali","section":"§4, Theorem 15 and Definition 14 (axiom T)"},{"comment":"Proposition 35 is stated without proof and is load-bearing for Theorem 34. It asserts two things: that G*+_1 corresponds to V_1^+_1, and that G*+_1 is a normal proof system. Normality (Definition 26) requires G*+_1 to satisfy the same 'logic of polynomial provability' as G*_1 and G*_1 ≤^1_p G*+_1. The latter is plausible because G*+_1 extends G*_1 by axioms, but the former is exactly the kind of soundness claim that already fails for G*_1 in Theorem 15. Adding a new axiom schema to the proof system changes the provability predicate; no proof is provided that the modal logic, including axiom T, remains V_1^1-valid or G*_1-valid for G*+_1. The assertion that adding propositional counterparts of ¬A′∨¬B′ to G*_1 yields the same correspondence as adding ¬A′∨¬B′ to V_1^1 is also nontrivial and is not established. Until Proposition 35 is proved, Theorem 34 cannot be derived from Theorem 29.","section":"§5, Proposition 35"},{"comment":"Even granting Theorem 29 and Proposition 35, the final step of Theorem 34 applies the uniform effective interpolation property to the formulas ¬A′(x,P) and ¬B′(x,Q). But Definition 1 defines uniform effective interpolation only for pairs of Σ^{1,b}_0 formulas. The negations of Σ^{1,b}_0 formulas are Π^{1,b}_0, not Σ^{1,b}_0. No extension of the definition or of the transfer theorem to Π^{1,b}_0 formulas is stated or proved in the manuscript. The proof requires a strengthened version of the interpolation/disjunction property for a class of formulas that the paper does not handle. This is a load-bearing gap: it is exactly the step that produces a proof in G*+_1 of either ¬⟨A′⟩_n or ¬⟨B′⟩_n and hence the separator C∈E.","section":"§5, Theorem 34"},{"comment":"The proof of Theorem 29 refers to 'Theorem 30' before Theorem 30 is stated. This is a presentation issue, not a technical one, but it reflects a broader organizational problem: Theorem 30 appears after the theorem that depends on it, and the reader is forced to re-derive the dependency. Reordering would help. I do not count this as a technical error.","section":"§4, Theorem 29 vs Theorem 30"}],"minor_comments":[{"comment":"The title contains a typo: 'Suffciently' should be 'Sufficiently'.","section":"Title"},{"comment":"'Suppose the proof systen G*_1 ...' — 'systen' should be 'system'.","section":"§4, Lemma 16"},{"comment":"Notation is occasionally ambiguous: in Definition 31, L_A is written as {A(n) | ⟨A(x)⟩_n is satisfiable}; it should clarify that A(n) is a string and n is its numerical encoding. Similar notational issues occur around the translation ⟨α(x)⟩_n.","section":"§2, Definition 4 and §5, Definition 31"},{"comment":"The proof says 'without loss of generality, we assume that only Σ^q_1 formulas occur in every proof in the system G*_1'; this assumption is used but not justified in detail. A brief justification or reference would be helpful.","section":"§3, Theorem 5"},{"comment":"The modal calculus includes both △ and ▲ operators and their subscripted variants, and it is easy to lose track of which variants satisfy which axioms. A table or a displayed list of all initial sequents would substantially improve readability.","section":"§4, Definition 14"},{"comment":"The statement says 'there exists an algorithm which works in exponential time with respect to an input n of length O(log n)'; this is equivalent to polynomial time in 1^n, but the phrasing is potentially confusing. Clarify whether the input is a natural number n or a binary string.","section":"§5, Theorem 36"}],"recommendation":"reject","confidential_remarks":"The central results are interesting if true, but the current manuscript has load-bearing unproved assertions, and the soundness theorem for the modal logic appears to be false as stated. The unproved Proposition 35 is also presented as a black box. These are not local repairs: the proof strategy itself depends on reflection principles that V_1^1 cannot provide. I would not encourage a revision within the current scope; a fundamentally different approach would be needed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nTwo things to know up front. The paper is original: the .2/.3 properties, the modal logic of polynomial provability, and the transfer template from G*1 to arbitrary 'normal' systems are genuinely new, as is the conditional NE-separation consequence. If the main theorem ever closes, it is a real bridge from proof complexity to E vs NE. But the central argument does not close. The stress-test lands on the soundness of the modal logic (Theorem 15): the proof is explicitly left to the reader, and taking axiom T with an atom interpreted as a false sentence forces V1^1 to prove a bounded consistency statement for G*1 that is equivalent, formally inside V1^1, to Con(G*1). That is beyond what any consistent theory as strong as V1^1 can prove. So Theorem 15 is not merely deferred; it is false as stated, and everything downstream—Lemmas 16, 17, 21, 23 and Theorems 20, 24, 29—depends on it.\n\nTwo further soft spots, in proportion. Proposition 35, which asserts that G*1+ is normal and corresponds to V1+1, is stated without proof and is load-bearing for the NE∩coNE=E collapse; that is a genuine gap. And Theorem 34 applies uniform effective interpolation to the Π1,b0 formulas ¬A', ¬B', while Definition 1 only defines it for Σ1,b0 formulas; likely repairable by symmetry, but as written the call is out of scope.\n\nCredit where due: Theorem 5's argument is substantive, the Cook-Levin-style reduction in Theorem 32 is solid, and the paper is candid about its gaps—it flags both deferred proofs rather than hiding them. The reader's REJECT verdict is fair; the conditional may be repairable, but the current manuscript does not support its main claims.\n\nThis is a paper for proof complexity researchers, bounded-arithmetic people, and anyone interested in a modal attack on NE vs coNE. It deserves a serious referee rather than a desk reject: the flaws are pinpointable, the ideas are reusable, and a mandatory revision—prove or repair soundness of the modal logic, prove Proposition 35, and fix the Σ/Π mismatch—could put the transfer on solid ground. Send it to review, with clear instructions that the author must address these three points before the claims can stand.","headline":"Original conditional machinery that deserves referee time; the unproved and likely false soundness theorem for the modal logic, plus two other explicit gaps, keep the main claims from holding as written.","tokens_in":22335,"tokens_out":13048,"would_cite":false,"duration_ms":137136,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F20","03B45","68Q15"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims to show that uniform effective interpolation in Extended Frege would transfer to every normal proof system and collapse NE∩coNE to E.","keywords":["proof complexity","effective interpolation","effective disjunction","Extended Frege","bounded arithmetic","modal provability logic","NE/coNE collapse","uniform effective properties"],"falsifier":"Find one disjoint NE-pair (A,B) and prove that no set in E separates them; if such a pair exists while EF had uniform effective interpolation, Theorem 34 would be false. A more local falsifier: formalize the modal logic and check the sequent ⇒▲_{i+1}^p(△_i^p A⇒A) (or any initial sequent of Definition 14) for V_1^1-validity, and check G*^{+1}_1 for normality for a concrete NE-pair—a single counterexample to either unproved step breaks the transfer chain before any complexity collapse is derived.","tokens_in":21393,"feed_emoji":"🔗","tokens_out":13677,"duration_ms":118747,"temperature":0.7,"pith_summary":"The paper's central claim is a transfer theorem: if the quantified propositional proof system G*_1 (equivalent to Extended Frege) has the uniform effective disjunction property, then every normal proof system has it, and if G*_1 has the uniform effective interpolation property, every normal proof system has that too. The transfer is routed through a modal logic of polynomial provability, whose box-like operators talk about proofs of bounded length, and through two modal properties named .2 and .3. The complexity-theoretic payoff is conditional: assuming EF has uniform effective interpolation, every disjoint pair of languages in NE is separated by a language in E, so NE∩coNE=E—the exponential-time analogue of NP∩coNP=P. A second consequence gives an exponential-time algorithm that, for any NE-pair covering the naturals, decides which of the two sets contains a given input. The proof chain includes two unproved load-bearing steps: the soundness of the modal logic is left to the reader, and the enlarged system built from a disjoint NE-pair is declared normal without proof.","feed_headline":"If Extended Frege interpolates, NE∩coNE would collapse to E","feed_subtitle":"A single property of Extended Frege would force the exponential-time collapse NE∩coNE=E, via a modal logic of proof lengths.","key_machinery":"The key object is the logic of polynomial provability: a modal sequent calculus whose operators △_i and ▲_i formalize 'provable in G*_1 by a proof of length at most x^i' and, for ▲_i, 'with a proof produced by a polynomial-time algorithm'. Its arithmetic translations land in Σ^{1,b}_1 or Π^{1,b}_1 formulas of bounded arithmetic. The working parts are the modal axioms .2 and .3: .3 lets a proof reorder the hypotheses of two provability implications, and Lemma 23 performs that reordering inside the modal logic; Theorem 24 then carries .3 from G*_1 to every system that simulates it with polynomial overhead; Lemma 28 converts .3 into uniform effective disjunction or interpolation. The enlarged s","core_discovery":"The core discovery is a reduction: uniform effective interpolation of G*_1 forces the same property on every normal proof system. The mechanism is the .3-property, a modal splitting principle that lets one prove, for any two formulas, a disjunction of the two implications between their provability statements, with a polynomial-time witness when interpolation is assumed. The paper shows .3 transfers from G*_1 to any system that simulates G*_1 with polynomial overhead and respects the logic of polynomial provability, and that in such a normal system .3 can be converted back into uniform effective interpolation. This transfer is then applied to an enlarged proof system built by adding, for a di","pith_inferences":["Editor's inference: the most economical test of the paper's conditional is to formalize the omitted soundness proof (Theorem 15) and the unproved normality claim (Proposition 35) in a weak base theory; a gap in either would locate exactly where the transfer breaks.","Editor's inference: the construction of G*^{+1}_1 suggests a searchable counterexample strategy—find a disjoint NE-pair for which the enlarged system fails normality or the logic's soundness; that would block the collapse without directly refuting EF's interpolation property.","Editor's inference: the paper leaves the complexity consequences of uniform effective disjunction (without interpolation) unexplored; an extension that carries the disjunction version through Definition 1's Σ^{1,b}_0 restriction might yield a weaker but unconditional separation statement."],"forward_implications":["If EF has the uniform effective interpolation property, every disjoint pair of NE languages has a separator in E, and in particular NE∩coNE=E.","If EF has the uniform effective interpolation property, then for any NE-pair A1,A2 with A1∪A2=N there is an exponential-time algorithm that, on input n (of length O(log n)), outputs an i with n∈Ai.","If EF has only the uniform effective disjunction property, every normal proof system inherits that disjunction property; this part needs no polynomial-time witness.","The transfer works through the .3-property, so the same conclusion follows if G*_1 starts from the .2 modal axiom rather than from the disjunction or interpolation property.","A single failure of the transfer in any normal proof system would imply that G*_1 lacks the corresponding uniform property: the two properties are equivalent across the class of normal systems."],"fun_headline_variants":["EF interpolation would collapse NE∩coNE to E","If EF uniformly interpolates, then NE∩coNE=E","Extended Frege interpolation would imply NE∩coNE=E","Uniform interpolation in EF collapses NE∩coNE to E","If Extended Frege interpolates, NE∩coNE equals E"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The load-bearing premise is that the logic of polynomial provability is sound (Theorem 15, whose proof is left to the reader) and that the enlarged system G*^{+1}_1, built by adding an arbitrary disjoint NE-pair as axioms, is still normal (Proposition 35, stated without proof); the collapse also requires applying uniform effective interpolation to the negated formulas ¬A′,¬B′, which the definition of uniform effective interpolation only gives for Σ^{1,b}_0 formulas.","fun_headline_variants_meta":{"raw":{"variants":["EF interpolation would collapse NE∩coNE to E","If EF uniformly interpolates, then NE∩coNE=E","Extended Frege interpolation would imply NE∩coNE=E","Uniform interpolation in EF collapses NE∩coNE to E","If Extended Frege interpolates, NE∩coNE equals E"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000618,"raw_usage":{"total_tokens":2747,"prompt_tokens":831,"completion_tokens":1916,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":575,"completion_tokens_details":{"reasoning_tokens":1833}},"tokens_in":575,"tokens_out":1916,"duration_ms":12351,"temperature":1.0,"reasoning_tokens":1833,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T06:26:13.629273+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find one disjoint NE-pair (A,B) and prove that no set in E separates them; if such a pair exists while EF had uniform effective interpolation, Theorem 34 would be false. A more local falsifier: formalize the modal logic and check the sequent ⇒▲_{i+1}^p(△_i^p A⇒A) (or any initial sequent of Definition 14) for V_1^1-validity, and check G*^{+1}_1 for normality for a concrete NE-pair—a single counterexample to either unproved step breaks the transfer chain before any complexity collapse is derived.","supporting_citations":[],"review_version":1}