9 problems

Mockingbird partial-order and lattice conjecture. The relation $\preccurlyeq$ on the terms over ${\operatorname{\mathbf{M}}}$ is a partial order relation, and each $\equiv$-equival…

Let $R$ be an operator-only Pure Recursive Calculus with a recursor rule of the form … The step argument $s$ is unrestricted, and an internally definable measure means a measure sa…

Universality conjecture. The same result should hold for arbitrary programming languages: as soon as a language is Turing-complete, it should interpret the authors' logical systems…

A proof forest consists of the cut-reduction system described in the paper, with reductions generated by its cut-reduction rules. Strong normalization conjecture. The cut-reduction…

Let ${\mathbb Q}_{\textup{\textbf{a}}}$ be the common meadow of rational numbers, with an absorbing element for undefined inversion. A datatype defining rewrite system (DDRS) is a…

Let ${\mathbb Q}_0$ be the meadow of rational numbers with totalized inversion. An equational initial algebra specification is a finite set of equations whose initial algebra is…

Strong normalization conjecture. The cut-reduction rules are strongly normalizing: every reduction sequence is of finite length.

Effectiveness conjecture. We conjecture that there is a way to make the comparison relations introduced here effective.

Ordering-type conjecture. We conjecture that such an ordering for Gödel's $T$ will have the Bachmann–Howard ordinal as order type.