First-order logic in the Medvedev lattice

DOI10.1007/S11225-015-9615-2zbMATH Open1378.03033DBLPjournals/sLogica/Kuyper15arXiv1408.5311OpenAlexW2130837870WikidataQ59431839 ScholiaQ59431839MaRDI QIDQ897478FDOQ897478

Authors: Rutger Kuyper 

Publication date: 7 December 2015

Published in: Studia Logica (Search for Journal in Brave)

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 Medvedev hyperdoctrine. We also study the intermediate logic that the Medvedev hyperdoctrine gives us, where we focus in particular on subintervals of the Medvedev hyperdoctrine 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 Medvedev hyperdoctrine and prove an analogue of Tennenbaum's theorem on computable models of arithmetic.

Full work available at URL: https://arxiv.org/abs/1408.5311

Recommendations

• Intermediate logics and factors of the Medvedev lattice
• scientific article; zbMATH DE number 4059356
• Mass problems and intuitionistic higher-order logic
• Kripke models, distributive lattices, and Medvedev degrees
• Constructive logic and the Medvedev lattice

zbMATH Keywords

first-order logicintuitionistic logicMedvedev degrees

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Logical aspects of lattices and related structures (03G10) Other degrees and reducibilities in computability and recursion theory (03D30)

Cites Work

• Constructivism in mathematics. An introduction. Volume I
• Handbook of logic in computer science. Vol. 5: Logical and algebraic methods
• Tripos theory in retrospect
• Semantical investigations in Heyting's intuitionistic logic
• Title not available (Why is that?)
• Realizability. An introduction to its categorical side
• Title not available (Why is that?)
• Classical recursion theory. The theory of functions and sets of natural numbers
• Zur Deutung der intuitionistischen Logik
• Adjointness in Foundations
• A survey of Mučnik and Medvedev degrees
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Mass problems and intuitionistic higher-order logic
• Natural factors of the Medvedev lattice capturing IPC
• Decidable Kripke models of intuitionistic theories
• Computable Kripke models and intermediate logics
• Completeness properties of heyting's predicate calculus with respect to re models

Cited In (4)

• Intermediate logics and factors of the Medvedev lattice
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for publication: First-order logic in the Medvedev lattice

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q897478)