The first collapsing-function identity for worms and spiders

Let \uppsi0\uppsi_0 be the ordinal collapsing function and let \cond\cond_{\top} denote the corresponding worm/spider collapsing operation. The first collapsing-function identity. One has

\uppsi0\Upomegaω1=\cond(0\atopwithdelims\Upomegaω1).\uppsi_0{\Upomega^\omega 1}=\cond_{\top}\left({0 \atopwithdelims \langle \rangle{\Upomega^\omega 1}}\top\right).

This identity is presented as a conjecture because the paper concludes with it as a proposed translation between the two notation systems; the supplied context gives no proof or resolution.

Sources & referencesView supporting material

Primary source

David Fernández-Duque, “Worms and Spiders: Reflection calculi and ordinal notation systems”, arXiv:1605.08867 (2017).

Progress summary

Never refreshed

Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.

Solutions 0

No solutions have been posted yet.