Mass problems and intuitionistic higher-order logic

Abstract

In this paper we study a model of intuitionistic higher-order logic which we call 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, the Muchnik reals, which are different from the Cauchy reals and the Dedekind reals. Within the Muchnik topos we obtain a choice principle $(\forall x \exists y A (x, y)) \Rightarrow \exists w \forall x A (x, w x)$ and a bounding principle $(\forall x \exists y A (x, y)) \Rightarrow \exists z \forall x \exists y (y ⩽ T (x, z) \land 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. In a separate document we provide an English translation of Muchnik’s 1963 paper on Muchnik degrees.

Keywords

Degrees of unsolvability Muchnik degrees mass problems intuitionism computable analysis higher-order logic topos theory sheaves sheaf theory Kolmogorov

1. Introduction

1.1. Intuitionism and Kolmogorov’s calculus of problems

In the early part of the 20th century, foundations of mathematics was dominated by Georg Cantor’s set theory and David Hilbert’s program of finitistic reductionism. The harshest critic of set theory and Hilbert’s program was L.E.J. Brouwer. Brouwer proposed a constructive approach to mathematics called intuitionism. The philosophical basis of intuitionism was spelled out in Brouwer’s 1907 Ph.D. thesis, entitled “On the foundations of mathematics”. The mathematical consequences were developed in Brouwer’s subsequent papers, 1912–1928. In Brouwer’s view, mathematics allows the construction of mathematical objects on the basis of intuition. Mathematical objects are mental constructs, and mathematics is independent of logic1

¹
On the contrary, logic is an application or part of mathematics (according to Brouwer).

and cannot be founded upon the axiomatic method. In particular, Brouwer rejected Hilbert’s formalism, Cantor’s set theory, and the law of the excluded middle. For more on the history of intuitionism and Brouwer’s work, see [29] and [30, Chapter 1].

One of Brouwer’s principal students was Arend Heyting. Heyting’s primary contribution was, ironical as it may sound, the formalization of intuitionistic logic and arithmetic. Heyting also proposed what is now called the proof interpretation for intuitionistic logic. In this interpretation, the meaning of a proposition A is given by explaining what constitutes a proof of A, and proofs of a logically compound A are explained in terms of proofs of its constituents. A version of this interpretation is described in [30, Chapter 1].

The great mathematician A.N. Kolmogorov published two papers on intuitionism. In his 1932 paper [13]2

1.3. Recursive mathematics and degrees of unsolvability

1.3.1. Recursive mathematics

Informally and non-rigorously, a k-place partial function $f : \subseteq N^{k} \to N$ is said to be effectively calculable if there is an effective procedure such that, given a k-tuple $(m_{1}, \dots, m_{k}) \in N^{k}$ , the procedure halts if and only if $(m_{1}, \dots, m_{k})$ belongs to the domain of f, in which case the procedure returns $f (m_{1}, \dots, m_{k})$ . Several formalizations of this informal idea were developed, among which were Kurt Gödel’s primitive recursive functions (1931), and the later extension of these to general recursive functions (1934), following a suggestion of Jacques Herbrand. There were also Alonzo Church’s λ-calculus and H.B. Curry’s combinatory logic. The equivalence of λ-calculus with combinatory logic was proved by J. Barkley Rosser, Sr. The equivalence of the Herbrand/Gödel recursive functions with the λ-definable functions was proved by Church and S.C. Kleene in 1936. Alan Turing in 1936–1937 defined a class of algorithms, now called Turing machines, and argued convincingly that the class of effectively calculable functions coincides with the class of functions computable by Turing machines. Independently of Turing, Emil Post and A.A. Markov developed their own mathematical models for computation. Church’s thesis is the statement that for each of the above formalisms, the class of functions generated by the formalism coincides with the class of effectively calculable functions. Church’s thesis is now almost universally accepted, but no rigorous proof is possible, because of the non-rigorous nature of the effective calculability concept.

As noted in [29], the discovery of precise definitions of effective calculability and Church’s thesis had no impact on the philosophical basis of intuitionism. Each of these formal definitions describes algorithms in terms of a specific language, which is contrary to Brouwer’s view of mathematics as the languageless activity of the ideal mathematician. Turing’s analysis is not tied to a specific formalism, but his arguments are based on manipulation of symbols and appeals to physical limitations on computing. Such arguments are incompatible with Brouwer’s idea of mathematics as a free creation.

Our discussion above is based on [30, Chapter 1] and on [6,22,29].

1.3.2. Unsolvable problems and Turing degrees

A convincing example of a function which is not effectively calculable was given by Turing in 1936 via the halting problem. This was the first example of an unsolvable decision problem. Soon afterward, many other mathematical problems were shown to be unsolvable, for instance Hilbert’s 10th problem, the word problem for groups, and the problem of finding a completion of first-order arithmetic. Eventually it became desirable to compare the amounts of unsolvability inherent in such problems. Informally and vaguely, a problem A is said to be solvable relative to a problem B if there exists a Turing algorithm which provides a solution of A given a solution of B. If in addition B is not solvable relative to A, then B is strictly more unsolvable than A, i.e., problem B has a strictly greater degree of unsolvability than problem A.

The concept of oracle machines, described by Turing in 1939, gave a means of comparing unsolvable problems. In 1944 Emil Post introduced the rigorous notion of Turing reducibility and Turing degrees as a formalization of degrees of unsolvability associated with decision problems. See [6,22] and Section 5.1 below.

1.3.3. Mass problems and Muchnik degrees

In order to formalize Kolmogorov’s calculus of problems, Y.T. Medvedev [20] introduced mass problems. A mass problem is a subset of the Baire space $N^{N} = {f ∣ f : N \to N}$ . A mass problem is identified with its set of solutions. Informally, to “solve” a mass problem P means to “find” or “construct” an element of the set $P \subseteq N^{N}$ . Formally, if P and Q are mass problems, P is said to be strongly reducible or Medvedev reducible to Q, written $P ⩽ s Q$ , if there exists a partial functional from the Baire space to itself which is Turing computable and maps each element of Q to some element of P. It can be shown that $⩽ s$ is a reflexive and transitive relation on the powerset of $N^{N}$ . The strong degree or Medvedev degree of a mass problem P, denoted $deg s (P)$ , is the equivalence class consisting of all mass problems Q which are strongly equivalent to P, i.e., $P ⩽ s Q$ and $Q ⩽ s P$ . Following Kolmogorov’s ideas [13] concerning the calculus of problems, Medvedev proved rigorously that the collection of all strong degrees, denoted $D s$ , is a model of intuitionistic propositional calculus.

Later Albert A. Muchnik [21]3

³
See also our English translation [2] of Muchnik’s paper [21].

introduced another notion of reducibility for mass problems, known as weak reducibility or Muchnik reducibility. A mass problem P is said to be weakly reducible to a mass problem Q, written

P ⩽ w Q

, if for each

g \in Q

there exists a partial functional which is Turing computable and maps g to some

f \in P

. Again,

⩽ w

is a reflexive and transitive relation on the powerset of

N^{N}

. The weak degree or Muchnik degree of a mass problem P, denoted

deg w (P)

, is the equivalence class consisting of all mass problems Q which are weakly equivalent to P, i.e.,

P ⩽ w Q

and

Q ⩽ w P

. Still following Kolmogorov [13], Muchnik proved that the collection of all weak degrees, denoted

D w

, is a model of intuitionistic propositional calculus.

Thus each of $D w$ and $D s$ provides a rigorous implementation of Kolmogorov’s non-rigorous calculus of problems. Muchnik [21] says that the difference between weak and strong reducibility of mass problems is analogous to the difference between proving the existence of a solution of a differential equation versus effectively finding such a solution.

Section 5.1 below provides further details on mass problems and Muchnik degrees. For a more extensive discussion, see [27]. For more on Muchnik degrees and their relationship to intuitionistic propositional calculus, see [15,26,28].

1.4. Goals of this paper

The purpose of this paper is to extend Muchnik’s interpretation of intuitionistic propositional calculus to intuitionistic higher-order logic. The extension is defined in terms of a sheaf model based on the Muchnik degrees. We call our sheaf model the Muchnik topos. We feel that our study of the Muchnik topos helps to strengthen the connection between two important subjects, intuitionism and degrees of unsolvability. In order to make the paper accessible to various groups of readers, we include background material on sheaf models and degrees of unsolvability.

There is a related line of research, known as realizability, which was initiated by Kleene in 1945 [12] and further developed by other researchers including Martin Hyland and Jaap van Oosten. Both the realizability interpretation and our Muchnik topos interpretation provide close connections between intuitionism and recursion theory. However, the two interpretations are quite different. For a historical account and survey of realizability, see [32]. For recent work on the realizability topos, see [19,33].

1.5. Outline of this paper

The plan of this paper is as follows.

Sections 2 through 4 consist of background material concerning sheaf models and intuitionism. In Section 2 we describe sheaves (a.k.a., sheaves of sets) over topological spaces, and we explain how the sheaves over any fixed topological space form a model of intuitionistic higher-order logic. In Section 3 we discuss sheaf models over topological spaces of a particular kind, namely, poset spaces. We also discuss a choice principle which fails in some sheaf models but which holds in sheaf models over poset spaces. In Section 4 we explain how the number systems $N$ (the natural numbers), $Q$ (the rational numbers), and $R$ (the real numbers) are standardly represented as sheaves within sheaf models of intuitionistic mathematics.

The heart of this paper is Section 5. In Section 5.1 we review the definitions of Turing degrees and Muchnik degrees, and we note that Muchnik degrees can be identified with upwardly closed sets of Turing degrees. We then define the Muchnik topos to be the sheaf model over the poset of Turing degrees. In Section 5.2 we introduce a new representation of the intuitionistic real number system, which we call the Muchnik reals. The idea is that a Muchnik real “comes into existence” only when we have enough Turing oracle power to compute it. In Section 5.3 we prove a choice principle and a bounding principle for the Muchnik reals. Thus it emerges that intuitionistic analysis based on the Muchnik reals bears some formal similarity to recursive analysis.

In a separate document [2] we offer an English translation of Muchnik’s paper [21]. This is the paper where Muchnik defined the Muchnik degrees and used them to interpret intuitionistic propositional calculus along the lines which had suggested by Kolmogorov. This paper is important for us, because our Muchnik topos interpretation may be viewed as a natural extension of Muchnik’s interpretation, from intuitionistic propositional calculus [21, Section 1] to intuitionistic mathematics as a whole.

2. Sheaves and intuitionistic higher-order logic

In this section we provide background material on sheaf theory and intuitionistic higher-order logic. Our main references are [1], [30, Chapter 14], and [9]. This section and the next two sections are mostly expository. Detailed proofs of many of these well known results are provided in [1].

2.1. Sheaves over a topological space

Definition 2.1.
Let T be a topological space. Let $Ω = {U \subseteq T ∣ U is open}$ . A sheaf over T is an ordered triple $M = (M, E_{M}, ↿_{M})$ (we omit the subscripts on E and ↿ when there is no chance of confusion), where M is a set and E and ↿ are functions, $E : M \to Ω$ and $↿ : M \times Ω \to M$ , with the following properties.
$a ↿ E (a) = a$ for all $a \in M$ .

$E (a ↿ U) = E (a) \cap U$ for all $a \in M$ and all $U \in Ω$ .

$(a ↿ U) ↿ V = a ↿ (U \cap V)$ for all $a \in M$ and all $U, V \in Ω$ .

M is partially ordered by letting $a ⩽ b$ if and only if $a = b ↿ E (a)$ .

Say that $a, b \in M$ are compatible if $a ↿ E (b) = b ↿ E (a)$ . Say that $C \subseteq M$ is compatible if the elements of C are pairwise compatible. Then, any compatible set $C \subseteq M$ has a supremum or least upper bound with respect to ⩽, denoted $sup C$ . That is, for all $d \in M$ we have $sup C ⩽ d$ if and only if $a ⩽ d$ for all $a \in C$ .
Elements of a sheaf M are called sections of M. A global section is a section a such that $E (a) = T$ . The operations E and ↿ are called extent and restriction respectively. Thus, for any $a \in M$ and $U \in Ω$ , $E (a) \in Ω$ is the extent of a and $a ↿ U \in M$ is the restriction of a to U.
Remark 2.2.
A sheaf over a topological space can also be defined in various other ways, one of which is as a special kind of presheaf, where a presheaf is a contravariant functor from Ω to the category of sets. The equivalence of these various definitions can be established easily. See [10] for more on the history and development of sheaf theory.
Example 2.3.
A good example of a sheaf over T is $\begin{matrix} C o (T, X) = {a : dom (a) \to X ∣ dom (a) \in Ω, a is continuous}, \end{matrix}$ where X is any topological space, with E and ↿ given by $E (a) = dom (a) =$ the domain4
⁴
For any function a we write $dom (a) =$ the domain of a, and $rng (a) =$ the range of a.

of a, and $a ↿ U = a ↾ U =$ the restriction of a to $U \cap dom (a) \in Ω$ .
Example 2.4.
Ω itself is a sheaf over T, with $E (U) = U$ and $U ↿ V = U \cap V$ for all $U, V \in Ω$ . Note that $Ω ≅ C o (T, {0})$ where ${0}$ is the one-point space.
Example 2.5.
Let T and Ω be as in Definition 2.1. We define $\begin{matrix} Ω 1 = {(V, U) ∣ V, U \in Ω, V \subseteq U} \end{matrix}$ with E and ↿ given by $E ((V, U)) = U$ and $(V, U) ↿ W = (V \cap W, U \cap W)$ for all $(V, U) \in Ω 1$ and all $W \in Ω$ . It can be shown that $Ω 1$ is a sheaf over T. In fact, $Ω 1 ≅ C o (T, S)$ where S is the Sierpiński space, i.e., the topological space ${0, 1}$ with open sets ∅, ${1}$ , ${0, 1}$ . For details see [1, pages 16–17].
Definition 2.6.
Let $(M, E_{M}, ↿_{M})$ and $(N, E_{N}, ↿_{N})$ be sheaves over T. We say that $(N, E_{N}, ↿_{N})$ is a subsheaf of $(M, E_{M}, ↿_{M})$ if $N \subseteq M$ and $E_{N}$ and $↿_{N}$ are inherited from M, i.e., $E_{N} (a) = E_{M} (a)$ and $a ↿_{N} U = a ↿_{M} U$ for all $a \in N$ and all $U \in Ω$ .
Example 2.7.
Let X be a topological space. A function a from a subset of T into X is said to be locally constant if for every $t \in dom (a)$ there exists an open set $V \in Ω$ such that $t \in V$ and a is constant on $V \cap dom (a)$ . Clearly locally constant functions are continuous. Let $\begin{matrix} C_{o}^{lc} (T, X) = {a \in C o (T, X) ∣ a is locally constant} . \end{matrix}$ Then $C_{o}^{lc} (T, X)$ is a subsheaf of $C o (T, X)$ . However, $\begin{matrix} C_{o}^{c} (T, X) = {a \in C o (T, X) ∣ a is constant} \end{matrix}$ is in general not a sheaf, hence not a subsheaf of $C_{o}^{lc} (T, X)$ .
Lemma 2.8.
Let M be a sheaf over T.
For all $a, b \in M$ , if $a ⩽ b$ then $E (a) \subseteq E (b)$ .

If C is a compatible subset of M, then $c = sup C$ if and only if $E (c) = ⋃_{a \in C} E (a)$ and $a ⩽ c$ for all $a \in C$ .

If ${U_{i} ∣ i \in I}$ is a family of open subsets of T, and if $c \in M$ , then ${c ↿ U_{i} ∣ i \in I}$ is a compatible subset of M and ${sup}_{i \in I} (c ↿ U_{i}) = c ↿ ⋃_{i \in I} U_{i}$ .

Every bounded subset of M is compatible and has a least upper bound.

Proof.
The result can be found (without proof) in [30, Volume II, Chapter 14, pages 740–741]. A detailed proof is in [1, pages 13–16]. □
Definition 2.9.
Let M and N be sheaves over T.
The product sheaf is $\begin{matrix} M \times N = {(a, b) ∣ a \in M, b \in N, E (a) = E (b)} \end{matrix}$ with E and ↿ given by $E ((a, b)) = E (a)$ and $(a, b) ↿ U = (a ↿ U, b ↿ U)$ .

For all $U \in Ω$ the restriction sheaf is $\begin{matrix} M ↿ U = {a ↿ U ∣ a \in M} = {a \in M ∣ E (a) \subseteq U}, \end{matrix}$ with E and ↿ inherited from M.

A sheaf morphism $M \overset{φ}{\to} N$ is a mapping $φ : M \to N$ satisfying $E (φ (a)) = E (a)$ and $φ (a ↿ U) = φ (a) ↿ U$ for all $a \in M$ and all $U \in Ω$ .

The function sheaf is $\begin{matrix} N^{M} = {(φ, U) ∣ U \in Ω, M ↿ U \overset{φ}{\to} N ↿ U} \end{matrix}$ with E and ↿ defined by $E ((φ, U)) = U$ and $(φ, U) ↿ V = (φ ↿ V, U \cap V)$ where $(φ ↿ V) (a) = φ (a) ↿ V$ for all $a \in M ↿ (U \cap V)$ and all $V \in Ω$ .

Remark 2.10.
The product sheaf, the restriction sheaf, and the function sheaf are indeed sheaves over T. A detailed proof is in [1, pages 20–28].
Definition 2.11.
For any sheaf M we define the power sheaf $P (M)$ to be the function sheaf $Ω 1^{M}$ where $Ω 1$ is as in Example 2.5.
Remark 2.12.
Another definition of the power sheaf appears in [9,30]. It can be shown that the other definition is equivalent to our Definition 2.11. For details see [1, pages 28–35].
Remark 2.13.
Given a topological space T, let $Sh (T)$ be the category whose objects are the sheaves over T and whose morphisms are the sheaf morphisms over T. The category $Sh (T)$ is the most basic examples of a topos.
2.2. The language of higher-order logic

We now describe a many-sorted language L for intuitionistic higher-order logic.

Definition 2.14.
The language L is defined as follows.
The sorts of L are generated as follows.

There is a collection of ground sorts.5
⁵
A.k.a., basic sorts or primitive sorts.

If σ and τ are sorts, then so is $σ \times τ$ , the product sort of σ and τ.

If σ and τ are sorts, then so is $σ \to τ$ , the function sort from σ to τ.

If σ is a sort, then so is $P σ$ , the power sort of σ.

The symbols of L are:
for each sort σ, an infinite supply of variables $x^{σ}, y^{σ}, \dots$ ;

for each sort σ, an existence predicate $E^{σ}$ of type $(σ)$ , an equality predicate $=^{σ}$ of type $(σ, σ)$ , and a membership predicate $\in^{σ}$ of type $(σ, P σ)$ ;

for all sorts σ and τ, a pairing operator $π^{σ, τ}$ of type $(σ, τ, σ \times τ)$ and projection operators $π_{1}^{σ, τ}$ and $π_{2}^{σ, τ}$ of types $(σ \times τ, σ)$ and $(σ \times τ, τ)$ respectively, and an application operator ${Ap}^{σ, τ}$ of type $(σ \to τ, σ, τ)$ ;

propositional connectives ¬, ∧, ∨, ⇒, ⇔;

quantifiers ∀, ∃.
When there is no danger of confusion, we may omit superscripts indicating sorts and types.

The terms of L are generated as follows.

Each variable of sort σ is a term of sort σ.

If s and t are terms of sort σ and τ respectively, and if π is of type $(σ, τ, σ \times τ)$ , then $π s t$ is a term of sort $σ \times τ$ .

If r is a term of sort $σ \times τ$ , and if $π_{1}$ , $π_{2}$ are of type $(σ \times τ, σ)$ and $(σ \times τ, τ)$ respectively, then $π_{1} r$ and $π_{2} r$ are terms of sort σ and τ respectively.

If s and t are terms of sort σ and $σ \to τ$ respectively, and if Ap is of type $(σ \to τ, σ, τ)$ , then $Ap t s$ is a term of sort τ. We usually write $t s$ instead of $Ap t s$ .

The atomic formulas of L are:

$r = s$ , where r and s are terms of sort σ and = is of type $(σ, σ)$ ;

$s \in t$ , where s and t are terms of sort σ and $P σ$ respectively, and ∈ is of type $(σ, P σ)$ ;

$E s$ , where s is a term of sort σ and E is of type $(σ)$ .

The formulas of L are generated as follows.

Each atomic formula is a formula.

If A, B are formulas then so are $\neg A$ , $A \land B$ , $A \lor B$ , $A \Rightarrow B$ , $A \Leftrightarrow B$ .

If A is a formula and x is a variable, then $\forall x A$ and $\exists x A$ are formulas.

Definition 2.15.
The complexity of a formula A is the number of occurrences of propositional connectives ¬, ∧, ∨, ⇒, ⇔ and quantifiers ∀, ∃ in A. An occurrence of a variable $x^{σ}$ in A is said to be bound in A if it is within the scope of a quantifier $\forall x^{σ}$ or $\exists x^{σ}$ in A. A variable $x^{σ}$ is said to be free in A if at least one occurrence of $x^{σ}$ in A is not bound in A. A formula A is called a sentence if no variables are free in A.
Remark 2.16.
For a more extensive discussion, see [31]. We could include additional predicates and operators in L, but they are not needed for our purpose.

2.3. Sheaf models of intuitionistic mathematics

In this subsection we explain how sheaves over topological spaces provide models of intuitionistic higher-order logic and intuitionistic mathematics.

Definition 2.17.
Let T be a topological space. Let μ be a mapping which assigns to each ground sort σ of L a sheaf $M_{σ}$ over T. We inductively extend μ to the compound sorts of L by letting $M_{σ \times τ} = M_{σ} \times M_{τ}$ (product sheaf), $M_{σ \to τ} = M_{τ}^{M_{σ}}$ (function sheaf), and $M_{P σ} = P (M_{σ})$ (power sheaf). For each sort σ of L and each section $a \in M_{σ}$ , we extend L by adding a constant symbol $a = a^{σ}$ of sort σ, which is now also a term of sort σ. The extended language is denoted $L (μ)$ . A term of $L (μ)$ is said to be closed if it contains no variables.
Definition 2.18.
To each $L (μ)$ -sentence A we assign a truth value $[[A]] \in Ω$ .
To each closed $L (μ)$ -term s of sort σ, we assign a value $[[s]] \in M_{σ}$ .

If $a \in M_{σ}$ let $[[a]] = a$ .

If s and t are closed terms of sorts σ and τ respectively, let $[[π s t]] = ([[s]] ↿ E ([[t]]), [[t]] ↿ E ([[s]]))$ .

If r is a closed term of sort $σ \times τ$ , then $[[r]] = (a, b)$ for some $(a, b) \in M_{σ} \times M_{τ}$ and we let $[[π_{1} r]] = a$ and $[[π_{2} r]] = b$ .

Suppose t is a closed term of sort $σ \to τ$ with $[[t]] = (φ, U) \in M_{τ}^{M_{σ}}$ . If s is a closed term of sort σ, let $[[Ap t s]] = [[t s]] = φ ([[s]] ↿ U)$ .

For atomic $L (μ)$ -sentences A, we define $[[A]] \in Ω$ as follows.

If r and s are closed terms of sort σ, let $\begin{matrix} [[r = s]] = ⋃ {U \in Ω ∣ U \subseteq E ([[r]]) \cap E ([[s]]), [[r]] ↿ U = [[s]] ↿ U} . \end{matrix}$

If s is a closed term of sort σ, let $[[E^{σ} s]] = [[s = s]] = E ([[s]])$ .

If s is a closed term of sort σ and t is a closed term of sort $P σ$ with $[[t]] = (φ, U) \in P (M_{σ}) = Ω 1^{M_{σ}}$ , let $[[s \in t]] = V$ where $φ ([[s]] ↿ U) = (V, E ([[s]]) \cap U)$ .

For non-atomic $L (μ)$ -sentences A, we define $[[A]] \in Ω$ by induction on the complexity of A, using the notation $S^{\circ} =$ the interior of S.

Propositional connectives: $\begin{array}{rcl} [[\neg A]] = {(T ∖ [[A]])}^{\circ}, \\ [[A \land B]] = [[A]] \cap [[B]], [[A \lor B]] = [[A]] \cup [[B]], \\ [[A \Rightarrow B]] = ([[A]] \Rightarrow [[B]]) where (U \Rightarrow V) = {((T ∖ U) \cup V)}^{\circ}, \\ [[A \Leftrightarrow B]] = [[A \Rightarrow B]] \cap [[B \Rightarrow A]] . \end{array}$

Quantifiers: $\begin{array}{rcl} [[\exists x^{σ} A (x^{σ})]] = ⋃_{a \in M_{σ}} [[E a \land A (a)]], \\ [[\forall x^{σ} A (x^{σ})]] = {(⋂_{a \in M_{σ}} [[E a \Rightarrow A (a)]])}^{\circ} . \end{array}$

Definition 2.19.
For $L (μ)$ -sentences A we write $Sh (T, μ) ⊧ A$ to mean that $[[A]] = T$ . An L-formula A is said to be valid for sheaf models if for all topological spaces T and all $μ : σ \mapsto M_{σ}$ as above, $Sh (T, μ) ⊧$ the universal closure of A. Let $IHOL$ be the formal system of intuitionistic higher-order logic as formulated in [25] and [30, Chapter 14].
Theorem 2.20.
The axioms and rules of $IHOL$ are valid for sheaf models.
Proof.
See [9, Theorem 7.3] and [30, Theorem 5.15]. □

For instance, substitution of equals is intuitionistically valid, hence provable in $IHOL$ , so we have: Theorem 2.21.
Let x be a variable of sort σ, let r and s be closed $L (μ)$ -terms of sort σ, and let $A (x)$ be an $L (μ)$ -formula with no free variables other than x. Then $Sh (T, μ) ⊧ r = s \Rightarrow (A (r) \Leftrightarrow A (s))$ , hence $[[r = s]] \cap [[A (r)]] \subseteq [[A (s)]]$ .
Proof.
For a much more detailed proof, see [1, pages 42–48]. □
Remark 2.22.
By [9,30] we know that intuitionistic mathematics is formalizable in $IHOL$ . Thus Theorem 2.20 may be viewed as saying that, for any topological space T, $Sh (T)$ is a model of intuitionistic mathematics. Such models are known as sheaf models.

3. Poset spaces and choice principles

In this section we discuss sheaf models over a special class of topological spaces, the poset spaces. We show that some special cases of the axiom of choice are valid for sheaf models over poset spaces.

3.1. Poset spaces

Definition 3.1.
A poset6
⁶
I.e., a partially ordered set.

is a non-empty set K together with a binary relation ⩽ on K which is reflexive, antisymmetric, and transitive. A set $U \subseteq K$ is said to be upwardly closed if for all $α \in U$ and $β \in K$ , $α ⩽ β$ implies $β \in U$ . The upwardly closed subsets of K are the open sets of a topology on K, the Alexandrov topology. A poset space is a poset endowed with the Alexandrov topology. The category of sheaves over a poset space K is denoted $Sh (K)$ .
Remark 3.2.
As is well known, the category $Sh (K)$ is equivalent to the category of K-sets, where a K-set is a collection of sets indexed by K together with a collection of maps between these sets that satisfy certain conditions. For details, see for instance [1, pages 52–56].
Lemma 3.3.
Let K be a poset space.
For any $α \in K$ there is a smallest open set containing α, namely $\begin{matrix} U_{α} = {β \in K ∣ α ⩽ β} . \end{matrix}$

K is locally connected, i.e., for any $α \in K$ and any neighborhood U of α, there is a connected neighborhood of α included in U.

For all families of subsets of K we have ${(⋂_{i \in I} S_{i})}^{\circ} = ⋂_{i \in I} S_{i}^{\circ}$ .

If U is an open subset of K, and if X is a $T_{1}$ space, 7
⁷
A $T_{1}$ space is a topological space in which every point is a closed set. Examples of $T_{1}$ spaces are $R$ , $N$ , $N^{N}$ , etc. All discrete spaces are $T_{1}$ spaces.

then every continuous function $f : U \to X$ is locally constant.

Proof.
This is well known and straightforward. See [1, pages 50–51]. □
Definition 3.4.
A poset K is said to be directed if for all $α, β \in K$ there exists $γ \in K$ such that $α ⩽ γ$ and $β ⩽ γ$ . A poset space is said to be directed if the underlying poset is directed.
Lemma 3.5.
Let U be an open set in a directed poset space. Let X be any set. Then, every locally constant function $f : U \to X$ is constant.
Proof.
The proof is straightforward. See for instance [1, pages 51–52]. □
3.2. Choice principles over poset spaces

In this subsection we show that sheaf models over poset spaces satisfy certain special cases of the axiom of choice.

Definition 3.6.
Let σ and τ be L-sorts. The axiom of choice for $σ \to τ$ , denoted $AC (σ, τ)$ , is the universal closure of $\begin{matrix} (\forall x \exists y A (x, y)) \Rightarrow \exists w \forall x A (x, w x), \end{matrix}$ where x, y, w are variables of sort $σ, τ, σ \to τ$ respectively, and $A (x, y)$ is any L-formula in which w does not occur.
Remark 3.7.
A model of intuitionistic higher-order logic cannot satisfy $AC (σ, τ)$ for all sorts σ, τ unless it is also a model of classical higher-order logic. This is because, as shown in [5], the full axiom of choice implies the law of the excluded middle. However, as we shall now see, models such as $Sh (T, μ)$ may satisfy $AC (σ, τ)$ for some particular choices of σ and τ.
Definition 3.8.
Let T be a topological space, and let X be a set. As in Example 2.7 let $C_{o}^{lc} (T, X)$ be the sheaf of locally constant functions from open subsets of T into X. We define $\hat{X} sh = C_{o}^{lc} (T, X)$ . Note that for each $x \in X$ there is a global section $\hat{x}$ of $\hat{X} sh$ which maps T into ${x}$ . The sheaf $\hat{X} sh$ is called a simple sheaf. See [9] and [30, page 782].
Theorem 3.9.
Let K be a poset space. If $M_{σ}$ is a simple sheaf over K, then $Sh (K, μ)$ satisfies $AC (σ, τ)$ .
Proof.
We may safely assume that $A (x, y)$ has no free variables other than x and y. Letting $U = [[\forall x \exists y A (x, y)]]$ , it will suffice to show that $U \subseteq [[\exists w \forall x A (x, w x)]]$ .

Let X be a set such that $M_{σ} = \hat{X} sh$ . For each $x \in X$ we have $\hat{x} \in \hat{X} sh$ and $E (\hat{x}) = K$ , hence $\begin{array}{rcl} U & = & {(⋂_{a \in \hat{X} sh} (E (a) \Rightarrow [[\exists y A (a, y)]]))}^{\circ} \\ \subseteq & ⋂_{x \in X} (E (\hat{x}) \Rightarrow [[\exists y A (\hat{x}, y)]]) \\ = & ⋂_{x \in X} [[\exists y A (\hat{x}, y)]] (because E (\hat{x}) = K) \\ = & ⋂_{x \in X} ⋃_{b \in M_{τ}} (E (b) \cap [[A (\hat{x}, b)]]) . \end{array}$

Fix $α \in U$ . Using the axiom of choice externally, we choose for each $x \in X$ a $b_{x} \in M_{τ}$ such that $α \in E (b_{x}) \cap [[A (\hat{x}, b_{x})]]$ . Since $E (b_{x}) \cap [[A (\hat{x}, b_{x})]]$ is open, it follows by Lemma 3.3 that $U_{α} \subseteq E (b_{x}) \cap [[A (\hat{x}, b_{x})]]$ . We shall now define a sheaf morphism from $\hat{X} sh ↿ U_{α}$ into $M_{τ}$ . Let $a \in \hat{X} sh ↿ U_{α}$ be given. For all $x, y \in X$ such that $x \neq y$ we have $a^{- 1} (x) \cap a^{- 1} (y) = \emptyset$ , hence the set ${b_{x} ↿ a^{- 1} (x) ∣ x \in X} \subseteq M_{τ}$ is compatible, hence the least upper bound $\begin{matrix} φ (a) = sup_{x \in X} (b_{x} ↿ a^{- 1} (x)) \in M_{τ} \end{matrix}$ exists. We have $E (a) \subseteq U_{α} \subseteq E (b_{x})$ , hence $E (φ (a)) = ⋃_{x \in X} E (b_{x} ↿ a^{- 1} (x)) = ⋃_{x \in X} a^{- 1} (x) = E (a)$ by Lemma 2.8. Moreover, for any open set $V \subseteq K$ we have $φ (a ↿ V) = {sup}_{x \in X} (b_{x} ↿ {(a ↿ V)}^{- 1} (x)) = {sup}_{x \in X} (b_{x} ↿ (a^{- 1} (x) \cap V)) = ({sup}_{x \in X} (b_{x} ↿ a^{- 1} (x))) ↿ V = φ (a) ↿ V$ . Thus φ preserves extent and restriction, so we have a sheaf morphism $\begin{matrix} \hat{X} sh ↿ U_{α} \overset{φ}{\to} M_{τ} ↿ U_{α}, \end{matrix}$ i.e., $(φ, U_{α}) \in M_{τ}^{\hat{X} sh}$ .

We claim that $U_{α} \cap E (a) \subseteq [[A (a, (φ, U_{α}) a)]]$ for all $a \in \hat{X} sh$ . To see this, fix $β \in U_{α} \cap E (a)$ . For some $x \in X$ we have $a (β) = x$ , hence $U_{β} \subseteq a^{- 1} (x) \subseteq E (a)$ and $\hat{x} ↿ U_{β} = a ↿ U_{β}$ , hence $U_{β} \subseteq [[\hat{x} = a]]$ . Moreover $b_{x} ↿ U_{β} = φ (a ↿ U_{α}) ↿ U_{β}$ and $U_{β} \subseteq E (b_{x})$ , hence $U_{β} \subseteq [[b_{x} = φ (a ↿ U_{α})]]$ , and clearly $U_{β} \subseteq U_{α} \cap E (a) = [[φ (a ↿ U_{α}) = (φ, U_{α}) a]]$ . Therefore, from $U_{β} \subseteq [[A (\hat{x}, b_{x})]]$ it follows by Theorem 2.21 that $U_{β} \subseteq [[A (a, (φ, U_{α}) a)]]$ , and this proves the claim.

Our claim easily implies that $\begin{array}{rcl} U_{α} & \subseteq & ⋂_{a \in \hat{X} sh} {((K ∖ E (a)) \cup [[A (a, (φ, U_{α}) a)]])}^{\circ} \\ = & [[\forall x A (x, (φ, U_{α}) x)]] . \end{array}$ But then, since $E ((φ, U_{α})) = U_{α}$ , we have $\begin{array}{rcl} U_{α} & \subseteq & E ((φ, U_{α})) \cap [[\forall x A (x, (φ, U_{α}) x)]] \\ \subseteq & ⋃_{(ψ, V) \in M_{τ}^{\hat{X} sh}} (E ((ψ, V)) \cap [[\forall x A (x, (ψ, V) x)]]) \\ = & [[\exists w \forall x A (x, w x)]] . \end{array}$ Since $α \in U$ was arbitrary, we conclude that $U \subseteq [[\exists w \forall x A (x, w x)]]$ . This completes the proof of Theorem 3.9. □
Remark 3.10.
Theorem 3.9 fails for sheaf models over arbitrary topological spaces. In particular, see [1, pages 77–79] and [30, page 788] for a proof that $AC (σ, σ)$ fails in $Sh (R, μ)$ when $M_{σ} = \hat{N} sh$ . See also Remark 4.15 below.
Remark 3.11.
One might think that Theorem 3.9 should hold whenever $M_{σ}$ is a subsheaf of a simple sheaf over K. However, the following example shows otherwise. Let $K = {- \infty} \cup {- i ∣ i \in N}$ with the natural linear ordering, $- \infty < - j < - i$ for all $i, j \in N$ with $i < j$ . Let $M_{σ} = C o (K, {0}) ↿ {- i ∣ i \in N}$ . For all $m, n \in N$ let $b_{m, n} \in C o (K, N)$ be the constant function with domain ${- i ∣ i < m}$ and value n. Let $M_{τ}$ be the subsheaf of $C o (K, N)$ consisting of all $b_{m, n}$ such that $m < n$ . Note that for each sheaf morphism $(φ, U) \in M_{σ \to τ}$ we have $U \subseteq {- i ∣ i \in N} ⫋ K$ . Let x, y, w be variables of sort $σ, τ, σ \to τ$ respectively. Now $[[\forall x \exists y (y = y)]] = ⋂_{a \in M_{σ}} ((K ∖ E (a)) \cup ⋃_{b_{m, n} \in M_{τ}} E (b_{m, n})) = K$ and $[[\exists w \forall x (w x = w x)]] = ⋃_{(φ, U) \in M_{σ \to τ}} (U \cap [[\forall x ((φ, U) x, (φ, U) x)]]) = {- i ∣ i \in N}$ . This implies that $[[\forall x \exists y (y = y)]] ⫋ [[\exists w \forall x (w x = w x)]]$ . Thus $AC (σ, τ)$ fails in $Sh (K)$ for the formula $A (x, y) \equiv (y = y)$ .

4. Sheaf representations of the number systems

Let T be a topological space. In this section we discuss the representation of the number systems $N$ , $Q$ , and $R$ within the sheaf model $Sh (T)$ .

4.1. The natural numbers

Recall from Definition 3.8 that $\hat{N} sh = C_{o}^{lc} (T, N)$ where $N$ is the set of natural numbers. In this subsection we argue that the sheaf $\hat{N} sh$ is appropriately viewed as representing the natural number system within $Sh (T)$ .

Definition 4.1.
A system is an ordered triple $(X, c, f)$ where X is a set, $c \in X$ , and $f : X \to X$ . A Peano system is a system which satisfies $\forall x (f x \neq c)$ and $\forall x \forall y (f (x) = f (y) \Rightarrow x = y)$ and $\begin{matrix} \forall Y ((Y \subseteq X \land c \in Y \land \forall x (x \in Y \Rightarrow f (x) \in Y)) \Rightarrow Y = X) . \end{matrix}$
Theorem 4.2.
The following familiar facts are intuitionistically valid.
Given a Peano system $(X, c, f)$ and a system $(X^{'}, c^{'}, f^{'})$ , there is a unique $h : X \to X^{'}$ satisfying $h (c) = c^{'}$ and $\forall x (h (f (x)) = f^{'} (h (x)))$ .

Any two Peano systems are isomorphic.

In any Peano system $(X, f, c)$ there are uniquely determined functions satisfying the primitive recursion equations, identifying c with 0 and f with the successor function S. In particular, there are uniquely determined operations + and · on X satisfying $\begin{array}{rcl} x + c = x, x + f (y) = f (x + y), \\ x \cdot c = c, x \cdot f (y) = (x \cdot y) + x \end{array}$ for all $x, y \in X$ .

Proof.
See [30, Chapter 3]. □
Remark 4.3.
We interpret Definition 4.1 and Theorem 4.2 in $Sh (T)$ by letting X be a sheaf over T, c a section of X, $f : X \to X$ a sheaf morphism, and Y a section of the power sheaf $P (X)$ . By Theorem 2.20 we know that Theorem 4.2 is valid in $Sh (T)$ . Therefore, the following theorem implies that $\hat{N} sh$ is the “correct” representation of the natural number system as a sheaf over T.
Theorem 4.4.
Let T be a topological space. Let $\hat{0} \in \hat{N} sh$ be the global section given by $\hat{0} (t) = 0$ for all $t \in T$ . Let $\hat{S} : \hat{N} sh \to \hat{N} sh$ be the sheaf morphism given by $(\hat{S} (a)) (t) = a (t) + 1$ for all $a \in \hat{N} sh$ and all $t \in E (a)$ . Then $Sh (T)$ satisfies that $(\hat{N} sh, \hat{0}, \hat{S})$ is a Peano system.
Proof.
The above theorem is derived from the discussion in [30, Volume I, Chapter 3, page 165 & Volume II, Chapter 15, page 783]. A detailed proof is in [1, pages 58–61]. □
Remark 4.5.
Similarly, the sheaves in $Sh (T)$ corresponding to $Z$ , the ring of integers, and $Q$ , the field of rational numbers, are $\hat{Z} sh$ and $\hat{Q} sh$ respectively. See also [9, Chapter III] and [30, Chapter 15].

4.2. The real numbers

In classical mathematics, the Cauchy reals (real numbers constructed as equivalence classes of Cauchy sequences of rational numbers) and the Dedekind reals (real numbers constructed as Dedekind cuts of rational numbers) are equivalent. Intuitionistically, they are not necessarily equivalent. In this subsection we discuss various sheaf models where they are and are not equivalent.

Definition 4.6.
Classically, we use $R$ to denote the space of real numbers with the usual topology. Intuitionistically, we use $R_{C}$ and $R_{D}$ to denote the Cauchy reals and the Dedekind reals respectively. In particular, given a topological space T, we use $R_{C}$ and $R_{D}$ to denote the sheaves in $Sh (T)$ which are obtained by carrying out the usual Cauchy and Dedekind constructions within $Sh (T)$ . For details see [8] and [30, Volume I, Chapter 5, and Volume II, Chapter 15, page 784].
Definition 4.7.
Fix a topological space T. Recall from Section 2.1 that $C o (T, X)$ (respectively $C_{o}^{lc} (T, X)$ ) is the sheaf of continuous (respectively locally constant) functions from open subsets of T into X. If M is any one the sheaves $R_{C}$ , $R_{D}$ , $C o (T, R)$ , or $C_{o}^{lc} (T, R)$ , there is a natural isomorphism of $\hat{Q} sh = C o (T, Q) = C_{o}^{lc} (T, Q)$ onto a subsheaf of M, corresponding to the natural embedding of $Q$ into $R$ . Here $Q$ is the space of rational numbers with the discrete topology. If $M_{1}$ and $M_{2}$ are any two of these sheaves, we say that $M_{1}$ is $Q$ -embeddable8
⁸
For example, we always have $C_{o}^{lc} (T, R) ⫅_{Q} C o (T, R)$ .

into $M_{2}$ , denoted $M_{1} ⫅_{Q} M_{2}$ , if there is an isomorphism of $M_{1}$ onto a subsheaf of $M_{2}$ which commutes with the natural embeddings of $\hat{Q} sh$ into $M_{1}$ and $M_{2}$ . There can be at most one such isomorphism, because $Q$ is dense in $R$ . We say that $M_{1}$ and $M_{2}$ are $Q$ -isomorphic, denoted $M_{1} ≅ Q M_{2}$ , if the range of this isomorphism is $M_{2}$ .
Theorem 4.8.
Let T be a topological space. Within $Sh (T)$ we have $R_{D} ≅ Q C o (T, R)$ . Moreover, if T is locally connected then $R_{C} ≅ Q C_{o}^{lc} (T, R)$ .
Proof.
See [8, pages 288–289], [9, pages 384–385], and [30, pages 784–789]. □
Corollary 4.9.
In $Sh (R)$ we have $R_{C} ≇ Q R_{D}$ .
Proof.
$R$ is locally connected, so $R_{C} ≅ Q C_{o}^{lc} (R, R)$ and $R_{D} ≅ Q C o (R, R)$ . On the other hand, there are continuous real-valued functions on $R$ which are not locally constant, e.g., the identity function on $R$ . Thus $C_{o}^{lc} (R, R) ⫋_{Q} C o (R, R)$ , and from this it follows that $C_{o}^{lc} (R, R) ≇ Q C o (R, R)$ . □
Corollary 4.10.
Let K be a poset space. In $Sh (K)$ we have $R_{C} ≅ Q R_{D} ≅ Q C_{o}^{lc} (K, R) = C o (K, R)$ . Moreover, $Sh (K, μ)$ satisfies $AC (σ, τ)$ for $M_{σ} = R_{C}$ .
Proof.
By Lemma 3.3 K is locally connected and all continuous functions from open subsets of K into $R$ are locally constant. Thus Theorem 4.8 implies that $R_{C} ≅ Q R_{D} ≅ Q C o (K, R) = C_{o}^{lc} (K, R) = \hat{R} sh$ . Theorem 3.9 tells us that $Sh (K, μ)$ satisfies $AC (σ, τ)$ for $M_{σ} = \hat{R} sh$ , but since $R_{C} ≅ Q \hat{R} sh$ we get the same conclusion for $M_{σ} = R_{C}$ . □
Corollary 4.11.
Let K be a directed poset space. In $Sh (K)$ we have $R_{C} ≅ Q R_{D} ≅ Q C_{o}^{c} (K, R) = C_{o}^{lc} (K, R) = C o (K, R)$ .
Proof.
This follows from the previous corollary plus Lemma 3.5. □
Definition 4.12.
The axiom of countable choice is the special case $M_{σ} = \hat{N} sh$ of $AC (σ, τ)$ as formulated in Definition 3.6. More formally, for any topological space T we say that $Sh (T)$ satisfies ${AC}_{0}$ if $Sh (T, μ) ⊧ AC (σ, τ)$ whenever $M_{σ} = \hat{N} sh$ .
Theorem 4.13.
Let T be a topological space. If $Sh (T)$ satisfies ${AC}_{0}$ , then $Sh (T)$ satisfies $R_{C} ≅ Q R_{D}$ .
Proof.
It is known intuitionistically that the axiom of countable choice implies that the Cauchy reals and the Dedekind reals are isomorphic over $Q$ . Therefore, by Theorem 2.20, this implication holds in $Sh (T)$ . See also [8, page 289] and [30, pages 274 and 788–789]. □
Corollary 4.14.
Let T be a locally connected topological space. If $Sh (T)$ satisfies ${AC}_{0}$ then $C o (T, R) = C_{o}^{lc} (T, R)$ .
Proof.
This is immediate from Theorems 4.8 and 4.13. □
Remark 4.15.
We noted in Remark 3.10 that ${AC}_{0}$ fails in $Sh (R)$ . Now Corollaries 4.9 and 4.14 provide another proof of this fact.
Theorem 4.16.
${AC}_{0}$ and $R_{C} ≅ Q R_{D}$ hold in $Sh (K)$ for any poset space K.
Proof.
This is immediate from Theorems 3.9 and 4.13. □
Remark 4.17.
It is well known (see [30, Volume II, Chapter 15] or [1, Proposition 4.6.6]) that $Sh (N^{N}) ⊧ {AC}_{0}$ , where $N^{N}$ is the Baire space. However, there are continuous functions from $N^{N}$ into $R$ which are not locally constant. Thus $N^{N}$ is an example of a topological space T such that in $Sh (T)$ we have $R_{C} ≅ Q R_{D} ≅ Q C o (T, R) ⫌_{Q} C_{o}^{lc} (T, R)$ and hence $R_{C} ≇ Q C_{o}^{lc} (T, R)$ .

5. The Muchnik topos and the Muchnik reals

In this section we discuss a particular sheaf model which we call the Muchnik topos. We show that the Muchnik topos provides a model of intuitionistic mathematics which is a natural extension of the well known Kolmogorov/Muchnik interpretation of intuitionistic propositional calculus via mass problems under weak reducibility, i.e., Muchnik degrees. Within the Muchnik topos we define a sheaf representation of the real number system which we call the Muchnik reals. We prove a choice principle and a bounding principle for the Muchnik reals.

5.1. The Muchnik topos

Definition 5.1.
For $f, g \in N^{N}$ we say that f is Turing reducible to g, denoted $f ⩽ T g$ , if f is computable using g as a Turing oracle. It can be shown that $⩽ T$ is transitive and reflexive on $N^{N}$ . We say that f is Turing equivalent to g, denoted $f \equiv T g$ , if $f ⩽ T g$ and $g ⩽ T f$ . Clearly $\equiv T$ is an equivalence relation on $N^{N}$ . The Turing degree of f, denoted $deg T (f)$ , is the equivalence class of f under $\equiv T$ . The set of all Turing degrees is denoted $D T$ . We partially order $D T$ by letting $deg T (f) ⩽ deg T (g)$ if and only if $f ⩽ T g$ .
Lemma 5.2.
Some well known facts about the poset $D T$ are as follows.
There is a bottom Turing degree $0 = deg T (f)$ for computable $f \in N^{N}$ .

Any two Turing degrees have a supremum, i.e., a least upper bound, given by $sup (deg T (f), deg T (g)) = deg T ((f, g))$ where $(f, g) \in N^{N}$ is given by $(f, g) (2 i) = f (i)$ and $(f, g) (2 i + 1) = g (i)$ for all $i \in N$ .

However, two incomparable Turing degrees may or may not have an infimum, i.e., a greatest lower bound, in $D T$ .

Thus $D T$ is an upper semilattice, hence a directed poset, but not a lattice.

Definition 5.3.
A mass problem is a set $P \subseteq N^{N}$ . For $P, Q \subseteq N^{N}$ we say that P is weakly reducible to Q, denoted $P ⩽ w Q$ , if for all $g \in Q$ there exists $f \in P$ such that $f ⩽ T g$ . Clearly $⩽ w$ is reflexive and transitive on the powerset of $N^{N}$ . We say that P is weakly equivalent to Q, denoted $P \equiv w Q$ , if $P ⩽ w Q$ and $Q ⩽ w P$ . Clearly $\equiv w$ is an equivalence relation on the power set of $N^{N}$ . The weak degree or Muchnik degree of a mass problem P, denoted $deg w (P)$ , is the equivalence class of P under $\equiv w$ . The set of all Muchnik degrees is denoted $D w$ . We partially order $D w$ by letting $deg w (P) ⩽ deg w (Q)$ if and only if $P ⩽ w Q$ .
Remark 5.4.
There is a natural embedding of the Turing degrees, $D T$ , into the Muchnik degrees, $D w$ , given by $deg T (f) \mapsto deg w ({f})$ . This embedding is one-to-one and order preserving, i.e., $f ⩽ T g$ if and only if ${f} ⩽ w {g}$ . Moreover, this embedding preserves the bottom Turing degree $0$ and the supremum of any two Turing degrees. However, it does not preserve the infimum of two incomparable Turing degrees, even when the infimum exists.
Definition 5.5.
A lattice is a poset such that for any two elements a and b there exists a supremum or least upper bound, $sup (a, b)$ , and an infimum or greatest lower bound, $inf (a, b)$ . A lattice is said to be complete if for every set of elements ${a_{i}}_{i \in I}$ there exists a supremum or least upper bound, ${sup}_{i \in I} a_{i}$ , and an infimum or greatest lower bound, ${inf}_{i \in I} a_{i}$ . Note that every complete lattice has a top element and a bottom element. A complete lattice is said to be completely distributive if it satisfies ${sup}_{i \in I} {inf}_{j \in J} a_{i j} = {inf}_{f : I \to J} {sup}_{i \in I} a_{i f (i)}$ and ${inf}_{i \in I} {sup}_{j \in J} a_{i j} = {sup}_{f : I \to J} {inf}_{i \in I} a_{i f (i)}$ for all ${a_{i j}}_{i \in I, j \in J}$ .
Remark 5.6.
Our reference for lattice theory is Birkhoff, second edition [3]. Our reason for preferring the second edition to the third edition is explained in [26, Remark 1.5].
Definition 5.7.
A set $U \subseteq D T$ is said to be upwardly closed if $deg T (g) \in U$ whenever $deg T (f) \in U$ for some $f ⩽ T g$ . Let $U (D T)$ be the set of upwardly closed subsets of $D T$ . We partially order $U (D T)$ by the subset relation: $U ⩽ V$ if and only if $U \subseteq V$ . Clearly $U (D T)$ is a complete and completely distributive lattice. To prove this, one uses only the fact that $D T$ is a poset.
Theorem 5.8.
The posets $D w$ and $U (D T)$ are dually isomorphic. That is, there is an order-reversing one-to-one correspondence between $D w$ and $U (D T)$ .
Proof.
Define $Ψ : U (D T) \to D w$ by letting $Ψ (U) = deg w ({f ∣ deg T (f) \in U})$ for all $U \in U (D T)$ . It is straightforward to verify that Ψ is one-to-one, onto, and order-reversing, i.e., $U \subseteq V$ if and only if $Ψ (U) ⩾ Ψ (V)$ . In proving these properties, one uses only the fact that $⩽ T$ is reflexive and transitive on $N^{N}$ . □
Corollary 5.9.
$D w$ is a complete and completely distributive lattice. The lattice operations in $D w$ are given by $\begin{array}{rcl} sup (a, b) = Ψ (Ψ^{- 1} (a) \cap Ψ^{- 1} (b)), inf (a, b) = Ψ (Ψ^{- 1} (a) \cup Ψ^{- 1} (b)), \\ sup_{i \in I} a_{i} = Ψ (⋂_{i \in I} Ψ^{- 1} (a_{i})), inf_{i \in I} a_{i} = Ψ (⋃_{i \in I} Ψ^{- 1} (a_{i})), \end{array}$ where Ψ is as in the proof of Theorem 5.8. Moreover, the top degree in $D w$ is $\infty = Ψ (\emptyset) = deg w (\emptyset)$ and the bottom degree in $D w$ is $0 = Ψ (D T) = deg w ({f ∣ f is computable})$ .
Definition 5.10.
We define the Muchnik topos to be the sheaf model $Sh (D T)$ . Here $D T$ is a poset space as usual (see Section 3.1 above), with the Alexandrov topology, where the open sets are the upward closed subsets of $D T$ .
Remark 5.11.
Our terminology “the Muchnik topos” is motivated by Theorem 5.8. Note that set Ω of truth values in $Sh (D T)$ is just $U (D T)$ which corresponds via Ψ to the Muchnik lattice $D w$ . Moreover, the propositional connectives of Section 2 correspond via Ψ to lattice operations in $D w$ . Namely, for all $L (μ)$ -sentences A and B, letting $Ψ ([[A]]) = a$ and $Ψ ([[B]]) = b$ we have $\begin{array}{rcl} Ψ ([[A \land B]]) = sup (a, b), Ψ ([[A \lor B]]) = inf (a, b), \\ Ψ ([[A \Rightarrow B]]) = imp (a, b) = inf {c ∣ sup (a, c) ⩾ b}, \\ Ψ ([[\neg A]]) = imp (a, \infty) . \end{array}$ In addition, $Sh (D T, μ) ⊧ A \Rightarrow B$ if and only if $a ⩾ b$ , i.e., $[[A]] \subseteq [[B]]$ , and $Sh (D T, μ) ⊧ B$ if and only if $b = 0$ , i.e., $[[B]] = D T$ . Thus the Muchnik topos $Sh (D T)$ provides a natural extension of Muchnik’s $D w$ interpretation of intuitionistic propositional calculus [21, Section 1] to intuitionistic higher-order logic. See also our translation of [21] in a separate document [2].
Theorem 5.12.
The Muchnik topos $Sh (D T)$ satisfies $AC (σ, τ)$ whenever $M_{σ}$ is a simple sheaf. In particular, $Sh (D T)$ satisfies $AC (σ, τ)$ whenever $M_{σ} = R_{C}$ .
Proof.
This follows from Theorem 3.9 and Corollary 4.10 since $D T$ is a poset. □
Theorem 5.13.
In the Muchnik topos $Sh (D T)$ , the Cauchy reals $R_{C}$ and the Dedekind reals $R_{D}$ are $Q$ -isomorphic to each other and to $C o (D T, R) = C_{o}^{lc} (D T, R) = C_{o}^{c} (D T, R)$ .
Proof.
This follows from Corollary 4.11 because $D T$ is a directed poset. □
5.2. The Muchnik reals

Definition 5.14.
Let $# : Q \to N$ be a standard Gödel numbering of the rational numbers. For instance, we could define $# (q)$ for $q \in Q$ by $\begin{matrix} # (q) = \{\begin{matrix} 1 & if q = 0, \\ 2 \cdot 3^{a} \cdot 5^{b} & if q = a / b where a, b \in N ∖ {0} and gcd (a, b) = 1, \\ 4 \cdot 3^{a} \cdot 5^{b} & if q = - a / b where a, b \in N ∖ {0} and gcd (a, b) = 1 . \end{matrix} \end{matrix}$ For real numbers $x \in R$ we define the Turing degree of x to be $deg T (x) = deg T (f_{x})$ where $f_{x} \in N^{N}$ is given by $f_{x} (i) = 1$ if $i = # (q)$ for some $q \in Q$ such that $q < x$ , otherwise $f_{x} (i) = 0$ , for all $i \in N$ .
Definition 5.15.
In $Sh (D T)$ , the Muchnik reals are the sections of the sheaf $\begin{matrix} R_{M} = {a \in C_{o}^{c} (D T, R) ∣ \forall d (d \in dom (a) \Rightarrow deg T (a (d)) ⩽ d)} . \end{matrix}$ For $a \in R_{M}$ such that $a \neq \emptyset$ , let $\overline{a} \in R$ be such that $rng (a) = {\overline{a}}$ , and let $\hat{a} =$ the maximal $b \in R_{M}$ such that $a ⩽ b$ , i.e., the unique $\hat{a} \in R_{M}$ such that $rng (\hat{a}) = {\overline{a}}$ and $dom (\hat{a}) =$ the Turing upward closure of ${deg T (\overline{a})}$ . For $a = \emptyset$ let $\hat{a} = \emptyset$ and let $\overline{a}$ be undefined. Note that $\emptyset \neq a ⩽ b$ implies $\overline{a} = \overline{b}$ and $\hat{a} = \hat{b}$ .
Remark 5.16.
As we know from Theorem 5.13, the Cauchy reals $R_{C}$ and the Dedekind reals $R_{D}$ are represented in $Sh (D T)$ by $C_{o}^{c} (D T, R)$ , the sheaf of constant functions from upward closed sets of Turing degrees into $R$ . However, not all such constant functions are Muchnik reals. The Muchnik reals are those $a \in C_{o}^{c} (D T, R)$ such that either $a = \emptyset$ or $dom (a) \subseteq$ the upward closure of ${deg T (\overline{a})}$ where $rng (a) = {\overline{a}}$ . Thus $R_{M}$ is a proper subsheaf of $C_{o}^{c} (D T, R)$ , so $R_{M} ⫋_{Q} R_{C} ≅ Q R_{D}$ . Informally, a Muchnik real is a real number which “comes into existence” only when we have enough Turing oracle power to compute it. We shall see that the Muchnik reals in $Sh (D T)$ behave much like the recursive reals in recursive mathematics. See especially Corollaries 5.21 and 5.22 below.
5.3. A bounding principle for the Muchnik reals

By Theorem 5.12 the Muchnik topos $Sh (D T)$ satisfies a choice principle for $R_{C}$ , the Cauchy reals. In this subsection we prove that for $R_{M}$ , the Muchnik reals, $Sh (D T)$ satisfies not only a choice principle but also a bounding principle.

Definition 5.17.

Let r, s, t be closed terms of sort σ where $M_{σ} = R_{M}$ . Then $a, b, c \in R_{M}$ where $a = [[r]]$ , $b = [[s]]$ , $c = [[t]]$ . We define $[[r ⩽ T s]] = E (a) \cap E (b)$ if $a, b \neq \emptyset$ and $\overline{a} ⩽ T \overline{b}$ , otherwise $[[r ⩽ T s]] = \emptyset$ . We define $[[r ⩽ T (s, t)]] = E (a) \cap E (b) \cap E (c)$ if $a, b, c \neq \emptyset$ and $\overline{a} ⩽ T (\overline{b}, \overline{c})$ , otherwise $[[r ⩽ T (s, t)]] = \emptyset$ . Our bounding principle $BP (σ, σ)$ for the Muchnik reals is $\begin{matrix} (\forall x \exists y A (x, y)) \Rightarrow \exists z \forall x \exists y (y ⩽ T (x, z) \land A (x, y)), \end{matrix}$ where x, y, z are variables of sort σ and $A (x, y)$ is any L-formula which does not contain z.

Remark 5.18.

Let $A (x, y)$ be a formula expressing that x is Turing reducible to y, and let $B (x, y, z)$ be a formula expressing that x is Turing reducible to $(y, z)$ . For Muchnik reals $a, b, c \in R_{M}$ it can be shown that $[[A (a, b)]] = [[a ⩽ T b]]$ and $[[B (a, b, c)]] = [[a ⩽ T (b, c)]]$ where $[[a ⩽ T b]]$ and $[[a ⩽ T (b, c)]]$ are as in Definition 5.17. These equations confirm the appropriateness of Definition 5.17.

Theorem 5.19.

The Muchnik topos $Sh (D T)$ satisfies a combined choice and bounding principle $ACBP (σ, σ)$ for the Muchnik reals, $\begin{matrix} (\forall x \exists y A (x, y)) \Rightarrow \exists w \exists z \forall x (w x ⩽ T (x, z) \land A (x, w x)), \end{matrix}$ where x, y, z are variables of sort σ, w is a variable of sort $σ \to σ$ , $A (x, y)$ is any L-formula which does not contain z or w, and $M_{σ} = R_{M}$ .

Proof.

We may safely assume that $A (x, y)$ has no free variables other than x and y. Letting $U = [[\forall x \exists y A (x, y)]]$ and $V = [[\exists w \exists z \forall x (w x ⩽ T (x, z) \land A (x, w x))]]$ , it will suffice to show that $U \subseteq V$ . Fix $c = \hat{c} \neq \emptyset$ in $R_{M}$ such that $E (c) \subseteq U$ . It will suffice to show that $E (c) \subseteq V$ .

For each $a \neq \emptyset$ in $R_{M}$ we have $deg T ((\overline{a}, \overline{c})) \in E (\hat{a}) \cap E (c) = E (\hat{a} ↿ E (c)) \subseteq E (c) \subseteq U$ , so choose $b \in R_{M}$ such that $deg T ((\overline{a}, \overline{c})) \in E (b) \cap [[A (\hat{a} ↿ E (c), b)]]$ . The choice of b depends only on $\overline{a}$ and c, but not on a. We then have $\overline{b} ⩽ T (\overline{a}, \overline{c})$ and $E (b) \supseteq E (\hat{a}) \cap E (c)$ , so by Theorem 2.21 it follows that $E (a) \cap E (c) \subseteq [[b ⩽ T (a, c)]] \cap [[A (a, b)]]$ . Moreover, since b depends only on $\overline{a}$ and c, but not on a, we have a sheaf morphism $\begin{matrix} R_{M} ↿ E (c) \overset{φ}{\to} R_{M} ↿ E (c), \end{matrix}$ where $φ (a ↿ E (c)) = b ↿ E (a) \cap E (c)$ for all $a \in R_{M}$ . Thus $(φ, E (c)) \in R_{M}^{R_{M}}$ and $[[(φ, E (c)) a]] = b ↿ E (a) \cap E (c)$ , so by Theorem 2.21 we have $E (a) \cap E (c) \subseteq [[(φ, E (c)) a ⩽ T (a, c)]] \cap [[A (a, (φ, E (c)) a)]]$ . Since this holds for all $a \in R_{M}$ , we now see that $E (c) \subseteq V$ , and the proof is complete. □

Remark 5.20.

In our proof of Theorem 5.19, one may avoid using the axiom of choice, as follows. First, given $a \neq \emptyset$ in $R_{M}$ , let $e_{a}$ be the smallest index $e \in N$ of a partial recursive functional $Φ_{e}$ such that $Φ_{e} ((\overline{a}, \overline{c})) = \overline{b}$ for some $b \in R_{M}$ such that $deg T ((\overline{a}, \overline{c})) \in E (b) \cap [[A (\hat{a} ↿ E (c), b)]]$ . Then, choose $b = \hat{b}$ .

Corollary 5.21.

$Sh (D T)$ satisfies $AC (σ, σ)$ and $BP (σ, σ)$ for $M_{σ} = R_{M}$ .

Proof.

Within the formal system $IHOL$ , $AC (σ, σ)$ and $BP (σ, σ)$ are logical consequences of $ACBP (σ, σ)$ . Therefore, the corollary follows from Theorems 5.19 and 2.20. More details may be found in [1, pages 99–106]. □

Corollary 5.22.

Let σ be a sort such that $M_{σ} = R_{M}$ . Let x and y be variables of sort σ, and let w be a variable of sort $σ \to σ$ . If $Sh (D T, μ)$ satisfies $\forall x \exists y A (x, y)$ , then $Sh (D T, μ)$ satisfies $\exists w \forall x (w x ⩽ T x \land A (x, w x))$ .

Proof.

In the first paragraph of the proof of Theorem 5.19, we now have $U = D T$ , so we can choose $c = \hat{c} \neq \emptyset$ in $R_{M}$ such that ${deg}_{T} (\overline{c}) = 0$ , i.e., $E (c) = D T$ . The rest of the proof of Theorem 5.19 shows that $V = D T$ . Moreover, for all $a \neq \emptyset$ in $R_{M}$ we have $deg T (\overline{a}, \overline{c}) = deg T (\overline{a})$ , hence $E (a) \subseteq [[(φ, D T) a ⩽ T a]] \cap [[A (a, (φ, D T) a)]]$ . Since this holds for all $a \in R_{M}$ , we now see that $V = [[\forall x ((φ, D T) x ⩽ T x \land A (x, (φ, D T) x))]]$ . This completes the proof. □

Theorem 5.23.

$Sh (D T)$ satisfies $AC (σ, τ)$ whenever $M_{σ} = R_{M}$ .

Proof.

Repeat the proof of Theorem 5.19 but skip the parts that involve $⩽ T$ . □

Remark 5.24.

Theorem 5.23 resembles Theorem 5.12. However, Theorem 5.12 applies only when $M_{σ}$ is a simple sheaf, while in Theorem 5.23 we have $M_{σ} = R_{M}$ which is not a simple sheaf. See also Remark 3.11 above.

Footnotes

Acknowledgements

Simpson’s research was partially supported by the Eberly College of Science at the Pennsylvania State University, and by Simons Foundation Collaboration Grant 276282.

References

[1]

S.S.

Basu, A model of intuitionism based on Turing degrees, PhD thesis, The Pennsylvania State University, 2013, available at: http://etda.libraries.psu.edu/paper/19078/.

[2]

S.S.

Basu and

S.G.

Simpson, Translation of Muchnik’s paper, Computability 5 (2016), 49–59.

[3]

Birkhoff, Lattice Theory, 2nd edn, American Mathematical Society Colloquium Publications, Vol. 25, American Mathematical Society, 1948, XIII + 283 pp.

[4]

Coquand, Kolmogorov’s contribution to intuitionistic logic, in: Kolmogorov’s Heritage in Mathematics,

Charpentier,

Lesne and

N.K.

Nikolski, eds, Springer, Berlin, 2007, pp. 19–40.

[5]

Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society 51(1) (1975), 175–178.

[6]

H.B.

Enderton, Computability Theory, Elsevier, 2011, XI + 174 pp.

[7]

Fernández Díez, Five observations concerning the intended meaning of the intuitionistic logical constants, Journal of Philosophical Logic 29(4) (2000), 409–424.

[8]

M.P.

Fourman and

J.M.E.

Hyland, Sheaf models for analysis, in: Applications of Sheaves,

M.P.

Fourman,

C.J.

Mulvey and

D.S.

Scott, eds, Lecture Notes in Mathematics, Vol. 753, Springer-Verlag, Berlin, 1979, pp. 280–301.

[9]

M.P.

Fourman and

D.S.

Scott, Sheaves and logic, in: Applications of Sheaves,

M.P.

Fourman,

C.J.

Mulvey and

D.S.

Scott, eds, Lecture Notes in Mathematics, Vol. 753, Springer-Verlag, Berlin, 1979, pp. 302–401.

10.

[10]

J.W.

Gray, Fragments of the history of sheaf theory, in: Applications of Sheaves,

M.P.

Fourman,

C.J.

Mulvey and

D.S.

Scott, eds, Lecture Notes in Mathematics, Vol. 753, Springer-Verlag, Berlin, 1979, pp. 1–79.

11.

[11]

P.T.

Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Vol. I, II, Oxford Logic Guides, Vol. 43, 44, Clarendon Press, 2002, XXII + 1089 + 71 pp.

12.

[12]

S.C.

Kleene, On the interpretation of intuitionistic number theory, Journal of Symbolic Logic 10 (1945), 109–124.

13.

[13]

Kolmogoroff, Zur Deutung der intuitionistischen Logik, Mathematische Zeitschrift 35(1) (1932), 58–65.

14.

[14]

A.N.

Kolmogorov, On the interpretation of intuitionistic logic (translation of Zur Deutung der intuitionistischen Logik, Mathematische Zeitschrift35(1) (1932), 58–65), in: Selected Works of A. N. Kolmogorov, Vol. I,

V.M.

Tikhomirov, ed., Mathematics and Its Applications, Soviet Series, Vol. 25, Kluwer Academic Publishers Group, Dordrecht, 1991, pp. 151–158.

15.

[15]

Kuyper, Natural factors of the Muchnik lattice capturing IPC, Annals of Pure and Applied Logic 164(10) (2013), 1025–1036.

16.

[16]

Lambek and

P.J.

Scott, Introduction to Higher-Order Categorical Logic, Cambridge Studies in Advanced Mathematics, Vol. 7, Cambridge Univ. Press, 1986, X + 293 pp.

17.

[17]

S.M.

Lane, Categories for the Working Mathematician, 2nd edn, Springer, 1998, XII + 314 pp.

18.

[18]

S.M.

Lane and

Moerdijk, Sheaves in Geometry and Logic, Universitext, Springer-Verlag, New York, 1992, XII + 627 pp.

19.

[19]

Lee and

van Oosten, Basic subtoposes of the effective topos, Annals of Pure and Applied Logic 164(9) (2013), 866–883.

20.

[20]

Y.T.

Medvedev, Degrees of difficulty of mass problems, Doklady Academii Nauk SSSR 104(4) (1955), 501–504 (in Russian).

21.

[21]

A.A.

Muchnik, On strong and weak reducibility of algorithmic problems, Sibirskii Matematicheskii Zhurnal 4(6) (1963), 1328–1341 (in Russian).

22.

[22]

RogersJr., Theory of Recursive Functions and Effective Computability, McGraw-Hill, 1967, XIX + 482 pp.

23.

[23]

Scott, Extending the topological interpretation to intuitionistic analysis, Compositio Mathematica 20 (1968), 194–210.

24.

[24]

Scott, Extending the topological interpretation to intuitionistic analysis, II, in: Intuitionism and Proof Theory,

Kino,

Myhill and

R.E.

Vesley, eds, Studies in Logic and the Foundations of Mathematics, Vol. 60, Elsevier, 1970, pp. 235–255.

25.

[25]

Scott, Identity and existence in intuitionistic logic, in: Applications of Sheaves,

M.P.

Fourman,

C.J.

Mulvey and

D.S.

Scott, eds, Lecture Notes in Mathematics, Vol. 753, Springer-Verlag, Berlin, 1979, pp. 660–696.

26.

[26]

S.G.

Simpson, Mass problems and intuitionism, Notre Dame Journal of Formal Logic 49(2) (2008), 127–136.

27.

[27]

S.G.

Simpson, Mass problems associated with effectively closed sets, Tohoku Mathematical Journal 63(4) (2011), 489–517.

28.

[28]

Sorbi and

S.A.

Terwijn, Intuitionistic logic and Muchnik degrees, Algebra Universalis 67(2) (2012), 175–188.

29.

[29]

A.S.

Troelstra, History of constructivism in the twentieth century, in: Set Theory, Arithmetic, and Foundations of Mathematics: Theorems, Philosophies, Lecture Notes in Logic, Vol. 36, Association for Symbolic Logic, La Jolla, California, 2011, pp. 150–179.

30.

[30]

A.S.

Troelstra and

van Dalen, Constructivism in Mathematics, an Introduction, Studies in Logic and the Foundations of Mathematics, North-Holland, 1988, Vol. I, No. 121, XX + 342 + XIV pp; Vol. II, No. 123, XVIII + 536 + LII pp.

31.

[31]

van Dalen, Logic and Structure, 4th edn, Universitext, Springer, 2008, X + 263 pp.

32.

[32]

van Oosten, Realizability: A historical essay, Mathematical Structures in Computer Science 12(3) (2002), 239–263.

33.

[33]

van Oosten, Realizability: An Introduction to Its Categorical Side, Studies in Logic and the Foundations of Mathematics, Vol. 152, Elsevier, 2008, XII + 310 pp.

Mass problems and intuitionistic higher-order logic

Abstract

Keywords

1. Introduction

1.1. Intuitionism and Kolmogorov’s calculus of problems

1 On the contrary, logic is an application or part of mathematics (according to Brouwer).

1.3. Recursive mathematics and degrees of unsolvability

1.3.1. Recursive mathematics

1.3.2. Unsolvable problems and Turing degrees

1.3.3. Mass problems and Muchnik degrees

3 See also our English translation [2] of Muchnik’s paper [21].

1.5. Outline of this paper

2. Sheaves and intuitionistic higher-order logic

2.1. Sheaves over a topological space

3.1. Poset spaces

4.1. The natural numbers

5.1. The Muchnik topos

Footnotes

Acknowledgements

References

¹
On the contrary, logic is an application or part of mathematics (according to Brouwer).

³
See also our English translation [2] of Muchnik’s paper [21].