Mass problems and intuitionism

Stephen G. Simpson^{∗} Department of Mathematics Pennsylvania State University http://www.math.psu.edu/simpson/ simpson@math.psu.edu

First draft: July 25, 2007 This draft: April 28, 2008

Notre Dame Journal of Formal Logic, 49, 2008, 127–136

Abstract

Let P_{w} be the lattice of Muchnik degrees of nonempty Π_{1}^{0} subsets of 2^{ω}. The lattice P_{w} has been studied extensively in previous publications. In this note we prove that the lattice P_{w} is not Brouwerian.

1 Introduction

Definition 1. Let ω denote the set of natural numbers, ω = {0, 1, 2, …}. Let ω^{ω} denote the Baire space, ω^{ω} = {f | f : ω → ω}. Following Medvedev [27] and Rogers [32, §13.7] we define a mass problem to be an arbitrary subset of ω^{ω}. For mass problems P and Q we say that P is Medvedev reducible or strongly reducible to Q, abbreviated P ≤_{s} Q, if there exists a partial recursive functional Ψ such that Ψ(g) ∈ P for all g ∈ Q. We say that P is Muchnik reducible or weakly reducible to Q, abbreviated P ≤_{w} Q, if for all g ∈ Q there exists f ∈ P such that f is Turing reducible to g. Clearly Medvedev reducibility implies Muchnik reducibility, but the converse does not hold.

Definition 2. A Medvedev degree or degree of difficulty or strong degree is an equivalence class of mass problems under mutual Medvedev reducibility. A Muchnik degree or weak degree is an equivalence class of mass problems under mutual Muchnik reducibility. We write deg_{s}(P) = the Medvedev degree of P. We write deg_{w}(P) = the Muchnik degree of P. Let D_{s} be the set of Medvedev degrees, partially ordered by Medvedev reducibility. There is a natural embedding of the Turing degrees into D_{s} given by deg_{T} (f) ↦ deg_{s}({f}). Let D_{w} be the set of Muchnik degrees, partially ordered by Muchnik reducibility. There is a natural embedding of the Turing degrees into D_{w} given by deg_{T} (f) ↦ deg_{w}({f}). Here {f} is the singleton set whose only element is f.

∗The author thanks Sebastiaan Terwijn for helpful correspondence. The author’s research was partially supported by the United States National Science Foundation, grants DMS-0600823 and DMS-0652637, and by the Cada and Susan Grove Mathematics Enhancement Endowment at the Pennsylvania State University.

Definition 3. Let L be a lattice. For a, b ∈ L we define a ⇒ b to be the unique minimum x ∈ L such that sup(a, x) ≥ b. Note that a ⇒ b may or may not exist in L. Following Birkhoff [8, 9] (first two editions) and McKinsey/Tarski [25] we say that L is Brouwerian if a ⇒ b exists in L for all a, b ∈ L and L has a top element. It is known (see Birkhoff [9, §IX.12] [10, §II.11] or McKinsey/Tarski [25] or Rasiowa/Sikorski [31, §I.12]) that if L is Brouwerian then L is distributive and has a bottom element and for all a ≤ b in L the sublattice

{x ∈ L | a ≤ x ≤ b}

is again Brouwerian.

Remark 1. Given a Brouwerian lattice L, we may view L as a model of firstorder intuitionistic propositional calculus. Namely, for a, b ∈ L we define a∧b = sup(a, b), a ∨ b = inf(a, b), a ⇒ b as above, and ¬ a = (a ⇒ 1) where 1 is the top element of L. We may also define a ⊢ b if and only if a ≥ b in L. There is a completeness theorem (see Tarski [52] or McKinsey/Tarski [24, 25, 26] or Rasiowa/Sikorski [31, §IX.3] or Rasiowa [30, §XI.8]) saying that a first-order propositional formula is intuitionistically provable if and only if it evaluates identically to the bottom element in all Brouwerian lattices.

Remark 2. Brouwerian lattices have also been studied under other names and with other notation and terminology. A pseudo-Boolean algebra is a lattice L such that the dual of L is Brouwerian; see Rasiowa/Sikorski [31] and Rasiowa [30]. Pseudo-Boolean algebras are also known as Heyting algebras; see Balbes/Dwinger [2, Chapter IX], Fourman/Scott [18], and Grätzer [19]. Brouwerian lattices are also known as Brouwer algebras; see Sorbi [48, 49], Sorbi/Terwijn [51], and Terwijn [53, 54, 55, 56, 57]. Remarkably, the so-called Brouwerian lattices of Birkhoff [10] (third edition) are dual to those of Birkhoff [8, 9] (first two editions). We adhere to the terminology of Birkhoff [8, 9].

