Understanding the proof of Definition by Recursion

I’m currently reading Logic and Structure by Dirk van Dalen and I am having struggles proving Theorem $2.1.6$ (Definition by Recursion) on page $10$.

Warning Before someone flags this question as a duplicate of Definition by Recursion, I invite you, at least, to read the end of this post (there I explain briefly why I am posting this). Thank you.

What do we have

Here are some of the definitions and results introduced in the book that might be helpful for the sequel. The chapter on Propositional Logic ($\mathsf{PC}$) starts by introducing the alphabet for ($\mathsf{PC}$)

Definition $2.1.1$ The language of propositional logic has an alphabet consisting of

$(i)$ proposition symbols: $p_0, p_1, p_2, \dots$,

$(ii)$ connectives: $\wedge$, $\vee$, $\rightarrow$, $\neg$, $\leftrightarrow$, $\bot$,

$(iii)$ auxiliary symbols: $($, $)$.

and the method for obtaining well formed propositional formulas (we will take propositional formulas to be any string of objects of the alphabet from $\mathsf{PC}$)

Definition $2.1.2$ The set $\mathsf{PROP}$ of propositions is the smallest set $X$ with the properties

$(i)$ $p_i \in X$ ($i \in N$), $\bot \in X$,

$(ii)$ $\varphi, \psi \in X \implies (\varphi \wedge \psi), (\varphi \vee \psi), (\varphi \rightarrow \psi), (\varphi \leftrightarrow \psi) \in X$,

$(iii)$ $\varphi \in X \implies (\neg \varphi) \in X$.

Because we are dealing with inductive definitions, one can easily prove the following induction principle.

Theorem $2.1.3$ (Induction Principle) Let $A$ be a property, then $A(\varphi)$ for all $\varphi \in \mathsf{PROP}$ if

$(i)$ $A(p_i)$, for all $i$, and $A(\bot$),

$(ii)$ $A(\varphi), A(\psi) \implies A((\varphi \square \psi))$,

$(iii)$ $A(\varphi) \implies A((\neg \varphi))$.

(NOTE: in Theorem $2.1.3$ $(ii)$, let $\square \in \{\wedge, \vee, \rightarrow, \leftrightarrow\}$)

After this, Dalen introduced the notion of formation sequence of a given propositional formula.

Definition $2.1.4$ A sequence $\varphi_0$, $\varphi_1$, $\dots$, $\varphi_n$ is a formation sequence of $\varphi$ if $\varphi_n = \varphi$ and for all $i \leq n$ $\varphi_i$ is atomic or

\begin{align*} & \varphi_i = (\varphi_j \square \varphi_k) \quad \text{for certain } j, k < i, \quad \text{or} \\ & \varphi_i = (\neg \varphi_j) \quad \text{for certain } j < i. \end{align*}

Further, Dalen proves that the set $\mathsf{PROP}$ is exactly the set of propositions having formation sequence.

Theorem $2.1.5$ $\mathsf{PROP}$ is the set of all expressions having formation sequences.

The problem

Later, on page $10$, it is stated the following theorem.

Theorem $2.1.6$ (Definition by Recursion) Let mapping $H_{\square} \colon A^2 \to A$ and $H_{\neg} \colon A \to A$ be given and let $H_{at}$ be a map from the set of atoms into $A$, then there exists exactly one mapping $F \colon PROP \to A$ such that

$$\begin{cases} F(\varphi) = H_{at}(\varphi) \text{ for $\varphi$ atomic} \\ F((\varphi \square \psi)) = H_{\square}(F(\varphi), F(\psi)) \\ F((\neg \varphi)) = H_{\neg}(F(\varphi)) \end{cases}.$$

The suggestion

Exercise $11$ (page $14$ and $15$) helps how to prove this statement. Although, I’m having a really rough time trying to understand it. Hence, any help is more than welcomed.

$a)$ Give an inductive definition of the function $F$, defined by recursion on $\mathsf{PROP}$ from the functions $H_{at}$, $H_{\square}$, $H_{\neg}$, as a set $F^{\text{$*$}}$ of pairs.

I don’t quite know where to start. One think that occurs to me, was to define $F^{\text{$*$}}$ is a similar way as the set $\mathsf{PROP}$ was defined. Hence, I defined $F^{\text{$*$}}$ as the smallest set $Y$ such that

$(i)$ $(p_i, H_{at}(p_i)) \in F^{\text{$*$}} (i \in N), (\bot, H_{at}(\bot)) \in F^{\text{$*$}}$,

$(ii)$ $(\varphi_1, \psi_1), (\varphi_2, \psi_2) \in F^{\text{$*$}} \implies ((\varphi_1 \square \varphi_2), H_{\square}(\psi_1, \psi_2)) \in F^{\text{$*$}}$,

$(iii)$ $(\varphi_1, \psi_1) \in F^{\text{$*$}} \implies ((\neg \varphi_1), H_{\neg}(\psi_1)) \in F^{\text{$*$}}$.

$b)$ Formulate and prove for $F^{\text{$*$}}$ the induction principle.

I honestly don’t know how can I formulate this. I mean, Theorem $2.1.3$ allows us to prove that a certain property is true for all the propositions (elements of $\mathsf{PROP}$). But in this case, we have ordered pairs, and we don’t even know what are the $H$’s maps.

$c)$ Prove that $F^{\text{$*$}}$ is indeed a function on $\mathsf{PROP}$.

After reading this, I realize that maybe the principle that we must formulate and prove will help us proving that $F^{\text{$*$}}$ is a function on $\mathsf{PROP}$.

$d)$ Prove that it is the unique function on $\mathsf{PROP}$ satisfying the recursion equations.

I believe that this is a typical uniqueness proof, but are there any special care that I must take in this point?

I tried to search for the Definition by Recursion Theorem from Set Theory (I though that maybe this presented here could be a particular case of a more general one). Although (and I don’t know why) the Recursion Theorems that I found seem not feet in this case.

I also found that this question was already asked here Definition by Recursion and an answer is given there. But I would appreciate if someone could give more details about the argument, because it does not seem clear to me.

Thank you in advance for your attention.

Solution 1:

$\DeclareMathOperator{Prop}{Prop}$You will want to prove that $\forall p \in \Prop \exists! a \in A ((p, a) \in F^*)$.

To do this, you will proceed by induction on $p$.

Edit: you will require the unique readability theorem to make this proof work. It's rather critical. This theorem is actually equivalent to induction on formulas + unique readability, so it's not surprising that you would need both principles to prove the recursion principle.

Base case: $p = p_i$ or $p = \bot$. Hint: consider $G = \{(p', a) \in F^* | p' = p \implies a = H_{at}(p)\}$, and prove that $G$ satisfies properties (i), (ii), and (iii) in your definition of $F^*$ and thus equals $F^*$.

$\neg$-inductive step: $p = \neg q$ and there is a unique $a \in A$ such that $(q, a) \in F^*$. Hint: consider $G = \{(p', a') \in F^* | p' = p \implies a' = H_\neg(a)\}$.

Binary inductive step: exercise.

Once you have this result, you see that $F^*$ is indeed a function $\Prop \to A$. From here, use the definition of $F^*$ to show uniqueness.