Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Failure of the strong feasible disjunction property

Jan Krajicek

Abstract

A propositional proof system $P$ has the strong feasible disjunction property iff there is a constant $c \geq 1$ such that whenever $P$ admits a size $s$ proof of $\bigvee_i α_i$ with no two $α_i$ sharing an atom then one of $α_i$ has a $P$-proof of size $\le s^c$. It was proved by K. (2025) that no proof system strong enough admits this property assuming a computational complexity conjecture and a conjecture about proof complexity generators. Here we build on Ilango (2025) and Ren et al. (2025) and prove the same result under two purely computational complexity hypotheses: - there exists a language in class E that requires exponential size circuits even if they are allowed to query an NP oracle, - there exists a P/poly demi-bit in the sense of Rudich (1997).

Failure of the strong feasible disjunction property

Abstract

A propositional proof system has the strong feasible disjunction property iff there is a constant such that whenever admits a size proof of with no two sharing an atom then one of has a -proof of size . It was proved by K. (2025) that no proof system strong enough admits this property assuming a computational complexity conjecture and a conjecture about proof complexity generators. Here we build on Ilango (2025) and Ren et al. (2025) and prove the same result under two purely computational complexity hypotheses: - there exists a language in class E that requires exponential size circuits even if they are allowed to query an NP oracle, - there exists a P/poly demi-bit in the sense of Rudich (1997).

Paper Structure

This paper contains 15 sections, 4 theorems, 15 equations.

Table of Contents

  1. Proof complexity preliminaries
  2. Generator from demi-bits
  3. (1)
  4. (2)
  5. (3)
  6. (4)
  7. (5)
  8. (6)
  9. The failure of the fdp
  10. (1)
  11. (2)
  12. (3)
  13. (4)
  14. (5)
  15. A remark on uniformity

Key Result

Theorem 1.1

There exists a pps with $1$ of advice that simulates all pps with $1$ of advice and, in particular, it simulates all pps. $\blacktriangleleft$$\blacktriangleleft$

Theorems & Definitions (6)

  • Theorem 1.1: Cook-K.CK
  • Conjecture 1.2: Kra-dual, Kra-strong, k4
  • Theorem 1.3: k4
  • Conjecture 2.1: Demi-bit conjecture, Rudich Rud
  • Theorem 2.2: Ilango Ila
  • Theorem 3.1