Disjunction-free
disjunction property
Emil Jeřábek

Institute of Mathematics
Czech Academy of Sciences
jerabek@math.cas.cz
https://users.math.cas.cz/~jerabek/

Computability in Europe, Batumi
Shota Rustaveli State University, 27 July 2023

Outline
1 Classical proof complexity

2 Non-classical proof complexity

3 Lower bound for implicational logic

Classical proof complexity
1 Classical proof complexity

2 Non-classical proof complexity

3 Lower bound for implicational logic

Propositional proof systems
Proof system (pps): relation P ⊆ Form × Σ∗ s.t.
I P is decidable in polynomial time
I ϕ is a tautology ⇐⇒ ∃π P(ϕ, π)
Main measure: length (=size) of proofs
I P polynomially bounded if all tautologies ϕ have P-proofsof size ≤ |ϕ|c
I P p-simulates Q (P ≥p Q):
polynomial-time translation of Q-proofs to P-proofs
I P and Q are p-equivalent (P ≡p Q): P ≥p Q & Q ≥p P
Theorem (Cook, Reckhow ’79):
NP = coNP ⇐⇒ ∃ polynomially bounded pps
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

1:17

Frege (aka Hilbert-style) systems
R: finite set of schematic Frege rules α1 , . . . , αk ` α0R-derivation of ϕ from Γ: ϕ0 , . . . , ϕt = ϕ where each ϕiderived from ϕj , j < i by an instance of an R-rule, or ϕi ∈ ΓIf Γ `R ϕ ⇐⇒ Γ  ϕ: Frege system FR
I typically: modus ponens + axiom schemata
I all Frege systems p-equivalent (Reckhow ’76)=⇒ write F = FRI p-equivalent to tree-like Frege F∗ (Krajı́ček ’94)
I p-equivalent to sequent calculus and natural deduction(Reckhow ’76)
I known lower bounds: number of lines Ω(n), size Ω(n2 )(Krajı́ček ’95)
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

2:17

Feasible interpolation
General lower bound method for weak pps (Krajı́ček ’97):
P has feasible interpolation if for every P-proof Π ofβ(~p , ~r ) → α(~p , q~ )there exists a Boolean circuit C (~p ), |C | ≤ |Π|c , s.t.
 β(~p , ~r ) → C (~p ), C (~p ) → α(~p , q~ )Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

3:17Feasible interpolation
General lower bound method for weak pps (Krajı́ček ’97):
P has feasible interpolation if for every P-proof Π ofα(~p , q~ ) ∨ β(~p , ~r )there exists a Boolean circuit C (~p ), |C | ≤ |Π|c , s.t.
C (~p )  α(~p , q~ ),¬C (~p )  β(~p , ~r )Theorem: If P has f.i., and ∃ a disjoint NP-pair not separable
by polynomial-size circuits, then P is not polynomially boundedEmil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

3:17

Circuit lower bounds
Lower bounds on the size of general circuits:
I random functions {0, 1}n → {0, 1}: size & 2n /n whp
I explicit functions: size ≥ 5n or so=⇒ f.i. only yields conditional lower bounds
Monotone circuits (∧, ∨, 0, 1):
I Razborov ’85: superpolynomial lower bound for Clique
I Alon–Boppana ’87: improved to exponential lower boundI also applies to the Clique–Colouring NP-pair (Tardos ’87)
Theorem (Alon–Boppana’87):√For k = b nc, any monotone circuit separating k-colourablen-vertex graphs from graphs containing a (k + 1)-clique has
1/4size nΩ(n )Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

4:17

Monotone feasible interpolation
P has monotone feasible interpolation if for every P-proof Π ofα(~p , q~ ) ∨ β(~p , ~r )where p~ only occur positively in α,
there exists a monotone circuit C (~p ), |C | ≤ |Π|c , s.t.
C (~p )  α(~p , q~ ),¬C (~p )  β(~p , ~r )Theorem: If P has m.f.i. then P is not polynomially bounded
Example:Resolution has f.i. and m.f.i.
Frege likely does not
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

5:17

Non-classical proof complexity
1 Classical proof complexity

2 Non-classical proof complexity

3 Lower bound for implicational logic

Non-classical Frege systems
L finitely axiomatizable propositional logic =⇒ Frege system L-F
Unconditional exponential lower bounds for many logics L:
I Hrubeš ’07,’09: some modal logics, intuitionistic logic(Frege, Extended Frege)
I J. ’09: extensions of K4 or IPC with unbounded branching
I Jalali ’21: extensions of FL included in . . .
Further strengthening:
I exponential separation between Extended Frege andSubstitution Frege (J. ’09)
I purely implicational tautologies (J. ’17)
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

6:17

