Forcing with Sequences of Models of Two Types

We present an approach to forcing with finite sequences of models that uses models of two types. This approach builds on earlier work of Friedman and Mitchell on forcing to add clubs in cardinals larger than ℵ1, with finite conditions. We use the two-type approach to give a new proof of the consistency of the proper forcing axiom. The new proof uses a finite support forcing, as opposed to the countable support iteration in the standard proof. The distinction is important since a proof using finite supports is more amenable to generalizations to cardinals greater than ℵ1.