Prawitz's conjecture on logically valid inference rules

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 $\mathfrak{J}$ on every base $\mathfrak{B}$. Let $\texttt{IL}$ denote intuitionistic logic, and say that $\mathscr{R}$ is derivable in $\texttt{IL}$ when adding $\mathscr{R}$ to $\texttt{IL}$ does not yield any new derivable conclusions. Prawitz's conjecture. If $\mathscr{R}$ is logically valid relative to some $\mathfrak{J}$, then $\mathscr{R}$ is derivable in $\texttt{IL}$.

The conjecture concerns completeness for inference rules in Prawitz's proof-theoretic semantics, rather than merely completeness for the associated logical-consequence relation. The paper discusses it in the monotonic miP-tV setting; its resolution is not established in the supplied text.