Remark 3. It is known that D_{s} and D_{w} are Brouwerian lattices. There is a natural homomorphism of D_{s} onto D_{w} given by deg_{s}(P) ↦ deg_{w}(P). This homomorphism preserves the binary lattice operations sup and inf and the top and bottom elements, but it does not preserve the binary if-then operation ⇒.

Remark 4. The relationship between mass problems and intuitionism has a considerable history. Indeed, it seems fair to say that the entire subject of mass problems originated from intuitionistic considerations. The impetus came from Kolmogorov 1932 [22, 23] who informally proposed to view Heyting’s intuitionistic propositional calculus [20] as a “calculus of problems” (“Aufgabenrechnung”). This idea amounts to what is now known as the BHK or Brouwer/Heyting/Kolmogorov interpretation of the intuitionistic propositional connectives; see Troelstra/van Dalen [59, §§1.3.1 and 1.5.3]. Elaborating Kolmogorov’s idea, Medvedev 1955 [27] introduced D_{s} and noted that D_{s} is a Brouwerian lattice. Later Muchnik 1963 [28] introduced D_{w} and noted that D_{w} is a Brouwerian lattice. Some further papers in this line are Skvortsova [47], Sorbi [48, 49, 50], Sorbi/Terwijn [51], and Terwijn [54, 53, 55, 56, 57].

Definition 4. Let 2^{ω} denote the Cantor space, 2^{ω} = {f | f : ω → {0, 1}}. Following Simpson [40] let P_{s} be the sublattice of D_{s} consisting of the Medvedev degrees of nonempty Π_{1}^{0} subsets of 2^{ω}, and let P_{w} be the sublattice of D_{w} consisting of the Muchnik degrees of nonempty Π_{1}^{0} subsets of 2^{ω}.

Remark 5. The lattices P_{s} and P_{w} are mathematically rich and have been studied extensively. See Alfeld [1], Binns [3, 4, 5, 6], Binns/Simpson [7], Cenzer/Hinman [11], Cole/Simpson [13], Kjos-Hanssen/Simpson [21], Simpson [34, 35, 37, 38, 39, 40, 41, 42, 43, 45, 44], Simpson/Slaman [46], and Terwijn [54]. It is known that P_{w} contains not only the recursively enumerable Turing degrees [42] but also many specific, natural Muchnik degrees which arise from foundationally interesting topics. Among these foundationally interesting topics are algorithmic randomness [40, 42], reverse mathematics [36, 40, 41, 43], almost everywhere domination [43], hyperarithmeticity [13], diagonal nonrecursiveness [40, 42], subrecursive hierarchies [21, 40], resource-bounded computational complexity [21, 40], and Kolmogorov complexity [21]. Recently Simpson [44] has applied P_{s} and P_{w} to prove a new theorem in symbolic dynamics.

Remark 6. It is known that P_{s} and P_{w} are distributive lattices with top and bottom elements. Moreover, the natural lattice homomorphism of D_{s} onto D_{w} restricts to a natural lattice homomorphism of P_{s} onto P_{w} preserving top and bottom elements.

Remark 7. In view of Remarks 3, 4, 5 and 6, it is natural to ask whether P_{s} and P_{w} are Brouwerian lattices. The purpose of this note is to show that P_{w} is not a Brouwerian lattice. Letting 1 denote the top element of P_{w}, we shall produce a family of Muchnik degrees p ∈ P_{w} such that p ⇒ 1 does not exist in P_{w}. In other words, ¬ p does not exist in P_{w}.

Remark 8. It remains open whether P_{s} is a Brouwerian lattice. Terwijn [54] has shown that the dual of P_{s} is not a Brouwerian lattice. It remains open whether the dual of P_{w} is a Brouwerian lattice.

2 Proof that P_{w} is not Brouwerian

In this section we prove that the lattice P_{w} is not Brouwerian.

Definition 5. For f, g ∈ ω^{ω} we write f ≤_{T} g to mean that f is Turing reducible to g, i.e., f is computable relative to the Turing oracle g. We write g′ = the Turing jump of g. In particular 0′ = the halting problem = the Turing jump of 0. We use standard recursion-theoretic notation from Rogers [32]. We say that f is majorized by g if f(n) < g(n) for all n.

