Consider some arbitrary language $S$ written over a given (propositional) signature with a finite collection of finitary constructors, and consider a procedure that receives as input an arbitrary finite Hilbert system $H$, that is, a finite number of axioms and inference rules over $S$. Let $L_H$ be the **logic** inductively defined by $H$ as usual. Let $P_H$ be the problem of ascertaining whether $L_H$ is a decidable logic, that is, deciding about the derivability from $H$ of formulas of $S$.

Is $P_H$ decidable?

(I suspect the answer is negative, and that one could somehow codify the Halting Problem in $P_H$. Before further investigating the matter, I would be happy though to learn if some literature already exists on this subject.)

mathematical folklore. Nonetheless, I have so far failed to find published references to such a result, which would seem to constitute an important bridge between proof systems and automata theory. $\endgroup$