More about \(\lambda \)-support iterations of \((<\lambda)\)-complete forcing notions (Q365678)

The notion of proper forcing was introduced by Shelah, who showed that the countable support (CS) iteration of proper forcings is proper. The search for the right definition of \(\lambda\)-properness is one of the main problems in iterated forcing theory. The first attempt could be to do nothing special and just repeat what we have done for CS iterations. We say a notion of forcing \(\mathbb{P}\) is \(\lambda\)-proper in the standard setting, where \(\lambda^{<\lambda}=\lambda,\) if for all sufficiently large regular cardinals \(\chi\), there is some \(x\in H(\chi)\) such that, whenever \(M\) is an elementary submodel of \(H(\chi)\) satisfying \(|M|=\lambda\), \(x, \mathbb{P}\in M\), \(M^{<\lambda} \subseteq M\), and \(p\) is an element of \(M \cap \mathbb{P}\), there is a condition \(q\leq p\) such that \(q \Vdash\)``\(M[\dot{G}_\mathbb{P}] \cap\mathrm{Ord}=M\cap\mathrm{Ord}\)''. It is easily seen that if \(\mathbb{P}\) is \(\lambda\)-proper in the standard setting, then forcing with \(\mathbb{P}\) preserves \(\lambda^+\), and in fact it preserves stationary subsets of \(\lambda^+.\) The main reason that the above definition is not the right definition for properness for higher cardinals is connected with the preservation under iterations. Though the CS iteration of proper forcings is proper, if one tries to repeat the proof of the preservation theorem for \(\lambda\)-support iterations of \(\lambda\)-proper forcing notions, then one faces difficulties at limit stages of cofinality less than \(\lambda\) caused by the fact that it is inconvenient to diagonalize \(\lambda\) objects in less than \(\lambda\) steps. In fact, the search for the right definition of \(\lambda\)-properness is still far from being completed. This paper is a continuation of some of the earlier papers by the authors, and it is a further step toward answering the above question. They introduce the concept of ``semi-pure properness'' and show that for an inaccessible cardinal \(\lambda\), the \(\lambda\)-support iteration of semi-purely proper forcing notions is \(\lambda\)-proper in the standard setting, and hence it does not collapse \(\lambda^+\). They also introduce some classes of \(\lambda\)-complete semi-pure forcing notions, including the forcing notions \(\mathbb{Q}^1_\lambda\) and \(\mathbb{Q}^2_\lambda\), and show that the statement ``\(\mathbb{Q}^1_\lambda\) and \(\mathbb{Q}^2_\lambda\) are forcing equivalent'' is independent of ZFC.