Existence of recursive function. 
Given a function defined by recursion of the form:
  $$\begin{align*}
& H: AT \longmapsto A,\; AT = \{\top, \bot\}\cup \Sigma\\
& H_{\square}: A^2 \longmapsto A, \; \square\in \{\vee, \wedge, \to, \leftrightarrow\}\\
& H_{\neg}: A \longmapsto A
\end{align*}$$
  show that there is a unique function $F$ satisfying:
  $$\begin{align*}
& F(\varphi) = H(\varphi), \; \varphi \in AT\\
&F\left( (\varphi_1 \square \varphi_2)\right) = H_{\square}\left(F(\varphi_1), F(\varphi_2)\right)\\
& F(\neg\varphi) = H_{\neg}(F(\varphi))
\end{align*}$$

I think I managed to prove uniqueness by induction on the number of connectives. Let $G$ be a function satisfying what $F$ satisfies above. I'd like to prove that for all $\varphi \in L_{\Sigma}$, $F(\varphi) = G(\varphi)$.
Then the base case would be when the number of connectives of $\varphi$ is $0$, that is, $\varphi \in AT$, but that follows from the hypothesis. So let's assume the result holds for $\varphi$ when $\varphi$ has a number $n$ of connectives and prove the result for $n+1$. We have two cases:
First, if $\varphi = \neg \varphi_1$, then
$$G(\varphi) = G(\neg\varphi_1) = H_{\neg}\left( G(\varphi_1)\right) = H_{\neg}\left(F(\varphi_1)\right) = F(\neg\varphi_1) = F(\varphi)$$
And second, if $\varphi = \varphi_1 \square \varphi_2$, then
$$G(\varphi_1 \square \varphi_2) = H_{\square}\left( G(\varphi_1), G(\varphi_2)\right) = H_{\square}\left(F(\varphi_1),F(\varphi_2)\right) = F(\varphi_1\square\varphi_2)$$
since by the induction hypothesis, $F(\varphi) = G(\varphi)$ when $\varphi$ is a formula with less than $n$ connectives. 
Now, if this is true (feedback on this would also be helpful :D) I just need to prove the existence of such function $F$, but I have no clue on where to start, so a hint on this would be also helpful. Thanks.
 A: Let's assume that $S$ is the set of all expressions that can be constructed out of $\Sigma, \land, \lor, \neg, \rightarrow, \leftrightarrow, \bot, \top$ as follows:


*

*For every $\varphi \in \Sigma$: $\varphi \in S$

*$\bot \in S$

*$\top \in S$

*For every $\varphi \in S$: $\neg \varphi \in S$

*For every $\varphi_1 \in S$ and $\varphi_2 \in S$: $\varphi_1 \land \varphi_2 \in S$ 

*For every $\varphi_1 \in S$ and $\varphi_2 \in S$: $\varphi_1 \lor \varphi_2 \in S$ 

*For every $\varphi_1 \in S$ and $\varphi_2 \in S$: $\varphi_1 \rightarrow \varphi_2 \in S$ 

*For every $\varphi_1 \in S$ and $\varphi_2 \in S$: $\varphi_1 \leftrightarrow \varphi_2 \in S$ 
(and that nothing else is in $S$)
I assume that F is supposed to be a function from $S$ to $A$. 
Well, it seems to me that the existence of the function F is guaranteed by the very fact that H is given, and that the properties that F needs to satisfy can be treated as a recursive definition of F over H using the very recursion that defines the syntactical structire of any $\varphi$. As such, $F$ is well-defined, and existence and uniqueness are all guaranteed.
