In this talk, I will give an introduction to the technique of forcing with side conditions and present some of the results obtained using the recently introduced symmetric matrices of models of two types.
The idea of adding systems of countable models as side conditions has been exploited extensively by Todorčević to build forcing notions that preserve cardinals and obtain consequences of forcing axioms at the level of the first uncountable cardinal.
The addition of models of a second type in recent work of Neeman, Asperó-Mota, Veličković, and others has proven to be very effective in pushing these results one cardinal higher, but most importantly, it has opened the door to obtaining consistent high analogs of classical strong forcing axioms.