[Proof Complexity] A new preprint
Martin Maxa
mrmaxa at gmail.com
Wed Jan 7 09:23:02 CET 2026
Dear all,
My new preprint "Effective Disjunction and Effective Interpolation in
Sufficiently Strong Proof Systems"
is available on ArXiv: http://arxiv.org/abs/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} = N$; then there exists an exponential time algorithm
which for
every input n (of length O(logn)) finds i ∈ {1,2} such that $n \in A_{i}$.
Suggestions and comments are most welcome!
Best wishes
Martin Maxa
More information about the Proof-Complexity
mailing list