We now turn our attention to theorems whose proofs use Π2 constructions. We begin, in Section 5.1, by stating lemmas that isolate combinatorial properties of Π2 constructions. We then implement Π2 constructions to prove the existence of a high computably enumerable degree in Section 5.2, the Sacks Jump Inversion Theorem in Section 5.3, the Minimal Pair Theorem in Section 5.4 and an embedding of the pentagon into the computably enumerable degrees in Section 5.5.

Π2 Constructions

Requirements such as the thickness requirements discussed in Chapter 2 act to construct functionals that are total on given oracles, so require the declaration of infinitely many axioms. Such requirements cannot be handled by level 1 constructions, as a node of T1 will generally have the responsibility to declare only finitely many axioms for such functionals. This will introduce a coordination problem, as nodes having the responsibility to declare axioms on the same argument will appear on incomparable paths through T1.

Some requirements of the form Φ(A) = W can be handled by level 2 constructions. These constructions capture what are traditionally called infinite injury constructions. For those familiar with infinite injury constructions, we describe how these constructions are simulated by level 2 constructions.

A typical infinite injury construction will assign requirements to nodes of a tree T2, that can always be taken to be a binary tree. The nodes of the tree are prioritized, using the lexicographical ordering of these nodes. A computation of the current path through T2 is made at each stage of the construction, and action is carried out for nodes that lie along the current path.