Mass problems and intuitionistic higher-order logic

DOI10.3233/COM-150041arXiv1408.2763MaRDI QIDQ6253873

Publication date: 12 August 2014

Abstract: In this paper we study a model of intuitionistic higher-order logic which we call emph{the Muchnik topos}. The Muchnik topos may be defined briefly as the category of sheaves of sets over the topological space consisting of the Turing degrees, where the Turing cones form a base for the topology. We note that our Muchnik topos interpretation of intuitionistic mathematics is an extension of the well known Kolmogorov/Muchnik interpretation of intuitionistic propositional calculus via Muchnik degrees, i.e., mass problems under weak reducibility. We introduce a new sheaf representation of the intuitionistic real numbers, emph{the Muchnik reals}, which are different from the Cauchy reals and the Dedekind reals. Within the Muchnik topos we obtain a emph{choice principle}

(f o r a l l x, e x i s t s y, A (x, y)) R i g h t a r r o w e x i s t s w, f o r a l l x, A (x, w x)

and a emph{bounding principle}

(f o r a l l x, e x i s t s y, A (x, y)) R i g h t a r r o w e x i s t s z, f o r a l l x, e x i s t s y, (y l e_{m a t h r m T} (x, z) l a n d A (x, y))

where

x, y, z

range over Muchnik reals,

w

ranges over functions from Muchnik reals to Muchnik reals, and

A (x, y)

is a formula not containing

w

or

z

. For the convenience of the reader, we explain all of the essential background material on intuitionism, sheaf theory, intuitionistic higher-order logic, Turing degrees, mass problems, Muchnik degrees, and Kolmogorov's calculus of problems. We also provide an English translation of Muchnik's 1963 paper on Muchnik degrees.

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Other degrees and reducibilities in computability and recursion theory (03D30) Subsystems of classical logic (including intuitionistic logic) (03B20) Higher-order logic (03B16)

This page was built for publication: Mass problems and intuitionistic higher-order logic

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