Mass problems and intuitionism
Stephen G. Simpson^{1}
Department of Mathematics
First draft: July 25, 2007
This draft: April 28, 2008
Notre Dame Journal of Formal Logic, 49, 2008, 127136
Pennsylvania State University
Abstract:
Let
be the lattice of Muchnik degrees of nonempty
subsets of
. The lattice
has been studied
extensively in previous publications. In this note we prove that
the lattice
is not Brouwerian.
Definition 1
Let
denote the set of natural numbers,
. Let
denote the
Baire space,
.
Following Medvedev [
27] and Rogers [
32, §13.7] we
define a
mass problem to be an arbitrary subset of
. For mass problems
and
we say that
is
Medvedev reducible or
strongly reducible to
,
abbreviated
, if there exists a partial recursive
functional
such that
for all
. We say
that
is
Muchnik reducible or
weakly reducible to
, abbreviated
, if for all
there exists
such that
is Turing reducible to
. 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
the Medvedev degree of
. We write
the Muchnik degree of
. Let
be
the set of Medvedev degrees, partially ordered by Medvedev
reducibility. There is a natural embedding of the Turing degrees
into
given by
. Let
be
the set of Muchnik degrees, partially ordered by Muchnik
reducibility. There is a natural embedding of the Turing degrees
into
given by
. Here
is the singleton set whose only element is
.
Definition 3
Let
be a lattice. For
we define
to be the
unique minimum
such that
. Note that
may or may not exist in
. Following Birkhoff
[
8,
9] (first two editions) and
McKinsey/Tarski [
25] we say that
is
Brouwerian if
exists in
for all
and
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
is Brouwerian
then
is distributive and has a bottom element and for all
in
the sublattice
is again Brouwerian.
Remark 1
Given a Brouwerian lattice
, we may view
as a model of
firstorder intuitionistic propositional calculus. Namely, for
we define
,
,
as above, and
where
is the top
element of
. We may also define
if and only if
in
. 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 firstorder 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
pseudoBoolean
algebra is a lattice
such that the dual of
is Brouwerian;
see Rasiowa/Sikorski [
31] and Rasiowa [
30].
PseudoBoolean 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 socalled 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
and
are Brouwerian lattices. There is
a natural homomorphism of
onto
given by
. This homomorphism preserves the binary
lattice operations
and
and the top and bottom
elements, but it does not preserve the binary ifthen 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
and noted that
is a
Brouwerian lattice. Later Muchnik 1963 [
28]
introduced
and noted that
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
denote the
Cantor space,
. Following Simpson [
40] let
be the sublattice of
consisting of the Medvedev degrees of
nonempty
subsets of
, and let
be the
sublattice of
consisting of the Muchnik degrees of nonempty
subsets of
.
Remark 5
The lattices
and
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], KjosHanssen/Simpson [
21],
Simpson
[
34,
35,
37,
38,
39,
40,
41,
42,
43,
45,
44],
Simpson/Slaman [
46], and Terwijn [
54]. It is
known that
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], resourcebounded computational complexity
[
21,
40], and Kolmogorov complexity [
21].
Recently Simpson [
44] has applied
and
to prove a
new theorem in symbolic dynamics.
Remark 6
It is known that
and
are distributive lattices with top
and bottom elements. Moreover, the natural lattice homomorphism of
onto
restricts to a natural lattice homomorphism of
onto
preserving top and bottom elements.
Remark 7
In view of Remarks
3,
4,
5
and
6, it is natural to ask whether
and
are Brouwerian lattices. The purpose of this note is to show that
is not a Brouwerian lattice. Letting
denote the top
element of
, we shall produce a family of Muchnik degrees
such that
does not exist in
. In
other words,
does not exist in
.
Remark 8
It remains open whether
is a Brouwerian lattice. Terwijn
[
54] has shown that the dual of
is not a
Brouwerian lattice. It remains open whether the dual of
is a
Brouwerian lattice.
In this section we prove that the lattice is not Brouwerian.
Definition 5
For
we write
to mean that
is
Turing reducible to
, i.e.,
is computable relative to
the Turing oracle
. We write
the Turing jump of
. In
particular
the halting problem
the Turing jump of
. We
use standard recursiontheoretic notation from Rogers [
32].
We say that
is majorized by if
for all
.
We begin with four well known lemmas.
Lemma 1
Given we can find such that is
.
Proof.Since , it follows by Post's Theorem (see for instance
[32, §14.5, Theorem VIII]) that is . From
this it follows that the singleton set is . Let
be a recursive
predicate such that our is the unique
such
that
holds. Let
where
is defined by the least such
that holds. It is easy to verify that and
is .
Lemma 2
If is and is nonrecursive, then is not
majorized by any recursive function.
Proof.This lemma is equivalent to, for instance, [40, Theorem
4.15].
Lemma 3
For all nonempty sets
we have
.
Proof.This lemma is a restatement of the well known Kleene Basis Theorem.
Namely, every nonempty subset of contains an
element which is . See for instance the proof of
[42, Lemma 5.3].
Lemma 4
Let
be nonempty such that no element
of is recursive. Then we can find
such that
and
.
Proof.By Lemma 3 it suffices to find
such that and
. To construct we
may proceed as in the proof of Lemma 5 below. The
construction is easier than in Lemma 5, because we can
ignore .
Lemma 5
Let
be nonempty . Let be such
that and
. Then we can find
such that and
and
.
Proof.We adapt the technique of Posner/Robinson [29].
Let
be a recursive tree such that
paths through . By Lemmas 1 and
2 we may safely assume that is not majorized by any
recursive function.
For integers and strings
we write
where the least such that either
or .
Note that the mapping
is recursive and monotonic, i.e.,
implies
. Moreover, for all
we have if and only if
. Here we are writing
In order to prove Lemma 5, we shall inductively define
an increasing sequence of strings
,
. We shall then let
.
In presenting the construction, we shall identify strings with their
Gödel numbers.
Stage . Let
the empty string.
Stage . Assume that has been defined. The definition
of will be given in a finite number of substages.
Substage . Let
.
Substage . Assume that has been defined. Let
the least such that either
and
or
and
.
Note that exists, because otherwise would be
majorized by the recursive function least
such that
and
. If (1) holds with
let
. If (2) holds
with let
. This completes our description of the
construction.
We claim that, within each stage , (2) holds for some .
Otherwise, we would have infinite increasing sequences of strings
and
with
for all . Moreover, these
sequences would be recursive relative to , namely
where least such
that (1) holds. Thus, letting
, we would have
and . Thus , a contradiction. This proves
our claim.
From the previous claim it follows that is defined for all
. By construction, the sequence
, is
recursive relative to . Moreover, is recursive relative to
,
because for all we have
.
Finally let
. Clearly .
We claim that the sequence
is
. Namely, given , we may use and as
oracles to compute as follows. We begin with
. Given we use the oracle
to compute
. Then, using the oracle ,
we ask whether there exists
such that
and
. If so, we compute
the least such . If not, we use the
oracle to compute
. This
proves our claim.
From the previous claim it follows that
. Hence
.
We claim that
. To see this, let be such that
is a total function.
Consider what happened at stage of the construction. Consider
the least such that (2) holds, i.e.,
. Since
(2) holds, there does not exist such that
and
. In particular,
letting be an initial segment of such that
and
, we have
. Hence
. This proves our
claim.
From the two previous claims, it follows that . The
proof of Lemma 5 is now finished.
Remark 9
By a similar argument we can prove the following. Let
be
. Let
be of hyperimmune Turing degree such that
. Let
be such that
. Then we can
find
such that
and
and
.
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
is not Brouwerian.
Proof.Let be the set of completions of Peano Arithmetic. Recall
from Simpson [40] that
the top
element of . By Lemma 4 let be such that
and
. Let
and note that
. By Lemmas 1 and
6 we have
.
It is well known (see for instance [40, Remark 3.9]) that
is a complete lattice. This means that for all
the least upper bound
and the greatest
lower bound
exist in . Therefore, within ,
let
and note that
in . In other words,
in .
We claim that
. Otherwise, let
where
is nonempty . Since
, we have
for all
. Since
, it follows that
.
By Lemma 5 let be such that and
and
. Let
and note that
. By Lemmas 1 and
6 we have
. By Lemma 3 we
have
, hence
contradicting the definition of .
This proves our claim.
Because
it follows that
does not
exist in . Thus is not Brouwerian.
Remark 10
The same proof shows that for all
in
we can find
in
such that
does not exist in
. On the other hand, we know at least a few nontrivial
instances where
exists in
. For example,
letting
be the Muchnik degree of the set of 1random reals,
Theorem 8.12 of Simpson [
40] tells us that
in
and
exists in
. In fact,
in
is equal to
in
, which is equal to
. We do not know any instances of
where
exists in
and both
and
are
in
.
 1

