Iterated club shooting and the stationary logic constructible model

In this paper, we investigate iterating the construction of [Formula: see text], the [Formula: see text]-like inner model constructed using stationary logic. We show that it is possible to force over generic extensions of [Formula: see text] to obtain a model of [Formula: see text], and to obtain models in which the sequence of iterated [Formula: see text]s is decreasing of arbitrarily large order types. For this, we prove distributivity and stationary-set preservation properties for countable iterations of club-shooting forcings using mutually stationary sets, and introduce the notion of mutually fat sets which yields better distributivity results even for uncountable iterations.