Principle of recursion for inductively defined relations

Question

If we consider a relation $R$ and then its symmetric-reflexive-transitive closure --say $R^*$--, is there a recursion principle associated with $R^*$?

It seems to me that such unique function is not able to distinguish between the symmetric-transitive cases. Makes sense?

Thanks in advance.

Answer 1

I think that the best setting in which your problem could be approached is that of proof-relevant dependent type theories, but I'll try to give you an answer that doesn't rely on much theory.

What you call "recursion principle" is easy to state for natural numbers for the simple reason that, given $n$, there is only one way to prove that it is a natural number: either $n = 0$, so the proof follows by the axiom that $0 \in \mathbb{N}$, or $n = \mathsf{s}(m)$, and so one reduces to prove that $m$ is a natural number (and goes on in this way).

For a given binary relation $S \subseteq D \times D$ and $x, y \in D$ there could be more than one proof for $x S y$. For example, consider a relation $R$ and the smallest equivalence relation $R^*$ containing $R$, as in your question. If $x R x$ for some $x$, then $x R^* x$ could be proven either from the fact that $x R x$ or from the reflexivity of $R^*$. In a proof-relevant environment this distinction matters.

So, in order to construct a recursion principle, we need to consider the sets $R^*(x, y)$ of "proofs that $x R^* y$" for all $x, y$. These sets could be defined inductively in this way:

1. If $x R y$, then $\mathsf{sup}(x, y) \in R^*(x, y)$ (a proof that $xRy$ is a proof that $x R^* y$, i.e. $R^* \supseteq R$);
2. If $x = y$, then $\mathsf{refl}(x, y) \in R^*(x, y)$ (reflexivity);
3. If $s \in R^*(y, x)$, then $\mathsf{sym}(s) \in R^*(x, y)$ (symmetry);
4. If $s_1 \in R^*(x, z)$ and $s_2 \in R^*(z, y)$, then $\mathsf{trans}(s_1, s_2) \in R^*(x, y)$ (transitivity).

Then the recursion principle is the following (I denote $A \rightarrow B$ the set of functions from $A$ to $B$ for simplicity; $\prod$ is the cartesian product):

Let $X$ be a set, and suppose we are given functions $$f \in R \rightarrow X,$$ $$g \in D \rightarrow X,$$ $$h \in \prod_{y \in D} \prod_{x \in D} (R^*(y, x) \times X \rightarrow X),$$ $$k \in \prod_{x \in D} \prod_{z \in D} \prod_{y \in D} (R^*(x, z) \times X \times R^*(z, y) \times X \rightarrow X)$$ Then there is a unique function $$F \in \prod_{x \in D} \prod_{y \in D} (R^*(x, y) \rightarrow X)$$ such that: $$F(\mathsf{sup}(x, y)) = f(x, y)$$ $$F(\mathsf{refl}(x, y)) = g(x) = g(y)$$ $$F(\mathsf{sym}(s)) = h(s, F(s))$$ $$F(\mathsf{trans}(s_1, s_2)) = k(s_1, F(s_1), s_2, F(s_2))$$