We begin with four well known lemmas.

Lemma 1. Given f ≤_{T} 0′ we can find g ≡_{T} f such that {g} is Π_{1}^{0}.

Proof. Since f ≤_{T} 0′, it follows by Post’s Theorem (see for instance [32, §14.5, Theorem VIII]) that f is Δ_{2}^{0}. From this it follows that the singleton set {f} is Π_{2}^{0}. Let R ⊆ ω^{ω} × ω × ω be a recursive predicate such that our f is the unique f ∈ ω^{ω} such that ∀m ∃n R(f, m, n) holds. Let g = f ⊕ h where h ∈ ω^{ω} is defined by h(m) = the least n such that R(f, m, n) holds. It is easy to verify that g ≡_{T} f and {g} is Π_{1}^{0}. □

Lemma 2. If {f} is Π_{1}^{0} and f is nonrecursive, then f is not majorized by any recursive function.

Proof. This lemma is equivalent to, for instance, [40, Theorem 4.15]. □

Lemma 3. For all nonempty Π_{1}^{0} sets Q ⊆ 2^{ω} we have Q ≤_{w} {0′}.

Proof. This lemma is a restatement of the well known Kleene Basis Theorem. Namely, every nonempty Π_{1}^{0} subset of 2^{ω} contains an element which is ≤_{T} 0′. See for instance the proof of [42, Lemma 5.3]. □

Lemma 4. Let Q ⊆ 2^{ω} be nonempty Π_{1}^{0} such that no element of Q is recursive. Then we can find g ∈ ω^{ω} such that 0 <_{T} g <_{T} 0′ and Q ≰_{w} {g}.

Proof. By Lemma 3 it suffices to find g ∈ ω^{ω} such that 0 <_{T} g ≤_{T} 0′ and Q ≰_{w} {g}. To construct g we may proceed as in the proof of Lemma 5 below. The construction is easier than in Lemma 5, because we can ignore f. □

Lemma 5. Let Q ⊆ 2^{ω} be nonempty Π_{1}^{0}. Let f be such that 0 <_{T} f <_{T} 0′ and Q ≰_{w} {f}. Then we can find g ∈ ω^{ω} such that 0 <_{T} g <_{T} 0′ and Q ≰_{w} {g} and f ⊕ g ≡_{T} 0′.

Proof. We adapt the technique of Posner/Robinson [29].

Let U ⊆ ω^{<ω} be a recursive tree such that Q = {paths through U}. By Lemmas 1 and 2 we may safely assume that f is not majorized by any recursive function.

For integers e ∈ ω and strings σ ∈ ω^{<ω} we write

Φ_{e}(σ) = ⟨φ_{e,|σ|}^{(1),σ}(i) | i < j⟩

where j = the least i such that either φ_{e,|σ|}^{(1),σ}(i) ↑ or i ≥ |σ|. Note that the mapping Φ_{e} : ω^{<ω} → ω^{<ω} is recursive and monotonic, i.e., σ ⊆ τ implies Φ_{e}(σ) ⊆ Φ_{e}(τ). Moreover, for all g, h ∈ ω^{ω} we have g ≥_{T} h if and only if ∃e (Φ_{e}(g) = h). Here we are writing

Φ_{e}(g) = ⋃_{n=0}^{∞} Φ_{e}(g ↾ n) .

In order to prove Lemma 5, we shall inductively define an increasing sequence of strings τ_{e} ∈ ω^{<ω}, e = 0, 1, 2, . . .. We shall then let g = ⋃_{e=0}^{∞} τ_{e}. In presenting the construction, we shall identify strings with their Gödel numbers.

Stage 0. Let τ_{0} = ⟨⟩ = the empty string.

Stage e + 1. Assume that τ_{e} has been defined. The definition of τ_{e+1} will be given in a finite number of substages.

Substage 0. Let σ_{e,0} = τ_{e}.

Substage i + 1. Assume that σ_{e,i} has been defined. Let n_{e,i} = the least n such that either

(1) ∃σ < f(n) [ σ_{e,i}^{⌢}⟨n⟩ ⊆ σ and Φ_{e}(σ_{e,i}) ⊂ Φ_{e}(σ) ∈ U ]

or