Christopher Alfeld.
Nonbranching degrees in the Medvedev lattice of
classes.
Journal of Symbolic Logic, 72:8197, 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
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:327335, 2003.
 5

Stephen Binns.
Small classes.
Archive for Mathematical Logic, 45:393410, 2006.
 6

Stephen Binns.
Hyperimmunity in
.
Notre Dame Journal of Formal Logic, 48:293316, 2007.
 7

Stephen Binns and Stephen G. Simpson.
Embeddings into the Medvedev and Muchnik lattices of
classes.
Archive for Mathematical Logic, 43:399414, 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 classes.
Archive for Mathematical Logic, 42:583600, 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

COMPTHY email list.
http://listserv.nd.edu/archives/compthy.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 email 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. SpringerVerlag,
1979.
XIV + 779 pages.
 18

Michael P. Fourman and Dana S. Scott.
Sheaves and logic.
In [17], pages 302401, 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, Physicalischmathematische Klasse, pages 4256, 1930.
 21

Bjørn KjosHanssen 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:5865, 1932.
 23

Andrei N. Kolmogorov.
On the interpretation of intuitionistic logic.
In [58], pages 151158 and 451466, 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:141191, 1944.
 25

J. C. C. McKinsey and Alfred Tarski.
On closed elements in closure algebras.
Annals of Mathematics, 47:122162, 1946.
 26

