Structural Induction

The principle of mathematical induction on the natural numbers is well known: it states that the set of natural numbers \(\mathbb{N}\) is the smallest set containing \(0\) and closed under the successor operation \(n \mapsto n + 1\). Thus, to prove some property \(P\) about all natural numbers, it suffices to demonstrate that the set

\[A = \{x \in \mathbb{N} \mid P(x)\}\]

contains \(0\) (i.e., that \(P(0)\) holds) and is closed under the successor operation (i.e., that \(P(n+1)\) holds whenever \(P(n)\) holds). Since \(\mathbb{N}\) is the smallest such set, it follows that \(\mathbb{N} \subseteq A\). Since, by construction, \(A \subseteq \mathbb{N}\), it then follows that \(A = \mathbb{N}\), i.e., that \(P(n)\) is satisfied for all \(n \in \mathbb{N}\). This is summarized as follows:

• Prove \(P(0\)).
• Prove \(P(n+1)\) assuming \(P(n)\) for an arbitrary \(n \in \mathbb{N}\).

The natural numbers also permit the definition of primitive recursive functions, i.e., functions \(f : \mathbb{N} \rightarrow \mathbb{N}\) such that

• \(f(0) = c\),
• \(f(n+1) = g(f(n))\),

where \(c \in \mathbb{N}\) is some constant and \(g : \mathbb{N} \rightarrow \mathbb{N}\) is another primitive recursive function and certain functions (such as constant functions) are taken for granted (more general schemas of primitive recursion are possible too).

It is possible to generalize induction to structural induction. In structural induction, we first define a set using a certain inductive process. Roughly, we consider some "ambient" set \(X\). Then, the powerset \(\mathcal{P}(X)\) represents all possible candidate sets. We define an operation \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) that produces "new" elements \(F(A)\) from existing elements \(A \subseteq X\). We start with nothing (i.e., \(\emptyset\)), then produce certain "atoms" ex nihilo (i.e., \(F(\emptyset)\)), and then apply various "constructors" to construct new elements \(F(F(\emptyset))\). We then iterate this process indefinitely:

\[\emptyset \subseteq F(\emptyset) \subseteq F(F(\emptyset)) \subseteq F(F(F(\emptyset))) \subseteq \dots.\]

We want this process to terminate at a fixed point, i.e., some set \(\mu F\) such that \(F(\mu F) = \mu F\). As long as such a fixed point is guaranteed to exist (which occurs when \(F\) is monotone), this yields a general procedure for inductive definitions: we specify the ambient set \(X\), the monotone map \(F\), and define the intended set as the fixed point \(\mu F\). Moreover, this yields an attendant inductive proof principle: we can show that \(\mu F \subseteq A\) whenever \(F(A) \subseteq A\), which permits us to prove properties in a manner similar to ordinary mathematical induction: in particular, if we let

\[A = \{x \in \mu F \mid P(x)\},\]

then \(A \subseteq \mu F\) by construction, and, if \(F(A) \subseteq A\), then \(\mu F \subseteq A\), so \(\mu F =A \), i.e., \(P(x)\) holds for all \(x \in \mu F\).

A similar procedure also permits us to define structurally recursive functions.

We will now proceed to describe structural induction in more detail. First, we start with some preliminaries about monotone maps and their fixed points.

Fixed Points

Definition (Monotone Map). Let \(X\) be any set. A function \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) is monotone if \(F(A) \subseteq F(B)\) whenever \(A \subseteq B\) for any \(A,B \subseteq X\).

Note. A monotone map can be defined for an arbitrary poset (partially-ordered set), but we do not require this level of generality. We are only interested in the poset \((\mathcal{P}(X), \subseteq)\).

Definition (Pre-Fixed Point). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. A set \(A \subseteq X\) is a pre-fixed point if \(F(A) \subseteq A\).

Definition (Fixed Point). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. A set \(A \subseteq X\) is a fixed point of \(F\) if \(F(A) = A\).

Definition (Least Pre-Fixed Point). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. A pre-fixed point \(A \subseteq X\) is the least pre-fixed point of \(F\) if \(A \subseteq B\) for every pre-fixed point \(B\). This means that the following diagram commutes:

\begin{CD}F(A) @>\subseteq>> F(B) \\ @V\subseteq VV @VV\subseteq V \\ A @>>\subseteq> B \end{CD}

Note that least pre-fixed points are necessarily unique, since if \(A\) and \(B\) are both least pre-fixed points, then, by definition, \(A \subseteq B\) and \(B \subseteq A\), so \(A = B\).

