# 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. Commented Oct 16, 2015 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? Commented Oct 16, 2015 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. Commented Oct 16, 2015 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? Commented Oct 16, 2015 at 14:38
• Also, when referencing material you should give the authors in clear text, too. Commented Oct 16, 2015 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.