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

  • 2
    $\begingroup$ 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 $\endgroup$ Dec 3, 2015 at 20:00
  • $\begingroup$ @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. $\endgroup$
    – J Marcos
    Dec 3, 2015 at 20:31
  • 2
    $\begingroup$ If I understand it correctly you are looking for Post--Linial theorems. $\endgroup$ Dec 4, 2015 at 8:51
  • $\begingroup$ Well noted, @KarelChvalovský. I am now checking the papers by Yntema and by Ihrig on the subject. $\endgroup$
    – J Marcos
    Dec 5, 2015 at 12:19

1 Answer 1


$P_H$ is not decidable.

The proof is just like the proof for halting problem.

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.