# 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. 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? 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. 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? 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.