Abstract
Gödel’s famous result about the completeness of first order deduction can be cast in the general framework of institutions. For this we use Henkin’s method of proving completeness which is very generic and has been exploited over time by producing similar proofs of completeness for various logical systems. This paper sets out a general framework with the purpose to incorporates many of these proofs as examples. As a consequence of this abstraction, the completeness theorem becomes available for many “first order” logical systems that appear in the area of logic or computer science.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Adámek, J., Rosický, J.: Locally Presentable and Accessible Categories. London Mathematical Society Lecture Notes, vol. 189. Cambridge University Press, Cambridge (1994)
Burmeister, P.: A Model Theoretic Oriented Approach to Partial Algebras. Akademie-Verlag (1986)
Diaconescu, R.: Institution-independent Model Theory (to appear)
Diaconescu, R.: An institution-independent proof of Craig Interpolation Theorem. Studia Logica 77(1), 59–79 (2004)
Diaconescu, R.: Institutions with proofs. Journal of Logic and Computation (2006)
Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)
Găină, D., Popescu, A.: An institution-independent proof of Robinson consistency theorem. Studia Logica (to appear)
Henkin, L.: The completeness of the first-order functional calculus. Journal of Symbolic Logic 14(3), 159–166 (1949)
Henkin, L.: The discovery of my completeness proofs. Bulletin of Symbolic Logic 2(2), 127–158 (1996)
Huet, G., Oppen, D.C.: Equations and rewrite rules: a survey. Formal Language Theory: Perspectives and Open Problems, 349–405 (1980)
MacLane, S.: Categories for the Working Mathematician. Springer, New York (1998)
Meseguer, J.: General logics. In: Logic Colloquium 87, pp. 275–329. North Holland, Amsterdam (1989)
Mossakowski, T., Goguen, J., Diaconescu, R., Tarlecki, A.: What is a logic? Logica Universalis (2005)
Petria, M., Diaconescu, R.: Abstract Beth definability in institutions. Journal of Symbolic Logic 71(3), 1002–1028 (2006)
Tarlecki, A.: Bits and pieces of the theory of institutions. In: Poigné, A., Pitt, D.H., Rydeheard, D.E., Abramsky, S. (eds.) Category Theory and Computer Programming. LNCS, vol. 240, Springer, Heidelberg (1986)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Petria, M. (2007). An Institutional Version of Gödel’s Completeness Theorem. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds) Algebra and Coalgebra in Computer Science. CALCO 2007. Lecture Notes in Computer Science, vol 4624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73859-6_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-73859-6_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73857-2
Online ISBN: 978-3-540-73859-6
eBook Packages: Computer ScienceComputer Science (R0)