A structure may be implemented within a set theory ZFC, or another set theory such as NBG, NFU, ETCS.About ETCS see Type theory#Mathematical foundations Alternatively, a structure may be treated in the framework of first-order logic, second-order logic, higher-order logic, a type theory, homotopy type theory etc.A reasonable choice of an ambient framework should not alter basic properties of a structure, but can alter provability of finer properties. For example, some theorems about the natural numbers are provable in set theory (and some other strong systems) but not provable in first-order logic; see Paris–Harrington theorem and Goodstein's theorem. The same applies to definability; see for example Tarski's undefinability theorem.
