Decidability conjecture for non-hypothetical logic over Peano Arithmetic

The language and proof system of non-hypothetical logic are considered over the axioms of Peano Arithmetic, denoted by $\mathsf{PA}$, in a purely relational language. One may also add a fixed theorem of $\mathsf{PA}$ as an additional axiom. Decidability conjecture. Non-hypothetical logic is decidable over the axioms of $\mathsf{PA}$ and, more ambitiously, over any fixed theorem of $\mathsf{PA}$ taken as an additional axiom. The paper defends these conjectures by drafting an algorithm for deciding the former; the supplied text does not establish whether either conjecture is resolved.