Untyped λ-calculus: proof that for any binary relation $R \vDash \lozenge \Rightarrow R^* \vDash \lozenge$

65 Views Asked by At

I'm currently in the process of reading Barendregt's "The Lambda Calculus - Its Syntax and Semantics" (1985 revised edition) and I've stumbled across a lemma whose proof I can't quite comprehend. The lemma (3.2.2) states that for all binary relations R on a set the following holds: $$R \vDash\lozenge\Rightarrow R^*\vDash\lozenge$$, where $\lozenge$ is the diamond property of a relation:$$R\vDash\lozenge\iff\forall M,M_1,M_2\left[(M,M_1)\in R \wedge (M,M_2)\in R \Rightarrow \exists M_3[(M_1,M_3)\in R \wedge (M_2,M_3)\in R]\right]$$, and $R^*$ is the transitive closure of $R$:$$\forall M,N[(M,N)\in R\Rightarrow(M,N)\in R^*]$$ and $$\forall M,N,L[(M,N)\in R^*\wedge(N,L)\in R^*\Rightarrow(M,L)\in R^*)].$$

The proof makes use of category theory and is simply a diagram. Trying to make sense of it, I thought the continuous lines meant the relation $R$, and the dashed lines either the application of $\lozenge$ on the relation or $R^*$, but I don't fully understand it.

What exactly does the diagram mean and how does it prove the lemma? Is there a more rigurous approach to proving this rather than a drawing?

Edit: in the (very clear) answer I received, it was pointed out to me that the diagram I couldn't understand doesn't have anything to do with category theory. I'm sorry for my lack of understanding and poor choice of words - I have striked out the observation.

1

There are 1 best solutions below

2
On BEST ANSWER

There is no category theory here.

Suppose $MR^\ast M_1$ and $MR^\ast M_2$. Then $M$ is represented by the top-left corner of the diagram, and $M_1$ and $M_2$ are represented by the bottom-left and top-right corners (or the other way around). Since $R^\ast$ is the transitive closure of $R$, we have, for some $n, m \ge 1$, the relations $A_0RA_1R\cdots RA_n$ and $B_0RB_1R\cdots RB_m$, where $A_0 = B_0 = M$, $A_n = M_1$, and $B_m = M_2$.

The diagram represents the case where $n = 2$ and $m=3$. We have $A_1$ at the middle of the left side, and $B_1, B_2$ along the top. The lines between points in the diagram represent $R$.

The argument works like this. We start with just the top and left sides of the diagram. Since $R\vDash\lozenge$, we obtain an element $N$ such that $A_1RN$ and $B_1RN$. This element corresponds to the lower-right corner of the top-left square. By repeatedly applying $\lozenge$, we will eventually obtain the lower-right corner of the diagram, which is the element $M_3$ we need to establish $R^\ast\vDash\lozenge$ for these $M$, $M_1$, and $M_2$.

A more formal argument would use induction on $n$ and $m$.