(2) ¬ ∃σ [ σ_{e,i}^{⌢}⟨n⟩ ⊆ σ and Φ_{e}(σ_{e,i}) ⊂ Φ_{e}(σ) ∈ U ] .

Note that n_{e,i} exists, because otherwise f(n) would be majorized by the recursive function l_{e,i}(n) = least σ such that σ_{e,i}^{⌢}⟨n⟩ ⊆ σ and Φ_{e}(σ_{e,i}) ⊂ Φ_{e}(σ) ∈ U. If (1) holds with n = n_{e,i} let σ_{e,i+1} = l_{e,i}(n_{e,i}). If (2) holds with n = n_{e,i} let τ_{e+1} = σ_{e,i}^{⌢}⟨n_{e,i}, 0′(e)⟩. This completes our description of the construction.

We claim that, within each stage e + 1, (2) holds for some i. Otherwise, we would have infinite increasing sequences of strings

σ_{e,0} ⊂ σ_{e,1} ⊂ ⋯ ⊂ σ_{e,i} ⊂ σ_{e,i+1} ⊂ ⋯

and

Φ_{e}(σ_{e,0}) ⊂ Φ_{e}(σ_{e,1}) ⊂ ⋯ ⊂ Φ_{e}(σ_{e,i}) ⊂ Φ(σ_{e,i+1}) ⊂ ⋯

with Φ_{e}(σ_{e,i}) ∈ U for all i. Moreover, these sequences would be recursive relative to f, namely σ_{e,i+1} = l_{e,i}(n_{e,i}) where n_{e,i} = least n such that (1) holds. Thus, letting h = ⋃_{i=0}^{∞} Φ_{e}(σ_{e,i}), we would have h ∈ Q and h ≤_{T} f. Thus Q ≤_{w} {f}, a contradiction. This proves our claim.

From the previous claim it follows that τ_{e} is defined for all e = 0, 1, 2, . . .. By construction, the sequence ⟨τ_{0}, τ_{1}, …, τ_{e}, τ_{e+1}, …⟩, is recursive relative to 0′. Moreover, 0′ is recursive relative to ⟨τ_{0}, τ_{1}, …, τ_{e}, τ_{e+1}, …⟩, because for all e we have 0′(e) = τ_{e+1}(|τ_{e+1}| − 1).

Finally let g = ⋃_{e=0}^{∞} τ_{e}. Clearly g ≤_{T} 0′.

We claim that the sequence ⟨τ_{0}, τ_{1}, …, τ_{e}, τ_{e+1}, …⟩ is ≤_{T} f ⊕ g. Namely, given τ_{e}, we may use f and g as oracles to compute τ_{e+1} as follows. We begin with σ_{e,0} = τ_{e}. Given σ_{e,i} we use the oracle g to compute n_{e,i} = g(|σ_{e,i}|). Then, using the oracle f, we ask whether there exists σ < f(n_{e,i}) such that σ_{e,i}^{⌢}⟨n_{e,i}⟩ ⊆ σ and Φ_{e}(σ_{e,i}) ⊂ Φ_{e}(σ) ∈ U. If so, we compute σ_{e,i+1} = the least such σ. If not, we use the oracle g to compute τ_{e+1} = g ↾ |σ_{e,i}| + 2. This proves our claim.

From the previous claim it follows that 0′ ≤_{T} f ⊕ g. Hence 0′ ≡_{T} f ⊕ g. We claim that Q ≰_{w} {g}. To see this, let e be such that Φ_{e}(g) = ⋃_{e=0}^{∞} Φ_{e}(τ_{e})

is a total function. Consider what happened at stage e + 1 of the construction. Consider the least i such that (2) holds, i.e., τ_{e+1} = σ_{e,i}^{⌢}⟨n_{e,i}, 0′(e)⟩. Since (2) holds, there does not exist σ such that σ_{e,i}^{⌢}⟨n_{e,i}⟩ ⊆ σ and Φ_{e}(σ_{e,i}) ⊂ Φ_{e}(σ) ∈ U. In particular, letting τ be an initial segment of g such that σ_{e,i}^{⌢}⟨n_{e,i}⟩ ⊆ τ and Φ_{e}(σ_{e,i}) ⊂ Φ_{e}(τ), we have Φ_{e}(τ) ∉ U. Hence Φ_{e}(g) ∉ Q. This proves our claim.

From the two previous claims, it follows that 0 <_{T} g <_{T} 0′. The proof of Lemma 5 is now finished. □

