Propositional Logic: For which natural numbers $n$ are there elements of $\mathcal{L_0}$ of length $n$? Let $\mathcal{L_0}$ be the smallest set $L$ of finite sequences of $\textit{logical symbols}= \{(\enspace)\enspace\neg\}$ and $\textit{propositional symbols}=\{A_n|n\in\mathbb{N}\}$ for $n \in \mathbb{N}$ satisfying the following properties:
(1) For each propositional symbol $A_n$ with $n\in\mathbb{N}$,
\begin{multline}
A_n \in L.
\end{multline}
(2) For each pair of finite sequences $s$ and $t$, if $s$ and $t$ belong to $L$, then
\begin{multline}
(\neg s) \in L
\end{multline} and
\begin{multline}
(s \to t) \in L.
\end{multline}
For which natural numbers $n$ are there elements of $\mathcal{L_0}$  of length $n$?
 A: The smaller lengths $1,4,5$ are the basic forms, which are obvious:
(a) $n=1$: The atom $A_i$
(b) $n=4$: $(\neg A_i)$
(c) $n=5$: $(A_i \to A_j)$
Note we can't have length $0$, it wouldn't be an element of $\mathcal{L_0}$. Can't have $2$ or $3$ or $6$ since the above are the most basic elements, and we can't increase an element by anything other than three or four. 
Now we seek the next possible values of $n$. We can take our basic forms (b) and (c) and increase them by the lowest possible counts of three or four by repeatedly surrounding them, represented here by $x$, by $(\neg x)$or $(x\to A_i)$, which will give an element of $\mathcal{L_0}$ in the form of (2) or (3). Call these  operations $\delta$ and $\gamma$ respectively.
$\delta$ surrounds element with $(\neg \enspace\enspace )$.
$\gamma$ surrounds element with $(\enspace\enspace\to A_i)$.
This gives us the result:
Start with (b). We have a length four element. apply $\delta$ repeatedly. This gives
$n = 7,10,13,16,19,22...$
Now, instead apply $\gamma$ to (b) repeatedly. This gives
$n = 8,12,16,20,24...$
Now for (b) apply $\delta$ first, then $\gamma$. We get
$n=7,11$
Note now that we have $10,11,12$ in succession. We see we can use $\delta$ to increase any of these by three, which implies $n\geq 10$, meaning we can achieve any value for $n$ equal to or beyond $10$.
We showed above that sequences of length $7$ and $8$ exist. All that remains is to find a sequence of length $9$. This is done by applying $\gamma$ to (c). $5+4=9$.
So therefore $\{n=1,4,5 \lor n\geq 7|n \in \mathbb{N}\}$.
A: Since this is a logic problem, I'm assuming $0\in \mathbb N$. It doesn't matter much anyway.
Claim: For all $n\in \{n\in \mathbb N\colon n=1\lor n=4\lor n=5\lor n\ge 7\}$, there exists a formula of length $n$.
Proof: If $n=1$, take any propositional symbol. 
If $n=4$, take $(\neg A)$, where $A$ is a propositional symbol.
If $n=5$, take $(A\to A)$, where $A$ is a propositional symbol.
Suppose $n\ge 7$.
If $n\equiv _31$, then $n=3(k+2)+1$, for some $k\in \mathbb N$. 
As per (2), given a formula, you can always add three logical symbols to it in such way that the resulting formula is in $\mathcal{L_0}$ . So, if there is a formula of length $1$ (and there is), you can obtain formulas in $\mathcal{L_0}$  with length $3(k+2)+1$, by using (2) $k+2$ times. This can be proved by induction on $k$.
If $n\equiv _30$, then $n=3(k+4)$ for some $k\in \mathbb N$ or $n=9$. In the latter case, take a formula of length $5$ and use (3) to add three logical symbols  and a propositional symbol to it and still obtain a formula in $\mathcal{L_0}$ . In the former case, just use (2) to add three logical symbols repeatedly.
If $n\equiv _32$, then $n=3(k+1)+5$. Use (2) to get a formula in $\mathcal{L_0}$  of the desired length. $\large \square$
Another claim: There are no formulas of length $0, 2,3$ or $6$ in $\mathcal{L_0}$.
Proof: There are no formulas of length $0$ in $\mathcal{L_0}$ because, by definition, a formula of length $0$ is a map whose domain is empty, but any such map must have $\varnothing$ as its codomain and $\varnothing\neq \{(,),\neg\}$.
There are no formulas of length $2$ or $3$ in $\mathcal{L_0}$ because propositional letters have length $1$ and (2) and (3) yield formulas of length at least $4$.
There are no formulas of length $6$ for if there existed $s\in \mathcal{L_0}$ with length $6$, one would have $s=(\neg t)$ or $s=(t\to r)$, for some $t,r\in \mathcal{L_0}$. In the first case $t$ would have length $3$, which isn't possible. In the second case the length of both $t$ and $r$ could not exceed $3$, so both $t$ and $r$ would be propositional symbols which have length $1$ and $s$ would have length $5$. $\large \square$
