Prove2Me

Soundness of the depth-dd Frege system FdF_d

Proved
FdVersusFdSucc.depth_frege_sound

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

logicproof-complexity

Let d≥0d\ge 0 and let π\pi be an FdF_d-proof of a formula AA. Then AA is a tautology:

π is an Fd-proof of A ⟹ ∀v, v(A)=1.\pi \text{ is an } F_d\text{-proof of } A\ \Longrightarrow\ \forall v,\ v(A)=1.

This is the basic correctness property of the proof system FdF_d and confirms that the lower and upper bounds in the mission are about a genuine propositional proof system.

Preamble
import Definitions.Def_FdVersusFdSucc_defs

open Filter
Formal statement
namespace FdVersusFdSucc

/-- Soundness of `F_d`: every formula with an `F_d`-proof is a tautology. -/
theorem depth_frege_sound (d : ℕ) (π : List Sequent) (A : Formula)
    (h : IsDepthProofOf d π A) : A.IsTautology := by sorry

end FdVersusFdSucc
Source
Standard property of bounded-depth Frege / sequent calculus systems; 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