Abstract
Kolmogorov introduced an informal calculus of problems in an attempt to provide a classical semantics for intuitionistic logic. This was later formalised by Medvedev and Muchnik as what has come to be called the Medvedev and Muchnik lattices. However, they only formalised this for propositional logic, while Kolmogorov also discussed the universal quantifier. We extend the work of Medvedev to first-order logic, using the notion of a first-order hyperdoctrine from categorical logic, to a structure which we will call the hyperdoctrine of mass problems. We study the intermediate logic that the hyperdoctrine of mass problems gives us, and we study the theories of subintervals of the hyperdoctrine of mass problems in an attempt to obtain an analogue of Skvortsova’s result that there is a factor of the Medvedev lattice characterising intuitionistic propositional logic. Finally, we consider Heyting arithmetic in the hyperdoctrine of mass problems and prove an analogue of Tennenbaum’s theorem on computable models of arithmetic.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Balbes R., Dwinger P.: Distributive Lattices. University of Missouri Press, Columbia (1975)
Basu, S. S., and S. G. Simpson, Mass problems and higher-order intuitionistic logic, 2014. arxiv:1408.2763.
Chagrov A., Zakharyaschev M.: Modal Logic. Clarendon Press, Oxford (1997)
Gabbay D. M.: Properties of Heyting’s predicate calculus with respect to r.e. models. The Journal of Symbolic Logic 41(1), 81–94 (1976)
Gabbay D.M.: Semantical Investigations in Heyting’s Intuitionistic Logic. Springer, Berlin (1981)
Hinman P.G.: A survey of Mučnik and Medvedev degrees. The Bulletin of Symbolic Logic 18(2), 161–229 (2012)
Ishihara H., Khoussainov B., Nerode A.: Computable Kripke models and intermediate logics. Information and Computation 143, 205–230 (1998)
Ishihara H., Khoussainov B., Nerode A.: Decidable Kripke models of intuitionistic theories. Annals of Pure and Applied Logic 93, 115–123 (1998)
Kleene, S. C., and R. E. Vesley, The Foundations of Intuitionistic Mathematics, Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Company, Amsterdam, 1965.
Kolmogorov A.: Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift 35(1), 58–65 (1932)
Kolmogorov, A., On the interpretation of intuitionistic logic, in V. M. Tikhomirov (ed.), Selected Works of A. N. Kolmogorov, Vol. I: Mathematics and Mechanics, Kluwer, Boston, 1991, pp. 151–158.
Kuyper R.: Natural factors of the Medvedev lattice capturing IPC. Archive for Mathematical Logic 53(7), 865–879 (2014)
Lawvere F.W.: Adjointness in foundations. Dialectica 23, 281–296 (1969)
Medvedev, Yu. T., Degrees of difficulty of the mass problems, Doklady Akademii Nauk SSSR, (NS) 104(4):501–504, 1955.
Muchnik, A. A., On strong and weak reducibilities of algorithmic problems, Sibirskii Matematicheskii Zhurnal 4:1328–1341, 1963.
Odifreddi, P. G., Classical Recursion Theory, Vol. 125 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1989.
Pitts, A. M., Notes on Categorical Logic, Computer Laboratory, University of Cambridge, Lent Term, 1989.
Pitts, A. M., Categorical logic, in S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (eds.), Logic and Algebraic Methods, Vol. 5 of Handbook of Logic in Computer Science, Clarendon Press, Oxford, 2000, pp. 39–128.
Pitts A.M.: Tripos theory in retrospect. Mathematical Structures in Computer Science. 12, 265–279 (2002)
Skvortsova E.Z.: A faithful interpretation of the intuitionistic propositional calculus by means of an initial segment of the Medvedev lattice. Sibirskii Matematicheskii Zhurnal 29(1), 171–178 (1988)
Sorbi, A., The Medvedev lattice of degrees of difficulty, in S. B. Cooper, T. A. Slaman, and S. S. Wainer (eds.), Computability, Enumerability, Unsolvability: Directions in Recursion Theory, Vol. 224 of London Mathematical Society Lecture Notes, Cambridge University Press, Cambridge, 1996, pp. 289–312.
Tennenbaum S.: Non-Archimedean models for arithmetic. Notices of the American Mathematical Society 6, 270 (1959)
Troelstra, A. S., and D. van Dalen, Constructivism in Mathematics, Vol. 1, North Holland, Amsterdam, 1988.
van Oosten, J., Realizability: An Introduction to Its Categorical Side, Vol. 152 of Studies in Logic and the Foundations of Mathematics, Elsevier, Amsterdam, 2008.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Kuyper, R. First-Order Logic in the Medvedev Lattice. Stud Logica 103, 1185–1224 (2015). https://doi.org/10.1007/s11225-015-9615-2
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-015-9615-2