28 problems

Separation conjecture. For every derivation $T\vdash_{\mathsf{SKS}}R$, there is a derivation of the form

Interpolation conjecture. For every derivation $T\vdash_{\mathsf{SKS}}R$, there is a structure $P$ and derivations

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…

The paper considers the classical positive free logic systems appearing in Theorem … are proper. (b) \mathbf{CPF}^{\begin{sideways}\begin{sideways}iota…

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…

Pakhomov–Freund conjectures. The following two equivalences are conjectured:

Let $\operatorname{KT}_{\ell}(\omega)$ denote labelled Kruskal's theorem with labels drawn from $\omega$, and let $\operatorname{KT}_{\ell}(n)$ denote its restriction to labels bel…

Let $\models$ be the logical-consequence relation defined in the paper's monotonic proof-theoretic semantics, and let $\texttt{IL}$ denote intuitionistic logic. Completeness over…

Let $\mathscr{R}$ be an inference rule, let $\mathfrak{J}$ be a justification structure, and let logical validity relative to $\mathfrak{J}$ mean validity relative to…

$\Sigma^1_2$-altitude characterization conjecture. $\mathsf{Alt}_{\Sigma^1_2}(R)$ is equal to the least height of such a transitive model $M$.

Proof-theoretic dilator conjecture. The proof-theoretic ordinals satisfy

Let $\Lambda$ be over the base structure $\mathfrak{B}_1$, and let $den^*_1$ be a denotation relative to $\Lambda$ such that, for some operational symbol $\phi$ of $\Lambda$,…

An operational type is a specification of the premises and conclusion of a rule together with the domains and co-domains governing its discharged assumptions. Let…

Isomorphism conjecture. There is an isomorphism

Let $\mathbf{MLTT}^-$ be Martin-Löf type theory without $W$-types, let $\mathbf{UA}$ denote the univalence axiom, and let $\mathbb{R}_{\mathbf{HIT}}$ denote the axiom that the high…

Sound reflection hierarchy classification conjecture. For every $n\in\mathbb{N}$, both of the following hold: (1) there exists a $0^{(n)}$-recursive sequence $(T_n)_{n<\omega}$ of…

Monotone-operator classification conjecture. For some $\beta\preceq\alpha$ and some true sentence $\varphi$, for every $\psi$ such that $T+\psi\vdash\varphi$,

Let $T$ be a strong system with an ordinal analysis based on ordinal representation systems $\mathsf{OT}$. These systems give rise to functors … that send dilators to ordinal repre…

Classification conjecture for monotone proof-theoretic operators. Suppose $\mathfrak{g}$ is monotone, non-constant, and recursive, with $\mathfrak{g}(\varphi)\in\Pi_1$ for every se…

Intermediate-extension conjecture. There is a proper normal extension $\mathbf{L}$ of $\mathbf{E}$ such that

Separation property for $\mathbf{E}$. Any formula derivable in $\mathbf{E}$ is also derivable using only the axioms in group $(\mathbf{i})$ and those groups among $(\mathbf{c})$–…

Lower-bounds sharpening conjecture. Then

Lower-bounds phase-transition conjecture. Under these assumptions,

Transfer-principle conservation conjecture. Under these hypotheses, the displayed internal consequence follows. The claim is introduced as a consequence that would establish the pr…