I am trying to prove that all statements are logically equivalent to a statement that does not use negation and in which the only logical connective used is nand (defined as $\neg(p\ \land\ q)$ for statements $p,q$).
In brief, the way I am doing it is with two cases:
Let $S$ be a statement. If $S$ is atomic, then we are done (the statement that does not use negation or logical connectives other than nand with which $S$ is logically equivalent is $S$ itself). If $S$ is non-atomic, then we simply have to show that all possible mappings of $(p,q)$ to the boolean domain (there are 16 of them) can be represented using only nand, where $p\ \otimes\ q \Leftrightarrow S$ and $\otimes$ is some logical connective.
The part I am unsure of is whether it is safe to jump to the idea that $S$ can always be represented as $p\ \otimes\ q$. It seems natural that if $S\ \Leftrightarrow\ (p\ \otimes\ q)\ \otimes\ r$ (the two instances of $\otimes$ need not necessarily refer to the same logical connective), for example, then you would apply the arguments in the second case twice: first to part in parentheses, and then to the whole expression.
How might I convey this idea of recursion in a rigorous proof? Do I even need to? I.e. is it implied?
Take your favorite set of complete logical connectives. {AND, OR, NOT} obviously works, but so does {AND, NOT} and {OR, NOT} if you want to do a simple lemma invoking De Morgan's laws. Then show that every member of that set can be expressed with just NAND.
Then you can let $S$ represent the set of boolean expressions that are equivalent to an expression just using literals and NAND as a connector. You know that all literals are in $S$ by definition. And you know that if $A\in S$ and $B\in S$, then $A\land B\in S$, $A\lor B\in S$, and $\neg A\in S$, by what you proved in the previous paragraph and the induction hypothesis. Therefore, by induction on the construction of boolean expressions, $S$ represents all boolean expressions.