Effective Disjunction and Effective Interpolation in Suffciently Strong Proof Systems

Martin Maxa

REVIEW 4 major objections 6 minor 5 references

Effective Disjunction and Effective Interpolation in Suffciently Strong Proof Systems

T0 review · 4 major / 6 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2601.02821 v2 pith:EG447RO5 submitted 2026-01-06 math.LO

Martin Maxa This is my paper · ORCID

classification math.LO MSC 03F2003B4568Q15

keywords proofcomplexityeffectiveinterpolationdisjunctionExtendedFregeboundedarithmeticmodalprovabilitylogicNE/coNEcollapseuniformproperties

topics P versus NP

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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

What would settle it

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.

Watch

Extended reading notes

Core claim

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

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Colleague,

Two 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.

Two 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.

Credit 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.

This 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.

Referee Report

4 major / 6 minor

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.

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 (4)

[§4, Theorem 15 and Definition 14 (axiom T)] 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
[§5, Proposition 35] 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.
[§5, Theorem 34] 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.
[§4, Theorem 29 vs Theorem 30] 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.

minor comments (6)

[Title] The title contains a typo: 'Suffciently' should be 'Sufficiently'.
[§4, Lemma 16] 'Suppose the proof systen G*_1 ...' — 'systen' should be 'system'.
[§2, Definition 4 and §5, Definition 31] 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.
[§3, Theorem 5] 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.
[§4, Definition 14] 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.
[§5, Theorem 36] 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.

Circularity Check

1 steps flagged · score 4.0 of 10

The written proof has a circular dependency: Theorem 29 and Theorem 30 each cite the other for the transfer of the .3-property to normal systems; unproved modal-logic soundness is a separate correctness gap.

other [Theorem 29 proof and Theorem 30 proof (Section 4)]
"From Theorem 30, it then follows that every normal proof system for which G∗1 ≤1_p S holds also has the .3-property. [...] (1) If G∗1 has the .2-property, then from Theorem 20, it also has the uniform effective disjunction property. Now apply Theorem 29."

Theorem 29's proof derives the key transfer step (G*1 has .3 ⇒ normal S has .3) by citing Theorem 30. Theorem 30's proof derives its conclusion by applying Theorem 29. As written, the two proofs are mutually dependent: neither is established before the other. The transfer step is exactly what Theorem 24 proves independently, so the cycle is avoidable, but the text as given does not break it.

full rationale

The paper's main claim is a conditional transfer (if G*1/EF has a uniform property, then every 'normal' S has it), and the proof uses a newly introduced 'logic of polynomial provability'. There is no fitted data, no prediction-as-fit, and no self-citation chain. The single concrete circularity in the written derivation is the mutual dependency between Theorem 29 and Theorem 30: Theorem 29's proof cites Theorem 30 to transfer the .3-property to normal systems, and Theorem 30's proof applies Theorem 29; since Theorem 24 already supplies that transfer, this appears to be a cross-reference error, but as written it is a cycle. Separately flagged but not circular: Theorem 15 (soundness of the modal logic) is not proved ('we leave the proof to the reader'), and its axiom T is a reflection principle for G*1 that is not known to be provable in V1^1; Prop. 35 (normality of G*1+) is also stated without proof and is load-bearing for the NE∩coNE=E collapse. These are unsupported premises/correctness risks rather than reductions of the target to its inputs, so they do not by themselves raise the circularity score above the moderate range.

Assumptions & free parameters 0 free parameters · 5 assumptions · 2 invented entities

The central conditional result rests on a large custom deductive apparatus: a new modal provability logic, a normality condition asserted for all sufficiently strong systems, and the unproved normality of the system built from a disjoint NE-pair. The only free 'parameters' are the modal indices i,j,k, which are existential integers rather than fitted data.

assumptions (5)

ad hoc to paper The polynomial-provability modal logic of Definition 14 is V1^1-valid and hence sound for G*1 (Theorem 15).
This newly introduced logic carries the transfer proofs; the paper leaves the proof to the reader, and a single unsound rule would invalidate Theorems 20, 24, and 29.
ad hoc to paper Every sufficiently strong proof system—including G*_i for i≥2 and G*+_1—is normal, i.e. obeys the same polynomial-provability logic and satisfies G*1 ≤1_p S (Definition 26; Proposition 35).
Normality is asserted without proof ('We state the following proposition without proof' for Prop. 35); the transfer theorem and the NE∩coNE=E conclusion depend on it.
domain assumption V1^1 proves Claim 22: for Σ1,b0 α, ∀P α(x,P) ↔ ∀π ¬Prf_{G*1}(p(x),⟨∃P¬α⟩)[π], relying on bounded reflection and polynomial provability of true Σ^q_1 tautologies.
Used in Theorem 20 to convert second-order universal statements into statements about absence of short proofs; it is a standard-style bounded-arithmetic fact but not proved in detail.
domain assumption G*1 proofs may be assumed to contain only Σ^q_1 formulas (stated WLOG without proof near the start of §3).
The proof of Claim 6/Theorem 5 uses this to make the induction on proof trees go through; no justification is supplied.
domain assumption EF and G*1 are interchangeable ('properties of the proof system G*1 (or equivalently EF)').
The transfer and collapse theorems move between EF and G*1 without a proof of p-equivalence in the relevant sense.

