Let $R(f)$ and $ER(f)$ be the minimum-size for unsat proofs of $f$ in Resolution and Extended Resolution respectively. What's the best bound we have on $D=\min_f (R(f)-ER(f))$ where $f$ belongs to a worst-case family of boolean formulae? Since no superpolynomial lower bounds are known on Extended Resolution, we don't have a good upper bound on $D$, so I'm interested in lower bounds on $D$.
Edit: Clarified question as per Kaveh's answer below
Your definition of $D$ is not clear, if it is $D = \max_f (R(f) - ER(f))$, then it is exponential.
There are DNFs whose shortest proofs in ER is exponentially shorter than their shortest proofs in R e.g. PHP (pigeon hole principle) has polynomial size ER-proofs but only exponential size R-proofs.
Unsatisfiability of $f$ is the same as $\lnot f$ being a tautology. Let $\lnot f$ be as PHP. Then $R(f)$ is exponential where as $ER(f)$ is polynomial, so the difference is exponential. Also it cannot be more than exponential.
Addendum:
If $D = \min_f (R(f) - ER(f))$ then it is 0. Take $\lnot f=\top$ and it has one line proof in both. (R is included in ER so it cannot be less than 0.)