Feasible disjunction property
P proof system for L ⊇ IPC:
P has the feasible disjunction property if given a P-proof ofϕ0 ∨ ϕ1 , we can compute in polynomial time i ∈ {0, 1} suchthat `L ϕiModal logics: the same with 2ϕ0 ∨ 2ϕ1
Example: IPC-F has f.d.p.
(Buss–Pudlák ’01) f.d.p. can serve the role of f.i.
=⇒ conditional lower bounds(Hrubeš ’07) analogue of monotone f.i.
=⇒ unconditional lower bounds
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

7:17

f.d.p. serving as f.i.
P ≥p IPC-F closed under substitution of 0, 1:
I α(~p , q~ ) ∨ β(~p , ~r ) classical tautology =⇒ IPC proves(∗)^(pi ∨ ¬pi ) → ¬¬α(~p , q~ ) ∨ ¬¬β(~p , ~r )i<nI if P has f.d.p. and (∗) has a short P-proof:
small circuit C such that for all ~a ∈ {0, 1}n ,C (~a) = 1 =⇒ ` ¬¬α(~a, q~ )C (~a) = 0 =⇒ ` ¬¬β(~a, ~r )Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

8:17

f.d.p. serving as f.i.
P ≥p IPC-F closed under substitution of 0, 1:
I α(~p , q~ ) ∨ β(~p , ~r ) classical tautology =⇒ IPC proves(∗)^(pi ∨ ¬pi ) → ¬¬α(~p , q~ ) ∨ ¬¬β(~p , ~r )i<nI if P has f.d.p. and (∗) has a short P-proof:
small circuit C such thatC (~p )  α(~p , q~ ),¬C (~p )  β(~p , ~r )Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

8:17

In a galaxy far, far away
Persistent claims by L. Gordeev and E. H. Haeusler (2016–):
I implicational IPC tautologies have polynomial-size proofs
in dag-like natural deduction
I NP = PSPACE
I published (’19,’20), some people seem to take it seriously
Flatly contradicts known lower bounds, but this requires acomplex argument, hard to track down by non-specialists:
I IPC-F lower bounds (Hrubeš ’07)
I monotone circuit lower bounds (Alon–Boppana ’87)
I reduction to implicational logic (J. ’17)
I simulation of natural deduction by Frege (idea Reckhow ’76,Cook–Reckhow ’79, but for a different system)=⇒ desire for something simpler/more direct
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

9:17

Lower bound for implicational logic1 Classical proof complexity

2 Non-classical proof complexity

3 Lower bound for implicational logic

Intuitionistic/minimal implicational logic
Language: →, atoms p0 , p1 , p2 , . . .
the set of formulas: Form
Notation: ϕ → ψ → χ → ω = (ϕ → (ψ → (χ → ω)))Frege system F→ :` (ϕ → ψ → χ) → (ϕ → ψ) → (ϕ → χ)
`ϕ→ψ→ϕϕ, ϕ → ψ ` ψ
Sequent calculus LJ→ : structural rules (incl. cut) +ϕ =⇒ ϕΓ =⇒ ϕ Γ, ψ =⇒ αΓ, ϕ → ψ =⇒ αEmil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

Γ, ϕ =⇒ ψΓ =⇒ ϕ → ψ

10:17

Natural deduction
Prawitz-style tree-like natural deduction:[ϕ] ←− discharged..
.

ψϕ ϕ→ψ
(→I)
ψϕ→ψ
I every leaf of the proof tree must be discharged(→E)

Gordeev & Haeusler dag-like natural deduction NM→ :I every leaf of the proof dag must be discharged
on every path to the root
I checkable in polynomial-time:
inductively compute for each node v ∈ V the set
Av = {γu : u leaf, undischarged on some path to v }Notation: hV , E i underlying dag, γv = formula label of node v
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

11:17

Efficient Kleene’s slash
For P ⊆ Form: a P-slash is a unary predicate |ϕ on Form s.t.
|(ϕ → ψ) ⇐⇒ (|ϕ and ϕ ∈ P =⇒ |ψ)
{z}
|
kϕ