Definition (Least Fixed Point). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. A fixed point \(\mu F \subseteq X\) of \(F\) is the least fixed point of \(F\) if \(\mu F \subseteq A\) for every fixed point \(A\) of \(F\).

Note that least fixed points are necessarily unique, since if \(A\) and \(B\) are both least fixed points, then, by definition, \(A \subseteq B\) and \(B \subseteq A\), so \(A = B\). Thus, we simply write \(\mu F\) to denote this unique fixed point.

The least fixed point is also called an inductively-defined set. As we will demonstrate, the map \(F\) represents "rules" for producing elements and the least fixed point is closed under such production rules.

Since the empty set is a subset of every set, for any monotone map \(F\), there is an ascending chain

\[F(\emptyset) \subseteq F(F(\emptyset)) \subseteq F(F(F(\emptyset))) \subseteq \dots.\]

Intuitively, this means we start with nothing (\(\emptyset\)), we apply the axioms of the production rules (the elements \(F(\emptyset)\) that are produced ex nihilo), and then we apply the production rules to produce new elements \(F(F(\emptyset))\) and iterate this production process indefinitely. We want to determine the limit of this ascending chain. One way to compute this limit is by taking a union of such iterations:

\[\bigcup_{n \in \mathbb{N}}F^n(\emptyset),\]

where \(F^n\) is defined via ordinary induction on the natural numbers as

• \(F^0(A) = A\),
• \(F^{n+1}(A) = F(F^n(A))\).

However, there is a technical issue with this approach: it is not the case in general that

\[F\left(\bigcup_{n \in \mathbb{N}}X_n\right) = \bigcup_{n \in \mathbb{N}}F(X_n).\]

A map \(F\) satisfying this condition is called \(\omega\)-continuous. If indeed the map is \(\omega\)-continuous, then the union is a fixed point, since

\[F\left(\bigcup_{n \in \mathbb{N}}F^n(\emptyset)\right) = \bigcup_{n \in \mathbb{N}}F(F^n(\emptyset)) = \bigcup_{n \in \mathbb{N}}F^n(\emptyset).\]

However, we do not want to place such a strong requirement on the map \(F\). We seek a definition that will work for any monotone map.

For a set \(A\) to be a limit of this ascending chain, it must be the case that \(F(A) \subseteq A\), i.e., it must be a pre-fixed point. In particular, we want the least such pre-fixed point. We can simply take the intersection of all pre-fixed points.

Note that we cannot define the least fixed point as the intersection of all fixed points, namely

\[\cap\{S \subseteq X \mid F(S) = S\},\]

since the intersection of fixed points is not guaranteed to be a fixed point.

However, the intersection of pre-fixed points is guaranteed to be a pre-fixed point. If we intersect all pre-fixed points, we will obtain the least pre-fixed point. Since the least pre-fixed point is also a fixed point, this suffices to obtain the least fixed point.

This leads to the following theorem.

Theorem (Least Fixed Point). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. Then:

\[\mu F = \cap \{S \subseteq X \mid F(S) \subseteq S \}.\]

Proof. Suppose that \(x \in F(\mu F)\), \(S \subseteq X\), and \(F(S) \subseteq S\). Then, by construction, \(\mu F \subseteq S\), and, since \(F\) is monotone, \(F(\mu F) \subseteq F(S)\), and thus \(F(\mu F) \subseteq S\) and \(x \in S\). Since \(S\) was arbitrary, it follows that \(x \in \mu F\). Since \(x\) was arbitrary, it follows that \(F(\mu F) \subseteq \mu F\). Conversely, suppose that \(x \in \mu F\). Then, since \(F(\mu F) \subseteq \mu F\) and \(F\) is monotone, it follows that \(F(F(\mu F)) \subseteq F(\mu F)\). By construction, this means that \(x \in F(\mu F)\). Since \(x\) was arbitrary, \(\mu F \subseteq F(\mu F)\). Thus, \(F(\mu F) = \mu F\), so \(\mu F\) is a fixed point of \(F\).

Next, suppose that \(F(A) = A\) for some set \(A \subseteq X\). Suppose that \(x \in \mu F\). Then, since \(F(A) \subseteq A\), it follows that \(x \in A\). Since \(x\) was arbitrary, \(\mu F \subseteq A\). Thus, \(\mu F\) is the least fixed point of \(F\). \(\square\)