Remark 9. By a similar argument we can prove the following. Let S ⊆ ω^{ω} be Σ_{3}^{0}. Let f ∈ ω^{ω} be of hyperimmune Turing degree such that S ≰_{w} {f}. Let h ∈ ω^{ω} be such that f ⊕ 0′ ≤_{T} h. Then we can find g ∈ ω^{ω} such that 0 <_{T} g <_{T} h and S ≰_{w} {g} and f ⊕ g ≡_{T} g′ ≡_{T} g ⊕ 0′ ≡_{T} h.

Lemma 6. Let P ⊆ 2^{ω} be nonempty Π_{1}^{0}. Let S ⊆ ω^{ω} be Σ_{3}^{0}. Then

deg_{w}(P ∪ S) ∈ P_{w} .

Proof. This is Simpson’s Embedding Lemma. See [42, Lemma 3.3] or [45]. □

We are now ready to prove our main result.

Theorem 1. P_{w} is not Brouwerian.

Proof. Let PA be the set of completions of Peano Arithmetic. Recall from Simpson [40] that deg_{w}(PA) = 1 = the top element of P_{w}. By Lemma 4 let f be such that 0 <_{T} f <_{T} 0′ and PA ≰_{w} {f}. Let

p = deg_{w}(PA ∪ {f})

and note that p < 1. By Lemmas 1 and 6 we have p ∈ P_{w}.

It is well known (see for instance [40, Remark 3.9]) that D_{w} is a complete lattice. This means that for all A ⊆ D_{w} the least upper bound sup(A) and the greatest lower bound inf(A) exist in D_{w}. Therefore, within D_{w}, let

q = inf({x ∈ P_{w} | sup(p, x) = 1})

and note that sup(p, q) = 1 in D_{w}. In other words, q ≥ (p ⇒ 1) in D_{w}.

We claim that q ∉ P_{w}. Otherwise, let q = deg_{w}(Q) where Q ⊆ 2^{ω} is nonempty Π_{1}^{0}. Since sup(p, q) = 1, we have PA ≤_{w} {f ⊕ h} for all h ∈ Q. Since PA ≰_{w} {f}, it follows that Q ≰_{w} {f}. By Lemma 5 let g be such that 0 <_{T} g <_{T} 0′ and Q ≰_{w} {g} and f ⊕ g ≡_{T} 0′. Let

q_{0} = deg_{w}(Q ∪ {g})

and note that q_{0} < q. By Lemmas 1 and 6 we have q_{0} ∈ P_{w}. By Lemma 3 we have PA ≤_{w} {0′} ≡_{w} {f ⊕ g}, hence sup(p, q_{0}) = 1 contradicting the definition of q. This proves our claim.

Because q ∉ P_{w} it follows that p ⇒ 1 does not exist in P_{w}. Thus P_{w} is not Brouwerian. □

Remark 10. The same proof shows that for all q > 0 in P_{w} we can find p < q in P_{w} such that p ⇒ q does not exist in P_{w}. On the other hand, we know at least a few nontrivial instances where p ⇒ q exists in P_{w}. For example, letting r be the Muchnik degree of the set of 1-random reals, Theorem 8.12 of Simpson [40] tells us that r < 1 in P_{w} and r ⇒ 1 exists in P_{w}. In fact, r ⇒ 1 in P_{w} is equal to r ⇒ 1 in D_{w}, which is equal to 1. We do not know any instances of p, q ∈ P_{w} where p ⇒ q exists in P_{w} and both p and p ⇒ q are < q in P_{w}.

References

[1] Christopher Alfeld. Non-branching degrees in the Medvedev lattice of Π_{1}^{0} classes. Journal of Symbolic Logic, 72:81–97, 2007.

[2] Raymond Balbes and Philip Dwinger. Distributive Lattices. University of Missouri Press, 1974. XIII + 294 pages.

[3] Stephen Binns. The Medvedev and Muchnik Lattices of Π_{1}^{0} Classes. PhD thesis, Pennsylvania State University, August 2003. VII + 80 pages.

[4] Stephen Binns. A splitting theorem for the Medvedev and Muchnik lattices. Mathematical Logic Quarterly, 49:327–335, 2003.

[5] Stephen Binns. Small Π_{1}^{0} classes. Archive for Mathematical Logic, 45:393– 410, 2006.

[6] Stephen Binns. Hyperimmunity in 2^{ℕ}. Notre Dame Journal of Formal Logic, 48:293–316, 2007.

