Existence of recursive function.

Question

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.

Answer 1

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:

1. For every $\varphi \in \Sigma$: $\varphi \in S$

2. $\bot \in S$

3. $\top \in S$

4. For every $\varphi \in S$: $\neg \varphi \in S$

5. For every $\varphi_1 \in S$ and $\varphi_2 \in S$: $\varphi_1 \land \varphi_2 \in S$

6. For every $\varphi_1 \in S$ and $\varphi_2 \in S$: $\varphi_1 \lor \varphi_2 \in S$

7. For every $\varphi_1 \in S$ and $\varphi_2 \in S$: $\varphi_1 \rightarrow \varphi_2 \in S$

8. 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.