Theorem. Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. A set \(A\) is the least pre-fixed point of \(F\) if and only if it is the least fixed point of \(F\).

Proof. Suppose that \(A\) is the least pre-fixed point of \(F\). Then, by definition, \(F(A) \subseteq A\), and, since \(F\) is monotone, \(F(F(A)) \subseteq F(A)\), and \(F(A)\) is a pre-fixed point of \(F\). Since \(A\) is the least pre-fixed point, it follows that \(A \subseteq F(A)\), and hence \(A = F(A)\) and \(A\) is a fixed point of \(F\).

Conversely, suppose that \(A\) is the least fixed point of \(F\). Then, by definition, \(F(A) = A\) and also \(F(A) \subseteq A\) and \(A\) is a pre-fixed point of \(F\). Let \(B\) be any pre-fixed point of \(F\). By definition, \(F(B) \subseteq B\). By the Least Fixed Point theorem,

\[A = \cap \{S \subseteq X \mid F(S) \subseteq S \}.\]

It follows that \(A \subseteq B\). Thus, since \(B\) was arbitrary, \(A\) is the least fixed point of \(F\). \(\square\)

Structurally-Inductive Proofs

Combining the previous theorems on pre-fixed and fixed points, we immediately arrive at the following corollary:

Corollary (Inductive Proof Principle). Let \(X\) be any set and and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any monotone map. For any pre-fixed point \(A\), \(\mu F \subseteq A\).

It isn't obvious why this constitutes a proof principle, so some explanation is required. Typically, this principle is applied in the special case when \(A \subseteq \mu F\). Let \(P\) be any predicate on elements of \(\mu F\), and consider its comprehension:

\[A = \{x \in \mu F \mid P(x)\}.\]

By construction, \(A \subseteq \mu F\). If we can demonstrate that \(A\) is a pre-fixed point of \(F\), i.e., that \(F(A) \subseteq A\), then by the inductive proof principle, it follows that \(\mu F \subseteq A\) and hence \(\mu F = A\). In other words, the predicate \(P\) is satisfied for all elements \(x \in \mu F\). The inductive proof principle thus permits us to prove that every element of some inductively-defined set satisfies a given property.

If we think of \(F\) as a set of "rules" for producing new elements \(F(A)\) from existing elements \(A\), then this indicates that \(A\) is closed under these rules.

Example: First-Order Logic

Structural induction is often used to define syntax. First, we define a stock of symbols. For first-order logic, this includes the following:

• A countable set of variables \(\mathcal{V}\).
• A set of constant symbols \(\mathcal{C}\).
• A set of function symbols \(\mathcal{F}\).
• A set of relation symbols \(\mathcal{R}\).
• A set of syntactic symbols \(\mathcal{S} = \{\exists, (, ), \neg, \lor, =, \bot\} \cup \{,\}\).

We assume that these sets are disjoint. We also include an arity function \(a : \mathcal{F} \cup \mathcal{R} \rightarrow \mathbb{N}\) that assigns an arity (number of arguments) to each function and relation symbol.

The alphabet \(\Sigma\) of symbols is then defined as

\[\Sigma = \mathcal{V} \cup \mathcal{C} \cup \mathcal{F} \cup \mathcal{R} \cup \mathcal{S}.\]

Here, we write the symbols using metavariables such as \(\exists\) or \(\neg\) or \(f\) or \(R\), etc. Each of these metavariables stands for some set that is an element of \(\Sigma\). It does not matter which set defines a symbol, as long as it is unique.

We then consider a set of candidate strings, i.e., the set of all finite sequences of symbols from this alphabet, namely,

\[\Sigma^* = \bigcup_{n \in \mathbb{N}}\Sigma^n,\]

where \(\Sigma^n\) can be understood either as the set of all functions from the finite set \(n\) to \(\Sigma\) or as the set of all \(n\)-tuples of elements of \(\Sigma\) (each is isomorphic). We will treat strings as sequences. Note that \(\Sigma^0 = \{\varepsilon\}\) contains a single element representing the empty sequence \(\varepsilon\).

The set \(\Sigma\) contains all possible sequences, including ill-formed sequences such as

