A formalised language for the propositional calculus consists of:
an infinite (countable) set of propositional variables p_0, p_1,...;
a set of propositional connectives (conjunction, disjunction, etc.);
a set of auxiliary signs (parentheses).
A formula is defined as a propositional variable or any finite sequence of propositional symbols (i.e. strings of propositional variables with connective(s) and, perhaps, parentheses).
Why is the set of propositional variables required to be countable? Isn't it something artificial in requiring it to be so if we are only interested in finite sequences of propositional symbols?
Also, as a related question: Could we consider a finite set of propositional variables and develop the same propositional calculus?