Feferman–Vaught theorem

The Feferman–Vaught theorem in model theory is a theorem by Solomon Feferman and Robert Lawson Vaught that shows how to reduce, in an algorithmic way, the first-order theory of a product of structures to the first-order theory of elements of the structure.

The theorem is considered to be one of the standard results in model theory. The theorem extends the previous result of Andrzej Mostowski on direct products of theories. It generalizes (to formulas with arbitrary quantifiers) the property in universal algebra that equalities (identities) carry over to direct products of algebraic structures (which is a consequence of one direction of Birkhoff's theorem).