invented entities (2)

Normal proof system (Definition 26)
purpose: Defines the class of 'sufficiently strong' proof systems to which the transfer theorem applies; includes G*_i and the enlarged G*+_1.
No independent evidence beyond assertion; normality carries the modal logic's algorithmic ▲-semantics, which is close in strength to the property being transferred.
Logic of polynomial provability with modal operators △i, △i_p, ▲i, ▲i_p (Definitions 8–14)
purpose: Gives a proof-theoretic calculus used to prove transfer of .2/.3 properties.
Introduced for this paper; soundness (Theorem 15) is deferred to the reader, so no external falsifiable handle is provided.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Effective Disjunction and Effective Interpolation in Suffciently Strong Proof Systems." pith.science (2026). https://pith.science/paper/EG447RO5

@misc{pith2026260102821,
  author       = {Pith},
  title        = {Pith review of: Effective Disjunction and Effective Interpolation in Suffciently Strong Proof Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EG447RO5}},
  note         = {Machine review of arXiv:2601.02821}
}

abstract

In this article, we deal with the uniform effective disjunction property and the uniform effective interpolation property, which are weaker versions of the classical effective disjunction property and the effective interpolation property.\\ The main result of the paper is as follows: Suppose the proof system $EF$ (Extended Frege) has the uniform effective disjunction property, then every sufficiently strong proof system $S$ that corresponds to a theory $T$, which is a theory in the same language as the theory $V_{1}^{1}$, also has the uniform effective disjunction property. Furthermore, if we assume that $EF$ has the uniform effective interpolation property, then the proof system $S$ also has the uniform effective interpolation property.\\ From this, it easily follows that if $EF$ has the uniform effective interpolation property, then for every disjoint $NE$-pair, there exists a set in $E$ that separates this pair. Thus, if $EF$ has the uniform effective interpolation property, it specifically holds that $NE \cap coNE = E$. Additionally, at the end of the article, the following is proven: Suppose the proof system $EF$ has the uniform effective interpolation property, and let $A_{1}$ and $A_{2}$ be a (not necessarily disjoint) NE-pair such that $A_{1} \cup A_{2} = \mathbb{N}$; then there exists an exponential time algorithm which for every input $n$ (of length $O(\log n)$) finds $i\in\{1,2\}$ such that $n\in A_{i}$.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

5 extracted references

[1]

Pudlák,The Lengths of Proofs, in Handbook of Proof Theory, 1998

P. Pudlák,The Lengths of Proofs, in Handbook of Proof Theory, 1998

1998
[2]

Krajíček,Bounded arithmetic, propositional logic, and complexity theory, 1995

J. Krajíček,Bounded arithmetic, propositional logic, and complexity theory, 1995

1995
[3]

Krajíček,Proof Complexity, 2019

J. Krajíček,Proof Complexity, 2019

2019
[4]

M. Baaz, A. Ciabattoni, C. G. Fermüller,Hypersequent Calculi for Gödel Logics — a Survey, Journal of Logic and Computation, Volume 13, Issue 6, 2003

2003
[5]

Kurokawa,Hypersequent Calculi for Modal Logics Extending S4, in In: Nakano, Y., Satoh, K., Bekki, D

H. Kurokawa,Hypersequent Calculi for Modal Logics Extending S4, in In: Nakano, Y., Satoh, K., Bekki, D. (eds) New Frontiers in Artificial Intelligence. JSAI 2014 25

2014

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.

[1] [1]

Pudlák,The Lengths of Proofs, in Handbook of Proof Theory, 1998

P. Pudlák,The Lengths of Proofs, in Handbook of Proof Theory, 1998

1998

[2] [2]

Krajíček,Bounded arithmetic, propositional logic, and complexity theory, 1995

J. Krajíček,Bounded arithmetic, propositional logic, and complexity theory, 1995

1995

[3] [3]

Krajíček,Proof Complexity, 2019

J. Krajíček,Proof Complexity, 2019

2019

[4] [4]

M. Baaz, A. Ciabattoni, C. G. Fermüller,Hypersequent Calculi for Gödel Logics — a Survey, Journal of Logic and Computation, Volume 13, Issue 6, 2003

2003

[5] [5]

Kurokawa,Hypersequent Calculi for Modal Logics Extending S4, in In: Nakano, Y., Satoh, K., Bekki, D

H. Kurokawa,Hypersequent Calculi for Modal Logics Extending S4, in In: Nakano, Y., Satoh, K., Bekki, D. (eds) New Frontiers in Artificial Intelligence. JSAI 2014 25

2014