Completeness of $F_d$ for tautologies of depth at most $d$

Proved

FdVersusFdSucc.depth_frege_complete

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

logicproof-complexity

Let $d\ge 0$ and let $A$ be a tautology with $\operatorname{depth}(A)\le d$ . Then $A$ has an $F_d$ -proof:

\operatorname{depth}(A)\le d,\ A \text{ tautology}\ \Longrightarrow\ \exists \pi,\ \pi \text{ is an } F_d\text{-proof of } A.

Together with soundness this shows that $F_d$ proves exactly the tautologies of depth at most $d$ , so the question of the mission is purely about proof size.

Preamble

import Definitions.Def_FdVersusFdSucc_defs

open Filter

Formal statement

namespace FdVersusFdSucc

/-- Completeness of `F_d` for depth-`d` formulas: every tautology of depth at most `d` has an
`F_d`-proof. -/
theorem depth_frege_complete (d : ℕ) (A : Formula) (hd : A.depth ≤ d)
    (hA : A.IsTautology) : ∃ π : List Sequent, IsDepthProofOf d π A := by sorry

end FdVersusFdSucc

Source

Standard (cut-free completeness of the sequent calculus with the subformula property); see J. Krajíček, Bounded arithmetic, propositional logic, and complexity theory, CUP 1995. Open Problem Garden, 'F_d versus F_{d+1}' (J. Krajíček), http://www.openproblemgarden.org/op/f_d_versus_f_d_1

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Completeness of FdF_dFd​ for tautologies of depth at most ddd

Completeness of $F_d$ for tautologies of depth at most $d$