×

Constructive reflectivity principles for regular theories. (English) Zbl 1480.03060

Summary: Classically, any structure for a signature \(\Sigma\) may be completed to a model of a desired regular theory \(\mathbb{T}\) by means of the chase construction or small object argument. Moreover, this exhibits \(\mathrm{Mod}(\mathbb T)\) as weakly reflective in \(\mathrm{Str}(\Sigma)\).
We investigate this in the constructive setting. The basic construction is unproblematic; however, it is no longer a weak reflection. Indeed, we show that various reflectivity principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e., set) models.
Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. While in this setting, we also give a version of one classical lemma which is trivial over discrete signatures but more interesting here: the abstraction of constants in a proof to variables.

MSC:

03F65 Other constructive mathematics
03G30 Categorical logic, topoi
18C10 Theories (e.g., algebraic theories), structure, and semantics
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abiteboul, S., Hull, R., and Vianu, V., Foundations of Databases, Addison-Wesley, Reading, MA, 1995. · Zbl 0848.68031
[2] Aczel, P., The type theoretic interpretation of constructive set theory, Logic Colloquium ’77 (MacIntyre, A., Pacholski, L., and Paris, J., editors), Studies in Logic and the Foundations of Mathematics, vol. 96, North-Holland, Amsterdam, New York, 1978, pp. 55-66. · Zbl 0481.03035
[3] Aczel, P., The relation reflection scheme. Mathematical Logic Quarterly, vol. 54 (2008), no. 1, pp. 5-11. · Zbl 1134.03038
[4] Adámek, J., Herrlich, H., Rosický, J., and Tholen, W., On a generalized small-object argument for the injective subcategory problem. Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. 43 (2002), no. 2, pp. 83-106. · Zbl 1002.18002
[5] Adámek, J. and Rosický, J., Locally Presentable and Accessible Categories, London Mathematical Society Lecture Note Series, vol. 189, Cambridge University Press, Cambridge, 1994. · Zbl 0795.18007
[6] Bell, J. L. and Machover, M., A Course in Mathematical Logic, North-Holland, Amsterdam, New York, Oxford, 1977. · Zbl 0359.02001
[7] Blass, A., Injectivity, projectivity, and the axiom of choice. Transactions of the American Mathematical Society, vol. 255 (1979), pp. 31-59. · Zbl 0426.03053
[8] Coste, M., Lombardi, H., and Roy, M.-F., Dynamical method in algebra: Effective Nullstellensätze, Annals of Pure and Applied Logic, vol. 111 (2001), no. 3, pp. 203-256. · Zbl 0992.03076
[9] Diaconescu, R., Institution-independent Model Theory, Studies in Universal Logic, Birkhäuser Verlag, Basel, 2008. · Zbl 1144.03001
[10] Fitting, M. C., Intuitionistic Logic, Model Theory and Forcing, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, London, 1969. · Zbl 0188.32003
[11] Hofmann, M., Extensional concepts in intensional type theory, Ph.D. thesis, University of Edinburgh, 1995.
[12] Johnstone, P. T., Sketches of an Elephant: A Topos Theory Compendium. vol. 1 and 2, Oxford Logic Guides, vol. 43 and 44, The Clarendon Press, Oxford University Press, New York, 2002. · Zbl 1071.18001
[13] Lambek, J. and Scott, P. J., Introduction to Higher Order Categorical Logic, Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, Cambridge, 1986. · Zbl 0596.03002
[14] Rathjen, M., Choice principles in constructive and classical set theories, Logic Colloquium ’02 (Chatzidakis, Z., Koepke, P., and Pohlers, W., editors), Association for Symbolic Logic, Lecture Notes in Logic, vol. 27, Peters, A. K., Wellesley, MA, 2006, pp. 299-326. · Zbl 1121.03065
[15] Troelstra, A. S. and van Dalen, D., Constructivism in Mathematics, Studies in Logic and the Foundations of Mathematics, vol. 121 and 123, North-Holland, Amsterdam, 1988. · Zbl 0661.03047
[16] van den Berg, B. and Moerdijk, I., The axiom of multiple choice and models for constructive set theory. Journal of Mathematical Logic, vol. 14 (2014), no. 1, 1450005. · Zbl 1337.03079
[17] Veldman, W., An intuitionistic completeness theorem for intuitionistic predicate logic, this Journal, vol. 41 (1976), no. 1, pp. 159-166. · Zbl 0355.02018
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.