×

zbMATH — the first resource for mathematics

An institution-independent proof of the Beth definability theorem. (English) Zbl 1134.03043
The authors develop a very general concept of Beth definability within the framework of the so-called ‘institutions’, a categorical abstract model theory which arose within algebraic specification theory, and within this context develop an abstract version of the classical first-order logic proof of the Beth definability theorem in dependence of Craig interpolation. The paper also studies the preservation of Craig interpolation and Beth definability along logic translations, understood as institution comorphisms.
Unfortunately the paper seems to contain a series of technical errors (for example it is stated that any commutative square of signature morphisms in classical first-order logic has the interpolation property, which is wrong), but perhaps they can be repaired.

MSC:
03G30 Categorical logic, topoi
03C40 Interpolation, preservation, definability
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aiguier, M., C. Gaston, and P. Le Gall, ’Feature Specification: a Logic-Independent Approach’, Tech. rep., Université d’Évry, 2004.
[2] Aiguier, M., and P.-Y. Schobbens, ’A Note on Robinson Consistency Lemma’, Tech. rep., Université d’Évry, 2006. Available at www.ibisc.univ-evry.fr/\(\sim\)aiguier.
[3] Barwise J (1974) ’Axioms for Abstract Model Theory’. Annals of Mathematical Logic 7: 221–265 · Zbl 0324.02034 · doi:10.1016/0003-4843(74)90016-3
[4] Borzyszkowski, T., ’Generalized Interpolation in CASL’, Information Processing letters, (2001). · Zbl 1099.68663
[5] Borzyszkowski T. (2002) ’Logical Systems for Structured Specifications’. Theoretical Computer Science 286: 197–245 · Zbl 1061.68104 · doi:10.1016/S0304-3975(01)00317-6
[6] Diaconescu R., (2002). ’Herbrand Theorems in Arbitrary Institutions’. Information Processing Letters 90(1): 29–39. · Zbl 1178.68132 · doi:10.1016/j.ipl.2004.01.005
[7] Diaconescu R. (2003). ’Institution-Independent Ultraproducts’. Fundamenta Informaticae 55(3-4): 321–348. · Zbl 1036.03055
[8] Diaconescu R. (2004) ’An Institution-Independent Proof of Craig Interpolation Property’. Studia Logica 77(1): 59–79 · Zbl 1048.03026 · doi:10.1023/B:STUD.0000034185.62660.d6
[9] Diaconescu R. (2004) ’Interpolation in Grothendieck Institutions’. Theoretical Computer Science 55(3-4): 321–348 · Zbl 1068.68083
[10] Diaconescu, R., J.A. Goguen, and P. Stefaneas, ’Logical Support for Modularisation’, in G. Huet, and G. Plotkin, (eds.), Logical Environment, 1993, pp. 83–130.
[11] Dimitrakos T., and Maibaum T. (2000) ’On a Generalized Modularization Theorem’. Information Processing Letter 74: 65–71 · Zbl 1003.68079 · doi:10.1016/S0020-0190(00)00037-5
[12] Fine K. (1979) ’Failures for the Interpolation Lemma in Quantified Modal Logic’. Journal of Symbolic Logic 44: 201–206 · Zbl 0415.03015 · doi:10.2307/2273727
[13] Gabbay D., and Maksimova L. (2004) Interpoation and Definability Volume 1. Clarendon Press, Oxford
[14] Găină D., and Popescu A. (2007) ’An Institution-Independent Proof of Robinson Consistency Theorem’. Studia Logica 85(1): 41–73 · Zbl 1123.03059 · doi:10.1007/s11225-007-9022-4
[15] Goguen, J., and R. Burstall, ’A Study in the Foundation of Programming Methodology: Specifications, Institutions, Charters and Parchments’, in D Pitt, S. Abramsky, A. Poigné, and D. Rydeheard, (eds.), Proceedings of the Conference on CategoryTheory and Computer Programming, vol. 240 of Lecture Notes in Computer Science, Springer Verlag, 1985, pp. 313–333. · Zbl 0615.68002
[16] Goguen J., and Burstall R. (1992) ’Institutions: Abstract Model Theory for Specification and Programming’. Journal of the Association for Computing Machinery 39(1): 95–146 · Zbl 0799.68134
[17] Salibra, A., and G. Scollo, ’Compactness and Löwenheim-Skolem Properties in Pre-Institution Categories’, in C.Rauszer, (ed.), Algebraic Methods in Logic and in Computer Science, vol. 28, Banach Center Publications, 1993, pp. 67–94. · Zbl 0792.03026
[18] Salibra A., and Scollo G. (1996) ’Interpolation and Compactness in Categories of Pre-Institutions’. Mathematical Structures in Computer Science 6(3): 261–286 · Zbl 0860.03035 · doi:10.1017/S0960129500001006
[19] Sernadas A., Sernadas C., and Caleiro C. (1999) ’Fibring of Logics as a Categorial Construction’. Journal of Logic and Computation 9(2): 149–179 · Zbl 0942.03064 · doi:10.1093/logcom/9.2.149
[20] Tarlecki A. (1985) ’On the Existence of Free Models in Abstract Algebraic Institutions’. Theoretical Computer Science 37(3): 269–304 · Zbl 0608.68014 · doi:10.1016/0304-3975(85)90094-5
[21] Tarlecki A. (1986) ’Quasi-Varieties in Abstract Algebraic Institutions’. Journal of Computer and System Science 33(3): 269–304 · Zbl 0622.68033 · doi:10.1016/0022-0000(86)90057-7
[22] Tarlecki, A., Algebraic Foundations of Systems Specification, chap. Institutions: An Abstract Framework for Formal Specifications, IFIP State-of-the-Art Reports, Springer Verlag, 1999.
[23] Tarski A. (1944) ’The Semantic Conception of Truth’. Philos. Phenomenological Research 4: 13–47 · Zbl 0061.00807
[24] Veloso P., and Fiadeiro S., Veloso J.-L. (2002) ’On Local Modularity and Interpolation in Entailment Systems’. Information Processing Letter 82: 203–211 · Zbl 1043.68075 · doi:10.1016/S0020-0190(01)00271-X
[25] Veloso P., and Maibaum T. (1995) ’On the Modularization Theorem for Logical Specifications’. Information Processing Letter, 53(5): 287–293 · Zbl 0875.68631 · doi:10.1016/0020-0190(94)00203-B
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.