The subcompleteness of diagonal Prikry (Q2288331)

Subcomplete forcing was introduced by Ronald Jensen as a generalization of complete forcing introduced by Shelah; see [\textit{R. Jensen}, Lect. Notes Ser., Inst. Math. Sci., Natl. Univ. Singap. 27, 83--182 (2014; Zbl 1351.03044)] for details on the topic. The importance about such forcing notions is that they do not add reals and are preserved under revised countable support iterations with some restraints. In earlier work, Jensen [loc. cit.] showed that Prikry forcing is subcomplete and \textit{G. Fuchs} [Arch. Math. Logic 57, No. 3--4, 273--284 (2018; Zbl 06860713)] showed the same result for Magidor forcing. The product Prikry forcing was introduced by \textit{M. Magidor} in his seminal paper [Ann. Math. Logic 10, 33--57 (1976; Zbl 0342.02051)]. This kind of forcing was studied extensively by \textit{G. Fuchs} [Arch. Math. Logic 44, No. 8, 935--971 (2005; Zbl 1077.03030)]. Suppose \(D\) is an infinite discrete set of measurable cardinals. For each \(\kappa \in D,\) let \(U(\kappa)\) be a normal measure on \(\kappa\) and let \(\mathcal{U}=\langle U(\kappa): \kappa \in D \rangle\). The corresponding Prikry product forcing, denoted \(\mathbb{D}(\mathcal{U})\), is a natural generalization of Prikry forcing, which changes the cofinality of each \(\kappa \in D\) into \(\omega\) by adding a Prikry sequence through \(\kappa\). In the paper under review, the author shows that the product Prikry forcing is subcomplete as well. The general strategy of the proof follows Jensen's [loc. cit.] ideas for getting the same result for Prikry forcing, and relies on the construction of elementary embeddings via collapsing and lifting up, and on Barwise's results on infinitary logics defined on countable admissible sets. The paper is carefully written.