J. C. C. McKinsey and Alfred Tarski.
Some theorems about the sentential calculi of Lewis and Heyting.
Journal of Symbolic Logic, 13:115, 1948.
 27

Yuri T. Medvedev.
Degrees of difficulty of mass problems.
Doklady Akademii Nauk SSSR, n.s., 104:501504, 1955.
In Russian.
 28

Albert A. Muchnik.
On strong and weak reducibilities of algorithmic problems.
Sibirskii Matematicheskii Zhurnal, 4:13281341, 1963.
In Russian.
 29

David B. Posner and Robert W. Robinson.
Degrees joining to .
Journal of Symbolic Logic, 46:714722, 1981.
 30

Helena Rasiowa.
An Algebraic Approach to NonClassical Logics.
Number 78 in Studies in Logic and the Foundations of Mathematics.
NorthHolland, 1974.
XV + 403 pages.
 31

Helena Rasiowa and Roman Sikorski.
The Mathematics of Metamathematics.
Number 41 in Polska Akademia Nauk, Monografie Matematyczne.
Panstwowe Wydawnictwo Naukowe, 1963.
519 pages.
 32

Hartley Rogers, Jr.
Theory of Recursive Functions and Effective
Computability.
McGrawHill, 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 email list [16], 13 August 1999.
 35

Stephen G. Simpson.
FOM: priority arguments; Kleener.e. degrees; Pi01 classes.
FOM email list [16], 16 August 1999.
 36

Stephen G. Simpson.
Subsystems of Second Order Arithmetic.
Perspectives in Mathematical Logic. SpringerVerlag, 1999.
XIV + 445 pages.
 37

Stephen G. Simpson.
Medvedev degrees of nonempty Pi01 subsets of
2omega.
COMPTHY email 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 email list [16], 27 February 2005.
 40

Stephen G. Simpson.
Mass problems and randomness.
Bulletin of Symbolic Logic, 11:127, 2005.
 41

Stephen G. Simpson.
sets and models of
.
In [33], pages 352378, 2005.
 42

Stephen G. Simpson.
An extension of the recursively enumerable Turing degrees.
Journal of the London Mathematical Society, 75:287297, 2007.
 43

Stephen G. Simpson.
Mass problems and almost everywhere domination.
Mathematical Logic Quarterly, 53:483492, 2007.
 44

Stephen G. Simpson.
Medvedev degrees of 2dimensional 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 313332, 2008.
 46

Stephen G. Simpson and Theodore A. Slaman.
Medvedev degrees of subsets of .
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:171178, 1988.
In Russian.
 48

Andrea Sorbi.
Some remarks on the algebraic structure of the Medvedev lattice.
Journal of Symbolic Logic, 55:831853, 1990.
 49

Andrea Sorbi.
Embedding Brouwer algebras in the Medvedev lattice.
Notre Dame Journal of Formal Logic, 32:266275, 1991.
 50

Andrea Sorbi.
The Medvedev lattice of degrees of difficulty.
In [15], pages 289312, 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:103134, 1938.
 53

Sebastiaan A. Terwijn.
Constructive logic and the Medvedev lattice.
Notre Dame Journal of Formal Logic, 47:7382, 2006.
 54

Sebastiaan A. Terwijn.
The Medvedev lattice of computably closed sets.
Archive for Mathematical Logic, 45:179190, 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:327340, 2007.
 57

Sebastiaan A. Terwijn.
On the structure of the Medvedev lattice.
Journal of Symbolic Logic, 73:543558, 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.
NorthHolland, 1988.
Volume I, XX + 342 + XIV pages.
Mass problems and intuitionism
This document was generated using the
LaTeX2HTML translator Version 200221 (1.71)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html split 0 massint
The translation was initiated by Stephen G Simpson on 20080428
Footnotes
 ... Simpson^{1}
 The author thanks Sebastiaan Terwijn
for helpful correspondence. The author's research was partially
supported by the United States National Science Foundation, grants
DMS0600823 and DMS0652637, and by the Cada and Susan Grove
Mathematics Enhancement Endowment at the Pennsylvania State
University.
Stephen G Simpson
20080428