11 problems

Special-case vertical non-uniqueness conjecture. Special cases are not vertically unique.

Vertical non-uniqueness conjecture. For every connective $\texttt{\#}$, if $\texttt{\#}\in\texttt{PC}$ but $\texttt{\#}\notin\texttt{PU}$, then $\texttt{\#}$ is not vertically inte…

Counterexample-sequent conjecture. For each such connective, a suitable sequent $s$ should exist for which the required failure of vertical interderivability can be established.

Exchange-free non-commutative picture conjecture. Dropping $\textsc{Exchange}$ should result in a finer-grained non-commutative picture akin to the ordered logic connectives.

Let ${{\mathrm {Ab}}}+\rul{IDC}^\vee+\rul{Arch}^\vee$ denote the infinitary extension of Abelian logic by the rules $\rul{IDC}^\vee$ and $\rul{Arch}^\vee$, and let $\alg{Z}$ be the…

A linear fibrational double category (LFDC) is a categorical structure with the substructural type-theoretic features described in the source, including type-level weakening, funct…

Completeness conjecture. An axiomatization for the one-variable fragment of the first-order version of full Lambek Calculus should be complete for valid equations, but not for cons…

Let $A$ be the algebra constructed in Section 4, and let $G$ be the Galois algebra constructed by Galatos and Jipsen. Isomorphism conjecture. The algebra $A$ is isomorphic to $G$.…

Sequent calculi conjecture. It should be possible to give perhaps labelled sequent calculi for ERL and $\mathrm{ERL}^*$ that provide a similar operational reading of evolution to t…

The paper considers the Lambek calculus with brackets and unit, denoted here by $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$, together with its multimodal version. The construction…

The paper concerns multi-type proof systems in which structural rules such as commutativity, associativity, weakening, and contraction are controlled through suitable modal operato…