Mass problems and intuitionism
Stephen G. Simpson1
Department of Mathematics
First draft: July 25, 2007
This draft: April 28, 2008
Notre Dame Journal of Formal Logic, 49, 2008, 127-136
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
first-order 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 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

such that the dual of

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

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 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

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], 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

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

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 recursion-theoretic 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 1-random 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.
Non-branching degrees in the Medvedev lattice of
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
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
classes.
Archive for Mathematical Logic, 45:393-410, 2006.
- 6
-
Stephen Binns.
Hyperimmunity in
.
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
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
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
.
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.
Panstwowe 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.
sets and models of
.
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
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: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.
Mass problems and intuitionism
This document was generated using the
LaTeX2HTML translator Version 2002-2-1 (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 2008-04-28
Footnotes
- ... Simpson1
- 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.
Stephen G Simpson
2008-04-28