In Girard's $\Pi^1_2$-logic, a dilator $D$ is a endofunctor which commutes with pull-back and direct limit on $\mathrm{ON}$, the category whose objects are ordinals and morphisms are strictly increasing functions. For dilator $D_0,D_1$, an embedding from $D_0$ to $D_1$ is a natural transformation from $D_0$ to $D_1$.

My question

Is a following statement true?

If dilators $D_0,D_1$ are bi-embedable, that is there is embeddings $T_0\colon D_0\Rightarrow D_1, T_1\colon D_1\Rightarrow D_0$, then $D_0=D_1$.

I think this statement is true because the fact embeddings of dilators is equal to injective homomorphism when dilators are considered as structures. However I can't check this fact because the paper is written in French….

Girard, Jean-Yves; Ressayre, Jean Pierre, Elements de logique $\Pi^1_n$, Recursion theory, Proc. AMS-ASL Summer Inst., Ithaca/N.Y. 1982, Proc. Symp. Pure Math. 42, 389-445 (1985). ZBL0573.03029.


No. For example consider the dilator $D$ that maps a well-order $A$ to the well-order consisting of denotations

  1. $(2n;x,y)$, where $y<_Ax$ are elements of $A$;
  2. $(2n+1;x)$, where $x\in A$.

The denotations are compared by lexicographical order. For a morphism $f \colon A\to B$ we as usual put $D(f)((m;x_1,\ldots,x_k))=(m;f(x_1),\ldots,f(x_k))$. Now consider the dilator $D'$ that omits from $D$ all the denotations of the form $(0;x,y)$. Clearly, $D$ and $D'$ are bi-embeddable, but not equal.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.