{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreifp2cu5ubjfpaapj6oz4mmw5rlejo5dgdwxbkrzly7q7q2a4bapmq",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mj62rdd7bbd2"
  },
  "path": "/report/2026/055",
  "publishedAt": "2026-04-10T17:47:30.000Z",
  "site": "https://eccc.weizmann.ac.il",
  "textContent": "Given a propositional proof system $P$, we may define a formula $\\text{Prf}^P_s(F)$ which is satisfiable if and only if the formula $F$ has a length $\\leq s$ refutation in $P$. These formulas have received much attention in recent years due to their fundamental nature --- if a powerful proof system $P$ cannot refute $\\text{Prf}^Q_s(F)$, and $P$ can formalize a set of techniques, then we cannot expect these techniques to prove lower bounds on $Q$ proofs --- as well as due to their relationship to proving non-automatability of proof systems, as pioneered by Atserias and Müller. We provide, to our knowledge, one of the first positive results regarding these principles.Let $\\text{Prf}^{\\mathrm{Frege}_d}_{s,l}$ denote the $\\text{Prf}$ formula for depth-$d$ Frege proofs of length $s$ and in which each line has size bounded by $l$. We show that in the regime of exponential length $s = 2^{n^\\varepsilon}$, and polynomial-line size $l=n^{O(1)}$, depth-$d$ Frege proofs can refute $\\text{Prf}_{s,l}^{\\mathrm{Frege}_d}(\\text{PHP}^{n+1}_n)$, and hence we give an example of a proof system $P$ which seemingly can prove its own lower bounds. In fact, our upper bounds can already be implemented in the fragment Res($\\log$), and hence even an apparently limited subsystem of depth-$d$ Frege is already capable of proving depth-$d$ Frege lower bounds. To the best of our knowledge, this is the first example of a propositional proof system which is capable of proving strong lower bounds against itself. We prove our results by using a constructive proof of the switching lemma due to Razborov, particularly its presentation by Urquhart and Fu, and combining it with a recent study of $\\text{Prf}^{\\text{Res}}$ by Li, Li, and Ren, in order to reduce the problem of refuting $\\text{Prf}_{s,l}^{\\mathrm{Frege}_d}(\\text{PHP}^{n+1}_n)$ to refuting the weak pigeonhole principle.",
  "title": "TR26-055 |  Res$(\\log)$ Proves Bounded-Depth Frege Lower Bounds | \n\n\tBen Davis, \n\n\tRobert Robere"
}