[7] Stephen Binns and Stephen G. Simpson. Embeddings into the Medvedev and Muchnik lattices of Π_{1}^{0} classes. Archive for Mathematical Logic, 43:399– 414, 2004.

[8] Garrett Birkhoff. Lattice Theory. American Mathematical Society, 1940. V + 155 pages.

[9] Garrett Birkhoff. Lattice Theory. Number 25 in Colloquium Publications. American Mathematical Society, revised edition, 1948. XIII + 283 pages.

[10] Garrett Birkhoff. Lattice Theory. Number 25 in Colloquium Publications. American Mathematical Society, third edition, 1967. VI + 418 pages.

[11] Douglas Cenzer and Peter G. Hinman. Density of the Medvedev lattice of Π_{1}^{0} classes. Archive for Mathematical Logic, 42:583–600, 2003.

[12] C.-T. Chong, Q. Feng, T. A. Slaman, W. H. Woodin, and Y. Yang, editors. Computational Prospects of Infinity: Proceedings of the Logic Workshop at the Institute for Mathematical Sciences, June 20 – August 15, 2005. Number 15 in Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore. World Scientific, 2008.

[13] Joshua A. Cole and Stephen G. Simpson. Mass problems and hyperarithmeticity. Journal of Mathematical Logic, 2008. Preprint, 28 November 2008, 20 pages, accepted for publication 17 April 2008.

[14] COMP-THY e-mail list. http://listserv.nd.edu/archives/comp-thy.html, September 1995 to the present.

[15] S. B. Cooper, T. A. Slaman, and S. S. Wainer, editors. Computability, Enumerability, Unsolvability: Directions in Recursion Theory. Number 224 in London Mathematical Society Lecture Note Series. Cambridge University Press, 1996. VII + 347 pages.

[16] FOM e-mail list. http://www.cs.nyu.edu/mailman/listinfo/fom/. September 1997 to the present.

[17] M. P. Fourman, C. J. Mulvey, and D. S. Scott, editors. Applications of Sheaves, Proceedings, Durham, 1977. Number 753 in Lecture Notes in Mathematics. Springer-Verlag, 1979. XIV + 779 pages.

[18] Michael P. Fourman and Dana S. Scott. Sheaves and logic. In [17], pages 302–401, 1979.

[19] George A. Grätzer. General Lattice Theory. Birkhäuser Verlag, second edition, 1998. XIX + 663 pages.

[20] Arend Heyting. Die formalen Regeln des intuitionistischen Aussagenkalküls. Sitzungsberichte der Preußischen Akademie der Wißenschaften, Physicalisch-mathematische Klasse, pages 42–56, 1930.

[21] Bjørn Kjos-Hanssen and Stephen G. Simpson. Mass problems and Kolmogorov complexity. 4 October 2006. Preprint, in preparation.

[22] A. Kolmogoroff. Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35:58–65, 1932.

[23] Andrei N. Kolmogorov. On the interpretation of intuitionistic logic. In [58], pages 151–158 and 451–466, 1991. Translation of [22] with commentary and additional references.

[24] J. C. C. McKinsey and Alfred Tarski. The algebra of topology. Annals of Mathematics, 45:141–191, 1944.

[25] J. C. C. McKinsey and Alfred Tarski. On closed elements in closure algebras. Annals of Mathematics, 47:122–162, 1946.

[26] J. C. C. McKinsey and Alfred Tarski. Some theorems about the sentential calculi of Lewis and Heyting. Journal of Symbolic Logic, 13:1–15, 1948.

[27] Yuri T. Medvedev. Degrees of difficulty of mass problems. Doklady Akademii Nauk SSSR, n.s., 104:501–504, 1955. In Russian.

[28] Albert A. Muchnik. On strong and weak reducibilities of algorithmic problems. Sibirskii Matematicheskii Zhurnal, 4:1328–1341, 1963. In Russian.

[29] David B. Posner and Robert W. Robinson. Degrees joining to 0′. Journal of Symbolic Logic, 46:714–722, 1981.

[30] Helena Rasiowa. An Algebraic Approach to Non-Classical Logics. Number 78 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1974. XV + 403 pages.

[31] Helena Rasiowa and Roman Sikorski. The Mathematics of Metamathematics. Number 41 in Polska Akademia Nauk, Monografie Matematyczne. Państwowe Wydawnictwo Naukowe, 1963. 519 pages.

