# Are these two equivalences really as “immediate” as Jean-Yves Girard claims?

Section 2.1.1 Phase spaces from Jean-Yves Girard's "Linear Logic : Its Syntax and Semantics" says

A phase space is a pair $(M,\bot)$, where $M$ is a commutative monoid (usually written multiplicatively) and $\bot$ is a subset of $M$. Given two subsets $X$ and $Y$ of $M$, one can define $X \multimap Y:=\{m\in M ; \forall n\in X \quad mn \in Y \}$. In particular, we can define for each subset $X$ of $M$ its orthogonal $X^\bot:=X\multimap \bot$. A fact is any subset of $M$ equal to its biorthogonal, or equivalently any subset of the form $Y^\bot$. It is immediate that $X\multimap Y$ is a fact as soon as $Y$ is a fact.

This section implicitly claims that the two equivalences $Y^\bot=Y^{\bot\bot\bot}$ and $X\multimap Y^\bot=(X\multimap Y^\bot)^{\bot\bot}$ (or equivalently $X\multimap Y=(X\multimap Y)^{\bot\bot}$ as soon as $Y=Y^{\bot\bot}$) are "immediate". In longer explicit form, these equivalences read ($\bot$ has been replaced by $Z$, to avoid confusion):

• $Y\multimap Z=((Y\multimap Z)\multimap Z)\multimap Z$
• $X\multimap Y=((X\multimap Y)\multimap Z)\multimap Z$ as soon as $Y=(Y\multimap Z)\multimap Z$
• $X\multimap Y\multimap Z=((X\multimap Y\multimap Z)\multimap Z)\multimap Z$

Because they are not "immediate" to me, I looked into "Girard, J.-Y. : Linear Logic, Theoretical Computer Science, London Mathematical 50:1, pp. 1-102, 1987". Here is paragraph

1.4 Immediate properties
(i) For any $G\subset P$, $G \subset G^{\bot\bot}$;
(ii) For any $G,H\subset P$, $G\subset H \to H^\bot \subset G^\bot$;
(iii) $G$ is a fact iff $G$ is of the form $H^\bot$ for some subset $H$ of $P$.

I agree that (i) and (ii) are immediate (and hence $Y^\bot\subset Y^{\bot\bot\bot}$ is also immediate). However, I fail to grasp intuitively why $H^\bot$ is always a fact (because $Y^{\bot\bot\bot}\subset Y^\bot$ is not immediate to me).

I can prove $Y\multimap Z=((Y\multimap Z)\multimap Z)\multimap Z$ by using "predicate logic", but my proof doesn't really help me to grasp intuitively why it is true. Translated to predicate logic, I want to show

$Lm:=\forall y\ Yy\to Zym$ is equivalent to $Rm:=\forall y'\ (\forall z\ (\forall y\ Yy\to Zyz)\to Zy'z)\to Zy'm$

For the "easy" direction, I replace $\forall z$ with $z=m$ and then use $(A\to B)\to B\Leftrightarrow A\lor B$:

$Rm \Leftarrow \forall y'\ ((\forall y\ Yy\to Zym)\to Zy'm)\to Zy'm \Leftrightarrow \forall y'\ (\forall y\ Yy\to Zym) \lor Zy'm \Leftrightarrow Lm$

For the "hard" direction, I replace $\forall y$ with $y=y'$ and then use $(A\to B)\to B\Leftrightarrow A\lor B$:

$Rm \Rightarrow \forall y'\ (\forall z\ (Yy'\to Zy'z)\to Zy'z)\to Zy'm \Leftrightarrow \forall y\ (\forall z\ Yy\lor Zyz)\to Zym \Leftrightarrow Lm$

I could try to explain why (i) and (ii) are immediate for me (or highlight that I only proved the "easier" equivalence), but the important point is probably that my "head" can stay inside the realm of set theory, and doesn't have to translate everything into predicate logic. For example, my "head" verifies (i) via $n\in G \land m\in G^\bot \Rightarrow mn \in \bot$. Of course I look for an "intuitive" understanding of the two equivalences, but any "short" proof that stays inside of set theory (and doesn't rely on predicate logic too much) should probably be good enough for showing that the statements are really as "immediate" as claimed.

## 1 Answer

Yes, these equivalences are immediate.

1.4 Immediate properties
(i) For any $G\subset P$, $G \subset G^{\bot\bot}$;
(ii) For any $G,H\subset P$, $G\subset H \to H^\bot \subset G^\bot$;
(iii) $G$ is a fact iff $G$ is of the form $H^\bot$ for some subset $H$ of $P$.

(i) can be verified via $n\in G \land m\in G^\bot \Rightarrow mn \in \bot$.
(ii) can be verified via $m\in H^\bot \Rightarrow \forall x\in H\ mn\in \bot \Rightarrow \forall x\in G\ mn\in \bot\Rightarrow m\in G$.
(iii) The direction $H^\bot\subset H^{\bot\bot\bot}$ follows from (i) via $H^\bot\subset (H^\bot)^{\bot\bot}$. The direction $H^{\bot\bot\bot}\subset H^\bot$ follows from (ii) via $H\subset H^{\bot\bot}\Rightarrow (H^{\bot\bot})^\bot\subset H^\bot$.

It is immediate that $X\multimap Y$ is a fact as soon as $Y$ is a fact.

This follows from $X\multimap Y\multimap Z=(XY)\multimap Z$ where $XY:=\{m\in M ; \exists x\in X\ \exists y\in Y \ m = xy \}$.