I need to find a formula for the number $n_m$ of equivalence classes of the set of propositional logical formulas only containing the propositional variables $p_0,...,p_m$ and only using the connective $\rightarrow$.
This is considering classical propositional logic, I know that what this question is really asking me is to figure out a formula for how many inequivalent formulas I can form with $m$ variables. I can use the variables and the connective more than once, therefore $(p \rightarrow q) \rightarrow q$ can be considered as an option. I have worked out that if $m=2$ (I only have $p$ and $q$), I can have 6 inequivalent formulas, so $m_2=6$. But I don't know how to generalise that information. I would very much appreciate your ideas.
The set of Boolean functions (i.e., functions from $\{0,1\}^n\to\{0,1\}$ for some $n\ge 1$) that can be produced from $n$ propositional variables and $\to$ is the clone $T_1^\infty$ in Post’s lattice. It has an alternative description as the set of Boolean functions bounded below by a variable: $f$ is such a function if there is a $k$ such that $f(p_1,\ldots,p_n)\ge p_k$ for all $\langle p_1,\ldots,p_n\rangle\in\{0,1\}^n$.
To put this a bit differently, suppose that you organize a truth table for $p_1,\ldots,p_n$, and the function $f$ in such a way that the truth value vectors $\langle p_1,\ldots,p_n\rangle$ are listed in numerical order when interpreted as binary numbers. For the function $f$ defined by the expression $(p_1\to p_2)\to p_2$, for instance, we have
$$\begin{array}{ccc} p_1&p_2&f\\ \hline 0&0&0\\ 0&1&1\\ 1&0&1\\ 1&1&1 \end{array}$$
We can then represent the function $f$ by the $2^n$-bit string $0111$. The bit string representations of the Boolean functions derivable from individual propositional variables and $\to$ are those that can be obtained from the bit strings for the individual variables by changing any number of zeroes to ones.
For $n=2$ the propositional variables are represented by $0011$ for $p_1$ and $0101$ for $p_2$, and the four other Boolean functions derivable from them with $\to$ are $0111,1011,1111$, and $1101$. For $n=3$ the propositional variables are represented by $00001111,00110011$, and $01010101$, and there are $35$ other Boolean functions that can be derived from them using only $\to$. These aren’t hard to count using an inclusion-exclusion argument. Each of the $3$ initial vectors has $4$ zeroes, any subset of which can be changed to ones, so at a first approximation there are $3\cdot 2^4=48$ Boolean functions of at most three variables derivable using only $\to$. However, any two of the initial vectors have $2$ zeroes in common, so for each of the $\binom32$ pairs of initial vectors we’ve counted $2^2$ functions twice; subtracting the over-counting leaves us with $48-3\cdot4=36$ Boolean functions as a second approximation. Finally, there is one zero that all three initial propositional vectors have in common. Its two possible values were counted three times initially and then subtracted three times, so we need to add them back in, and we find that
$$m_3=\binom312^{2^2}-\binom322^{2^1}+\binom332^{2^0}=38\;.$$
This argument generalizes to yield the formula
$$m_n=\sum_{k=1}^n(-1)^{k+1}\binom{n}k2^{2^{n-k}}\;.$$
The sequence turns out to be OEIS A005530, but there’s not much in the OEIS entry. The entry does note that this is also the number of degenerate Boolean functions of $n$ variables.
The counting argument is straightforward once one has the characterization of these Boolean functions as those that are bounded below by a variable. Verifying that is tedious but straightforward. It’s not hard to check that composition preserves the property of being bounded below by a variable. It’s a bit more work to check that one can get all of these functions from the initial propositional variables.
This can be done by induction on the number of propositional variables. Rather then write out the whole argument, I’ll illustrate what happens in the step from $n=2$ to $n=3$. By hypothesis we have the six Boolean functions of two variables whose string representations are $0011,0101,0111,1011,1101$, and $1111$. Adding the third variable just doubles each bit, so that we have $00001111,00110011,00111111,11001111,11110011$, and $11111111$ without actually making use of the third variable. Its own vector is $01010101$.
At this point we have every vector with just one $0$ except $11111110$, which is unobtainable: every composition of implications is true when all of the propositional variables are true. These can be used to get the possible vectors with $3$ zeroes (e.g., $10111111\to 00001111$ yields $01001111$), and they can then be combined with the $3$-zero vectors to get the possible $2$-zero vectors (e.g., $11101111\to 01001111$ is $01011111$).
There may well be easier ways to think about this; I’ve not worked with it before. But this should at least give you a way to think about the problem.