First-Order Logic in the Medvedev Lattice

详细信息    查看全文

• 作者：Rutger Kuyper
• 关键词：Medvedev degrees ; Intuitionistic logic ; First ; order logic ; 03D30 ; 03B20 ; 03G30
• 刊名：Studia Logica
• 出版年：2015
• 出版时间：December 2015
• 年：2015
• 卷：103
• 期：6
• 页码：1185-1224
• 全文大小：760 KB
• 参考文献：1.Balbes R., Dwinger P.: Distributive Lattices. University of Missouri Press, Columbia (1975)
  2.Basu, S. S., and S. G. Simpson, Mass problems and higher-order intuitionistic logic, 2014. arxiv:-408.-763 .
  3.Chagrov A., Zakharyaschev M.: Modal Logic. Clarendon Press, Oxford (1997)
  4.Gabbay D. M.: Properties of Heyting’s predicate calculus with respect to r.e. models. The Journal of Symbolic Logic 41(1), 81-4 (1976)CrossRef
  5.Gabbay D.M.: Semantical Investigations in Heyting’s Intuitionistic Logic. Springer, Berlin (1981)CrossRef
  6.Hinman P.G.: A survey of Mu?nik and Medvedev degrees. The Bulletin of Symbolic Logic 18(2), 161-29 (2012)CrossRef
  7.Ishihara H., Khoussainov B., Nerode A.: Computable Kripke models and intermediate logics. Information and Computation 143, 205-30 (1998)CrossRef
  8.Ishihara H., Khoussainov B., Nerode A.: Decidable Kripke models of intuitionistic theories. Annals of Pure and Applied Logic 93, 115-23 (1998)CrossRef
  9.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.
  10.Kolmogorov A.: Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift 35(1), 58-5 (1932)CrossRef
  11.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-58.
  12.Kuyper R.: Natural factors of the Medvedev lattice capturing IPC. Archive for Mathematical Logic 53(7), 865-79 (2014)CrossRef
  13.Lawvere F.W.: Adjointness in foundations. Dialectica 23, 281-96 (1969)CrossRef
  14.Medvedev, Yu. T., Degrees of difficulty of the mass problems, Doklady Akademii Nauk SSSR, (NS) 104(4):501-04, 1955.
  15.Muchnik, A. A., On strong and weak reducibilities of algorithmic problems, Sibirskii Matematicheskii Zhurnal 4:1328-341, 1963.
  16.Odifreddi, P. G., Classical Recursion Theory, Vol. 125 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1989.
  17.Pitts, A. M., Notes on Categorical Logic, Computer Laboratory, University of Cambridge, Lent Term, 1989.
  18.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-28.
  19.Pitts A.M.: Tripos theory in retrospect. Mathematical Structures in Computer Science. 12, 265-79 (2002)CrossRef
  20.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-78 (1988)
  21.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-12.
  22.Tennenbaum S.: Non-Archimedean models for arithmetic. Notices of the American Mathematical Society 6, 270 (1959)
  23.Troelstra, A. S., and D. van Dalen, Constructivism in Mathematics, Vol. 1, North Holland, Amsterdam, 1988.
  24.van Oosten, J., Realizability: An Introduction to Its Categorical Side, Vol. 152 of Studies in Logic and the Foundations of Mathematics, Elsevier, Amsterdam, 2008.
  
• 作者单位：Rutger Kuyper (1)
  
  1. Department of Mathematics, Radboud University Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands
  
• 刊物类别：Humanities, Social Sciences and Law
• 刊物主题：Philosophy
  Logic
  Mathematical Logic and Foundations
  Computational Linguistics
  
• 出版者：Springer Netherlands
• ISSN：1572-8730

文摘

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. Keywords Medvedev degrees Intuitionistic logic First-order logic