Noetherian theories

A first-order theory is Noetherian with respect to the collection of formulae [Formula: see text] if every definable set is a Boolean combination of instances of formulae in [Formula: see text] and the topology whose subbasis of closed sets is the collection of instances of arbitrary formulae in [Formula: see text] is Noetherian. We show the Noetherianity of the theory of proper pairs of algebraically closed fields in any characteristic with respect to the family of tame formulae as introduced in [A. Martin-Pizarro and M. Ziegler, Equational theories of fields, J. Symbolic Logic 85 (2020) 828–851, https://arxiv.org/abs/1702.05735 ], thus answering a question which was left open there.