2
$\begingroup$

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

Improve this question
$\endgroup$
4
  • 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$
    – Gerhard Paseman
    Commented 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
    Commented Dec 3, 2015 at 20:31
  • 2
    $\begingroup$ If I understand it correctly you are looking for Post--Linial theorems. $\endgroup$
    – Karel Chvalovský
    Commented 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
    Commented Dec 5, 2015 at 12:19

1 Answer 1

Reset to default
1
$\begingroup$

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

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .