In regards to the tautologies of a polynomially-bounded propositional proof system 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?
Your question is like asking what is the class of formulas for the problem SAT?
In the definition of SAT it is fixed to some fixed class, 
say those based on $\{\lnot, \land, \lor\}$ 
but it doesn't really matter usually whether 
we talk about formulas based on 
$\{\lnot, \land, \lor\}$ or $\{\bot, \to \}$ or 
any other complete set of Boolean connectives.
Therefore it is often not explicitly stated.
The reason is they can simulate each other with 
at most polynomial increase in the size of formulas.
Therefore it is often not explicitly mentioned.
If we pick an unusual one then things might be completely different.
E.g. DNF-SAT is in P, but this does not mean SAT is in P.
Similarly CNF-TAUT is in P and therefore 
if we define the concept of proof system for CNF-TAUT 
it has polynomially bounded proof system.
But again this does not mean that 
TAUT has polynomially bounded proof system.
The problem we are interested in is TAUT, not CNF-TAUT.
We want a polynomially bounded proof system for TAUT.

For the definition of proof system 
we have to similarly fix the class of tautologies. 
If we pick different classes we get different definitions.
TAUT being the dual to SAT 
it is natural to take the dual of the formulas for SAT 
(i.e. formulas based on connectives $\{\lnot, \land, \lor\}$).
It is also common to use DNF-TAUT as a dual to CNF-SAT
(there is a simple reduction from SAT to CNF-SAT 
using new extension variables such that 
the set of satisfying assignments of the original formula and resulting CNF
are P-isomorphic).
But as long as we can efficiently express DNF formulas 
it usually does not matter what we use.
It can be linear equations, or any class of computational objects 
as long as they can express DNFs with at most a polynomial increase in size. 
If that is not the case then 
the system is trivially not polynomially bounded as 
it is not a proof system for TAUT (or DNF-TAUT).
The book does not deal with cases where 
the class of formulas does not contain DNFs.

For the purpose of the book you can assume that the class of propositional formulas contains DNFs and every tautology means every DNF tautology.


  A proof system $Q$ is polynomially bounded if
  there is a polynomial $p$ such that
  for every DNF tautology $\varphi$ 
  there is a $Q$-proof $\pi$ such that
  $|\pi| \leq p(|\varphi|)$.


As you can see there is no mention of other proof systems.

If you want the more general definitions look at Reckhow's thesis.
Reckhow looks at the more general definition with different set of connectives
and classes of formulas. 
He shows that any two Frege systems polynomially simulate each other 
as long as we have a complete set of Boolean connectives. 
I think the simplest way to explain it is as follows: 


  If we have a complete set of connectives 
  we can express in polynomial size the truth of formulas 
  based on another finite set of Boolean connectives.


For more see the section in Reckhow's thesis 
discussing polynomial simulation 
between proof systems with different class of formulas.