Nonterminal descriptional complexity of regular languages Recently I became interested in grammar complexity of regular language. Prior to searching for literature, I tried to investigate it on my own, proving two lemmas from comment below.
I am aware of an old Grushka's article and a more recent paper by Dassow and Stiebe. I've also found Wolfsteiner's thesis.
What is the state of art of the study of grammar complexity? Could you explain simply the connection between grammar complexity and formal proof theory?
Lemma 1. Consider $L = (ab)^* + (ba)^*$:

There exists CFG with two variables which generates $L$
There exist no CFG with one variable which generates $L$

For proving (1) we may just consider the following CFG $$ S \rightarrow bAa \mid A , \, A \rightarrow abA \mid \varepsilon$$
The second proposition is a bit more tricky. Suppose that there exists CFG $G = (\{S\}, \{a, b\}, P, S)$ such that $L = L(G)$. Every production is $S \rightarrow \alpha$ for some $\alpha \in \{a, b, S\}^*$. Say, $\alpha = w_1 S w_2 S \ldots w_k S w_{k+1}$. Then $$u_1, \ldots u_k \in L \Rightarrow w_1 u_1 w_2 u_2 \ldots w_k u_k w_{k+1} \in L,$$ because as $L$ is generated by $G$, one can derive this word by using $S \rightarrow w_1 S w_2 S \ldots w_k S w_{k+1}$ and then deriving every $u_i$ from $S$'s. By using that we can prove that in right-hand side of every production $S$ can't be followed immediately by any symbol:

if $S$ is followed by $a$, we have subword $Sa$ in $\alpha$, then we can derive $ba$ from $S$, thus we can derive the word which contains two $a$'s in the row, which obviously doesn't lie in $L$;
if $S$ is followed by $b$, having subsword $Sb$ of $\alpha$ we can derive $ab$ from $S$ and thus obtain the word which contains two $b$'s in the row;
if we have subword $SS$ of $\alpha$, we can derive $ab$ from the first $S$ and $ba$ from the second.

Also $S$ can't follow neither letter nor $S$ in right-hand side of every production for the same reason. So $G$ can only have productions of sort $S \rightarrow S$ and $S \rightarrow w$ for $w \in L$. Thus $L(G)$ is finite, which is contradiction. $\Box$
I'd also like to suggest the following
Lemma 2. Let $w_1, \ldots w_n$ be some words. The language $w_1^* + \ldots + w_n^*$ is generated by CFG with one variable iff words $w_1, \ldots w_n$ commute pairwise, i. e. $w_i w_j = w_j w_i$ for every $i,j$.