Assuming determinacy, the model L[T2] does not depend on the choice of T2.

We shall prove the following theorem: If κ is an infinite cardinal and Γ: P(κ) → cf κ a partition of the power-set of κ then we can find a homogeneous ⊿-system of size κ such that the kernel of the ⊿-system is in the same partition class as all the members of the ⊿-system.

In this paper we discuss an interpretation of intuitionistic type theory in many-sorted arithmetic with so-called conditional application. Via the formulas-as-types correspondence the arithmetical system in turn can be embedded in ML, resulting in a characterization of strong Σ-elimination by an axiom of conditional choice.

It is well known that the hypothesis that all real numbers are constructible in the sense of Gödel [1] implies the existence of a Σ21 well-ordering of the Baire space [1, p. 67]. We are concerned with the converse to this theorem. From the assumption of the existence of a Σ21 well-ordering with total domain, we derive various consequences which in the presence of a nonconstructible real seem highly pathological. However, while several of these consequences are obviously absurd, none have as yet been disproven. Indeed some of the stranger consistency proofs of Jensen seem to indicate that there is a possibility that they may be consistent. I am referring to such results as existence of a model for ZF set theory in which the degrees of constructibility form a sequence of type ω + 1 with the (ω + 1)st degree being the only one which contains a nonconstructible real, and that degree being the degree of a Δ31 nonconstructible real.

In what follows we shall use the small Greek letters α, β, γ to range over the Baire space NN where N is the set of natural numbers. We assume that the reader is familiar with the use of trees to encode closed subsets of this space. The class Σ21 is the collection of all those subsets of the Baire space which can be defined by a formula which is Σ21 in a constructible parameter. Correspondingly Π21 will be taken to mean Π11 in a constructible parameter. The proof of the first lemma is left as an exercise. It involves nothing more than coding perfect sets by trees and then counting quantifiers.