In the book 'Logical Foundations of Proof Complexity', co-authored by Stephen Cook, the following definition is given:
A proof-system $F$ is said to be polynomially-bounded if there is a polynomial p(n) such that for all tautologies $A$, there is a proof $X$ of $A$ in $F$ such that |x| $\leq$ p(|A|). Informally, a proof system is polynomially-bounded if every tautology has a short proof in F.
My question is in regards to what "all tautologies" means. Is it in regards to every tautology in $F$ or any tuatology in in any adequate proof system, which first needs to be converted to an equivalent formula in $F$?
For example, let's say we are dealing with 2 very different proof-systems, A and B. Let's just assume for the moment that B is polynomially-bounded. Then every tautology in B has a short proof.
My question is: Given a tautology in system A--denoted as $\phi$--, is it necessary that the conversion from $\phi$ in A to its equivalent formula $\phi'$ in B happens in polynomial-time?
Or is the only thing that is necessary for B to be considered a polynomially-bounded proof system this: that once $\phi$ is represented in the system B (regardless of how long this conversion takes place), then this formula has a short proof in B?
So if it was inefficient to convert $\phi$ to $\phi'$, yet $\phi'$ nonetheless still had a short proof in system B, is B still considered a polynomially-bounded proof system?