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.