In regards to the tautologies of a polynomially-bounded propositional 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.