# [meta-]decision problem about decidability of finite Hilbert-style axiomatic systems

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.)

• Consider semi-Thue systems. For each one construct a Hilbert System. I think from this you can get your undecidability result. Gerhard "Pretty Sure About Being Unsure" Paseman, 2015.12.03 Dec 3, 2015 at 20:00
• @GerhardPaseman This is a good suggestion, surely as good as a translation of our problem into Wang tiles or to the Post correspondence problem. I was recently discussing the issue with colleagues by email, and one of them implied that this result was actually part of 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. Dec 3, 2015 at 20:31
• If I understand it correctly you are looking for Post--Linial theorems. Dec 4, 2015 at 8:51
• Well noted, @KarelChvalovský. I am now checking the papers by Yntema and by Ihrig on the subject. Dec 5, 2015 at 12:19

$P_H$ is not decidable.
We could just choose a programming language or similar things, e.g. combinatory logic, and encode $P_H$ into the language as a function.
We could define a set of inference rules $S$ : $$Eval(A,B) \over Eval(A,B')$$ where $A,B$ and $B'$ are expressions in the language, and $B'$ is $B$ after a step of evaluation. And $$Eval(A,\top) \over Eval(X,X)$$ where $\top$ is the expression of "true" in the language, $X$ could be any valid expression in the language. And $$Rules(R) \over Eval(P_H(R \cup \{{ \over Rules(R)}\}),P_H(R \cup \{{\over Rules(R)}\}))$$ where $R$ is a set of inference rules.
Deciding on $S\cup\{{ \over Rules(S)}\}$ in $P_H$ will lead to contradiction.