[32] Hartley Rogers, Jr. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967. XIX + 482 pages.

[33] S. G. Simpson, editor. Reverse Mathematics 2001. Number 21 in Lecture Notes in Logic. Association for Symbolic Logic, 2005. X + 401 pages.

[34] Stephen G. Simpson. FOM: natural r.e. degrees; Pi01 classes. FOM e-mail list [16], 13 August 1999.

[35] Stephen G. Simpson. FOM: priority arguments; Kleene-r.e. degrees; Pi01 classes. FOM e-mail list [16], 16 August 1999.

[36] Stephen G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, 1999. XIV + 445 pages.

[37] Stephen G. Simpson. Medvedev degrees of nonempty Pi^0_1 subsets of 2^omega. COMP-THY e-mail list [14], 9 June 2000.

[38] Stephen G. Simpson. Mass problems. 24 May 2004. Preprint, 24 pages, submitted for publication.

[39] Stephen G. Simpson. FOM: natural r.e. degrees. FOM e-mail list [16], 27 February 2005.

[40] Stephen G. Simpson. Mass problems and randomness. Bulletin of Symbolic Logic, 11:1–27, 2005.

[41] Stephen G. Simpson. Π_{1}^{0} sets and models of WKL_{0}. In [33], pages 352–378, 2005.

[42] Stephen G. Simpson. An extension of the recursively enumerable Turing degrees. Journal of the London Mathematical Society, 75:287–297, 2007.

[43] Stephen G. Simpson. Mass problems and almost everywhere domination. Mathematical Logic Quarterly, 53:483–492, 2007.

[44] Stephen G. Simpson. Medvedev degrees of 2-dimensional subshifts of finite type. Ergodic Theory and Dynamical Systems, 2008. Preprint, 8 pages, 1 May 2007, accepted for publication.

[45] Stephen G. Simpson. Some fundamental issues concerning degrees of unsolvability. In [12], pages 313–332, 2008.

[46] Stephen G. Simpson and Theodore A. Slaman. Medvedev degrees of Π_{1}^{0} subsets of 2^{ω}. July 2001. Preprint, 4 pages, in preparation, to appear.

[47] Elena Z. Skvortsova. A faithful interpretation of the intuitionistic propositional calculus by means of an initial segment of the Medvedev lattice. Sibirskii Matematicheskii Zhurnal, 29:171–178, 1988. In Russian.

[48] Andrea Sorbi. Some remarks on the algebraic structure of the Medvedev lattice. Journal of Symbolic Logic, 55:831–853, 1990.

[49] Andrea Sorbi. Embedding Brouwer algebras in the Medvedev lattice. Notre Dame Journal of Formal Logic, 32:266–275, 1991.

[50] Andrea Sorbi. The Medvedev lattice of degrees of difficulty. In [15], pages 289–312, 1996.

[51] Andrea Sorbi and Sebastiaan A. Terwijn. Intermediate logics and factors of the Medvedev lattice. Annals of Pure and Applied Logic, 2008. Preprint, 22 pages, 20 June 2006, to appear.

[52] Alfred Tarski. Der Aussagenkalkül und die Topologie. Fundamenta Mathematicae, 31:103–134, 1938.

[53] Sebastiaan A. Terwijn. Constructive logic and the Medvedev lattice. Notre Dame Journal of Formal Logic, 47:73–82, 2006.

[54] Sebastiaan A. Terwijn. The Medvedev lattice of computably closed sets. Archive for Mathematical Logic, 45:179–190, 2006.

[55] Sebastiaan A. Terwijn. Constructive Logic and Computational Lattices. Habilitationsschrift, Universität Wien, 2007. VI + 110 pages.

[56] Sebastiaan A. Terwijn. Kripke models, distributive lattices, and Medvedev degrees. Studia Logica, 85:327–340, 2007.

[57] Sebastiaan A. Terwijn. On the structure of the Medvedev lattice. Journal of Symbolic Logic, 73:543–558, 2008.

[58] V. M. Tikhomirov, editor. Selected Works of A. N. Kolmogorov, Volume I, Mathematics and Mechanics. Mathematics and its Applications, Soviet Series. Kluwer Academic Publishers, 1991. XIX + 551 pages.

[59] Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics, an Introduction. Studies in Logic and the Foundations of Mathematics. North-Holland, 1988. Volume I, XX + 342 + XIV pages.