\[,,\exists fff \neg \neg \exists \lor(((.\]

We want to separate the well-formed sequences such as

\[(\exists x)(P(x) \rightarrow Q(x)).\]

We begin by defining a class of well-formed strings called terms.

To this end, we define a monotone map \(T : \mathcal{P}(\Sigma^*) \rightarrow \mathcal{P}(\Sigma^*)\) as follows:

\begin{align*}T(S) &= \mathcal{V}^1 \\&\cup \mathcal{C}^1 \\&\cup \bigcup_{n \in \mathbb{N}} \{f(t_1, \dots, t_n) \mid f \in \mathcal{F} \text{ and } a(f) = n \text { and } (t_i)_{i=1}^n : n \rightarrow S\},\end{align*}

where \(\mathcal{V}^1\) and \(\mathcal{C}^1\) represent all respective singleton sequences (sequences with only a single element from the respective set),

Here, the notation

\[f(t_1, \dots, t_n) \]

indicates an explicit finite sequence of symbols such that is the concatenation of the respective sub-sequences. Define the concatenation of two sequences \((a_i)_{i=1}^m : m \rightarrow A\) and \((b_i)_{i=1}^n : n \rightarrow B\) as the sequence \((ab)_{i=1}^{m+n}\) defined as follows:

\[(ab)(i) = \begin{cases}a(i) & \text{if } i \le m \\ b(i) & \text{otherwise}.\end{cases}\]

Given \(n\) sequences \((a_i\vert_j)_{j=1}^{m_i}\), define their concatenation \((a_1a_2\dots a_n)_{j=1}^{\sum_{i=1}^n m_i}\) recursively as follows:

\[(a_1a_2\dots a_n)(j) = (a_1(a_2 \dots a_n))(j).\]

Then

\[f(t_1, \dots, t_n)\]

represents the concatenation of the following sequences:

• the singleton sequence whose sole element is \(f\)
• the singleton sequence whose sole element is \((\)
• the sequence \(t_1\) (since each term is itself a sequence of symbols)
• the singleton sequence whose sole element is \(,\)
• etc.

The map \(T\) constructs new strings from a set of strings \(S\); it represents the "rules" for producing new strings from existing strings. In particular, \(T\) tacitly represents the following rules:

• A string consisting of a variable is a term (since the set \(\mathcal{V}^1\) appears on the right-hand side of the definition of \(T\));
• A string consisting of a constant is a term (since the set \(\mathcal{C}^1\) appears on the right-hand side of the definition of \(T\));
• The string \(f(t_1, \dots, t_n)\) is a term whenever \(f \in \mathcal{F}\) (i.e., \(f\) is a function symbol), \(a(f) = n\), and \(t_1, \dots, t_n\) is a sequence of terms. The map \(T\) avoids impredicativity by referring to a set \(S\) representing an intermediate set of terms.

Recall that we are interested in the limit of the ascending chain

\[T(\emptyset) \subseteq T(T(\emptyset)) \subseteq T(T(T(\emptyset))) \subseteq \dots .\]

We previously established that this limit is precisely the least fixed point \(\mu T\). Thus, the set of terms is precisely \(\mu T\).

Next, we define the well-formed formulas. To this end, we define a monotone map \(F : \mathcal{P}(\Sigma^*) \rightarrow \mathcal{P}(\Sigma^*)\) as follows:

\begin{align}F(S) &= \{\bot\} \\&\cup \bigcup_{n \in \mathbb{N}}\{R(t_1, \dots, t_n) \mid R \in \mathcal{R} \text{ and } a(R) = n \text{ and } (t_i)_{i=1}^n : n \rightarrow \mu T \} \\&\cup \{(t_1 = t_2) \mid t_1, t_2 \in \mu T\} \\&\cup \{(\neg \varphi) \mid \varphi \in S\} \\&\cup \{(\varphi \lor \psi) \mid \varphi, \psi \in S\} \\&\cup \{((\exists x)\varphi) \mid x \in \mathcal{V} \text { and } \varphi \in S\}.\end{align}

This corresponds to the following rules:

• \(\bot\) is a formula.
• \(R(t_1, \dots, t_n)\) is a formula for every relation \(R\) with arity \(n\) and sequence of terms \(t_1, \dots, t_n\).
• \((t_1 = t_2)\) is a formula for all terms \(t_1\) and \(t_2\).
• \((\neg \varphi)\) is a formula for every formula \(\varphi\).
• \((\varphi \lor \psi)\) is a formula for all formulas \(\varphi\) and \(\psi\).
• \(((\exists x)\varphi)\) is a formula for every variable \(x\) and formula \(\varphi\).

The set of all formulas is \(\mu F\).

Next, we will indicate how to carry out inductive proofs about formulas. Suppose we wish to establish some property \(P\) for all formulas. We consider the set

\[A = \{x \in \mu F \mid P(x)\}.\]

If we can establish that \(A\) is a pre-fixed point of \(F\), i.e., that \(F(A) \subseteq A\), then the inductive proof principle indicates that \(A = \mu F\), i.e., \(P(x)\) is satisfied for all \(x \in \mu F\). Reading off the definition of \(F\), \(F(A) \subseteq A\) means precisely the following:

• \(\bot \in A\), i.e., \(P(\bot)\) is satisfied;
• \(\bigcup_{n \in \mathbb{N}}\{R(t_1, \dots, t_n) \mid R \in \mathcal{R} \text{ and } a(R) = n \text{ and } (t_i)_{i=1}^n : n \rightarrow \mu T \} \subseteq A\), i.e., for all \(n \in \mathbb{N}\) and for all \(R \in \mathcal{R}\) with \(a(R) = n\) and for all sequences of terms \((t_i)_{i=1}^n : n \rightarrow \mu T\), \(P(R(t_1, \dots, t_n))\) is satisfied;
• \(\{(t_1 = t_2) \mid t_1, t_2 \in \mu T\} \subseteq A\), i.e., for all terms \(t_1, t_2 \in \mu T\), \(P((t_1 = t_2))\) is satisfied;
• \(\{(\neg \varphi) \mid \varphi \in A\} \subseteq A\), i.e., for all formulas \(\varphi \in A\), i.e., formulas such that \(P(\varphi)\) is satisfied, \(P((\neg \varphi))\) is satsified;
• \(\{(\varphi \lor \psi) \mid \varphi, \psi \in A\} \subseteq A\), i.e., for all formulas \(\varphi, \psi \in A\), i.e., formulas such that \(P(\varphi)\) is satisfied and \(P(\psi)\) is satisfied, \(P((\varphi \lor \psi))\) is satisfied;
• \(\{((\exists x)\varphi) \mid x \in \mathcal{V} \text { and } \varphi \in A\} \subseteq A\), i.e., for every variable \(x \in \mathcal{V}\) and formula \(\varphi \in A\), i.e., formula such that \(P(\varphi)\) is satisfied, \(P(((\exists x)\varphi))\) is satisfied.

Typically, one would also need to carry out an inductive proof for terms first in order to establish the same result for formulas. Then, in the proof for formulas, it can be assumed that all terms satisfy the requisite property. Here,

\[A = \{x \in \mu T \mid P(x)\}.\]

Reading off the definition of \(T\), \(T(A) \subseteq A\) means precisely that

• \(\mathcal{V}^1 \subseteq A\), i.e., \(P(v)\) is satisfied for all variable strings \(v \in \mathcal{V}^1 \);
• \(\mathcal{C}^1 \subseteq A\), i.e., \(P(c)\) is satisfied for all constant strings \(c \in \mathcal{C}^1 \);
• \(\bigcup_{n \in \mathbb{N}} \{f(t_1, \dots, t_n) \mid f \in \mathcal{F} \text{ and } a(f) = n \text { and } (t_i)_{i=1}^n : n \rightarrow A\} \subseteq A\), i.e., for all \(n \in \mathbb{N}\) and for all \(f \in \mathcal{F}\) such that \(a(f) = n\) and for all sequences of terms \((t_i)_{i=1}^n : n \rightarrow A\), i.e., all sequences of terms such that \(P(t_i)\) is satisfied for all \(i \in \{1,\dots,n\}\), \(P(f(t_1, \dots, t_n))\) is satisfied.

Thus, we can summarize inductive proofs on formulas as follows:

• Prove that the property holds for all variables.
• Prove that the property holds for all constants.
• Prove that the property holds for all function applications \(f(t_1, \dots, t_n)\), assuming that it holds for each term \(t_1, \dots, t_n\).
• Prove that the property holds for \(\bot\).
• Prove that the property holds for all relation applications \(R(t_1, \dots, t_n)\), assuming that it holds for each term \(t_1, \dots, t_n\).
• Prove that the property holds for all equality applications \((t_1 = t_2)\), assuming that it holds for each term \(t_1\) and \(t_2\).
• Prove that the property holds for \((\neg \varphi)\), assuming that it holds for \(\varphi\).
• Prove that the property holds for \((\varphi \lor \psi)\), assuming that it holds for each formula \(\varphi\) and \(\psi\).
• Prove that the property holds for \(((\exists x)\varphi)\), assuming that it holds for \(\varphi\).

Structural Recursion

Structural induction can also be used to define structurally recursive functions. It is likewise possible to define relations by structural recursion.

Since, in set theory, functions are themselves sets, we can define functions by structural induction. However, in order for us to establish that the sets thus defined are indeed functions, we generally require that the domain of the function be a structurally inductive set so that we can exploit the inductive proof principle on this domain.

Consider the example of computing the free variables of a formula of first-order logic. First, we define a recursive function

\[\mathrm{Var} : \mu T \rightarrow \mathcal{P}(\mathcal{V})\]

that computes all variables within a term via structural recursion. We define a monotone map \(V_T\)

\[V_T : \mathcal{P}(\mu T \times \mathcal{P}(\mathcal{V})) \rightarrow \mathcal{P}(\mu T \times \mathcal{P}(\mathcal{V}))\]

as follows:

\begin{align*}V_T(S) &= \{(v, \{v\}) \mid v \in \mathcal{V}\} \\&\cup \{(c,\emptyset) \mid c \in \mathcal{C}\} \\&\cup \bigcup_{n \in \mathbb{N}}\left\{(f(t_1, \dots, t_n), \bigcup_{i=1}^n X_i) \mid f \in \mathcal{F} \text{ and } a(f) = n \text{ and } (t_i, X_i)_{i=1}^n : n \rightarrow S \right\}.\end{align*}

We then define the recursive function

\[\mathrm{Var} = \mu V_T.\]

We need to confirm that this is indeed a total function. Thus, we need to demonstrate that, for an arbitrary term \(t\), there exists a unique set \(X\) such that \((t, X) \in \mu V_T\). We proceed by induction:

• For any variable \(v \in \mathcal{V}\), \((v, \{v\}) \in \mu V_T\) by construction. This is the only way variables are introduced, so it is necessarily unique.
• For any constant \(c \in \mathcal{C}\), \((c, \emptyset) \in \mu V_T\) by construction. This is the only way constants are introduced, so it is necessarily unique.
• For any term \(f(t_1, \dots, t_n)\) where there exists a unique pair \((t_i, X_i) \in \mu V_T\), the pair \((f(t_1, \dots, t_n), \bigcup_{i=1}^n X_i)\) is also unique.

Our goal is to define a recursive function

\[\mathrm{Free} : \mu F \rightarrow \mathcal{P}(\mathcal{V})\]

that accepts a formula and outputs the set containing its free variables. We define a monotone map

\[V : \mathcal{P}(\mu F \times \mathcal{P}(\mathcal{V})) \rightarrow \mathcal{P}(\mu F \times \mathcal{P}(\mathcal{V}))\]

as follows:

\begin{align*}V(S) &= \{(\bot, \emptyset)\} \\&\cup \bigcup_{n \in \mathbb{N}}\left\{(R(t_1, \dots, t_n), \bigcup_{i=1}^n \mathrm{Var}(t_i)) \mid (t_i)_{i=1}^n : n \rightarrow \mu T \right\} \\&\cup \{((t_1 = t_2), \mathrm{Var}(t_1) \cup \mathrm{Var}(t_2)) \mid t_1, t_2 \in \mu T\} \\&\cup \{((\neg \varphi), X) \mid (\varphi, X) \in S\} \\&\cup \{((\varphi \lor \psi), X \cup Y) \mid (\varphi, X) \in S \text{ and } (\psi, Y) \in S\} \\&\cup \{(((\exists x)\varphi), X \setminus \{x\}) \mid (\varphi, X) \in S\}\end{align*}

A similar inductive argument shows that this relation represents a total function.

Conclusion

Though induction and recursion are fairly intuitive concepts that are typically taken for granted, it is nonetheless interesting that they can be analyzed in terms of more fundamental concepts such as the fixed points of monotone maps on powersets.

It is also possible to express induction and recursion in terms of well-founded relations and it is possible to extend induction and recursion to transfinite induction and recursion, which relies on the fact that the class of ordinal numbers is well-ordered.

There is a category-theoretic approach to structural induction and recursion in terms of initial algebras of endofunctors. This has been discussed in various places on this blog (such as this post and this post). Though this approach is fairly general, the category-theoretic approach works most straightforwardly with algebraic constructions.

Moreover, it is possible to dualize structural induction to structural coinduction. In this case, for syntactic definitions, the ambient set of all finite and infinite sequences of symbols from an alphabet is considered, and the theory is expressed in terms of the greatest fixed points of monotone maps on the respective powerset.