# Size of Propositional Formula

I am study this lecture The Complexity of Propositional Proofs. Here there is a term size of propositional formula (page 2),

Every tautology $\tau$ on $n$ variables has an $F$-proof in which thera are at most $2^{O(n)}$ formulas, each of which has size polynomial in the size of $\tau$

but here doesn't define that term. I have googled this term and I have found something similar length of propositional formula, which is defined as

The function $L(P)$ giving the length of a formula is defined by structural induction as follows:

• $L(p_i) = 1$, for all atomic formulas $p_i$
• $L(P ∧ Q)$ = 1 + $L(P ) + L(Q)$,
• $L(P ∨ Q) = 1 + L(P ) + L(Q)$,
• $L(¬P) = 1 + L(P)$.

My question is: Is the length and size of a formula the same?

• There are several different definitions of the length or size of a formula, but the most popular one is the one you quote. The lecture probably uses the same definition; length and size are synonymous in this case. – Yuval Filmus Oct 16 '15 at 14:18
• Size never occurs in the context of a formula in the lecture you link to. Can you be more specific and give a slide number? – Yuval Filmus Oct 16 '15 at 14:23
• Again, a page number would be very useful. The survey is quite long and nobody is going to skim it, looking at all occurrences of the term size. – Yuval Filmus Oct 16 '15 at 14:27
• Which part of the lecture are you referring to? The string 'size of' does not occur in the document you link. There is a part about the 'refutation resolution width' on slide 15. Is that what you mean? – Lieuwe Vinkhuijzen Oct 16 '15 at 14:38
• Also, when referencing material you should give the authors in clear text, too. – Raphael Oct 16 '15 at 15:34

In other places, however, it is mentioned that some formula has size $O(n)$. Here the exact encoding still doesn't matter, but there is a real difference between the two options mentioned above. Consider for example the formula $x_1 \lor \cdots \lor x_n$. Under the second option, such a formula has size $\Theta(n)$. However, any reasonable binary encoding of this formula will have size $\Theta(n\log n)$, since storing the indices also takes space. From the author's statement it follows that he uses a definition of the second kind.