First-order logic in the Medvedev lattice

TL;DR

This paper extends the Medvedev lattice framework to first-order logic using categorical hyperdoctrines, explores intermediate logics, and investigates computable models of arithmetic within this structure.

Contribution

It introduces the Medvedev hyperdoctrine for first-order logic and analyzes its logical properties and models, extending prior propositional work.

Findings

Development of the Medvedev hyperdoctrine for first-order logic

Identification of subintervals corresponding to intermediate logics

Proof of an analogue of Tennenbaum's theorem for arithmetic models

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.