An approximate Herbrand's theorem and definable functions in metric structures (Q2888633)

One famous form of Herbrand's theorem in first-order logic states that if \(T\) is a universal theory admitting quantifier elimination then for each formula \(\phi(\bar x,\bar y)\) there are tuples of terms \({\bar t}_1({\bar x}),\ldots, {\bar t}_k({\bar x})\) such that NEWLINE\[NEWLINET\vDash\phi(\bar x)\rightarrow\bigvee_{i=1}^k\phi(\bar x,\bar t_i(\bar x)).NEWLINE\]NEWLINE This theorem can be used to describe definable maps in certain theories and has applications in motivic measures. The author states some appropriate preservation theorems in continuous logic and use them to prove an approximate variant of Herbrand's theorem. He then applies it to describe definable functions in theories of Hilbert spaces and certain extensions. In particular, it is proved that in the theory of Hilbert spaces (or rather their unit balls) definable functions are piecewise approximated by affine maps \(\lambda x+v\).