Abstract
Through a reduction of the halting problem for register machines we prove that it is undecidable whether or not a coherent formula is a logical consequence of a coherent theory. We include a simple completeness proof for coherent logic. Although not published in the present form, these results seem to be folklore. Therefore we do not claim originality. Given the undecidability of the halting problem for register machines the presentation is self-contained.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bezem, M.A., Coquand, T.: Automating Geometric Logic, Report 33/04 Research Group on Mathematical Linguistics, Universitat Rovira i Virgili, Tarragona
Bezem, M.A., Springintveld, J.: A simple proof of the undecidability of inhabitation in λP. Journal of Functional Programming 6(5), 1–5 (1996)
Blass, A.: Topoi and computation. Bulletin of the EATCS 36, 57–65 (1998)
Coste, M., Lombardi, H., Roy, M.-F.: Dynamical methods in algebra: effective Nullstellensätze. Annals of Pure and Applied Logic 111(3), 203–256 (2001)
Goldblatt, R.: Topoi: the categorial analysis of logic. North-Holland, Amsterdam (1984) (revised edition)
Horn, A.: On sentences which are true of direct unions of algebras. Journal of Symbolic Logic 16(1), 14–21 (1951)
Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in Prolog. In: Lusk, E.‘., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 415–434. Springer, Heidelberg (1988)
Minsky, M.L.: Recursive unsolvability of Post’s problem of ‘tag’ and other topics in theory of Turing machines. Annals of Mathematics 74(3), 437–455 (1961)
Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12(1), 23–41 (1965)
Shepherdson, J.C., Sturgis, H.E.: Computability of recursive functions. Journal of the ACM 10, 217–255 (1963)
Shepherdson, J.C.: Undecidability of Horn clause logic and pure Prolog, unpublished manuscript (1985)
Skolem, T.: Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischen Sätze nebst einem Theoreme über dichte Mengen, Skrifter I 4(1–36), Det Norske Videnskaps-Akademi, 1920. Also in: Jens Erik Fenstad, editor, Selected Works in Logic by Th. Skolem, pp. 103–136, Universitetsforlaget, Oslo (1970)
Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism (to appear)
Terese: Term Rewriting Systems. CUP (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bezem, M. (2005). On the Undecidability of Coherent Logic. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds) Processes, Terms and Cycles: Steps on the Road to Infinity. Lecture Notes in Computer Science, vol 3838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11601548_2
Download citation
DOI: https://doi.org/10.1007/11601548_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30911-6
Online ISBN: 978-3-540-32425-6
eBook Packages: Computer ScienceComputer Science (R0)