Through a reduction of the halting problem for register ma- chines we prove that it is undecidable whether or not a coherent formula is a logical consequence of a coherent theory. We include a simple com- pleteness proof for coherent logic. Although not published in the present form, these results seem to be folklore. Therefore we do not claim original- ity. Given the undecidability of the halting problem for register machines the presentation is self-contained.
['Marc Bezem']
On the Undecidability of Coherent Logic