Class forcing and progressively closed iteration

84 Views Asked by At

In his published paper ('The Ground Axiom' https://arxiv.org/abs/math/0609064), Jonas Reitz gives the definition of progressively closed iteration (definition 92). Informally, an Ord-length forcing iteration $\{P_{\alpha}; \dot Q_{\beta}:\alpha, \beta\in Ord\}$ is progressively closed if for every ordinal $\beta$, on a tail of $\alpha$’s, $P_{\alpha}$ forces that $\dot Q_{\alpha}$ is <$\beta$-closed. Suppose that $P$ is a progressively closed iteration. I wuold like to prove that a forcing extension via $P$ is a model of GBC. In order to show that it is enough to prove that $P$ is a tame. Therefore, I need a proof of the following fact: If $P$ is a progressively closed iteration, than $P$ is a tame. Are there some references about that? Thank you.