I free to choose |p for atoms pI Kleene’s original Γ | ϕ has P = {ϕ : Γ ` ϕ},
we take for P an efficiently computable finite set
For a proof Π: P is Π-closed if ∀v (Av ⊆ P =⇒ γv ∈ P)
Lemma: Π proof of ϕ, P is Π-closed, | is a P-slash =⇒ |ϕI by induction on the length of the proof

Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

12:17

Constructibility of Π-closureclΠ (X ) = smallest Π-closed set P ⊇ X
Observation: ϕ ∈ clΠ (X ) =⇒ X ` ϕclΠ (X ) is computable in polynomial time, moreover:Lemma: Π proof, F = {ϕi : i < n} ⊆ Form, ϕ ∈ Form=⇒ ∃ monotone circuit C of size |Π|3 s.t.
C (x0 , . . . , xn−1 ) = 1 ⇐⇒ ϕ ∈ clΠ ({ϕi : xi = 1})
I describe inductive construction of closure
I only involves formulas from ΠI terminates in |Π| steps
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

13:17

Feasible disjunction property
Theorem: Given a proof Π of
ϕ = α0 (~p ) → u → α1 (~p ) → u → u,
we can compute in polynomial time i ∈ {0, 1} s.t. ` αi
Proof: P = clΠ (α0 → u, α1 → u), | P-slash s.t. -u
We have |ϕ =⇒ ∦(α0 → u) or ∦(α1 → u)∦(αi → u) =⇒ -(αi → u) =⇒ kαi =⇒ αi ∈ P
We can compute i s.t. αi ∈ P
Then: α0 → u, α1 → u ` αi
Substitute > for u =⇒ get ` αi
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

14:17

Monotone feasible interpolation
Theorem: Given a proof Π of(p0 → u) → (p00 → u) → u→ (p1 → u) → (p10 → u) → u→ (p2 → u) → (p20 → u) → u...

→ (pn → u) → (pn0 → u) → u→ α(~p , q~ ) → u → β(~p 0 , ~r ) → u → u,
there is a monotone circuit C of size |Π|3 such thatC (~p )  α(~p , q~ ),¬C (~p )  β(¬~p , ~r )Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

15:17

The lower boundτn : intuitionistic implicational tautologies of size O(n3 )expressing disjointness of the Clique–Colouring NP pair
Monotone feasible interpolation =⇒Lemma: If τn has a proof of size s, then there is a monotone
circuit of size s 3 separating the Clique–Colouring pairAlon–Boppana bound =⇒Theorem: Any proof of τn has size nΩ(n1/4 )Corollary: There are infinitely many intuitionistic implicational
1/12tautologies ϕ that require proofs of size |ϕ|Ω(|ϕ| )Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

16:17

Other calculi
The argument adapts to F→ or LJ→ :I adjust the definition of Π-closed sets
Actually: F→ ≡p LJ→ ≡p NM→ ≡p F∗→ ≡p LJ∗→ ≡p NM∗→|{z}tree-like versions

I F→ ≡p LJ→ ≡p NM→ go back to Reckhow ’76
I F→ ≡p F∗→ due to Krajı́ček, implicational version J. ’17
Further extensions of the lower bound (as in J. ’09, J. ’17):
I full language of IPC
I superintuitionistic logics IPC ⊆ L ⊆ BD2
I exponential separation between Extended Frege andSubstitution Frege
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

17:17

References
I N. Alon, R. B. Boppana: The monotone circuit complexity of Booleanfunctions, Combinatorica 7 (1987), 1–22
I S. R. Buss, P. Pudlák: On the computational content of intuitionistic
propositional proofs, APAL 109 (2001), 49–64
I S. A. Cook, R. A. Reckhow: The relative efficiency of propositional proof
systems, JSL 44 (1979), 36–50
I L. Gordeev, E. H. Haeusler: Proof compression and NP versus PSPACE, Studia
Logica 107 (2019), 53–83
I: Proof compression and NP versus PSPACE II, Bull. Sect. Logic
Univ. Lódź 49 (2020), 213–230
I: Proof compression and NP versus PSPACE II: addendum, Bull.
Sect. Logic Univ. Lódź 51 (2022), 197–205
I P. Hrubeš: Lower bounds for modal logics, JSL 72 (2007), 941–958
I: A lower bound for intuitionistic logic, APAL 146 (2007), 72–90

I: On lengths of proofs in non-classical logics, APAL 157 (2009),194–205

I R. Jalali: Proof complexity of substructural logics, APAL 172 (2021),
art. 102972, 31 pp
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023

References (cont’d)
I E. J.: Substitution Frege and extended Frege proof systems in non-classicallogics, APAL 159 (2009), 1–48
I: Proof complexity of intuitionistic implicational formulas, APAL 168(2017), 150–190
I: A simplified lower bound for implicational logic, 2023, 31 pp,
arXiv:2303.15090 [cs.LO]
I S. Jukna: Boolean function complexity: Advances and frontiers, Springer, 2012,xvi+620 pp
I J. Krajı́ček: Bounded arithmetic, propositional logic, and complexity theory,
Cambridge Univ. Press, 1995, xiv+343 pp
I J. Krajı́ček: Interpolation theorems, lower bounds for proof systems, andindependence results for bounded arithmetic, JSL 62 (1997), 457–486
I: Proof complexity, Cambridge Univ. Press, 2019, 530 pp
I A. A. Razborov: Lower bounds on the monotone complexity of some Booleanfunctions, Math. USSR, Doklady 31 (1985), 354–357
I R. A. Reckhow: On the lengths of proofs in the propositional calculus, Ph.D.
thesis, Univ. Toronto, 1976
I É. Tardos: The gap between monotone and non-monotone circuit complexity is
exponential, Combinatorica 7 (1987), 141–142
Emil Jeřábek Disjunction-free disjunction property CiE Batumi, 27 July 2023